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