Step |
Hyp |
Ref |
Expression |
1 |
|
elnn0 |
|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) ) |
2 |
|
elnn1uz2 |
|- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) ) |
3 |
|
orc |
|- ( N = 1 -> ( N = 1 \/ 2 < N ) ) |
4 |
3
|
a1d |
|- ( N = 1 -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
5 |
|
2z |
|- 2 e. ZZ |
6 |
5
|
eluz1i |
|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 2 <_ N ) ) |
7 |
|
2re |
|- 2 e. RR |
8 |
7
|
a1i |
|- ( N e. ZZ -> 2 e. RR ) |
9 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
10 |
8 9
|
leloed |
|- ( N e. ZZ -> ( 2 <_ N <-> ( 2 < N \/ 2 = N ) ) ) |
11 |
|
olc |
|- ( 2 < N -> ( N = 1 \/ 2 < N ) ) |
12 |
11
|
a1d |
|- ( 2 < N -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
13 |
|
eleq1 |
|- ( N = 2 -> ( N e. Odd <-> 2 e. Odd ) ) |
14 |
13
|
eqcoms |
|- ( 2 = N -> ( N e. Odd <-> 2 e. Odd ) ) |
15 |
|
2noddALTV |
|- 2 e/ Odd |
16 |
|
df-nel |
|- ( 2 e/ Odd <-> -. 2 e. Odd ) |
17 |
|
pm2.21 |
|- ( -. 2 e. Odd -> ( 2 e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
18 |
16 17
|
sylbi |
|- ( 2 e/ Odd -> ( 2 e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
19 |
15 18
|
ax-mp |
|- ( 2 e. Odd -> ( N = 1 \/ 2 < N ) ) |
20 |
14 19
|
syl6bi |
|- ( 2 = N -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
21 |
12 20
|
jaoi |
|- ( ( 2 < N \/ 2 = N ) -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
22 |
10 21
|
syl6bi |
|- ( N e. ZZ -> ( 2 <_ N -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) ) |
23 |
22
|
imp |
|- ( ( N e. ZZ /\ 2 <_ N ) -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
24 |
6 23
|
sylbi |
|- ( N e. ( ZZ>= ` 2 ) -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
25 |
4 24
|
jaoi |
|- ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
26 |
2 25
|
sylbi |
|- ( N e. NN -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
27 |
|
eleq1 |
|- ( N = 0 -> ( N e. Odd <-> 0 e. Odd ) ) |
28 |
|
0noddALTV |
|- 0 e/ Odd |
29 |
|
df-nel |
|- ( 0 e/ Odd <-> -. 0 e. Odd ) |
30 |
|
pm2.21 |
|- ( -. 0 e. Odd -> ( 0 e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
31 |
29 30
|
sylbi |
|- ( 0 e/ Odd -> ( 0 e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
32 |
28 31
|
ax-mp |
|- ( 0 e. Odd -> ( N = 1 \/ 2 < N ) ) |
33 |
27 32
|
syl6bi |
|- ( N = 0 -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
34 |
26 33
|
jaoi |
|- ( ( N e. NN \/ N = 0 ) -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
35 |
1 34
|
sylbi |
|- ( N e. NN0 -> ( N e. Odd -> ( N = 1 \/ 2 < N ) ) ) |
36 |
35
|
imp |
|- ( ( N e. NN0 /\ N e. Odd ) -> ( N = 1 \/ 2 < N ) ) |