# 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 𝐴 ∈ ℕ0
3dec.b 𝐵 ∈ ℕ0
Assertion 3dec 𝐴 𝐵 𝐶 = ( ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 )

### Proof

Step Hyp Ref Expression
1 3dec.a 𝐴 ∈ ℕ0
2 3dec.b 𝐵 ∈ ℕ0
3 dfdec10 𝐴 𝐵 𝐶 = ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 )
4 dfdec10 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
5 4 oveq2i ( 1 0 · 𝐴 𝐵 ) = ( 1 0 · ( ( 1 0 · 𝐴 ) + 𝐵 ) )
6 10nn 1 0 ∈ ℕ
7 6 nncni 1 0 ∈ ℂ
8 1 nn0cni 𝐴 ∈ ℂ
9 7 8 mulcli ( 1 0 · 𝐴 ) ∈ ℂ
10 2 nn0cni 𝐵 ∈ ℂ
11 7 9 10 adddii ( 1 0 · ( ( 1 0 · 𝐴 ) + 𝐵 ) ) = ( ( 1 0 · ( 1 0 · 𝐴 ) ) + ( 1 0 · 𝐵 ) )
12 5 11 eqtri ( 1 0 · 𝐴 𝐵 ) = ( ( 1 0 · ( 1 0 · 𝐴 ) ) + ( 1 0 · 𝐵 ) )
13 7 7 8 mulassi ( ( 1 0 · 1 0 ) · 𝐴 ) = ( 1 0 · ( 1 0 · 𝐴 ) )
14 13 eqcomi ( 1 0 · ( 1 0 · 𝐴 ) ) = ( ( 1 0 · 1 0 ) · 𝐴 )
15 7 sqvali ( 1 0 ↑ 2 ) = ( 1 0 · 1 0 )
16 15 eqcomi ( 1 0 · 1 0 ) = ( 1 0 ↑ 2 )
17 16 oveq1i ( ( 1 0 · 1 0 ) · 𝐴 ) = ( ( 1 0 ↑ 2 ) · 𝐴 )
18 14 17 eqtri ( 1 0 · ( 1 0 · 𝐴 ) ) = ( ( 1 0 ↑ 2 ) · 𝐴 )
19 18 oveq1i ( ( 1 0 · ( 1 0 · 𝐴 ) ) + ( 1 0 · 𝐵 ) ) = ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) )
20 12 19 eqtri ( 1 0 · 𝐴 𝐵 ) = ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) )
21 20 oveq1i ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 ) = ( ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 )
22 3 21 eqtri 𝐴 𝐵 𝐶 = ( ( ( ( 1 0 ↑ 2 ) · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 )