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 ↔ P gcd M = 1
2 1 3adant3 ⊢ P ∈ ℙ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ P ∥ M ↔ P gcd M = 1
3 2 anbi2d ⊢ P ∈ ℙ ∧ M ∈ ℤ ∧ N ∈ ℤ → P ∥ M ⋅ N ∧ ¬ P ∥ M ↔ P ∥ M ⋅ N ∧ P gcd M = 1
4 prmz ⊢ P ∈ ℙ → P ∈ ℤ
5 coprmdvds ⊢ P ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → P ∥ M ⋅ N ∧ P gcd M = 1 → P ∥ N
6 4 5 syl3an1 ⊢ P ∈ ℙ ∧ M ∈ ℤ ∧ N ∈ ℤ → P ∥ M ⋅ N ∧ P gcd M = 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