Definition df-dp2 33169

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

Assertion

Ref	Expression
df-dp2	⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

Detailed syntax breakdown of Definition df-dp2

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cdp2 33168	. 2 class _𝐴𝐵
4		c1 11102	. . . . 5 class 1
5		cc0 11101	. . . . 5 class 0
6	4, 5	cdc 12712	. . . 4 class ;10
7		cdiv 11872	. . . 4 class /
8	2, 6, 7	co 7412	. . 3 class (𝐵 / ;10)
9		caddc 11104	. . 3 class +
10	1, 8, 9	co 7412	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1570	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  33170  dp2eq2  33171  dp20u  33175  dp20h  33176  dp2cl  33177  dp2clq  33178  rpdp2cl  33179  dp2lt10  33181  dp2lt  33182  dp2ltsuc  33183  dp2ltc  33184  dpval  33187  dpfrac1  33189  dpval2  33190  dpval3  33191  dp3mul10  33195