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 e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M x. N ) /\ ( K gcd M ) = 1 ) -> K || N ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( M e. ZZ -> M e. CC )
2 zcn 
 |-  ( N e. ZZ -> N e. CC )
3 mulcom 
 |-  ( ( M e. CC /\ N e. CC ) -> ( M x. N ) = ( N x. M ) )
4 1 2 3 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) = ( N x. M ) )
5 4 breq2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K || ( M x. N ) <-> K || ( N x. M ) ) )
6 dvdsmulgcd 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( K || ( N x. M ) <-> K || ( N x. ( M gcd K ) ) ) )
7 6 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K || ( N x. M ) <-> K || ( N x. ( M gcd K ) ) ) )
8 5 7 bitrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K || ( M x. N ) <-> K || ( N x. ( M gcd K ) ) ) )
9 8 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || ( M x. N ) <-> K || ( N x. ( M gcd K ) ) ) )
10 9 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( K || ( M x. N ) <-> K || ( N x. ( M gcd K ) ) ) )
11 gcdcom 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K gcd M ) = ( M gcd K ) )
12 11 3adant3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd M ) = ( M gcd K ) )
13 12 eqeq1d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd M ) = 1 <-> ( M gcd K ) = 1 ) )
14 oveq2 
 |-  ( ( M gcd K ) = 1 -> ( N x. ( M gcd K ) ) = ( N x. 1 ) )
15 13 14 biimtrdi 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd M ) = 1 -> ( N x. ( M gcd K ) ) = ( N x. 1 ) ) )
16 15 imp 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( N x. ( M gcd K ) ) = ( N x. 1 ) )
17 2 mulridd 
 |-  ( N e. ZZ -> ( N x. 1 ) = N )
18 17 3ad2ant3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( N x. 1 ) = N )
19 18 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( N x. 1 ) = N )
20 16 19 eqtrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( N x. ( M gcd K ) ) = N )
21 20 breq2d 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( K || ( N x. ( M gcd K ) ) <-> K || N ) )
22 10 21 bitrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( K || ( M x. N ) <-> K || N ) )
23 22 biimpd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd M ) = 1 ) -> ( K || ( M x. N ) -> K || N ) )
24 23 ex 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd M ) = 1 -> ( K || ( M x. N ) -> K || N ) ) )
25 24 impcomd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M x. N ) /\ ( K gcd M ) = 1 ) -> K || N ) )