Definition df-dp2 32825

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12610. (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 32824	. 2 class _𝐴𝐵
4		c1 11029	. . . . 5 class 1
5		cc0 11028	. . . . 5 class 0
6	4, 5	cdc 12609	. . . 4 class ;10
7		cdiv 11795	. . . 4 class /
8	2, 6, 7	co 7353	. . 3 class (𝐵 / ;10)
9		caddc 11031	. . 3 class +
10	1, 8, 9	co 7353	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1540	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32826  dp2eq2  32827  dp20u  32831  dp20h  32832  dp2cl  32833  dp2clq  32834  rpdp2cl  32835  dp2lt10  32837  dp2lt  32838  dp2ltsuc  32839  dp2ltc  32840  dpval  32843  dpfrac1  32845  dpval2  32846  dpval3  32847  dp3mul10  32851