Theorem dvdsmultr2

Description: If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012)

	Ref	Expression
Assertion	dvdsmultr2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsmul2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )
2	1	biantrud	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 ↔ ( 𝐾 ∥ 𝑁 ∧ 𝑁 ∥ ( 𝑀 · 𝑁 ) ) ) )
3	2	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 ↔ ( 𝐾 ∥ 𝑁 ∧ 𝑁 ∥ ( 𝑀 · 𝑁 ) ) ) )
4		simp1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
5		simp3	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
6		zmulcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
7	6	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
8		dvdstr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( 𝐾 ∥ 𝑁 ∧ 𝑁 ∥ ( 𝑀 · 𝑁 ) ) → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )
9	4 5 7 8	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑁 ∧ 𝑁 ∥ ( 𝑀 · 𝑁 ) ) → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )
10	3 9	sylbid	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )