Definition df-dp2 31195

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12488. (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 31194	. 2 class _𝐴𝐵
4		c1 10922	. . . . 5 class 1
5		cc0 10921	. . . . 5 class 0
6	4, 5	cdc 12487	. . . 4 class ;10
7		cdiv 11682	. . . 4 class /
8	2, 6, 7	co 7307	. . 3 class (𝐵 / ;10)
9		caddc 10924	. . 3 class +
10	1, 8, 9	co 7307	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1539	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  31196  dp2eq2  31197  dp20u  31201  dp20h  31202  dp2cl  31203  dp2clq  31204  rpdp2cl  31205  dp2lt10  31207  dp2lt  31208  dp2ltsuc  31209  dp2ltc  31210  dpval  31213  dpfrac1  31215  dpval2  31216  dpval3  31217  dp3mul10  31221