Definition df-dp2 33481

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12816. (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 33480	. 2 class _𝐴𝐵
4		c1 11202	. . . . 5 class 1
5		cc0 11201	. . . . 5 class 0
6	4, 5	cdc 12815	. . . 4 class ;10
7		cdiv 11974	. . . 4 class /
8	2, 6, 7	co 7420	. . 3 class (𝐵 / ;10)
9		caddc 11204	. . 3 class +
10	1, 8, 9	co 7420	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1569	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is used by:  dp2eq1  33482  dp2eq2  33483  dp20u  33487  dp20h  33488  dp2cl  33489  dp2clq  33490  rpdp2cl  33491  dp2lt10  33493  dp2lt  33494  dp2ltsuc  33495  dp2ltc  33496  dpval  33499  dpfrac1  33501  dpval2  33502  dpval3  33503  dp3mul10  33507