coprmdvdsb

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

		Ref	Expression
	Assertion	coprmdvdsb	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to (K ∥ N \leftrightarrow K ∥ M \cdot N)$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to K \in ℤ$
2		simp3l	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to M \in ℤ$
3		simp2	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to N \in ℤ$
4		dvdsmultr2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ N \to K ∥ M \cdot N)$
5	1 2 3 4	syl3anc	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to (K ∥ N \to K ∥ M \cdot N)$
6		simp3r	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to K \gcd M = 1$
7		coprmdvds	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \cdot N \land K \gcd M = 1) \to K ∥ N)$
8	1 2 3 7	syl3anc	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to ((K ∥ M \cdot N \land K \gcd M = 1) \to K ∥ N)$
9	6 8	mpan2d	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to (K ∥ M \cdot N \to K ∥ N)$
10	5 9	impbid	$⊢ (K \in ℤ \land N \in ℤ \land (M \in ℤ \land K \gcd M = 1)) \to (K ∥ N \leftrightarrow K ∥ M \cdot N)$

Metamath Proof Explorer