Theorem coprmdvdsb

Description: Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014)

	Ref	Expression
Assertion	coprmdvdsb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → ( 𝐾 ∥ 𝑁 ↔ 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → 𝐾 ∈ ℤ )
2		simp3l	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → 𝑀 ∈ ℤ )
3		simp2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → 𝑁 ∈ ℤ )
4		dvdsmultr2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )
6		simp3r	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → ( 𝐾 gcd 𝑀 ) = 1 )
7		coprmdvds	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → 𝐾 ∥ 𝑁 ) )
8	1 2 3 7	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → ( ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → 𝐾 ∥ 𝑁 ) )
9	6 8	mpan2d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) → 𝐾 ∥ 𝑁 ) )
10	5 9	impbid	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ ( 𝐾 gcd 𝑀 ) = 1 ) ) → ( 𝐾 ∥ 𝑁 ↔ 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )