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

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
2 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
3 mulcom ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 · 𝑁 ) = ( 𝑁 · 𝑀 ) )
4 1 2 3 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) = ( 𝑁 · 𝑀 ) )
5 4 breq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ↔ 𝐾 ∥ ( 𝑁 · 𝑀 ) ) )
6 dvdsmulgcd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑁 · 𝑀 ) ↔ 𝐾 ∥ ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) ) )
7 6 ancoms ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑁 · 𝑀 ) ↔ 𝐾 ∥ ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) ) )
8 5 7 bitrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ↔ 𝐾 ∥ ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) ) )
9 8 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ↔ 𝐾 ∥ ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) ) )
10 9 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ↔ 𝐾 ∥ ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) ) )
11 gcdcom ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 gcd 𝑀 ) = ( 𝑀 gcd 𝐾 ) )
12 11 3adant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 gcd 𝑀 ) = ( 𝑀 gcd 𝐾 ) )
13 12 eqeq1d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) = 1 ↔ ( 𝑀 gcd 𝐾 ) = 1 ) )
14 oveq2 ⊢ ( ( 𝑀 gcd 𝐾 ) = 1 → ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) = ( 𝑁 · 1 ) )
15 13 14 syl6bi ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) = 1 → ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) = ( 𝑁 · 1 ) ) )
16 15 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) = ( 𝑁 · 1 ) )
17 2 mulid1d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 · 1 ) = 𝑁 )
18 17 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 1 ) = 𝑁 )
19 18 adantr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝑁 · 1 ) = 𝑁 )
20 16 19 eqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) = 𝑁 )
21 20 breq2d ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 ∥ ( 𝑁 · ( 𝑀 gcd 𝐾 ) ) ↔ 𝐾 ∥ 𝑁 ) )
22 10 21 bitrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ↔ 𝐾 ∥ 𝑁 ) )
23 22 biimpd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) → 𝐾 ∥ 𝑁 ) )
24 23 ex ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) = 1 → ( 𝐾 ∥ ( 𝑀 · 𝑁 ) → 𝐾 ∥ 𝑁 ) ) )
25 24 impcomd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 · 𝑁 ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → 𝐾 ∥ 𝑁 ) )