Definition df-dp2 32293

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12682. (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 32292	. 2 class _𝐴𝐵
4		c1 11113	. . . . 5 class 1
5		cc0 11112	. . . . 5 class 0
6	4, 5	cdc 12681	. . . 4 class ;10
7		cdiv 11875	. . . 4 class /
8	2, 6, 7	co 7411	. . 3 class (𝐵 / ;10)
9		caddc 11115	. . 3 class +
10	1, 8, 9	co 7411	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1541	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32294  dp2eq2  32295  dp20u  32299  dp20h  32300  dp2cl  32301  dp2clq  32302  rpdp2cl  32303  dp2lt10  32305  dp2lt  32306  dp2ltsuc  32307  dp2ltc  32308  dpval  32311  dpfrac1  32313  dpval2  32314  dpval3  32315  dp3mul10  32319