Metamath Proof Explorer

Theorem 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 ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ⋅ N ∧ K gcd M = 1 → K ∥ N

Proof

Step Hyp Ref Expression
1 zcn ⊢ M ∈ ℤ → M ∈ ℂ
2 zcn ⊢ N ∈ ℤ → N ∈ ℂ
3 mulcom ⊢ M ∈ ℂ ∧ N ∈ ℂ → M ⋅ N = N ⋅ M
4 1 2 3 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ⋅ N = N ⋅ M
5 4 breq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ⋅ N ↔ K ∥ N ⋅ M
6 dvdsmulgcd ⊢ N ∈ ℤ ∧ M ∈ ℤ → K ∥ N ⋅ M ↔ K ∥ N ⁢ M gcd K
7 6 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∥ N ⋅ M ↔ K ∥ N ⁢ M gcd K
8 5 7 bitrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ⋅ N ↔ K ∥ N ⁢ M gcd K
9 8 3adant1 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ⋅ N ↔ K ∥ N ⁢ M gcd K
10 9 adantr ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → K ∥ M ⋅ N ↔ K ∥ N ⁢ M gcd K
11 gcdcom ⊢ K ∈ ℤ ∧ M ∈ ℤ → K gcd M = M gcd K
12 11 3adant3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K gcd M = M gcd K
13 12 eqeq1d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K gcd M = 1 ↔ M gcd K = 1
14 oveq2 ⊢ M gcd K = 1 → N ⁢ M gcd K = N ⋅ 1
15 13 14 biimtrdi ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K gcd M = 1 → N ⁢ M gcd K = N ⋅ 1
16 15 imp ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → N ⁢ M gcd K = N ⋅ 1
17 2 mulridd ⊢ N ∈ ℤ → N ⋅ 1 = N
18 17 3ad2ant3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → N ⋅ 1 = N
19 18 adantr ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → N ⋅ 1 = N
20 16 19 eqtrd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → N ⁢ M gcd K = N
21 20 breq2d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → K ∥ N ⁢ M gcd K ↔ K ∥ N
22 10 21 bitrd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → K ∥ M ⋅ N ↔ K ∥ N
23 22 biimpd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ K gcd M = 1 → K ∥ M ⋅ N → K ∥ N
24 23 ex ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K gcd M = 1 → K ∥ M ⋅ N → K ∥ N
25 24 impcomd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ⋅ N ∧ K gcd M = 1 → K ∥ N