Step | Hyp | Ref
| Expression |
1 | | nncn 11838 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
2 | | peano2cn 11004 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
4 | | 2cn 11905 |
. . . . . 6
⊢ 2 ∈
ℂ |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
6 | | 2ne0 11934 |
. . . . . 6
⊢ 2 ≠
0 |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 2 ≠
0) |
8 | 3, 5, 7 | divcan2d 11610 |
. . . 4
⊢ (𝑁 ∈ ℕ → (2
· ((𝑁 + 1) / 2)) =
(𝑁 + 1)) |
9 | 1, 5, 7 | divcan2d 11610 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 / 2)) = 𝑁) |
10 | 9 | oveq1d 7228 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 / 2)) + 1) =
(𝑁 + 1)) |
11 | 8, 10 | eqtr4d 2780 |
. . 3
⊢ (𝑁 ∈ ℕ → (2
· ((𝑁 + 1) / 2)) =
((2 · (𝑁 / 2)) +
1)) |
12 | | nnz 12199 |
. . . . . 6
⊢ (((𝑁 + 1) / 2) ∈ ℕ →
((𝑁 + 1) / 2) ∈
ℤ) |
13 | | nnz 12199 |
. . . . . 6
⊢ ((𝑁 / 2) ∈ ℕ →
(𝑁 / 2) ∈
ℤ) |
14 | | zneo 12260 |
. . . . . 6
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
(𝑁 / 2) ∈ ℤ)
→ (2 · ((𝑁 + 1)
/ 2)) ≠ ((2 · (𝑁
/ 2)) + 1)) |
15 | 12, 13, 14 | syl2an 599 |
. . . . 5
⊢ ((((𝑁 + 1) / 2) ∈ ℕ ∧
(𝑁 / 2) ∈ ℕ)
→ (2 · ((𝑁 + 1)
/ 2)) ≠ ((2 · (𝑁
/ 2)) + 1)) |
16 | 15 | expcom 417 |
. . . 4
⊢ ((𝑁 / 2) ∈ ℕ →
(((𝑁 + 1) / 2) ∈
ℕ → (2 · ((𝑁 + 1) / 2)) ≠ ((2 · (𝑁 / 2)) + 1))) |
17 | 16 | necon2bd 2956 |
. . 3
⊢ ((𝑁 / 2) ∈ ℕ → ((2
· ((𝑁 + 1) / 2)) =
((2 · (𝑁 / 2)) + 1)
→ ¬ ((𝑁 + 1) / 2)
∈ ℕ)) |
18 | 11, 17 | syl5com 31 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ →
¬ ((𝑁 + 1) / 2) ∈
ℕ)) |
19 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑗 = 1 → (𝑗 + 1) = (1 + 1)) |
20 | 19 | oveq1d 7228 |
. . . . . 6
⊢ (𝑗 = 1 → ((𝑗 + 1) / 2) = ((1 + 1) / 2)) |
21 | 20 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = 1 → (((𝑗 + 1) / 2) ∈ ℕ ↔
((1 + 1) / 2) ∈ ℕ)) |
22 | | oveq1 7220 |
. . . . . 6
⊢ (𝑗 = 1 → (𝑗 / 2) = (1 / 2)) |
23 | 22 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = 1 → ((𝑗 / 2) ∈ ℕ ↔ (1 / 2) ∈
ℕ)) |
24 | 21, 23 | orbi12d 919 |
. . . 4
⊢ (𝑗 = 1 → ((((𝑗 + 1) / 2) ∈ ℕ ∨
(𝑗 / 2) ∈ ℕ)
↔ (((1 + 1) / 2) ∈ ℕ ∨ (1 / 2) ∈
ℕ))) |
25 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
26 | 25 | oveq1d 7228 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑗 + 1) / 2) = ((𝑘 + 1) / 2)) |
27 | 26 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = 𝑘 → (((𝑗 + 1) / 2) ∈ ℕ ↔ ((𝑘 + 1) / 2) ∈
ℕ)) |
28 | | oveq1 7220 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗 / 2) = (𝑘 / 2)) |
29 | 28 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑗 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈
ℕ)) |
30 | 27, 29 | orbi12d 919 |
. . . 4
⊢ (𝑗 = 𝑘 → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
(((𝑘 + 1) / 2) ∈
ℕ ∨ (𝑘 / 2) ∈
ℕ))) |
31 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) |
32 | 31 | oveq1d 7228 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑗 + 1) / 2) = (((𝑘 + 1) + 1) / 2)) |
33 | 32 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (((𝑗 + 1) / 2) ∈ ℕ ↔ (((𝑘 + 1) + 1) / 2) ∈
ℕ)) |
34 | | oveq1 7220 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑗 / 2) = ((𝑘 + 1) / 2)) |
35 | 34 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑗 / 2) ∈ ℕ ↔ ((𝑘 + 1) / 2) ∈
ℕ)) |
36 | 33, 35 | orbi12d 919 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
((((𝑘 + 1) + 1) / 2) ∈
ℕ ∨ ((𝑘 + 1) / 2)
∈ ℕ))) |
37 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
38 | 37 | oveq1d 7228 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑗 + 1) / 2) = ((𝑁 + 1) / 2)) |
39 | 38 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = 𝑁 → (((𝑗 + 1) / 2) ∈ ℕ ↔ ((𝑁 + 1) / 2) ∈
ℕ)) |
40 | | oveq1 7220 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑗 / 2) = (𝑁 / 2)) |
41 | 40 | eleq1d 2822 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑗 / 2) ∈ ℕ ↔ (𝑁 / 2) ∈
ℕ)) |
42 | 39, 41 | orbi12d 919 |
. . . 4
⊢ (𝑗 = 𝑁 → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
(((𝑁 + 1) / 2) ∈
ℕ ∨ (𝑁 / 2) ∈
ℕ))) |
43 | | df-2 11893 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
44 | 43 | oveq1i 7223 |
. . . . . . 7
⊢ (2 / 2) =
((1 + 1) / 2) |
45 | | 2div2e1 11971 |
. . . . . . 7
⊢ (2 / 2) =
1 |
46 | 44, 45 | eqtr3i 2767 |
. . . . . 6
⊢ ((1 + 1)
/ 2) = 1 |
47 | | 1nn 11841 |
. . . . . 6
⊢ 1 ∈
ℕ |
48 | 46, 47 | eqeltri 2834 |
. . . . 5
⊢ ((1 + 1)
/ 2) ∈ ℕ |
49 | 48 | orci 865 |
. . . 4
⊢ (((1 + 1)
/ 2) ∈ ℕ ∨ (1 / 2) ∈ ℕ) |
50 | | peano2nn 11842 |
. . . . . . 7
⊢ ((𝑘 / 2) ∈ ℕ →
((𝑘 / 2) + 1) ∈
ℕ) |
51 | | nncn 11838 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
52 | | add1p1 12081 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℂ → ((𝑘 + 1) + 1) = (𝑘 + 2)) |
53 | 52 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (((𝑘 + 1) + 1) / 2) = ((𝑘 + 2) / 2)) |
54 | | 2cnne0 12040 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
55 | | divdir 11515 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℂ ∧ 2 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑘 + 2) / 2) = ((𝑘 / 2) + (2 / 2))) |
56 | 4, 54, 55 | mp3an23 1455 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℂ → ((𝑘 + 2) / 2) = ((𝑘 / 2) + (2 /
2))) |
57 | 45 | oveq2i 7224 |
. . . . . . . . . . 11
⊢ ((𝑘 / 2) + (2 / 2)) = ((𝑘 / 2) + 1) |
58 | 56, 57 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → ((𝑘 + 2) / 2) = ((𝑘 / 2) + 1)) |
59 | 53, 58 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℂ → (((𝑘 + 1) + 1) / 2) = ((𝑘 / 2) + 1)) |
60 | 51, 59 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (((𝑘 + 1) + 1) / 2) = ((𝑘 / 2) + 1)) |
61 | 60 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) + 1) / 2) ∈ ℕ
↔ ((𝑘 / 2) + 1) ∈
ℕ)) |
62 | 50, 61 | syl5ibr 249 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑘 / 2) ∈ ℕ →
(((𝑘 + 1) + 1) / 2) ∈
ℕ)) |
63 | 62 | orim2d 967 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) / 2) ∈ ℕ ∨
(𝑘 / 2) ∈ ℕ)
→ (((𝑘 + 1) / 2)
∈ ℕ ∨ (((𝑘 +
1) + 1) / 2) ∈ ℕ))) |
64 | | orcom 870 |
. . . . 5
⊢ ((((𝑘 + 1) / 2) ∈ ℕ ∨
(((𝑘 + 1) + 1) / 2) ∈
ℕ) ↔ ((((𝑘 + 1)
+ 1) / 2) ∈ ℕ ∨ ((𝑘 + 1) / 2) ∈ ℕ)) |
65 | 63, 64 | syl6ib 254 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) / 2) ∈ ℕ ∨
(𝑘 / 2) ∈ ℕ)
→ ((((𝑘 + 1) + 1) / 2)
∈ ℕ ∨ ((𝑘 +
1) / 2) ∈ ℕ))) |
66 | 24, 30, 36, 42, 49, 65 | nnind 11848 |
. . 3
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) ∈ ℕ ∨
(𝑁 / 2) ∈
ℕ)) |
67 | 66 | ord 864 |
. 2
⊢ (𝑁 ∈ ℕ → (¬
((𝑁 + 1) / 2) ∈
ℕ → (𝑁 / 2)
∈ ℕ)) |
68 | 18, 67 | impbid 215 |
1
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔
¬ ((𝑁 + 1) / 2) ∈
ℕ)) |