Proof of Theorem nn0o1gt2
Step | Hyp | Ref
| Expression |
1 | | elnn0 9108 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | | elnnnn0c 9151 |
. . . . 5
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁)) |
3 | | 1z 9209 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
4 | | nn0z 9203 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
5 | | zleloe 9230 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 ≤ 𝑁 ↔ (1 < 𝑁 ∨ 1 = 𝑁))) |
6 | 3, 4, 5 | sylancr 411 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1 ≤ 𝑁 ↔ (1
< 𝑁 ∨ 1 = 𝑁))) |
7 | | 1zzd 9210 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℤ) |
8 | | zltp1le 9237 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)) |
9 | 7, 4, 8 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ (1
+ 1) ≤ 𝑁)) |
10 | | 1p1e2 8966 |
. . . . . . . . . . . . . 14
⊢ (1 + 1) =
2 |
11 | 10 | breq1i 3984 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
≤ 𝑁 ↔ 2 ≤ 𝑁) |
12 | 11 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ((1 + 1) ≤ 𝑁
↔ 2 ≤ 𝑁)) |
13 | | 2z 9211 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
14 | | zleloe 9230 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 ≤ 𝑁 ↔ (2 < 𝑁 ∨ 2 = 𝑁))) |
15 | 13, 4, 14 | sylancr 411 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (2 ≤ 𝑁 ↔ (2
< 𝑁 ∨ 2 = 𝑁))) |
16 | 9, 12, 15 | 3bitrd 213 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 ↔ (2
< 𝑁 ∨ 2 = 𝑁))) |
17 | | olc 701 |
. . . . . . . . . . . . . 14
⊢ (2 <
𝑁 → (𝑁 = 1 ∨ 2 < 𝑁)) |
18 | 17 | 2a1d 23 |
. . . . . . . . . . . . 13
⊢ (2 <
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
19 | | oveq1 5844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = 2 → (𝑁 + 1) = (2 + 1)) |
20 | 19 | oveq1d 5852 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = 2 → ((𝑁 + 1) / 2) = ((2 + 1) / 2)) |
21 | 20 | eqcoms 2167 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 =
𝑁 → ((𝑁 + 1) / 2) = ((2 + 1) /
2)) |
22 | 21 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) → ((𝑁 + 1) / 2) = ((2 + 1) /
2)) |
23 | | 2p1e3 8982 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 + 1) =
3 |
24 | 23 | oveq1i 5847 |
. . . . . . . . . . . . . . . . 17
⊢ ((2 + 1)
/ 2) = (3 / 2) |
25 | 22, 24 | eqtrdi 2213 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) → ((𝑁 + 1) / 2) = (3 /
2)) |
26 | 25 | eleq1d 2233 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) →
(((𝑁 + 1) / 2) ∈
ℕ0 ↔ (3 / 2) ∈
ℕ0)) |
27 | | 3halfnz 9280 |
. . . . . . . . . . . . . . . 16
⊢ ¬ (3
/ 2) ∈ ℤ |
28 | | nn0z 9203 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 2)
∈ ℕ0 → (3 / 2) ∈ ℤ) |
29 | 28 | pm2.24d 612 |
. . . . . . . . . . . . . . . 16
⊢ ((3 / 2)
∈ ℕ0 → (¬ (3 / 2) ∈ ℤ → (𝑁 = 1 ∨ 2 < 𝑁))) |
30 | 27, 29 | mpi 15 |
. . . . . . . . . . . . . . 15
⊢ ((3 / 2)
∈ ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)) |
31 | 26, 30 | syl6bi 162 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 2 = 𝑁) →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
32 | 31 | expcom 115 |
. . . . . . . . . . . . 13
⊢ (2 =
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
33 | 18, 32 | jaoi 706 |
. . . . . . . . . . . 12
⊢ ((2 <
𝑁 ∨ 2 = 𝑁) → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
34 | 33 | com12 30 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ ((2 < 𝑁 ∨ 2 =
𝑁) → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
35 | 16, 34 | sylbid 149 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (1 < 𝑁 →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
36 | 35 | com12 30 |
. . . . . . . . 9
⊢ (1 <
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
37 | | orc 702 |
. . . . . . . . . . 11
⊢ (𝑁 = 1 → (𝑁 = 1 ∨ 2 < 𝑁)) |
38 | 37 | eqcoms 2167 |
. . . . . . . . . 10
⊢ (1 =
𝑁 → (𝑁 = 1 ∨ 2 < 𝑁)) |
39 | 38 | 2a1d 23 |
. . . . . . . . 9
⊢ (1 =
𝑁 → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
40 | 36, 39 | jaoi 706 |
. . . . . . . 8
⊢ ((1 <
𝑁 ∨ 1 = 𝑁) → (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
41 | 40 | com12 30 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((1 < 𝑁 ∨ 1 =
𝑁) → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
42 | 6, 41 | sylbid 149 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1 ≤ 𝑁 →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)))) |
43 | 42 | imp 123 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 1 ≤ 𝑁) →
(((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
44 | 2, 43 | sylbi 120 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
45 | | oveq1 5844 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 + 1) = (0 + 1)) |
46 | | 0p1e1 8963 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
47 | 45, 46 | eqtrdi 2213 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝑁 + 1) = 1) |
48 | 47 | oveq1d 5852 |
. . . . . 6
⊢ (𝑁 = 0 → ((𝑁 + 1) / 2) = (1 / 2)) |
49 | 48 | eleq1d 2233 |
. . . . 5
⊢ (𝑁 = 0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔
(1 / 2) ∈ ℕ0)) |
50 | | halfnz 9279 |
. . . . . 6
⊢ ¬ (1
/ 2) ∈ ℤ |
51 | | nn0z 9203 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℕ0 → (1 / 2) ∈ ℤ) |
52 | 51 | pm2.24d 612 |
. . . . . 6
⊢ ((1 / 2)
∈ ℕ0 → (¬ (1 / 2) ∈ ℤ → (𝑁 = 1 ∨ 2 < 𝑁))) |
53 | 50, 52 | mpi 15 |
. . . . 5
⊢ ((1 / 2)
∈ ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁)) |
54 | 49, 53 | syl6bi 162 |
. . . 4
⊢ (𝑁 = 0 → (((𝑁 + 1) / 2) ∈ ℕ0 →
(𝑁 = 1 ∨ 2 < 𝑁))) |
55 | 44, 54 | jaoi 706 |
. . 3
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (((𝑁 + 1) / 2) ∈
ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
56 | 1, 55 | sylbi 120 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) / 2)
∈ ℕ0 → (𝑁 = 1 ∨ 2 < 𝑁))) |
57 | 56 | imp 123 |
1
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |