Metamath Proof Explorer

Theorem oddprmALTV

Description: A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015) (Revised by AV, 21-Jun-2020)

Ref Expression
Assertion oddprmALTV 
|- ( N e. ( Prime \ { 2 } ) -> N e. Odd )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( N e. ( Prime \ { 2 } ) <-> ( N e. Prime /\ N =/= 2 ) )
2 prmz 
 |-  ( N e. Prime -> N e. ZZ )
3 2 adantr 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> N e. ZZ )
4 necom 
 |-  ( N =/= 2 <-> 2 =/= N )
5 df-ne 
 |-  ( 2 =/= N <-> -. 2 = N )
6 4 5 sylbb 
 |-  ( N =/= 2 -> -. 2 = N )
7 6 adantl 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> -. 2 = N )
8 1ne2 
 |-  1 =/= 2
9 8 nesymi 
 |-  -. 2 = 1
10 9 a1i 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> -. 2 = 1 )
11 ioran 
 |-  ( -. ( 2 = N \/ 2 = 1 ) <-> ( -. 2 = N /\ -. 2 = 1 ) )
12 7 10 11 sylanbrc 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> -. ( 2 = N \/ 2 = 1 ) )
13 2nn 
 |-  2 e. NN
14 13 a1i 
 |-  ( N =/= 2 -> 2 e. NN )
15 dvdsprime 
 |-  ( ( N e. Prime /\ 2 e. NN ) -> ( 2 || N <-> ( 2 = N \/ 2 = 1 ) ) )
16 14 15 sylan2 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> ( 2 || N <-> ( 2 = N \/ 2 = 1 ) ) )
17 12 16 mtbird 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> -. 2 || N )
18 isodd3 
 |-  ( N e. Odd <-> ( N e. ZZ /\ -. 2 || N ) )
19 3 17 18 sylanbrc 
 |-  ( ( N e. Prime /\ N =/= 2 ) -> N e. Odd )
20 1 19 sylbi 
 |-  ( N e. ( Prime \ { 2 } ) -> N e. Odd )