Metamath Proof Explorer

Theorem nn0o1gt2

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

Ref Expression
Assertion nn0o1gt2 ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 elnnnn0c ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) )
3 1red ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
4 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
5 3 4 leloed ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ≤ 𝑁 ↔ ( 1 < 𝑁 ∨ 1 = 𝑁 ) ) )
6 1zzd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℤ )
7 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
8 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 < 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 ) )
9 6 7 8 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( 1 < 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 ) )
10 1p1e2 ⊢ ( 1 + 1 ) = 2
11 10 breq1i ⊢ ( ( 1 + 1 ) ≤ 𝑁 ↔ 2 ≤ 𝑁 )
12 11 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 + 1 ) ≤ 𝑁 ↔ 2 ≤ 𝑁 ) )
13 2re ⊢ 2 ∈ ℝ
14 13 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
15 14 4 leloed ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ≤ 𝑁 ↔ ( 2 < 𝑁 ∨ 2 = 𝑁 ) ) )
16 9 12 15 3bitrd ⊢ ( 𝑁 ∈ ℕ0 → ( 1 < 𝑁 ↔ ( 2 < 𝑁 ∨ 2 = 𝑁 ) ) )
17 olc ⊢ ( 2 < 𝑁 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
18 17 2a1d ⊢ ( 2 < 𝑁 → ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
19 oveq1 ⊢ ( 𝑁 = 2 → ( 𝑁 + 1 ) = ( 2 + 1 ) )
20 19 oveq1d ⊢ ( 𝑁 = 2 → ( ( 𝑁 + 1 ) / 2 ) = ( ( 2 + 1 ) / 2 ) )
21 20 eqcoms ⊢ ( 2 = 𝑁 → ( ( 𝑁 + 1 ) / 2 ) = ( ( 2 + 1 ) / 2 ) )
22 21 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 = 𝑁 ) → ( ( 𝑁 + 1 ) / 2 ) = ( ( 2 + 1 ) / 2 ) )
23 2p1e3 ⊢ ( 2 + 1 ) = 3
24 23 oveq1i ⊢ ( ( 2 + 1 ) / 2 ) = ( 3 / 2 )
25 22 24 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 = 𝑁 ) → ( ( 𝑁 + 1 ) / 2 ) = ( 3 / 2 ) )
26 25 eleq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 = 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( 3 / 2 ) ∈ ℕ0 ) )
27 3halfnz ⊢ ¬ ( 3 / 2 ) ∈ ℤ
28 nn0z ⊢ ( ( 3 / 2 ) ∈ ℕ0 → ( 3 / 2 ) ∈ ℤ )
29 28 pm2.24d ⊢ ( ( 3 / 2 ) ∈ ℕ0 → ( ¬ ( 3 / 2 ) ∈ ℤ → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
30 27 29 mpi ⊢ ( ( 3 / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
31 26 30 biimtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 = 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
32 31 expcom ⊢ ( 2 = 𝑁 → ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
33 18 32 jaoi ⊢ ( ( 2 < 𝑁 ∨ 2 = 𝑁 ) → ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
34 33 com12 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 < 𝑁 ∨ 2 = 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
35 16 34 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 1 < 𝑁 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
36 35 com12 ⊢ ( 1 < 𝑁 → ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
37 orc ⊢ ( 𝑁 = 1 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
38 37 eqcoms ⊢ ( 1 = 𝑁 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
39 38 2a1d ⊢ ( 1 = 𝑁 → ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
40 36 39 jaoi ⊢ ( ( 1 < 𝑁 ∨ 1 = 𝑁 ) → ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
41 40 com12 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 < 𝑁 ∨ 1 = 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
42 5 41 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ≤ 𝑁 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) ) )
43 42 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
44 2 43 sylbi ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
45 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 + 1 ) = ( 0 + 1 ) )
46 0p1e1 ⊢ ( 0 + 1 ) = 1
47 45 46 eqtrdi ⊢ ( 𝑁 = 0 → ( 𝑁 + 1 ) = 1 )
48 47 oveq1d ⊢ ( 𝑁 = 0 → ( ( 𝑁 + 1 ) / 2 ) = ( 1 / 2 ) )
49 48 eleq1d ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( 1 / 2 ) ∈ ℕ0 ) )
50 halfnz ⊢ ¬ ( 1 / 2 ) ∈ ℤ
51 nn0z ⊢ ( ( 1 / 2 ) ∈ ℕ0 → ( 1 / 2 ) ∈ ℤ )
52 51 pm2.24d ⊢ ( ( 1 / 2 ) ∈ ℕ0 → ( ¬ ( 1 / 2 ) ∈ ℤ → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
53 50 52 mpi ⊢ ( ( 1 / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
54 49 53 biimtrdi ⊢ ( 𝑁 = 0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
55 44 54 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
56 1 55 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( 𝑁 = 1 ∨ 2 < 𝑁 ) ) )
57 56 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )