This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnoddn2prmb

Description: A number is a prime number not equal to 2 iff it is an odd prime number. Conversion theorem for two representations of odd primes. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion nnoddn2prmb 
|- ( N e. ( Prime \ { 2 } ) <-> ( N e. Prime /\ -. 2 || N ) )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( N e. ( Prime \ { 2 } ) -> N e. Prime )
2 oddn2prm 
 |-  ( N e. ( Prime \ { 2 } ) -> -. 2 || N )
3 1 2 jca 
 |-  ( N e. ( Prime \ { 2 } ) -> ( N e. Prime /\ -. 2 || N ) )
4 simpl 
 |-  ( ( N e. Prime /\ -. 2 || N ) -> N e. Prime )
5 z2even 
 |-  2 || 2
6 breq2 
 |-  ( N = 2 -> ( 2 || N <-> 2 || 2 ) )
7 5 6 mpbiri 
 |-  ( N = 2 -> 2 || N )
8 7 a1i 
 |-  ( N e. Prime -> ( N = 2 -> 2 || N ) )
9 8 con3dimp 
 |-  ( ( N e. Prime /\ -. 2 || N ) -> -. N = 2 )
10 9 neqned 
 |-  ( ( N e. Prime /\ -. 2 || N ) -> N =/= 2 )
11 nelsn 
 |-  ( N =/= 2 -> -. N e. { 2 } )
12 10 11 syl 
 |-  ( ( N e. Prime /\ -. 2 || N ) -> -. N e. { 2 } )
13 4 12 eldifd 
 |-  ( ( N e. Prime /\ -. 2 || N ) -> N e. ( Prime \ { 2 } ) )
14 3 13 impbii 
 |-  ( N e. ( Prime \ { 2 } ) <-> ( N e. Prime /\ -. 2 || N ) )