Metamath Proof Explorer

Theorem 3dec

Description: A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)

Ref Expression
Hypotheses 3dec.a 
|- A e. NN0
3dec.b 
|- B e. NN0
Assertion 3dec 
|- ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C )

Proof

Step Hyp Ref Expression
1 3dec.a 
 |-  A e. NN0
2 3dec.b 
 |-  B e. NN0
3 dfdec10 
 |-  ; ; A B C = ( ( ; 1 0 x. ; A B ) + C )
4 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
5 4 oveq2i 
 |-  ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) )
6 10nn 
 |-  ; 1 0 e. NN
7 6 nncni 
 |-  ; 1 0 e. CC
8 1 nn0cni 
 |-  A e. CC
9 7 8 mulcli 
 |-  ( ; 1 0 x. A ) e. CC
10 2 nn0cni 
 |-  B e. CC
11 7 9 10 adddii 
 |-  ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) )
12 5 11 eqtri 
 |-  ( ; 1 0 x. ; A B ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) )
13 7 7 8 mulassi 
 |-  ( ( ; 1 0 x. ; 1 0 ) x. A ) = ( ; 1 0 x. ( ; 1 0 x. A ) )
14 13 eqcomi 
 |-  ( ; 1 0 x. ( ; 1 0 x. A ) ) = ( ( ; 1 0 x. ; 1 0 ) x. A )
15 7 sqvali 
 |-  ( ; 1 0 ^ 2 ) = ( ; 1 0 x. ; 1 0 )
16 15 eqcomi 
 |-  ( ; 1 0 x. ; 1 0 ) = ( ; 1 0 ^ 2 )
17 16 oveq1i 
 |-  ( ( ; 1 0 x. ; 1 0 ) x. A ) = ( ( ; 1 0 ^ 2 ) x. A )
18 14 17 eqtri 
 |-  ( ; 1 0 x. ( ; 1 0 x. A ) ) = ( ( ; 1 0 ^ 2 ) x. A )
19 18 oveq1i 
 |-  ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) ) = ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) )
20 12 19 eqtri 
 |-  ( ; 1 0 x. ; A B ) = ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) )
21 20 oveq1i 
 |-  ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C )
22 3 21 eqtri 
 |-  ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C )