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