Metamath Proof Explorer

Theorem oddprm

Description: A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion oddprm 
|- ( N e. ( Prime \ { 2 } ) -> ( ( N - 1 ) / 2 ) e. NN )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( N e. ( Prime \ { 2 } ) -> N e. Prime )
2 prmz 
 |-  ( N e. Prime -> N e. ZZ )
3 1 2 syl 
 |-  ( N e. ( Prime \ { 2 } ) -> N e. ZZ )
4 eldifsni 
 |-  ( N e. ( Prime \ { 2 } ) -> N =/= 2 )
5 4 necomd 
 |-  ( N e. ( Prime \ { 2 } ) -> 2 =/= N )
6 5 neneqd 
 |-  ( N e. ( Prime \ { 2 } ) -> -. 2 = N )
7 2z 
 |-  2 e. ZZ
8 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
9 7 8 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
10 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. Prime ) -> ( 2 || N <-> 2 = N ) )
11 9 1 10 sylancr 
 |-  ( N e. ( Prime \ { 2 } ) -> ( 2 || N <-> 2 = N ) )
12 6 11 mtbird 
 |-  ( N e. ( Prime \ { 2 } ) -> -. 2 || N )
13 1z 
 |-  1 e. ZZ
14 n2dvds1 
 |-  -. 2 || 1
15 omoe 
 |-  ( ( ( N e. ZZ /\ -. 2 || N ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( N - 1 ) )
16 13 14 15 mpanr12 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> 2 || ( N - 1 ) )
17 3 12 16 syl2anc 
 |-  ( N e. ( Prime \ { 2 } ) -> 2 || ( N - 1 ) )
18 prmnn 
 |-  ( N e. Prime -> N e. NN )
19 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
20 1 18 19 3syl 
 |-  ( N e. ( Prime \ { 2 } ) -> ( N - 1 ) e. NN0 )
21 nn0z 
 |-  ( ( N - 1 ) e. NN0 -> ( N - 1 ) e. ZZ )
22 evend2 
 |-  ( ( N - 1 ) e. ZZ -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
23 20 21 22 3syl 
 |-  ( N e. ( Prime \ { 2 } ) -> ( 2 || ( N - 1 ) <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
24 17 23 mpbid 
 |-  ( N e. ( Prime \ { 2 } ) -> ( ( N - 1 ) / 2 ) e. ZZ )
25 prmuz2 
 |-  ( N e. Prime -> N e. ( ZZ>= ` 2 ) )
26 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
27 nngt0 
 |-  ( ( N - 1 ) e. NN -> 0 < ( N - 1 ) )
28 nnre 
 |-  ( ( N - 1 ) e. NN -> ( N - 1 ) e. RR )
29 2rp 
 |-  2 e. RR+
30 29 a1i 
 |-  ( ( N - 1 ) e. NN -> 2 e. RR+ )
31 28 30 gt0divd 
 |-  ( ( N - 1 ) e. NN -> ( 0 < ( N - 1 ) <-> 0 < ( ( N - 1 ) / 2 ) ) )
32 27 31 mpbid 
 |-  ( ( N - 1 ) e. NN -> 0 < ( ( N - 1 ) / 2 ) )
33 1 25 26 32 4syl 
 |-  ( N e. ( Prime \ { 2 } ) -> 0 < ( ( N - 1 ) / 2 ) )
34 elnnz 
 |-  ( ( ( N - 1 ) / 2 ) e. NN <-> ( ( ( N - 1 ) / 2 ) e. ZZ /\ 0 < ( ( N - 1 ) / 2 ) ) )
35 24 33 34 sylanbrc 
 |-  ( N e. ( Prime \ { 2 } ) -> ( ( N - 1 ) / 2 ) e. NN )