Definition df-dp2 32963

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12620. (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 32962	. 2 class _𝐴𝐵
4		c1 11039	. . . . 5 class 1
5		cc0 11038	. . . . 5 class 0
6	4, 5	cdc 12619	. . . 4 class ;10
7		cdiv 11806	. . . 4 class /
8	2, 6, 7	co 7368	. . 3 class (𝐵 / ;10)
9		caddc 11041	. . 3 class +
10	1, 8, 9	co 7368	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1542	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32964  dp2eq2  32965  dp20u  32969  dp20h  32970  dp2cl  32971  dp2clq  32972  rpdp2cl  32973  dp2lt10  32975  dp2lt  32976  dp2ltsuc  32977  dp2ltc  32978  dpval  32981  dpfrac1  32983  dpval2  32984  dpval3  32985  dp3mul10  32989