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 N0N+120N=12<N

Proof

Step Hyp Ref Expression
1 elnn0 N0NN=0
2 elnnnn0c NN01N
3 1red N01
4 nn0re N0N
5 3 4 leloed N01N1<N1=N
6 1zzd N01
7 nn0z N0N
8 zltp1le 1N1<N1+1N
9 6 7 8 syl2anc N01<N1+1N
10 1p1e2 1+1=2
11 10 breq1i 1+1N2N
12 11 a1i N01+1N2N
13 2re 2
14 13 a1i N02
15 14 4 leloed N02N2<N2=N
16 9 12 15 3bitrd N01<N2<N2=N
17 olc 2<NN=12<N
18 17 2a1d 2<NN0N+120N=12<N
19 oveq1 N=2N+1=2+1
20 19 oveq1d N=2N+12=2+12
21 20 eqcoms 2=NN+12=2+12
22 21 adantl N02=NN+12=2+12
23 2p1e3 2+1=3
24 23 oveq1i 2+12=32
25 22 24 eqtrdi N02=NN+12=32
26 25 eleq1d N02=NN+120320
27 3halfnz ¬32
28 nn0z 32032
29 28 pm2.24d 320¬32N=12<N
30 27 29 mpi 320N=12<N
31 26 30 syl6bi N02=NN+120N=12<N
32 31 expcom 2=NN0N+120N=12<N
33 18 32 jaoi 2<N2=NN0N+120N=12<N
34 33 com12 N02<N2=NN+120N=12<N
35 16 34 sylbid N01<NN+120N=12<N
36 35 com12 1<NN0N+120N=12<N
37 orc N=1N=12<N
38 37 eqcoms 1=NN=12<N
39 38 2a1d 1=NN0N+120N=12<N
40 36 39 jaoi 1<N1=NN0N+120N=12<N
41 40 com12 N01<N1=NN+120N=12<N
42 5 41 sylbid N01NN+120N=12<N
43 42 imp N01NN+120N=12<N
44 2 43 sylbi NN+120N=12<N
45 oveq1 N=0N+1=0+1
46 0p1e1 0+1=1
47 45 46 eqtrdi N=0N+1=1
48 47 oveq1d N=0N+12=12
49 48 eleq1d N=0N+120120
50 halfnz ¬12
51 nn0z 12012
52 51 pm2.24d 120¬12N=12<N
53 50 52 mpi 120N=12<N
54 49 53 syl6bi N=0N+120N=12<N
55 44 54 jaoi NN=0N+120N=12<N
56 1 55 sylbi N0N+120N=12<N
57 56 imp N0N+120N=12<N