Definition df-dp2 31433

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12539. (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 31432	. 2 class _𝐴𝐵
4		c1 10973	. . . . 5 class 1
5		cc0 10972	. . . . 5 class 0
6	4, 5	cdc 12538	. . . 4 class ;10
7		cdiv 11733	. . . 4 class /
8	2, 6, 7	co 7337	. . 3 class (𝐵 / ;10)
9		caddc 10975	. . 3 class +
10	1, 8, 9	co 7337	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1540	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  31434  dp2eq2  31435  dp20u  31439  dp20h  31440  dp2cl  31441  dp2clq  31442  rpdp2cl  31443  dp2lt10  31445  dp2lt  31446  dp2ltsuc  31447  dp2ltc  31448  dpval  31451  dpfrac1  31453  dpval2  31454  dpval3  31455  dp3mul10  31459