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 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ N → K ∥ M ⋅ N

Proof

Step Hyp Ref Expression
1 dvdsmul2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∥ M ⋅ N
2 1 biantrud ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∥ N ↔ K ∥ N ∧ N ∥ M ⋅ N
3 2 3adant1 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ N ↔ K ∥ N ∧ N ∥ M ⋅ N
4 simp1 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ
5 simp3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ
6 zmulcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ⋅ N ∈ ℤ
7 6 3adant1 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M ⋅ N ∈ ℤ
8 dvdstr ⊢ K ∈ ℤ ∧ N ∈ ℤ ∧ M ⋅ N ∈ ℤ → K ∥ N ∧ N ∥ M ⋅ N → K ∥ M ⋅ N
9 4 5 7 8 syl3anc ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ N ∧ N ∥ M ⋅ N → K ∥ M ⋅ N
10 3 9 sylbid ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ N → K ∥ M ⋅ N