Definition df-dp2 32836

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12759. (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 32835	. 2 class _𝐴𝐵
4		c1 11185	. . . . 5 class 1
5		cc0 11184	. . . . 5 class 0
6	4, 5	cdc 12758	. . . 4 class ;10
7		cdiv 11947	. . . 4 class /
8	2, 6, 7	co 7448	. . 3 class (𝐵 / ;10)
9		caddc 11187	. . 3 class +
10	1, 8, 9	co 7448	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1537	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32837  dp2eq2  32838  dp20u  32842  dp20h  32843  dp2cl  32844  dp2clq  32845  rpdp2cl  32846  dp2lt10  32848  dp2lt  32849  dp2ltsuc  32850  dp2ltc  32851  dpval  32854  dpfrac1  32856  dpval2  32857  dpval3  32858  dp3mul10  32862