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 ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• )

Proof

Step Hyp Ref Expression
1 eluz2b3 โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ๐‘ โˆˆ โ„• โˆง ๐‘ โ‰  1 ) )
2 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
3 nn0o1gt2 โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ = 1 โˆจ 2 < ๐‘ ) )
4 2 3 sylan โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ = 1 โˆจ 2 < ๐‘ ) )
5 eqneqall โŠข ( ๐‘ = 1 โ†’ ( ๐‘ โ‰  1 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
6 5 a1d โŠข ( ๐‘ = 1 โ†’ ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ โ‰  1 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) ) )
7 nn0z โŠข ( ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 โ†’ ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„ค )
8 peano2zm โŠข ( ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„ค โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„ค )
9 7 8 syl โŠข ( ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„ค )
10 9 ad2antlr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โˆง 2 < ๐‘ ) โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„ค )
11 2cn โŠข 2 โˆˆ โ„‚
12 11 mullidi โŠข ( 1 ยท 2 ) = 2
13 nnre โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ )
14 13 ltp1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ < ( ๐‘ + 1 ) )
15 14 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ๐‘ < ( ๐‘ + 1 ) )
16 2re โŠข 2 โˆˆ โ„
17 peano2nn โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ + 1 ) โˆˆ โ„• )
18 17 nnred โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ + 1 ) โˆˆ โ„ )
19 lttr โŠข ( ( 2 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ( ๐‘ + 1 ) โˆˆ โ„ ) โ†’ ( ( 2 < ๐‘ โˆง ๐‘ < ( ๐‘ + 1 ) ) โ†’ 2 < ( ๐‘ + 1 ) ) )
20 16 13 18 19 mp3an2i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 < ๐‘ โˆง ๐‘ < ( ๐‘ + 1 ) ) โ†’ 2 < ( ๐‘ + 1 ) ) )
21 20 expdimp โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ( ๐‘ < ( ๐‘ + 1 ) โ†’ 2 < ( ๐‘ + 1 ) ) )
22 15 21 mpd โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ 2 < ( ๐‘ + 1 ) )
23 12 22 eqbrtrid โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ( 1 ยท 2 ) < ( ๐‘ + 1 ) )
24 1red โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ 1 โˆˆ โ„ )
25 18 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ( ๐‘ + 1 ) โˆˆ โ„ )
26 2rp โŠข 2 โˆˆ โ„+
27 26 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ 2 โˆˆ โ„+ )
28 24 25 27 ltmuldivd โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ( ( 1 ยท 2 ) < ( ๐‘ + 1 ) โ†” 1 < ( ( ๐‘ + 1 ) / 2 ) ) )
29 23 28 mpbid โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ 1 < ( ( ๐‘ + 1 ) / 2 ) )
30 18 rehalfcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„ )
31 30 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„ )
32 24 31 posdifd โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ ( 1 < ( ( ๐‘ + 1 ) / 2 ) โ†” 0 < ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) ) )
33 29 32 mpbid โŠข ( ( ๐‘ โˆˆ โ„• โˆง 2 < ๐‘ ) โ†’ 0 < ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) )
34 33 adantlr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โˆง 2 < ๐‘ ) โ†’ 0 < ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) )
35 elnnz โŠข ( ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„• โ†” ( ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„ค โˆง 0 < ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) ) )
36 10 34 35 sylanbrc โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โˆง 2 < ๐‘ ) โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„• )
37 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
38 xp1d2m1eqxm1d2 โŠข ( ๐‘ โˆˆ โ„‚ โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) = ( ( ๐‘ โˆ’ 1 ) / 2 ) )
39 37 38 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) = ( ( ๐‘ โˆ’ 1 ) / 2 ) )
40 39 eleq1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„• โ†” ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
41 40 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„• โ†” ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
42 41 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โˆง 2 < ๐‘ ) โ†’ ( ( ( ( ๐‘ + 1 ) / 2 ) โˆ’ 1 ) โˆˆ โ„• โ†” ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
43 36 42 mpbid โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โˆง 2 < ๐‘ ) โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• )
44 43 a1d โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โˆง 2 < ๐‘ ) โ†’ ( ๐‘ โ‰  1 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
45 44 expcom โŠข ( 2 < ๐‘ โ†’ ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ โ‰  1 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) ) )
46 6 45 jaoi โŠข ( ( ๐‘ = 1 โˆจ 2 < ๐‘ ) โ†’ ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ โ‰  1 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) ) )
47 4 46 mpcom โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ โ‰  1 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
48 47 impancom โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ โ‰  1 ) โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
49 1 48 sylbi โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• ) )
50 49 imp โŠข ( ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ( ๐‘ + 1 ) / 2 ) โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โˆ’ 1 ) / 2 ) โˆˆ โ„• )