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

Metamath Proof Explorer

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 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )