Metamath Proof Explorer


Theorem dvdscmul

Description: Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in ApostolNT p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

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