Definition df-dp2 32953

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12608. (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 32952	. 2 class _𝐴𝐵
4		c1 11027	. . . . 5 class 1
5		cc0 11026	. . . . 5 class 0
6	4, 5	cdc 12607	. . . 4 class ;10
7		cdiv 11794	. . . 4 class /
8	2, 6, 7	co 7358	. . 3 class (𝐵 / ;10)
9		caddc 11029	. . 3 class +
10	1, 8, 9	co 7358	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1541	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32954  dp2eq2  32955  dp20u  32959  dp20h  32960  dp2cl  32961  dp2clq  32962  rpdp2cl  32963  dp2lt10  32965  dp2lt  32966  dp2ltsuc  32967  dp2ltc  32968  dpval  32971  dpfrac1  32973  dpval2  32974  dpval3  32975  dp3mul10  32979