| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | peano2nn 12278 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) | 
| 2 | 1 | nncnd 12282 | . . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) | 
| 3 |  | 2cn 12341 | . . . . . 6
⊢ 2 ∈
ℂ | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) | 
| 5 |  | 2ne0 12370 | . . . . . 6
⊢ 2 ≠
0 | 
| 6 | 5 | a1i 11 | . . . . 5
⊢ (𝑁 ∈ ℕ → 2 ≠
0) | 
| 7 | 2, 4, 6 | divcan2d 12045 | . . . 4
⊢ (𝑁 ∈ ℕ → (2
· ((𝑁 + 1) / 2)) =
(𝑁 + 1)) | 
| 8 |  | nncn 12274 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 9 | 8, 4, 6 | divcan2d 12045 | . . . . 5
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 / 2)) = 𝑁) | 
| 10 | 9 | oveq1d 7446 | . . . 4
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 / 2)) + 1) =
(𝑁 + 1)) | 
| 11 | 7, 10 | eqtr4d 2780 | . . 3
⊢ (𝑁 ∈ ℕ → (2
· ((𝑁 + 1) / 2)) =
((2 · (𝑁 / 2)) +
1)) | 
| 12 |  | nnz 12634 | . . . . . 6
⊢ (((𝑁 + 1) / 2) ∈ ℕ →
((𝑁 + 1) / 2) ∈
ℤ) | 
| 13 |  | nnz 12634 | . . . . . 6
⊢ ((𝑁 / 2) ∈ ℕ →
(𝑁 / 2) ∈
ℤ) | 
| 14 |  | zneo 12701 | . . . . . 6
⊢ ((((𝑁 + 1) / 2) ∈ ℤ ∧
(𝑁 / 2) ∈ ℤ)
→ (2 · ((𝑁 + 1)
/ 2)) ≠ ((2 · (𝑁
/ 2)) + 1)) | 
| 15 | 12, 13, 14 | syl2an 596 | . . . . 5
⊢ ((((𝑁 + 1) / 2) ∈ ℕ ∧
(𝑁 / 2) ∈ ℕ)
→ (2 · ((𝑁 + 1)
/ 2)) ≠ ((2 · (𝑁
/ 2)) + 1)) | 
| 16 | 15 | expcom 413 | . . . 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 7438 | . . . . . . 7
⊢ (𝑗 = 1 → (𝑗 + 1) = (1 + 1)) | 
| 20 | 19 | oveq1d 7446 | . . . . . 6
⊢ (𝑗 = 1 → ((𝑗 + 1) / 2) = ((1 + 1) / 2)) | 
| 21 | 20 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = 1 → (((𝑗 + 1) / 2) ∈ ℕ ↔
((1 + 1) / 2) ∈ ℕ)) | 
| 22 |  | oveq1 7438 | . . . . . 6
⊢ (𝑗 = 1 → (𝑗 / 2) = (1 / 2)) | 
| 23 | 22 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = 1 → ((𝑗 / 2) ∈ ℕ ↔ (1 / 2) ∈
ℕ)) | 
| 24 | 21, 23 | orbi12d 919 | . . . 4
⊢ (𝑗 = 1 → ((((𝑗 + 1) / 2) ∈ ℕ ∨
(𝑗 / 2) ∈ ℕ)
↔ (((1 + 1) / 2) ∈ ℕ ∨ (1 / 2) ∈
ℕ))) | 
| 25 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) | 
| 26 | 25 | oveq1d 7446 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑗 + 1) / 2) = ((𝑘 + 1) / 2)) | 
| 27 | 26 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = 𝑘 → (((𝑗 + 1) / 2) ∈ ℕ ↔ ((𝑘 + 1) / 2) ∈
ℕ)) | 
| 28 |  | oveq1 7438 | . . . . . 6
⊢ (𝑗 = 𝑘 → (𝑗 / 2) = (𝑘 / 2)) | 
| 29 | 28 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = 𝑘 → ((𝑗 / 2) ∈ ℕ ↔ (𝑘 / 2) ∈
ℕ)) | 
| 30 | 27, 29 | orbi12d 919 | . . . 4
⊢ (𝑗 = 𝑘 → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
(((𝑘 + 1) / 2) ∈
ℕ ∨ (𝑘 / 2) ∈
ℕ))) | 
| 31 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) | 
| 32 | 31 | oveq1d 7446 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑗 + 1) / 2) = (((𝑘 + 1) + 1) / 2)) | 
| 33 | 32 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → (((𝑗 + 1) / 2) ∈ ℕ ↔ (((𝑘 + 1) + 1) / 2) ∈
ℕ)) | 
| 34 |  | oveq1 7438 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑗 / 2) = ((𝑘 + 1) / 2)) | 
| 35 | 34 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑗 / 2) ∈ ℕ ↔ ((𝑘 + 1) / 2) ∈
ℕ)) | 
| 36 | 33, 35 | orbi12d 919 | . . . 4
⊢ (𝑗 = (𝑘 + 1) → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
((((𝑘 + 1) + 1) / 2) ∈
ℕ ∨ ((𝑘 + 1) / 2)
∈ ℕ))) | 
| 37 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) | 
| 38 | 37 | oveq1d 7446 | . . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑗 + 1) / 2) = ((𝑁 + 1) / 2)) | 
| 39 | 38 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = 𝑁 → (((𝑗 + 1) / 2) ∈ ℕ ↔ ((𝑁 + 1) / 2) ∈
ℕ)) | 
| 40 |  | oveq1 7438 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝑗 / 2) = (𝑁 / 2)) | 
| 41 | 40 | eleq1d 2826 | . . . . 5
⊢ (𝑗 = 𝑁 → ((𝑗 / 2) ∈ ℕ ↔ (𝑁 / 2) ∈
ℕ)) | 
| 42 | 39, 41 | orbi12d 919 | . . . 4
⊢ (𝑗 = 𝑁 → ((((𝑗 + 1) / 2) ∈ ℕ ∨ (𝑗 / 2) ∈ ℕ) ↔
(((𝑁 + 1) / 2) ∈
ℕ ∨ (𝑁 / 2) ∈
ℕ))) | 
| 43 |  | df-2 12329 | . . . . . . . 8
⊢ 2 = (1 +
1) | 
| 44 | 43 | oveq1i 7441 | . . . . . . 7
⊢ (2 / 2) =
((1 + 1) / 2) | 
| 45 |  | 2div2e1 12407 | . . . . . . 7
⊢ (2 / 2) =
1 | 
| 46 | 44, 45 | eqtr3i 2767 | . . . . . 6
⊢ ((1 + 1)
/ 2) = 1 | 
| 47 |  | 1nn 12277 | . . . . . 6
⊢ 1 ∈
ℕ | 
| 48 | 46, 47 | eqeltri 2837 | . . . . 5
⊢ ((1 + 1)
/ 2) ∈ ℕ | 
| 49 | 48 | orci 866 | . . . 4
⊢ (((1 + 1)
/ 2) ∈ ℕ ∨ (1 / 2) ∈ ℕ) | 
| 50 |  | peano2nn 12278 | . . . . . . 7
⊢ ((𝑘 / 2) ∈ ℕ →
((𝑘 / 2) + 1) ∈
ℕ) | 
| 51 |  | nncn 12274 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 52 |  | add1p1 12517 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℂ → ((𝑘 + 1) + 1) = (𝑘 + 2)) | 
| 53 | 52 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℂ → (((𝑘 + 1) + 1) / 2) = ((𝑘 + 2) / 2)) | 
| 54 |  | 2cnne0 12476 | . . . . . . . . . . . 12
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 55 |  | divdir 11947 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℂ ∧ 2 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑘 + 2) / 2) = ((𝑘 / 2) + (2 / 2))) | 
| 56 | 3, 54, 55 | mp3an23 1455 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℂ → ((𝑘 + 2) / 2) = ((𝑘 / 2) + (2 /
2))) | 
| 57 | 45 | oveq2i 7442 | . . . . . . . . . . 11
⊢ ((𝑘 / 2) + (2 / 2)) = ((𝑘 / 2) + 1) | 
| 58 | 56, 57 | eqtrdi 2793 | . . . . . . . . . 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 2826 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) + 1) / 2) ∈ ℕ
↔ ((𝑘 / 2) + 1) ∈
ℕ)) | 
| 62 | 50, 61 | imbitrrid 246 | . . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑘 / 2) ∈ ℕ →
(((𝑘 + 1) + 1) / 2) ∈
ℕ)) | 
| 63 | 62 | orim2d 969 | . . . . 5
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) / 2) ∈ ℕ ∨
(𝑘 / 2) ∈ ℕ)
→ (((𝑘 + 1) / 2)
∈ ℕ ∨ (((𝑘 +
1) + 1) / 2) ∈ ℕ))) | 
| 64 |  | orcom 871 | . . . . 5
⊢ ((((𝑘 + 1) / 2) ∈ ℕ ∨
(((𝑘 + 1) + 1) / 2) ∈
ℕ) ↔ ((((𝑘 + 1)
+ 1) / 2) ∈ ℕ ∨ ((𝑘 + 1) / 2) ∈ ℕ)) | 
| 65 | 63, 64 | imbitrdi 251 | . . . 4
⊢ (𝑘 ∈ ℕ → ((((𝑘 + 1) / 2) ∈ ℕ ∨
(𝑘 / 2) ∈ ℕ)
→ ((((𝑘 + 1) + 1) / 2)
∈ ℕ ∨ ((𝑘 +
1) / 2) ∈ ℕ))) | 
| 66 | 24, 30, 36, 42, 49, 65 | nnind 12284 | . . 3
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 2) ∈ ℕ ∨
(𝑁 / 2) ∈
ℕ)) | 
| 67 | 66 | ord 865 | . 2
⊢ (𝑁 ∈ ℕ → (¬
((𝑁 + 1) / 2) ∈
ℕ → (𝑁 / 2)
∈ ℕ)) | 
| 68 | 18, 67 | impbid 212 | 1
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔
¬ ((𝑁 + 1) / 2) ∈
ℕ)) |