This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ↔ ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑀 ↔ ( 𝑃 gcd 𝑀 ) = 1 ) )
2 1 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑀 ↔ ( 𝑃 gcd 𝑀 ) = 1 ) )
3 2 anbi2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ∧ ¬ 𝑃 ∥ 𝑀 ) ↔ ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ∧ ( 𝑃 gcd 𝑀 ) = 1 ) ) )
4 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
5 coprmdvds ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ∧ ( 𝑃 gcd 𝑀 ) = 1 ) → 𝑃 ∥ 𝑁 ) )
6 4 5 syl3an1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ∧ ( 𝑃 gcd 𝑀 ) = 1 ) → 𝑃 ∥ 𝑁 ) )
7 3 6 sylbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ∧ ¬ 𝑃 ∥ 𝑀 ) → 𝑃 ∥ 𝑁 ) )
8 7 expd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑁 ) → ( ¬ 𝑃 ∥ 𝑀 → 𝑃 ∥ 𝑁 ) ) )
9 df-or ⊢ ( ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁 ) ↔ ( ¬ 𝑃 ∥ 𝑀 → 𝑃 ∥ 𝑁 ) )
10 8 9 imbitrrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑁 ) → ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁 ) ) )
11 ordvdsmul ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ ( 𝑀 · 𝑁 ) ) )
12 4 11 syl3an1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ ( 𝑀 · 𝑁 ) ) )
13 10 12 impbid ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑀 · 𝑁 ) ↔ ( 𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁 ) ) )