Proof of Theorem nn0o1gt2
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 2 | | elnnnn0c 12571 |
. . . . 5
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁)) |
| 3 | | 1red 11262 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℝ) |
| 4 | | nn0re 12535 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 5 | 3, 4 | leloed 11404 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1 ≤ 𝑁 ↔ (1
< 𝑁 ∨ 1 = 𝑁))) |
| 6 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℤ) |
| 7 | | nn0z 12638 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 8 | | zltp1le 12667 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)) |
| 9 | 6, 7, 8 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ (1
+ 1) ≤ 𝑁)) |
| 10 | | 1p1e2 12391 |
. . . . . . . . . . . . . 14
⊢ (1 + 1) =
2 |
| 11 | 10 | breq1i 5150 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
≤ 𝑁 ↔ 2 ≤ 𝑁) |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ((1 + 1) ≤ 𝑁
↔ 2 ≤ 𝑁)) |
| 13 | | 2re 12340 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
| 14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℝ) |
| 15 | 14, 4 | leloed 11404 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (2 ≤ 𝑁 ↔ (2
< 𝑁 ∨ 2 = 𝑁))) |
| 16 | 9, 12, 15 | 3bitrd 305 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ (2
< 𝑁 ∨ 2 = 𝑁))) |
| 17 | | olc 869 |
. . . . . . . . . . . . . 14
⊢ (2 <
𝑁 → (𝑁 = 1 ∨ 2 < 𝑁)) |
| 18 | 17 | 2a1d 26 |
. . . . . . . . . . . . 13
⊢ (2 <
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 19 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = 2 → (𝑁 + 1) = (2 + 1)) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = 2 → ((𝑁 + 1) / 2) = ((2 + 1) / 2)) |
| 21 | 20 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 =
𝑁 → ((𝑁 + 1) / 2) = ((2 + 1) /
2)) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) → ((𝑁 + 1) / 2) = ((2 + 1) /
2)) |
| 23 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 + 1) =
3 |
| 24 | 23 | oveq1i 7441 |
. . . . . . . . . . . . . . . . 17
⊢ ((2 + 1)
/ 2) = (3 / 2) |
| 25 | 22, 24 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) → ((𝑁 + 1) / 2) = (3 /
2)) |
| 26 | 25 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) →
(((𝑁 + 1) / 2) ∈
ℕ0 ↔ (3 / 2) ∈
ℕ0)) |
| 27 | | 3halfnz 12697 |
. . . . . . . . . . . . . . . 16
⊢ ¬ (3
/ 2) ∈ ℤ |
| 28 | | nn0z 12638 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 2)
∈ ℕ0 → (3 / 2) ∈ ℤ) |
| 29 | 28 | pm2.24d 151 |
. . . . . . . . . . . . . . . 16
⊢ ((3 / 2)
∈ ℕ0 → (¬ (3 / 2) ∈ ℤ → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 30 | 27, 29 | mpi 20 |
. . . . . . . . . . . . . . 15
⊢ ((3 / 2)
∈ ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)) |
| 31 | 26, 30 | biimtrdi 253 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 32 | 31 | expcom 413 |
. . . . . . . . . . . . 13
⊢ (2 =
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 33 | 18, 32 | jaoi 858 |
. . . . . . . . . . . 12
⊢ ((2 <
𝑁 ∨ 2 = 𝑁) → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 34 | 33 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ ((2 < 𝑁 ∨ 2 =
𝑁) → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 35 | 16, 34 | sylbid 240 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 36 | 35 | com12 32 |
. . . . . . . . 9
⊢ (1 <
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 37 | | orc 868 |
. . . . . . . . . . 11
⊢ (𝑁 = 1 → (𝑁 = 1 ∨ 2 < 𝑁)) |
| 38 | 37 | eqcoms 2745 |
. . . . . . . . . 10
⊢ (1 =
𝑁 → (𝑁 = 1 ∨ 2 < 𝑁)) |
| 39 | 38 | 2a1d 26 |
. . . . . . . . 9
⊢ (1 =
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 40 | 36, 39 | jaoi 858 |
. . . . . . . 8
⊢ ((1 <
𝑁 ∨ 1 = 𝑁) → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 41 | 40 | com12 32 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((1 < 𝑁 ∨ 1 =
𝑁) → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 42 | 5, 41 | sylbid 240 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1 ≤ 𝑁 →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
| 43 | 42 | imp 406 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁) →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 44 | 2, 43 | sylbi 217 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 45 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 + 1) = (0 + 1)) |
| 46 | | 0p1e1 12388 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 47 | 45, 46 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝑁 + 1) = 1) |
| 48 | 47 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 = 0 → ((𝑁 + 1) / 2) = (1 / 2)) |
| 49 | 48 | eleq1d 2826 |
. . . . 5
⊢ (𝑁 = 0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔
(1 / 2) ∈ ℕ0)) |
| 50 | | halfnz 12696 |
. . . . . 6
⊢ ¬ (1
/ 2) ∈ ℤ |
| 51 | | nn0z 12638 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℕ0 → (1 / 2) ∈ ℤ) |
| 52 | 51 | pm2.24d 151 |
. . . . . 6
⊢ ((1 / 2)
∈ ℕ0 → (¬ (1 / 2) ∈ ℤ → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 53 | 50, 52 | mpi 20 |
. . . . 5
⊢ ((1 / 2)
∈ ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)) |
| 54 | 49, 53 | biimtrdi 253 |
. . . 4
⊢ (𝑁 = 0 → (((𝑁 + 1) / 2) ∈ ℕ0 →
(𝑁 = 1 ∨ 2 < 𝑁))) |
| 55 | 44, 54 | jaoi 858 |
. . 3
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 56 | 1, 55 | sylbi 217 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) / 2)
∈ ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
| 57 | 56 | imp 406 |
1
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |