Description: An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0o1gt2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0 | |
|
2 | elnnnn0c | |
|
3 | 1red | |
|
4 | nn0re | |
|
5 | 3 4 | leloed | |
6 | 1zzd | |
|
7 | nn0z | |
|
8 | zltp1le | |
|
9 | 6 7 8 | syl2anc | |
10 | 1p1e2 | |
|
11 | 10 | breq1i | |
12 | 11 | a1i | |
13 | 2re | |
|
14 | 13 | a1i | |
15 | 14 4 | leloed | |
16 | 9 12 15 | 3bitrd | |
17 | olc | |
|
18 | 17 | 2a1d | |
19 | oveq1 | |
|
20 | 19 | oveq1d | |
21 | 20 | eqcoms | |
22 | 21 | adantl | |
23 | 2p1e3 | |
|
24 | 23 | oveq1i | |
25 | 22 24 | eqtrdi | |
26 | 25 | eleq1d | |
27 | 3halfnz | |
|
28 | nn0z | |
|
29 | 28 | pm2.24d | |
30 | 27 29 | mpi | |
31 | 26 30 | syl6bi | |
32 | 31 | expcom | |
33 | 18 32 | jaoi | |
34 | 33 | com12 | |
35 | 16 34 | sylbid | |
36 | 35 | com12 | |
37 | orc | |
|
38 | 37 | eqcoms | |
39 | 38 | 2a1d | |
40 | 36 39 | jaoi | |
41 | 40 | com12 | |
42 | 5 41 | sylbid | |
43 | 42 | imp | |
44 | 2 43 | sylbi | |
45 | oveq1 | |
|
46 | 0p1e1 | |
|
47 | 45 46 | eqtrdi | |
48 | 47 | oveq1d | |
49 | 48 | eleq1d | |
50 | halfnz | |
|
51 | nn0z | |
|
52 | 51 | pm2.24d | |
53 | 50 52 | mpi | |
54 | 49 53 | syl6bi | |
55 | 44 54 | jaoi | |
56 | 1 55 | sylbi | |
57 | 56 | imp | |