Definition df-dp2 33484

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12818. (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 33483	. 2 class _𝐴𝐵
4		c1 11204	. . . . 5 class 1
5		cc0 11203	. . . . 5 class 0
6	4, 5	cdc 12817	. . . 4 class ;10
7		cdiv 11976	. . . 4 class /
8	2, 6, 7	co 7420	. . 3 class (𝐵 / ;10)
9		caddc 11206	. . 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  33485  dp2eq2  33486  dp20u  33490  dp20h  33491  dp2cl  33492  dp2clq  33493  rpdp2cl  33494  dp2lt10  33496  dp2lt  33497  dp2ltsuc  33498  dp2ltc  33499  dpval  33502  dpfrac1  33504  dpval2  33505  dpval3  33506  dp3mul10  33510