Step | Hyp | Ref
| Expression |
1 | | oveq1 5857 |
. . . . . 6
⊢ (𝑗 = 1 → (𝑗 + 1) = (1 + 1)) |
2 | 1 | oveq1d 5865 |
. . . . 5
⊢ (𝑗 = 1 → ((𝑗 + 1) / 2) = ((1 + 1) / 2)) |
3 | 2 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = 1 → (((𝑗 + 1) / 2) ∈ ℕ ↔
((1 + 1) / 2) ∈ ℕ)) |
4 | | oveq1 5857 |
. . . . 5
⊢ (𝑗 = 1 → (𝑗 / 2) = (1 / 2)) |
5 | 4 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = 1 → ((𝑗 / 2) ∈ ℕ ↔ (1 / 2) ∈
ℕ)) |
6 | 3, 5 | orbi12d 788 |
. . 3
⊢ (𝑗 = 1 → ((((𝑗 + 1) / 2) ∈ ℕ ∨
(𝑗 / 2) ∈ ℕ)
↔ (((1 + 1) / 2) ∈ ℕ ∨ (1 / 2) ∈
ℕ))) |
7 | | oveq1 5857 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
8 | 7 | oveq1d 5865 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑗 + 1) / 2) = ((𝑘 + 1) / 2)) |
9 | 8 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = 𝑘 → (((𝑗 + 1) / 2) ∈ ℕ ↔ ((𝑘 + 1) / 2) ∈
ℕ)) |
10 | | oveq1 5857 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝑗 / 2) = (𝑘 / 2)) |
11 | 10 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = 𝑘 → ((𝑗 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈
ℕ)) |
12 | 9, 11 | orbi12d 788 |
. . 3
⊢ (𝑗 = 𝑘 → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
(((𝑘 + 1) / 2) ∈
ℕ ∨ (𝑘 / 2) ∈
ℕ))) |
13 | | oveq1 5857 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) |
14 | 13 | oveq1d 5865 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑗 + 1) / 2) = (((𝑘 + 1) + 1) / 2)) |
15 | 14 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝑗 + 1) / 2) ∈ ℕ ↔ (((𝑘 + 1) + 1) / 2) ∈
ℕ)) |
16 | | oveq1 5857 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝑗 / 2) = ((𝑘 + 1) / 2)) |
17 | 16 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((𝑗 / 2) ∈ ℕ ↔ ((𝑘 + 1) / 2) ∈
ℕ)) |
18 | 15, 17 | orbi12d 788 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
((((𝑘 + 1) + 1) / 2) ∈
ℕ ∨ ((𝑘 + 1) / 2)
∈ ℕ))) |
19 | | oveq1 5857 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
20 | 19 | oveq1d 5865 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑗 + 1) / 2) = ((𝑁 + 1) / 2)) |
21 | 20 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = 𝑁 → (((𝑗 + 1) / 2) ∈ ℕ ↔ ((𝑁 + 1) / 2) ∈
ℕ)) |
22 | | oveq1 5857 |
. . . . 5
⊢ (𝑗 = 𝑁 → (𝑗 / 2) = (𝑁 / 2)) |
23 | 22 | eleq1d 2239 |
. . . 4
⊢ (𝑗 = 𝑁 → ((𝑗 / 2) ∈ ℕ ↔ (𝑁 / 2) ∈
ℕ)) |
24 | 21, 23 | orbi12d 788 |
. . 3
⊢ (𝑗 = 𝑁 → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
(((𝑁 + 1) / 2) ∈
ℕ ∨ (𝑁 / 2) ∈
ℕ))) |
25 | | df-2 8924 |
. . . . . . 7
⊢ 2 = (1 +
1) |
26 | 25 | oveq1i 5860 |
. . . . . 6
⊢ (2 / 2) =
((1 + 1) / 2) |
27 | | 2div2e1 8997 |
. . . . . 6
⊢ (2 / 2) =
1 |
28 | 26, 27 | eqtr3i 2193 |
. . . . 5
⊢ ((1 + 1)
/ 2) = 1 |
29 | | 1nn 8876 |
. . . . 5
⊢ 1 ∈
ℕ |
30 | 28, 29 | eqeltri 2243 |
. . . 4
⊢ ((1 + 1)
/ 2) ∈ ℕ |
31 | 30 | orci 726 |
. . 3
⊢ (((1 + 1)
/ 2) ∈ ℕ ∨ (1 / 2) ∈ ℕ) |
32 | | peano2nn 8877 |
. . . . . 6
⊢ ((𝑘 / 2) ∈ ℕ →
((𝑘 / 2) + 1) ∈
ℕ) |
33 | | nncn 8873 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
34 | | add1p1 9114 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → ((𝑘 + 1) + 1) = (𝑘 + 2)) |
35 | 34 | oveq1d 5865 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℂ → (((𝑘 + 1) + 1) / 2) = ((𝑘 + 2) / 2)) |
36 | | 2cn 8936 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
37 | | 2ap0 8958 |
. . . . . . . . . . . 12
⊢ 2 #
0 |
38 | 36, 37 | pm3.2i 270 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ ∧ 2 # 0) |
39 | | divdirap 8601 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 2 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((𝑘 + 2) / 2) = ((𝑘 / 2) + (2 / 2))) |
40 | 36, 38, 39 | mp3an23 1324 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → ((𝑘 + 2) / 2) = ((𝑘 / 2) + (2 /
2))) |
41 | 27 | oveq2i 5861 |
. . . . . . . . . 10
⊢ ((𝑘 / 2) + (2 / 2)) = ((𝑘 / 2) + 1) |
42 | 40, 41 | eqtrdi 2219 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℂ → ((𝑘 + 2) / 2) = ((𝑘 / 2) + 1)) |
43 | 35, 42 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝑘 ∈ ℂ → (((𝑘 + 1) + 1) / 2) = ((𝑘 / 2) + 1)) |
44 | 33, 43 | syl 14 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (((𝑘 + 1) + 1) / 2) = ((𝑘 / 2) + 1)) |
45 | 44 | eleq1d 2239 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) + 1) / 2) ∈ ℕ
↔ ((𝑘 / 2) + 1) ∈
ℕ)) |
46 | 32, 45 | syl5ibr 155 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝑘 / 2) ∈ ℕ →
(((𝑘 + 1) + 1) / 2) ∈
ℕ)) |
47 | 46 | orim2d 783 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) / 2) ∈ ℕ ∨
(𝑘 / 2) ∈ ℕ)
→ (((𝑘 + 1) / 2)
∈ ℕ ∨ (((𝑘 +
1) + 1) / 2) ∈ ℕ))) |
48 | | orcom 723 |
. . . 4
⊢ ((((𝑘 + 1) / 2) ∈ ℕ ∨
(((𝑘 + 1) + 1) / 2) ∈
ℕ) ↔ ((((𝑘 + 1)
+ 1) / 2) ∈ ℕ ∨ ((𝑘 + 1) / 2) ∈ ℕ)) |
49 | 47, 48 | syl6ib 160 |
. . 3
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) / 2) ∈ ℕ ∨
(𝑘 / 2) ∈ ℕ)
→ ((((𝑘 + 1) + 1) / 2)
∈ ℕ ∨ ((𝑘 +
1) / 2) ∈ ℕ))) |
50 | 6, 12, 18, 24, 31, 49 | nnind 8881 |
. 2
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) ∈ ℕ ∨
(𝑁 / 2) ∈
ℕ)) |
51 | 50 | orcomd 724 |
1
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨
((𝑁 + 1) / 2) ∈
ℕ)) |