Definition df-dec

Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 1 0 . For example, ( ; ; ; 1 0 0 0 + ; ; ; 2 0 0 0 ) = ; ; ; 3 0 0 0 1kp2ke3k . (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 1-Aug-2021)

	Ref	Expression
Assertion	df-dec	⊢ ; 𝐴 𝐵 = ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cdc	⊢ ; 𝐴 𝐵
3		c9	⊢ 9
4		caddc	⊢ +
5		c1	⊢ 1
6	3 5 4	co	⊢ ( 9 + 1 )
7		cmul	⊢ ·
8	6 0 7	co	⊢ ( ( 9 + 1 ) · 𝐴 )
9	8 1 4	co	⊢ ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )
10	2 9	wceq	⊢ ; 𝐴 𝐵 = ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )