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 ⊢ 𝑇 ∈ ℕ0
nummul1c.2 ⊢ 𝑃 ∈ ℕ0
nummul1c.3 ⊢ 𝐴 ∈ ℕ0
nummul1c.4 ⊢ 𝐵 ∈ ℕ0
nummul1c.5 ⊢ 𝑁 = ( ( 𝑇 · 𝐴 ) + 𝐵 )
nummul1c.6 ⊢ 𝐷 ∈ ℕ0
nummul1c.7 ⊢ 𝐸 ∈ ℕ0
nummul1c.8 ⊢ ( ( 𝐴 · 𝑃 ) + 𝐸 ) = 𝐶
nummul1c.9 ⊢ ( 𝐵 · 𝑃 ) = ( ( 𝑇 · 𝐸 ) + 𝐷 )
Assertion nummul1c ( 𝑁 · 𝑃 ) = ( ( 𝑇 · 𝐶 ) + 𝐷 )

Proof

Step Hyp Ref Expression
1 nummul1c.1 ⊢ 𝑇 ∈ ℕ0
2 nummul1c.2 ⊢ 𝑃 ∈ ℕ0
3 nummul1c.3 ⊢ 𝐴 ∈ ℕ0
4 nummul1c.4 ⊢ 𝐵 ∈ ℕ0
5 nummul1c.5 ⊢ 𝑁 = ( ( 𝑇 · 𝐴 ) + 𝐵 )
6 nummul1c.6 ⊢ 𝐷 ∈ ℕ0
7 nummul1c.7 ⊢ 𝐸 ∈ ℕ0
8 nummul1c.8 ⊢ ( ( 𝐴 · 𝑃 ) + 𝐸 ) = 𝐶
9 nummul1c.9 ⊢ ( 𝐵 · 𝑃 ) = ( ( 𝑇 · 𝐸 ) + 𝐷 )
10 1 3 4 numcl ⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0
11 5 10 eqeltri ⊢ 𝑁 ∈ ℕ0
12 11 2 num0u ⊢ ( 𝑁 · 𝑃 ) = ( ( 𝑁 · 𝑃 ) + 0 )
13 0nn0 ⊢ 0 ∈ ℕ0
14 1 13 num0h ⊢ 0 = ( ( 𝑇 · 0 ) + 0 )
15 7 nn0cni ⊢ 𝐸 ∈ ℂ
16 15 addlidi ⊢ ( 0 + 𝐸 ) = 𝐸
17 16 oveq2i ⊢ ( ( 𝐴 · 𝑃 ) + ( 0 + 𝐸 ) ) = ( ( 𝐴 · 𝑃 ) + 𝐸 )
18 17 8 eqtri ⊢ ( ( 𝐴 · 𝑃 ) + ( 0 + 𝐸 ) ) = 𝐶
19 4 2 num0u ⊢ ( 𝐵 · 𝑃 ) = ( ( 𝐵 · 𝑃 ) + 0 )
20 19 9 eqtr3i ⊢ ( ( 𝐵 · 𝑃 ) + 0 ) = ( ( 𝑇 · 𝐸 ) + 𝐷 )
21 1 3 4 13 13 5 14 2 6 7 18 20 nummac ⊢ ( ( 𝑁 · 𝑃 ) + 0 ) = ( ( 𝑇 · 𝐶 ) + 𝐷 )
22 12 21 eqtri ⊢ ( 𝑁 · 𝑃 ) = ( ( 𝑇 · 𝐶 ) + 𝐷 )