Step |
Hyp |
Ref |
Expression |
1 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
2 |
|
peano2cn |
⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ ) |
3 |
1 2
|
syl |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ ) |
4 |
|
2cn |
⊢ 2 ∈ ℂ |
5 |
4
|
a1i |
⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ ) |
6 |
|
2ne0 |
⊢ 2 ≠ 0 |
7 |
6
|
a1i |
⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 ) |
8 |
3 5 7
|
divcan2d |
⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( 𝑁 + 1 ) ) |
9 |
1 5 7
|
divcan2d |
⊢ ( 𝑁 ∈ ℕ → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 ) |
10 |
9
|
oveq1d |
⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) = ( 𝑁 + 1 ) ) |
11 |
8 10
|
eqtr4d |
⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) |
12 |
|
nnz |
⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) |
13 |
|
nnz |
⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℤ ) |
14 |
|
zneo |
⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) |
15 |
12 13 14
|
syl2an |
⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ ) → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) |
16 |
15
|
expcom |
⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) ) |
17 |
16
|
necon2bd |
⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) ) |
18 |
11 17
|
syl5com |
⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) ) |
19 |
|
oveq1 |
⊢ ( 𝑗 = 1 → ( 𝑗 + 1 ) = ( 1 + 1 ) ) |
20 |
19
|
oveq1d |
⊢ ( 𝑗 = 1 → ( ( 𝑗 + 1 ) / 2 ) = ( ( 1 + 1 ) / 2 ) ) |
21 |
20
|
eleq1d |
⊢ ( 𝑗 = 1 → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( 1 + 1 ) / 2 ) ∈ ℕ ) ) |
22 |
|
oveq1 |
⊢ ( 𝑗 = 1 → ( 𝑗 / 2 ) = ( 1 / 2 ) ) |
23 |
22
|
eleq1d |
⊢ ( 𝑗 = 1 → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( 1 / 2 ) ∈ ℕ ) ) |
24 |
21 23
|
orbi12d |
⊢ ( 𝑗 = 1 → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( 1 + 1 ) / 2 ) ∈ ℕ ∨ ( 1 / 2 ) ∈ ℕ ) ) ) |
25 |
|
oveq1 |
⊢ ( 𝑗 = 𝑘 → ( 𝑗 + 1 ) = ( 𝑘 + 1 ) ) |
26 |
25
|
oveq1d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 + 1 ) / 2 ) = ( ( 𝑘 + 1 ) / 2 ) ) |
27 |
26
|
eleq1d |
⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) |
28 |
|
oveq1 |
⊢ ( 𝑗 = 𝑘 → ( 𝑗 / 2 ) = ( 𝑘 / 2 ) ) |
29 |
28
|
eleq1d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( 𝑘 / 2 ) ∈ ℕ ) ) |
30 |
27 29
|
orbi12d |
⊢ ( 𝑗 = 𝑘 → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑘 / 2 ) ∈ ℕ ) ) ) |
31 |
|
oveq1 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑘 + 1 ) + 1 ) ) |
32 |
31
|
oveq1d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑗 + 1 ) / 2 ) = ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ) |
33 |
32
|
eleq1d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) ) |
34 |
|
oveq1 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 / 2 ) = ( ( 𝑘 + 1 ) / 2 ) ) |
35 |
34
|
eleq1d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) |
36 |
33 35
|
orbi12d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ∨ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) ) |
37 |
|
oveq1 |
⊢ ( 𝑗 = 𝑁 → ( 𝑗 + 1 ) = ( 𝑁 + 1 ) ) |
38 |
37
|
oveq1d |
⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 + 1 ) / 2 ) = ( ( 𝑁 + 1 ) / 2 ) ) |
39 |
38
|
eleq1d |
⊢ ( 𝑗 = 𝑁 → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) ) |
40 |
|
oveq1 |
⊢ ( 𝑗 = 𝑁 → ( 𝑗 / 2 ) = ( 𝑁 / 2 ) ) |
41 |
40
|
eleq1d |
⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( 𝑁 / 2 ) ∈ ℕ ) ) |
42 |
39 41
|
orbi12d |
⊢ ( 𝑗 = 𝑁 → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑁 / 2 ) ∈ ℕ ) ) ) |
43 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
44 |
43
|
oveq1i |
⊢ ( 2 / 2 ) = ( ( 1 + 1 ) / 2 ) |
45 |
|
2div2e1 |
⊢ ( 2 / 2 ) = 1 |
46 |
44 45
|
eqtr3i |
⊢ ( ( 1 + 1 ) / 2 ) = 1 |
47 |
|
1nn |
⊢ 1 ∈ ℕ |
48 |
46 47
|
eqeltri |
⊢ ( ( 1 + 1 ) / 2 ) ∈ ℕ |
49 |
48
|
orci |
⊢ ( ( ( 1 + 1 ) / 2 ) ∈ ℕ ∨ ( 1 / 2 ) ∈ ℕ ) |
50 |
|
peano2nn |
⊢ ( ( 𝑘 / 2 ) ∈ ℕ → ( ( 𝑘 / 2 ) + 1 ) ∈ ℕ ) |
51 |
|
nncn |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ ) |
52 |
|
add1p1 |
⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 + 1 ) + 1 ) = ( 𝑘 + 2 ) ) |
53 |
52
|
oveq1d |
⊢ ( 𝑘 ∈ ℂ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) = ( ( 𝑘 + 2 ) / 2 ) ) |
54 |
|
2cnne0 |
⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) |
55 |
|
divdir |
⊢ ( ( 𝑘 ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑘 + 2 ) / 2 ) = ( ( 𝑘 / 2 ) + ( 2 / 2 ) ) ) |
56 |
4 54 55
|
mp3an23 |
⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 + 2 ) / 2 ) = ( ( 𝑘 / 2 ) + ( 2 / 2 ) ) ) |
57 |
45
|
oveq2i |
⊢ ( ( 𝑘 / 2 ) + ( 2 / 2 ) ) = ( ( 𝑘 / 2 ) + 1 ) |
58 |
56 57
|
eqtrdi |
⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 + 2 ) / 2 ) = ( ( 𝑘 / 2 ) + 1 ) ) |
59 |
53 58
|
eqtrd |
⊢ ( 𝑘 ∈ ℂ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) = ( ( 𝑘 / 2 ) + 1 ) ) |
60 |
51 59
|
syl |
⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) = ( ( 𝑘 / 2 ) + 1 ) ) |
61 |
60
|
eleq1d |
⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ↔ ( ( 𝑘 / 2 ) + 1 ) ∈ ℕ ) ) |
62 |
50 61
|
syl5ibr |
⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / 2 ) ∈ ℕ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) ) |
63 |
62
|
orim2d |
⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑘 / 2 ) ∈ ℕ ) → ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) ) ) |
64 |
|
orcom |
⊢ ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) ↔ ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ∨ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) |
65 |
63 64
|
syl6ib |
⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑘 / 2 ) ∈ ℕ ) → ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ∨ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) ) |
66 |
24 30 36 42 49 65
|
nnind |
⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑁 / 2 ) ∈ ℕ ) ) |
67 |
66
|
ord |
⊢ ( 𝑁 ∈ ℕ → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) ) |
68 |
18 67
|
impbid |
⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) ) |