coprmdvds

Description: Euclid's Lemma (see ProofWiki "Euclid's Lemma", 10-Jul-2021, https://proofwiki.org/wiki/Euclid's_Lemma ): If an integer divides the product of two integers and is coprime to one of them, then it divides the other. See also theorem 1.5 in ApostolNT p. 16. Generalization of euclemma . (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by AV, 10-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ M \in ℤ \to M \in ℂ$
2		zcn	$⊢ N \in ℤ \to N \in ℂ$
3		mulcom	$⊢ (M \in ℂ \land N \in ℂ) \to M \cdot N = N \cdot M$
4	1 2 3	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N = N \cdot M$
5	4	breq2d	$⊢ (M \in ℤ \land N \in ℤ) \to (K ∥ M \cdot N \leftrightarrow K ∥ N \cdot M)$
6		dvdsmulgcd	$⊢ (N \in ℤ \land M \in ℤ) \to (K ∥ N \cdot M \leftrightarrow K ∥ N (M \gcd K))$
7	6	ancoms	$⊢ (M \in ℤ \land N \in ℤ) \to (K ∥ N \cdot M \leftrightarrow K ∥ N (M \gcd K))$
8	5 7	bitrd	$⊢ (M \in ℤ \land N \in ℤ) \to (K ∥ M \cdot N \leftrightarrow K ∥ N (M \gcd K))$
9	8	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ M \cdot N \leftrightarrow K ∥ N (M \gcd K))$
10	9	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to (K ∥ M \cdot N \leftrightarrow K ∥ N (M \gcd K))$
11		gcdcom	$⊢ (K \in ℤ \land M \in ℤ) \to K \gcd M = M \gcd K$
12	11	3adant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \gcd M = M \gcd K$
13	12	eqeq1d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M = 1 \leftrightarrow M \gcd K = 1)$
14		oveq2	$⊢ M \gcd K = 1 \to N (M \gcd K) = N \cdot 1$
15	13 14	syl6bi	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M = 1 \to N (M \gcd K) = N \cdot 1)$
16	15	imp	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to N (M \gcd K) = N \cdot 1$
17	2	mulid1d	$⊢ N \in ℤ \to N \cdot 1 = N$
18	17	3ad2ant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N \cdot 1 = N$
19	18	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to N \cdot 1 = N$
20	16 19	eqtrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to N (M \gcd K) = N$
21	20	breq2d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to (K ∥ N (M \gcd K) \leftrightarrow K ∥ N)$
22	10 21	bitrd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to (K ∥ M \cdot N \leftrightarrow K ∥ N)$
23	22	biimpd	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K \gcd M = 1) \to (K ∥ M \cdot N \to K ∥ N)$
24	23	ex	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \gcd M = 1 \to (K ∥ M \cdot N \to K ∥ N))$
25	24	impcomd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \cdot N \land K \gcd M = 1) \to K ∥ N)$

Metamath Proof Explorer

Theorem coprmdvds

Proof