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∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N↔P∥M∨P∥N

Proof

Step Hyp Ref Expression
1 coprm ⊢P∈ℙ∧M∈ℤ→¬P∥M↔PgcdM=1
2 1 3adant3 ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→¬P∥M↔PgcdM=1
3 2 anbi2d ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N∧¬P∥M↔P∥ M⋅ N∧PgcdM=1
4 prmz ⊢P∈ℙ→P∈ℤ
5 coprmdvds ⊢P∈ℤ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N∧PgcdM=1→P∥N
6 4 5 syl3an1 ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N∧PgcdM=1→P∥N
7 3 6 sylbid ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N∧¬P∥M→P∥N
8 7 expd ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N→¬P∥M→P∥N
9 df-or ⊢P∥M∨P∥N↔¬P∥M→P∥N
10 8 9 imbitrrdi ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N→P∥M∨P∥N
11 ordvdsmul ⊢P∈ℤ∧M∈ℤ∧N∈ℤ→P∥M∨P∥N→P∥ M⋅ N
12 4 11 syl3an1 ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥M∨P∥N→P∥ M⋅ N
13 10 12 impbid ⊢P∈ℙ∧M∈ℤ∧N∈ℤ→P∥ M⋅ N↔P∥M∨P∥N