Metamath Proof Explorer

Theorem nn0o1gt2ALTV

Description: An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020) (Revised by AV, 21-Jun-2020)

Ref Expression
Assertion nn0o1gt2ALTV ⊢ N ∈ ℕ 0 ∧ N ∈ Odd → N = 1 ∨ 2 < N

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 elnn1uz2 ⊢ N ∈ ℕ ↔ N = 1 ∨ N ∈ ℤ ≥ 2
3 orc ⊢ N = 1 → N = 1 ∨ 2 < N
4 3 a1d ⊢ N = 1 → N ∈ Odd → N = 1 ∨ 2 < N
5 2z ⊢ 2 ∈ ℤ
6 5 eluz1i ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 2 ≤ N
7 2re ⊢ 2 ∈ ℝ
8 7 a1i ⊢ N ∈ ℤ → 2 ∈ ℝ
9 zre ⊢ N ∈ ℤ → N ∈ ℝ
10 8 9 leloed ⊢ N ∈ ℤ → 2 ≤ N ↔ 2 < N ∨ 2 = N
11 olc ⊢ 2 < N → N = 1 ∨ 2 < N
12 11 a1d ⊢ 2 < N → N ∈ Odd → N = 1 ∨ 2 < N
13 eleq1 ⊢ N = 2 → N ∈ Odd ↔ 2 ∈ Odd
14 13 eqcoms ⊢ 2 = N → N ∈ Odd ↔ 2 ∈ Odd
15 2noddALTV ⊢ 2 ∉ Odd
16 df-nel ⊢ 2 ∉ Odd ↔ ¬ 2 ∈ Odd
17 pm2.21 ⊢ ¬ 2 ∈ Odd → 2 ∈ Odd → N = 1 ∨ 2 < N
18 16 17 sylbi ⊢ 2 ∉ Odd → 2 ∈ Odd → N = 1 ∨ 2 < N
19 15 18 ax-mp ⊢ 2 ∈ Odd → N = 1 ∨ 2 < N
20 14 19 syl6bi ⊢ 2 = N → N ∈ Odd → N = 1 ∨ 2 < N
21 12 20 jaoi ⊢ 2 < N ∨ 2 = N → N ∈ Odd → N = 1 ∨ 2 < N
22 10 21 syl6bi ⊢ N ∈ ℤ → 2 ≤ N → N ∈ Odd → N = 1 ∨ 2 < N
23 22 imp ⊢ N ∈ ℤ ∧ 2 ≤ N → N ∈ Odd → N = 1 ∨ 2 < N
24 6 23 sylbi ⊢ N ∈ ℤ ≥ 2 → N ∈ Odd → N = 1 ∨ 2 < N
25 4 24 jaoi ⊢ N = 1 ∨ N ∈ ℤ ≥ 2 → N ∈ Odd → N = 1 ∨ 2 < N
26 2 25 sylbi ⊢ N ∈ ℕ → N ∈ Odd → N = 1 ∨ 2 < N
27 eleq1 ⊢ N = 0 → N ∈ Odd ↔ 0 ∈ Odd
28 0noddALTV ⊢ 0 ∉ Odd
29 df-nel ⊢ 0 ∉ Odd ↔ ¬ 0 ∈ Odd
30 pm2.21 ⊢ ¬ 0 ∈ Odd → 0 ∈ Odd → N = 1 ∨ 2 < N
31 29 30 sylbi ⊢ 0 ∉ Odd → 0 ∈ Odd → N = 1 ∨ 2 < N
32 28 31 ax-mp ⊢ 0 ∈ Odd → N = 1 ∨ 2 < N
33 27 32 syl6bi ⊢ N = 0 → N ∈ Odd → N = 1 ∨ 2 < N
34 26 33 jaoi ⊢ N ∈ ℕ ∨ N = 0 → N ∈ Odd → N = 1 ∨ 2 < N
35 1 34 sylbi ⊢ N ∈ ℕ 0 → N ∈ Odd → N = 1 ∨ 2 < N
36 35 imp ⊢ N ∈ ℕ 0 ∧ N ∈ Odd → N = 1 ∨ 2 < N