This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nummul1c

Description: The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses nummul1c.1 ⊢ T ∈ ℕ 0
nummul1c.2 ⊢ P ∈ ℕ 0
nummul1c.3 ⊢ A ∈ ℕ 0
nummul1c.4 ⊢ B ∈ ℕ 0
nummul1c.5 ⊢ N = T ⁢ A + B
nummul1c.6 ⊢ D ∈ ℕ 0
nummul1c.7 ⊢ E ∈ ℕ 0
nummul1c.8 ⊢ A ⁢ P + E = C
nummul1c.9 ⊢ B ⁢ P = T ⁢ E + D
Assertion nummul1c ⊢ N ⁢ P = T ⁢ C + D

Proof

Step Hyp Ref Expression
1 nummul1c.1 ⊢ T ∈ ℕ 0
2 nummul1c.2 ⊢ P ∈ ℕ 0
3 nummul1c.3 ⊢ A ∈ ℕ 0
4 nummul1c.4 ⊢ B ∈ ℕ 0
5 nummul1c.5 ⊢ N = T ⁢ A + B
6 nummul1c.6 ⊢ D ∈ ℕ 0
7 nummul1c.7 ⊢ E ∈ ℕ 0
8 nummul1c.8 ⊢ A ⁢ P + E = C
9 nummul1c.9 ⊢ B ⁢ P = T ⁢ E + D
10 1 3 4 numcl ⊢ T ⁢ A + B ∈ ℕ 0
11 5 10 eqeltri ⊢ N ∈ ℕ 0
12 11 2 num0u ⊢ N ⁢ P = N ⁢ P + 0
13 0nn0 ⊢ 0 ∈ ℕ 0
14 1 13 num0h ⊢ 0 = T ⋅ 0 + 0
15 7 nn0cni ⊢ E ∈ ℂ
16 15 addlidi ⊢ 0 + E = E
17 16 oveq2i ⊢ A ⁢ P + 0 + E = A ⁢ P + E
18 17 8 eqtri ⊢ A ⁢ P + 0 + E = C
19 4 2 num0u ⊢ B ⁢ P = B ⁢ P + 0
20 19 9 eqtr3i ⊢ B ⁢ P + 0 = T ⁢ E + D
21 1 3 4 13 13 5 14 2 6 7 18 20 nummac ⊢ N ⁢ P + 0 = T ⁢ C + D
22 12 21 eqtri ⊢ N ⁢ P = T ⁢ C + D