Definition df-dp2 32846

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12709. (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 32845	. 2 class _𝐴𝐵
4		c1 11130	. . . . 5 class 1
5		cc0 11129	. . . . 5 class 0
6	4, 5	cdc 12708	. . . 4 class ;10
7		cdiv 11894	. . . 4 class /
8	2, 6, 7	co 7405	. . 3 class (𝐵 / ;10)
9		caddc 11132	. . 3 class +
10	1, 8, 9	co 7405	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1540	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32847  dp2eq2  32848  dp20u  32852  dp20h  32853  dp2cl  32854  dp2clq  32855  rpdp2cl  32856  dp2lt10  32858  dp2lt  32859  dp2ltsuc  32860  dp2ltc  32861  dpval  32864  dpfrac1  32866  dpval2  32867  dpval3  32868  dp3mul10  32872