Step |
Hyp |
Ref |
Expression |
1 |
|
nncn |
|- ( N e. NN -> N e. CC ) |
2 |
|
peano2cn |
|- ( N e. CC -> ( N + 1 ) e. CC ) |
3 |
1 2
|
syl |
|- ( N e. NN -> ( N + 1 ) e. CC ) |
4 |
|
2cn |
|- 2 e. CC |
5 |
4
|
a1i |
|- ( N e. NN -> 2 e. CC ) |
6 |
|
2ne0 |
|- 2 =/= 0 |
7 |
6
|
a1i |
|- ( N e. NN -> 2 =/= 0 ) |
8 |
3 5 7
|
divcan2d |
|- ( N e. NN -> ( 2 x. ( ( N + 1 ) / 2 ) ) = ( N + 1 ) ) |
9 |
1 5 7
|
divcan2d |
|- ( N e. NN -> ( 2 x. ( N / 2 ) ) = N ) |
10 |
9
|
oveq1d |
|- ( N e. NN -> ( ( 2 x. ( N / 2 ) ) + 1 ) = ( N + 1 ) ) |
11 |
8 10
|
eqtr4d |
|- ( N e. NN -> ( 2 x. ( ( N + 1 ) / 2 ) ) = ( ( 2 x. ( N / 2 ) ) + 1 ) ) |
12 |
|
nnz |
|- ( ( ( N + 1 ) / 2 ) e. NN -> ( ( N + 1 ) / 2 ) e. ZZ ) |
13 |
|
nnz |
|- ( ( N / 2 ) e. NN -> ( N / 2 ) e. ZZ ) |
14 |
|
zneo |
|- ( ( ( ( N + 1 ) / 2 ) e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) ) |
15 |
12 13 14
|
syl2an |
|- ( ( ( ( N + 1 ) / 2 ) e. NN /\ ( N / 2 ) e. NN ) -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) ) |
16 |
15
|
expcom |
|- ( ( N / 2 ) e. NN -> ( ( ( N + 1 ) / 2 ) e. NN -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) ) ) |
17 |
16
|
necon2bd |
|- ( ( N / 2 ) e. NN -> ( ( 2 x. ( ( N + 1 ) / 2 ) ) = ( ( 2 x. ( N / 2 ) ) + 1 ) -> -. ( ( N + 1 ) / 2 ) e. NN ) ) |
18 |
11 17
|
syl5com |
|- ( N e. NN -> ( ( N / 2 ) e. NN -> -. ( ( N + 1 ) / 2 ) e. NN ) ) |
19 |
|
oveq1 |
|- ( j = 1 -> ( j + 1 ) = ( 1 + 1 ) ) |
20 |
19
|
oveq1d |
|- ( j = 1 -> ( ( j + 1 ) / 2 ) = ( ( 1 + 1 ) / 2 ) ) |
21 |
20
|
eleq1d |
|- ( j = 1 -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( 1 + 1 ) / 2 ) e. NN ) ) |
22 |
|
oveq1 |
|- ( j = 1 -> ( j / 2 ) = ( 1 / 2 ) ) |
23 |
22
|
eleq1d |
|- ( j = 1 -> ( ( j / 2 ) e. NN <-> ( 1 / 2 ) e. NN ) ) |
24 |
21 23
|
orbi12d |
|- ( j = 1 -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( 1 + 1 ) / 2 ) e. NN \/ ( 1 / 2 ) e. NN ) ) ) |
25 |
|
oveq1 |
|- ( j = k -> ( j + 1 ) = ( k + 1 ) ) |
26 |
25
|
oveq1d |
|- ( j = k -> ( ( j + 1 ) / 2 ) = ( ( k + 1 ) / 2 ) ) |
27 |
26
|
eleq1d |
|- ( j = k -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( k + 1 ) / 2 ) e. NN ) ) |
28 |
|
oveq1 |
|- ( j = k -> ( j / 2 ) = ( k / 2 ) ) |
29 |
28
|
eleq1d |
|- ( j = k -> ( ( j / 2 ) e. NN <-> ( k / 2 ) e. NN ) ) |
30 |
27 29
|
orbi12d |
|- ( j = k -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( k + 1 ) / 2 ) e. NN \/ ( k / 2 ) e. NN ) ) ) |
31 |
|
oveq1 |
|- ( j = ( k + 1 ) -> ( j + 1 ) = ( ( k + 1 ) + 1 ) ) |
32 |
31
|
oveq1d |
|- ( j = ( k + 1 ) -> ( ( j + 1 ) / 2 ) = ( ( ( k + 1 ) + 1 ) / 2 ) ) |
33 |
32
|
eleq1d |
|- ( j = ( k + 1 ) -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) ) |
34 |
|
oveq1 |
|- ( j = ( k + 1 ) -> ( j / 2 ) = ( ( k + 1 ) / 2 ) ) |
35 |
34
|
eleq1d |
|- ( j = ( k + 1 ) -> ( ( j / 2 ) e. NN <-> ( ( k + 1 ) / 2 ) e. NN ) ) |
36 |
33 35
|
orbi12d |
|- ( j = ( k + 1 ) -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN \/ ( ( k + 1 ) / 2 ) e. NN ) ) ) |
37 |
|
oveq1 |
|- ( j = N -> ( j + 1 ) = ( N + 1 ) ) |
38 |
37
|
oveq1d |
|- ( j = N -> ( ( j + 1 ) / 2 ) = ( ( N + 1 ) / 2 ) ) |
39 |
38
|
eleq1d |
|- ( j = N -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( N + 1 ) / 2 ) e. NN ) ) |
40 |
|
oveq1 |
|- ( j = N -> ( j / 2 ) = ( N / 2 ) ) |
41 |
40
|
eleq1d |
|- ( j = N -> ( ( j / 2 ) e. NN <-> ( N / 2 ) e. NN ) ) |
42 |
39 41
|
orbi12d |
|- ( j = N -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( N + 1 ) / 2 ) e. NN \/ ( N / 2 ) e. NN ) ) ) |
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 e. NN |
48 |
46 47
|
eqeltri |
|- ( ( 1 + 1 ) / 2 ) e. NN |
49 |
48
|
orci |
|- ( ( ( 1 + 1 ) / 2 ) e. NN \/ ( 1 / 2 ) e. NN ) |
50 |
|
peano2nn |
|- ( ( k / 2 ) e. NN -> ( ( k / 2 ) + 1 ) e. NN ) |
51 |
|
nncn |
|- ( k e. NN -> k e. CC ) |
52 |
|
add1p1 |
|- ( k e. CC -> ( ( k + 1 ) + 1 ) = ( k + 2 ) ) |
53 |
52
|
oveq1d |
|- ( k e. CC -> ( ( ( k + 1 ) + 1 ) / 2 ) = ( ( k + 2 ) / 2 ) ) |
54 |
|
2cnne0 |
|- ( 2 e. CC /\ 2 =/= 0 ) |
55 |
|
divdir |
|- ( ( k e. CC /\ 2 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( k + 2 ) / 2 ) = ( ( k / 2 ) + ( 2 / 2 ) ) ) |
56 |
4 54 55
|
mp3an23 |
|- ( k e. CC -> ( ( k + 2 ) / 2 ) = ( ( k / 2 ) + ( 2 / 2 ) ) ) |
57 |
45
|
oveq2i |
|- ( ( k / 2 ) + ( 2 / 2 ) ) = ( ( k / 2 ) + 1 ) |
58 |
56 57
|
eqtrdi |
|- ( k e. CC -> ( ( k + 2 ) / 2 ) = ( ( k / 2 ) + 1 ) ) |
59 |
53 58
|
eqtrd |
|- ( k e. CC -> ( ( ( k + 1 ) + 1 ) / 2 ) = ( ( k / 2 ) + 1 ) ) |
60 |
51 59
|
syl |
|- ( k e. NN -> ( ( ( k + 1 ) + 1 ) / 2 ) = ( ( k / 2 ) + 1 ) ) |
61 |
60
|
eleq1d |
|- ( k e. NN -> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN <-> ( ( k / 2 ) + 1 ) e. NN ) ) |
62 |
50 61
|
syl5ibr |
|- ( k e. NN -> ( ( k / 2 ) e. NN -> ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) ) |
63 |
62
|
orim2d |
|- ( k e. NN -> ( ( ( ( k + 1 ) / 2 ) e. NN \/ ( k / 2 ) e. NN ) -> ( ( ( k + 1 ) / 2 ) e. NN \/ ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) ) ) |
64 |
|
orcom |
|- ( ( ( ( k + 1 ) / 2 ) e. NN \/ ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) <-> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN \/ ( ( k + 1 ) / 2 ) e. NN ) ) |
65 |
63 64
|
syl6ib |
|- ( k e. NN -> ( ( ( ( k + 1 ) / 2 ) e. NN \/ ( k / 2 ) e. NN ) -> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN \/ ( ( k + 1 ) / 2 ) e. NN ) ) ) |
66 |
24 30 36 42 49 65
|
nnind |
|- ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. NN \/ ( N / 2 ) e. NN ) ) |
67 |
66
|
ord |
|- ( N e. NN -> ( -. ( ( N + 1 ) / 2 ) e. NN -> ( N / 2 ) e. NN ) ) |
68 |
18 67
|
impbid |
|- ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) ) |