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

Metamath Proof Explorer

Theorem oddprmALTV

Description: A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015) (Revised by AV, 21-Jun-2020)

Ref Expression
Assertion oddprmALTV ⊢ N ∈ ℙ ∖ 2 → N ∈ Odd

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ N ∈ ℙ ∖ 2 ↔ N ∈ ℙ ∧ N ≠ 2
2 prmz ⊢ N ∈ ℙ → N ∈ ℤ
3 2 adantr ⊢ N ∈ ℙ ∧ N ≠ 2 → N ∈ ℤ
4 necom ⊢ N ≠ 2 ↔ 2 ≠ N
5 df-ne ⊢ 2 ≠ N ↔ ¬ 2 = N
6 4 5 sylbb ⊢ N ≠ 2 → ¬ 2 = N
7 6 adantl ⊢ N ∈ ℙ ∧ N ≠ 2 → ¬ 2 = N
8 1ne2 ⊢ 1 ≠ 2
9 8 nesymi ⊢ ¬ 2 = 1
10 9 a1i ⊢ N ∈ ℙ ∧ N ≠ 2 → ¬ 2 = 1
11 ioran ⊢ ¬ 2 = N ∨ 2 = 1 ↔ ¬ 2 = N ∧ ¬ 2 = 1
12 7 10 11 sylanbrc ⊢ N ∈ ℙ ∧ N ≠ 2 → ¬ 2 = N ∨ 2 = 1
13 2nn ⊢ 2 ∈ ℕ
14 13 a1i ⊢ N ≠ 2 → 2 ∈ ℕ
15 dvdsprime ⊢ N ∈ ℙ ∧ 2 ∈ ℕ → 2 ∥ N ↔ 2 = N ∨ 2 = 1
16 14 15 sylan2 ⊢ N ∈ ℙ ∧ N ≠ 2 → 2 ∥ N ↔ 2 = N ∨ 2 = 1
17 12 16 mtbird ⊢ N ∈ ℙ ∧ N ≠ 2 → ¬ 2 ∥ N
18 isodd3 ⊢ N ∈ Odd ↔ N ∈ ℤ ∧ ¬ 2 ∥ N
19 3 17 18 sylanbrc ⊢ N ∈ ℙ ∧ N ≠ 2 → N ∈ Odd
20 1 19 sylbi ⊢ N ∈ ℙ ∖ 2 → N ∈ Odd