Definition df-dp2 32957

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12643. (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 32956	. 2 class _𝐴𝐵
4		c1 11037	. . . . 5 class 1
5		cc0 11036	. . . . 5 class 0
6	4, 5	cdc 12642	. . . 4 class ;10
7		cdiv 11805	. . . 4 class /
8	2, 6, 7	co 7363	. . 3 class (𝐵 / ;10)
9		caddc 11039	. . 3 class +
10	1, 8, 9	co 7363	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1547	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32958  dp2eq2  32959  dp20u  32963  dp20h  32964  dp2cl  32965  dp2clq  32966  rpdp2cl  32967  dp2lt10  32969  dp2lt  32970  dp2ltsuc  32971  dp2ltc  32972  dpval  32975  dpfrac1  32977  dpval2  32978  dpval3  32979  dp3mul10  32983