Metamath Proof Explorer

Theorem euclemma

Description: Euclid's lemma. A prime number divides the product of two integers iff it divides at least one of them. Theorem 1.9 in ApostolNT p. 17. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion euclemma 
|- ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( P || ( M x. N ) <-> ( P || M \/ P || N ) ) )

Proof

Step Hyp Ref Expression
1 coprm 
 |-  ( ( P e. Prime /\ M e. ZZ ) -> ( -. P || M <-> ( P gcd M ) = 1 ) )
2 1 3adant3 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( -. P || M <-> ( P gcd M ) = 1 ) )
3 2 anbi2d 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || ( M x. N ) /\ -. P || M ) <-> ( P || ( M x. N ) /\ ( P gcd M ) = 1 ) ) )
4 prmz 
 |-  ( P e. Prime -> P e. ZZ )
5 coprmdvds 
 |-  ( ( P e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || ( M x. N ) /\ ( P gcd M ) = 1 ) -> P || N ) )
6 4 5 syl3an1 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || ( M x. N ) /\ ( P gcd M ) = 1 ) -> P || N ) )
7 3 6 sylbid 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || ( M x. N ) /\ -. P || M ) -> P || N ) )
8 7 expd 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( P || ( M x. N ) -> ( -. P || M -> P || N ) ) )
9 df-or 
 |-  ( ( P || M \/ P || N ) <-> ( -. P || M -> P || N ) )
10 8 9 imbitrrdi 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( P || ( M x. N ) -> ( P || M \/ P || N ) ) )
11 ordvdsmul 
 |-  ( ( P e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || M \/ P || N ) -> P || ( M x. N ) ) )
12 4 11 syl3an1 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || M \/ P || N ) -> P || ( M x. N ) ) )
13 10 12 impbid 
 |-  ( ( P e. Prime /\ M e. ZZ /\ N e. ZZ ) -> ( P || ( M x. N ) <-> ( P || M \/ P || N ) ) )