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	⊢ ( 𝑁 · 𝑃 ) = ( ( 𝑇 · 𝐶 ) + 𝐷 )