Definition df-dp2 33010

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12686. (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 33009	. 2 class _𝐴𝐵
4		c1 11071	. . . . 5 class 1
5		cc0 11070	. . . . 5 class 0
6	4, 5	cdc 12685	. . . 4 class ;10
7		cdiv 11841	. . . 4 class /
8	2, 6, 7	co 7392	. . 3 class (𝐵 / ;10)
9		caddc 11073	. . 3 class +
10	1, 8, 9	co 7392	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1559	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  33011  dp2eq2  33012  dp20u  33016  dp20h  33017  dp2cl  33018  dp2clq  33019  rpdp2cl  33020  dp2lt10  33022  dp2lt  33023  dp2ltsuc  33024  dp2ltc  33025  dpval  33028  dpfrac1  33030  dpval2  33031  dpval3  33032  dp3mul10  33036