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 ) )