Definition df-dec 8369

Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000. (Contributed by Mario Carneiro, 17-Apr-2015.)

Assertion

Ref	Expression
df-dec	⊢ ;𝐴𝐵 = ((10 · 𝐴) + 𝐵)

Detailed syntax breakdown of Definition df-dec

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cdc 8368	. 2 class ;𝐴𝐵
4		c10 7972	. . . 4 class 10
5		cmul 6894	. . . 4 class ·
6	4, 1, 5	co 5512	. . 3 class (10 · 𝐴)
7		caddc 6892	. . 3 class +
8	6, 2, 7	co 5512	. 2 class ((10 · 𝐴) + 𝐵)
9	3, 8	wceq 1243	1 wff ;𝐴𝐵 = ((10 · 𝐴) + 𝐵)

This definition is referenced by:  deceq1  8370  deceq2  8371  decnncl  8380  deccl  8381  dec0u  8382  dec0h  8383  decnncl2  8385  declt  8388  decltc  8389  decsuc  8390  declti  8392  decsucc  8394  dec10p  8396  decma  8405  decmac  8406  decma2c  8407  decadd  8408  decaddc  8409  decmul1c  8414  decmul2c  8415  5t5e25  8443  6t6e36  8448  8t6e48  8459