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 ( 𝑃 ∈ ℙ → ( 𝑃 = 2 ∨ ¬ 2 ∥ 𝑃 ) )

Proof

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