Metamath Proof Explorer

Theorem nno

Description: An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion nno 
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN )

Proof

Step Hyp Ref Expression
1 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 nn0o1gt2 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )
4 2 3 sylan 
 |-  ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )
5 eqneqall 
 |-  ( N = 1 -> ( N =/= 1 -> ( ( N - 1 ) / 2 ) e. NN ) )
6 5 a1d 
 |-  ( N = 1 -> ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N =/= 1 -> ( ( N - 1 ) / 2 ) e. NN ) ) )
7 nn0z 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N + 1 ) / 2 ) e. ZZ )
8 peano2zm 
 |-  ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ )
9 7 8 syl 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ )
10 9 ad2antlr 
 |-  ( ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) /\ 2 < N ) -> ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ )
11 2cn 
 |-  2 e. CC
12 11 mulid2i 
 |-  ( 1 x. 2 ) = 2
13 nnre 
 |-  ( N e. NN -> N e. RR )
14 13 ltp1d 
 |-  ( N e. NN -> N < ( N + 1 ) )
15 14 adantr 
 |-  ( ( N e. NN /\ 2 < N ) -> N < ( N + 1 ) )
16 2re 
 |-  2 e. RR
17 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
18 17 nnred 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
19 lttr 
 |-  ( ( 2 e. RR /\ N e. RR /\ ( N + 1 ) e. RR ) -> ( ( 2 < N /\ N < ( N + 1 ) ) -> 2 < ( N + 1 ) ) )
20 16 13 18 19 mp3an2i 
 |-  ( N e. NN -> ( ( 2 < N /\ N < ( N + 1 ) ) -> 2 < ( N + 1 ) ) )
21 20 expdimp 
 |-  ( ( N e. NN /\ 2 < N ) -> ( N < ( N + 1 ) -> 2 < ( N + 1 ) ) )
22 15 21 mpd 
 |-  ( ( N e. NN /\ 2 < N ) -> 2 < ( N + 1 ) )
23 12 22 eqbrtrid 
 |-  ( ( N e. NN /\ 2 < N ) -> ( 1 x. 2 ) < ( N + 1 ) )
24 1red 
 |-  ( ( N e. NN /\ 2 < N ) -> 1 e. RR )
25 18 adantr 
 |-  ( ( N e. NN /\ 2 < N ) -> ( N + 1 ) e. RR )
26 2rp 
 |-  2 e. RR+
27 26 a1i 
 |-  ( ( N e. NN /\ 2 < N ) -> 2 e. RR+ )
28 24 25 27 ltmuldivd 
 |-  ( ( N e. NN /\ 2 < N ) -> ( ( 1 x. 2 ) < ( N + 1 ) <-> 1 < ( ( N + 1 ) / 2 ) ) )
29 23 28 mpbid 
 |-  ( ( N e. NN /\ 2 < N ) -> 1 < ( ( N + 1 ) / 2 ) )
30 18 rehalfcld 
 |-  ( N e. NN -> ( ( N + 1 ) / 2 ) e. RR )
31 30 adantr 
 |-  ( ( N e. NN /\ 2 < N ) -> ( ( N + 1 ) / 2 ) e. RR )
32 24 31 posdifd 
 |-  ( ( N e. NN /\ 2 < N ) -> ( 1 < ( ( N + 1 ) / 2 ) <-> 0 < ( ( ( N + 1 ) / 2 ) - 1 ) ) )
33 29 32 mpbid 
 |-  ( ( N e. NN /\ 2 < N ) -> 0 < ( ( ( N + 1 ) / 2 ) - 1 ) )
34 33 adantlr 
 |-  ( ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) /\ 2 < N ) -> 0 < ( ( ( N + 1 ) / 2 ) - 1 ) )
35 elnnz 
 |-  ( ( ( ( N + 1 ) / 2 ) - 1 ) e. NN <-> ( ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ /\ 0 < ( ( ( N + 1 ) / 2 ) - 1 ) ) )
36 10 34 35 sylanbrc 
 |-  ( ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) /\ 2 < N ) -> ( ( ( N + 1 ) / 2 ) - 1 ) e. NN )
37 nncn 
 |-  ( N e. NN -> N e. CC )
38 xp1d2m1eqxm1d2 
 |-  ( N e. CC -> ( ( ( N + 1 ) / 2 ) - 1 ) = ( ( N - 1 ) / 2 ) )
39 37 38 syl 
 |-  ( N e. NN -> ( ( ( N + 1 ) / 2 ) - 1 ) = ( ( N - 1 ) / 2 ) )
40 39 eleq1d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) / 2 ) - 1 ) e. NN <-> ( ( N - 1 ) / 2 ) e. NN ) )
41 40 adantr 
 |-  ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( ( ( N + 1 ) / 2 ) - 1 ) e. NN <-> ( ( N - 1 ) / 2 ) e. NN ) )
42 41 adantr 
 |-  ( ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) /\ 2 < N ) -> ( ( ( ( N + 1 ) / 2 ) - 1 ) e. NN <-> ( ( N - 1 ) / 2 ) e. NN ) )
43 36 42 mpbid 
 |-  ( ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) /\ 2 < N ) -> ( ( N - 1 ) / 2 ) e. NN )
44 43 a1d 
 |-  ( ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) /\ 2 < N ) -> ( N =/= 1 -> ( ( N - 1 ) / 2 ) e. NN ) )
45 44 expcom 
 |-  ( 2 < N -> ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N =/= 1 -> ( ( N - 1 ) / 2 ) e. NN ) ) )
46 6 45 jaoi 
 |-  ( ( N = 1 \/ 2 < N ) -> ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N =/= 1 -> ( ( N - 1 ) / 2 ) e. NN ) ) )
47 4 46 mpcom 
 |-  ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N =/= 1 -> ( ( N - 1 ) / 2 ) e. NN ) )
48 47 impancom 
 |-  ( ( N e. NN /\ N =/= 1 ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N - 1 ) / 2 ) e. NN ) )
49 1 48 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N - 1 ) / 2 ) e. NN ) )
50 49 imp 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN )