# 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}\in {ℕ}_{0}$
3dec.b ${⊢}{B}\in {ℕ}_{0}$
Assertion 3dec Could not format assertion : No typesetting found for |- ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-

### Proof

Step Hyp Ref Expression
1 3dec.a ${⊢}{A}\in {ℕ}_{0}$
2 3dec.b ${⊢}{B}\in {ℕ}_{0}$
3 dfdec10 Could not format ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) : No typesetting found for |- ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) with typecode |-
4 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
5 4 oveq2i Could not format ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) with typecode |-
6 10nn ${⊢}10\in ℕ$
7 6 nncni ${⊢}10\in ℂ$
8 1 nn0cni ${⊢}{A}\in ℂ$
9 7 8 mulcli ${⊢}10{A}\in ℂ$
10 2 nn0cni ${⊢}{B}\in ℂ$
11 7 9 10 adddii ${⊢}10\left(10{A}+{B}\right)=1010{A}+10{B}$
12 5 11 eqtri Could not format ( ; 1 0 x. ; A B ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) ) with typecode |-
13 7 7 8 mulassi ${⊢}10\cdot 10{A}=1010{A}$
14 13 eqcomi ${⊢}1010{A}=10\cdot 10{A}$
15 7 sqvali ${⊢}{10}^{2}=10\cdot 10$
16 15 eqcomi ${⊢}10\cdot 10={10}^{2}$
17 16 oveq1i ${⊢}10\cdot 10{A}={10}^{2}{A}$
18 14 17 eqtri ${⊢}1010{A}={10}^{2}{A}$
19 18 oveq1i ${⊢}1010{A}+10{B}={10}^{2}{A}+10{B}$
20 12 19 eqtri Could not format ( ; 1 0 x. ; A B ) = ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) with typecode |-
21 20 oveq1i Could not format ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for |- ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-
22 3 21 eqtri Could not format ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for |- ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-