This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-dp2

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec . (Contributed by David A. Wheeler, 15-May-2015) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	df-dp2	\|- _ A B = ( A + ( B / ; 1 0 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	\|- A
1		cB	\|- B
2	0 1	cdp2	\|- _ A B
3		caddc	\|- +
4		cdiv	\|- /
5		c1	\|- 1
6		cc0	\|- 0
7	5 6	cdc	\|- ; 1 0
8	1 7 4	co	\|- ( B / ; 1 0 )
9	0 8 3	co	\|- ( A + ( B / ; 1 0 ) )
10	2 9	wceq	\|- _ A B = ( A + ( B / ; 1 0 ) )