Metamath Proof Explorer

Theorem nn0o1gt2ALTV

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

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

Proof

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 biimtrdi 
 |-  ( 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 biimtrdi 
 |-  ( 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 biimtrdi 
 |-  ( 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 ) )