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

Metamath Proof Explorer

Theorem nummul2c

Description: The product of a decimal integer with a number (with carry). (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
nummul2c.7 ⊢ P ⁢ A + E = C
nummul2c.8 ⊢ P ⁢ B = T ⁢ E + D
Assertion nummul2c ⊢ P ⋅ N = 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 nummul2c.7 ⊢ P ⁢ A + E = C
9 nummul2c.8 ⊢ P ⁢ B = T ⁢ E + D
10 1 3 4 numcl ⊢ T ⁢ A + B ∈ ℕ 0
11 5 10 eqeltri ⊢ N ∈ ℕ 0
12 11 nn0cni ⊢ N ∈ ℂ
13 2 nn0cni ⊢ P ∈ ℂ
14 3 nn0cni ⊢ A ∈ ℂ
15 14 13 mulcomi ⊢ A ⁢ P = P ⁢ A
16 15 oveq1i ⊢ A ⁢ P + E = P ⁢ A + E
17 16 8 eqtri ⊢ A ⁢ P + E = C
18 4 nn0cni ⊢ B ∈ ℂ
19 13 18 9 mulcomli ⊢ B ⁢ P = T ⁢ E + D
20 1 2 3 4 5 6 7 17 19 nummul1c ⊢ N ⁢ P = T ⁢ C + D
21 12 13 20 mulcomli ⊢ P ⋅ N = T ⁢ C + D