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	⊢ _ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / ; 1 0 ) )

Detailed syntax breakdown

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