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