Definition df-dp2 32799

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12657. (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 32798	. 2 class _𝐴𝐵
4		c1 11076	. . . . 5 class 1
5		cc0 11075	. . . . 5 class 0
6	4, 5	cdc 12656	. . . 4 class ;10
7		cdiv 11842	. . . 4 class /
8	2, 6, 7	co 7390	. . 3 class (𝐵 / ;10)
9		caddc 11078	. . 3 class +
10	1, 8, 9	co 7390	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1540	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32800  dp2eq2  32801  dp20u  32805  dp20h  32806  dp2cl  32807  dp2clq  32808  rpdp2cl  32809  dp2lt10  32811  dp2lt  32812  dp2ltsuc  32813  dp2ltc  32814  dpval  32817  dpfrac1  32819  dpval2  32820  dpval3  32821  dp3mul10  32825