Definition df-dp2 31125

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12420. (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 31124	. 2 class _𝐴𝐵
4		c1 10856	. . . . 5 class 1
5		cc0 10855	. . . . 5 class 0
6	4, 5	cdc 12419	. . . 4 class ;10
7		cdiv 11615	. . . 4 class /
8	2, 6, 7	co 7268	. . 3 class (𝐵 / ;10)
9		caddc 10858	. . 3 class +
10	1, 8, 9	co 7268	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1541	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  31126  dp2eq2  31127  dp20u  31131  dp20h  31132  dp2cl  31133  dp2clq  31134  rpdp2cl  31135  dp2lt10  31137  dp2lt  31138  dp2ltsuc  31139  dp2ltc  31140  dpval  31143  dpfrac1  31145  dpval2  31146  dpval3  31147  dp3mul10  31151