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 ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Odd ) → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )

Proof

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