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 )