# 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`
` |-  ( ; 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 )`