Metamath Proof Explorer

Theorem nn0o1gt2

Description: An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020)

Ref Expression
Assertion nn0o1gt2 
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 elnnnn0c 
 |-  ( N e. NN <-> ( N e. NN0 /\ 1 <_ N ) )
3 1red 
 |-  ( N e. NN0 -> 1 e. RR )
4 nn0re 
 |-  ( N e. NN0 -> N e. RR )
5 3 4 leloed 
 |-  ( N e. NN0 -> ( 1 <_ N <-> ( 1 < N \/ 1 = N ) ) )
6 1zzd 
 |-  ( N e. NN0 -> 1 e. ZZ )
7 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
8 zltp1le 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( 1 < N <-> ( 1 + 1 ) <_ N ) )
9 6 7 8 syl2anc 
 |-  ( N e. NN0 -> ( 1 < N <-> ( 1 + 1 ) <_ N ) )
10 1p1e2 
 |-  ( 1 + 1 ) = 2
11 10 breq1i 
 |-  ( ( 1 + 1 ) <_ N <-> 2 <_ N )
12 11 a1i 
 |-  ( N e. NN0 -> ( ( 1 + 1 ) <_ N <-> 2 <_ N ) )
13 2re 
 |-  2 e. RR
14 13 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
15 14 4 leloed 
 |-  ( N e. NN0 -> ( 2 <_ N <-> ( 2 < N \/ 2 = N ) ) )
16 9 12 15 3bitrd 
 |-  ( N e. NN0 -> ( 1 < N <-> ( 2 < N \/ 2 = N ) ) )
17 olc 
 |-  ( 2 < N -> ( N = 1 \/ 2 < N ) )
18 17 2a1d 
 |-  ( 2 < N -> ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
19 oveq1 
 |-  ( N = 2 -> ( N + 1 ) = ( 2 + 1 ) )
20 19 oveq1d 
 |-  ( N = 2 -> ( ( N + 1 ) / 2 ) = ( ( 2 + 1 ) / 2 ) )
21 20 eqcoms 
 |-  ( 2 = N -> ( ( N + 1 ) / 2 ) = ( ( 2 + 1 ) / 2 ) )
22 21 adantl 
 |-  ( ( N e. NN0 /\ 2 = N ) -> ( ( N + 1 ) / 2 ) = ( ( 2 + 1 ) / 2 ) )
23 2p1e3 
 |-  ( 2 + 1 ) = 3
24 23 oveq1i 
 |-  ( ( 2 + 1 ) / 2 ) = ( 3 / 2 )
25 22 24 eqtrdi 
 |-  ( ( N e. NN0 /\ 2 = N ) -> ( ( N + 1 ) / 2 ) = ( 3 / 2 ) )
26 25 eleq1d 
 |-  ( ( N e. NN0 /\ 2 = N ) -> ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( 3 / 2 ) e. NN0 ) )
27 3halfnz 
 |-  -. ( 3 / 2 ) e. ZZ
28 nn0z 
 |-  ( ( 3 / 2 ) e. NN0 -> ( 3 / 2 ) e. ZZ )
29 28 pm2.24d 
 |-  ( ( 3 / 2 ) e. NN0 -> ( -. ( 3 / 2 ) e. ZZ -> ( N = 1 \/ 2 < N ) ) )
30 27 29 mpi 
 |-  ( ( 3 / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) )
31 26 30 syl6bi 
 |-  ( ( N e. NN0 /\ 2 = N ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) )
32 31 expcom 
 |-  ( 2 = N -> ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
33 18 32 jaoi 
 |-  ( ( 2 < N \/ 2 = N ) -> ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
34 33 com12 
 |-  ( N e. NN0 -> ( ( 2 < N \/ 2 = N ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
35 16 34 sylbid 
 |-  ( N e. NN0 -> ( 1 < N -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
36 35 com12 
 |-  ( 1 < N -> ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
37 orc 
 |-  ( N = 1 -> ( N = 1 \/ 2 < N ) )
38 37 eqcoms 
 |-  ( 1 = N -> ( N = 1 \/ 2 < N ) )
39 38 2a1d 
 |-  ( 1 = N -> ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
40 36 39 jaoi 
 |-  ( ( 1 < N \/ 1 = N ) -> ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
41 40 com12 
 |-  ( N e. NN0 -> ( ( 1 < N \/ 1 = N ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
42 5 41 sylbid 
 |-  ( N e. NN0 -> ( 1 <_ N -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) ) )
43 42 imp 
 |-  ( ( N e. NN0 /\ 1 <_ N ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) )
44 2 43 sylbi 
 |-  ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) )
45 oveq1 
 |-  ( N = 0 -> ( N + 1 ) = ( 0 + 1 ) )
46 0p1e1 
 |-  ( 0 + 1 ) = 1
47 45 46 eqtrdi 
 |-  ( N = 0 -> ( N + 1 ) = 1 )
48 47 oveq1d 
 |-  ( N = 0 -> ( ( N + 1 ) / 2 ) = ( 1 / 2 ) )
49 48 eleq1d 
 |-  ( N = 0 -> ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( 1 / 2 ) e. NN0 ) )
50 halfnz 
 |-  -. ( 1 / 2 ) e. ZZ
51 nn0z 
 |-  ( ( 1 / 2 ) e. NN0 -> ( 1 / 2 ) e. ZZ )
52 51 pm2.24d 
 |-  ( ( 1 / 2 ) e. NN0 -> ( -. ( 1 / 2 ) e. ZZ -> ( N = 1 \/ 2 < N ) ) )
53 50 52 mpi 
 |-  ( ( 1 / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) )
54 49 53 syl6bi 
 |-  ( N = 0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) )
55 44 54 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) )
56 1 55 sylbi 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N = 1 \/ 2 < N ) ) )
57 56 imp 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )