This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) · 𝐴 ) + 𝐵 )