Metamath Proof Explorer

Theorem dvdsmulc

Description: Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 3simpc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2 zmulcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 · 𝐾 ) ∈ ℤ )
3 2 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 · 𝐾 ) ∈ ℤ )
4 zmulcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 · 𝐾 ) ∈ ℤ )
5 4 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 · 𝐾 ) ∈ ℤ )
6 3 5 jca ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 · 𝐾 ) ∈ ℤ ∧ ( 𝑁 · 𝐾 ) ∈ ℤ ) )
7 6 3comr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 · 𝐾 ) ∈ ℤ ∧ ( 𝑁 · 𝐾 ) ∈ ℤ ) )
8 simpr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
9 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
10 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
11 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
12 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = ( 𝑥 · ( 𝑀 · 𝐾 ) ) )
13 9 10 11 12 syl3an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = ( 𝑥 · ( 𝑀 · 𝐾 ) ) )
14 13 3com13 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = ( 𝑥 · ( 𝑀 · 𝐾 ) ) )
15 14 3expa ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = ( 𝑥 · ( 𝑀 · 𝐾 ) ) )
16 15 3adantl3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = ( 𝑥 · ( 𝑀 · 𝐾 ) ) )
17 oveq1 ⊢ ( ( 𝑥 · 𝑀 ) = 𝑁 → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = ( 𝑁 · 𝐾 ) )
18 16 17 sylan9req ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑥 · 𝑀 ) = 𝑁 ) → ( 𝑥 · ( 𝑀 · 𝐾 ) ) = ( 𝑁 · 𝐾 ) )
19 18 ex ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = 𝑁 → ( 𝑥 · ( 𝑀 · 𝐾 ) ) = ( 𝑁 · 𝐾 ) ) )
20 1 7 8 19 dvds1lem ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝑀 · 𝐾 ) ∥ ( 𝑁 · 𝐾 ) ) )
21 20 3coml ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝑀 · 𝐾 ) ∥ ( 𝑁 · 𝐾 ) ) )