Definition df-dp2 32652

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12708. (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 32651	. 2 class _𝐴𝐵
4		c1 11139	. . . . 5 class 1
5		cc0 11138	. . . . 5 class 0
6	4, 5	cdc 12707	. . . 4 class ;10
7		cdiv 11901	. . . 4 class /
8	2, 6, 7	co 7417	. . 3 class (𝐵 / ;10)
9		caddc 11141	. . 3 class +
10	1, 8, 9	co 7417	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1533	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32653  dp2eq2  32654  dp20u  32658  dp20h  32659  dp2cl  32660  dp2clq  32661  rpdp2cl  32662  dp2lt10  32664  dp2lt  32665  dp2ltsuc  32666  dp2ltc  32667  dpval  32670  dpfrac1  32672  dpval2  32673  dpval3  32674  dp3mul10  32678