Definition df-dp2 33228

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12730. (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 33227	. 2 class _𝐴𝐵
4		c1 11119	. . . . 5 class 1
5		cc0 11118	. . . . 5 class 0
6	4, 5	cdc 12729	. . . 4 class ;10
7		cdiv 11889	. . . 4 class /
8	2, 6, 7	co 7423	. . 3 class (𝐵 / ;10)
9		caddc 11121	. . 3 class +
10	1, 8, 9	co 7423	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1570	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is used by:  dp2eq1  33229  dp2eq2  33230  dp20u  33234  dp20h  33235  dp2cl  33236  dp2clq  33237  rpdp2cl  33238  dp2lt10  33240  dp2lt  33241  dp2ltsuc  33242  dp2ltc  33243  dpval  33246  dpfrac1  33248  dpval2  33249  dpval3  33250  dp3mul10  33254