Definition df-dp2 32838

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12731. (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 32837	. 2 class _𝐴𝐵
4		c1 11153	. . . . 5 class 1
5		cc0 11152	. . . . 5 class 0
6	4, 5	cdc 12730	. . . 4 class ;10
7		cdiv 11917	. . . 4 class /
8	2, 6, 7	co 7430	. . 3 class (𝐵 / ;10)
9		caddc 11155	. . 3 class +
10	1, 8, 9	co 7430	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1536	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32839  dp2eq2  32840  dp20u  32844  dp20h  32845  dp2cl  32846  dp2clq  32847  rpdp2cl  32848  dp2lt10  32850  dp2lt  32851  dp2ltsuc  32852  dp2ltc  32853  dpval  32856  dpfrac1  32858  dpval2  32859  dpval3  32860  dp3mul10  32864