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

Metamath Proof Explorer

Theorem prm2orodd

Description: A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021)

Ref Expression
Assertion prm2orodd ⊢ P ∈ ℙ → P = 2 ∨ ¬ 2 ∥ P

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 dvdsprime ⊢ P ∈ ℙ ∧ 2 ∈ ℕ → 2 ∥ P ↔ 2 = P ∨ 2 = 1
3 1 2 mpan2 ⊢ P ∈ ℙ → 2 ∥ P ↔ 2 = P ∨ 2 = 1
4 eqcom ⊢ 2 = P ↔ P = 2
5 4 biimpi ⊢ 2 = P → P = 2
6 1ne2 ⊢ 1 ≠ 2
7 necom ⊢ 1 ≠ 2 ↔ 2 ≠ 1
8 eqneqall ⊢ 2 = 1 → 2 ≠ 1 → P = 2
9 8 com12 ⊢ 2 ≠ 1 → 2 = 1 → P = 2
10 7 9 sylbi ⊢ 1 ≠ 2 → 2 = 1 → P = 2
11 6 10 ax-mp ⊢ 2 = 1 → P = 2
12 5 11 jaoi ⊢ 2 = P ∨ 2 = 1 → P = 2
13 3 12 biimtrdi ⊢ P ∈ ℙ → 2 ∥ P → P = 2
14 13 con3d ⊢ P ∈ ℙ → ¬ P = 2 → ¬ 2 ∥ P
15 14 orrd ⊢ P ∈ ℙ → P = 2 ∨ ¬ 2 ∥ P