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\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to N\in \mathbb{P}$$
2		oddn2prm	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \neg 2\parallel N$$
3	1 2	jca	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)$$
4		simpl	$$⊢\left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)\to N\in \mathbb{P}$$
5		z2even	$$⊢2\parallel 2$$
6		breq2	$$⊢N=2\to \left(2\parallel N\leftrightarrow 2\parallel 2\right)$$
7	5 6	mpbiri	$$⊢N=2\to 2\parallel N$$
8	7	a1i	$$⊢N\in \mathbb{P}\to \left(N=2\to 2\parallel N\right)$$
9	8	con3dimp	$$⊢\left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)\to \neg N=2$$
10	9	neqned	$$⊢\left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)\to N\ne 2$$
11		nelsn	$$⊢N\ne 2\to \neg N\in \left\{2\right\}$$
12	10 11	syl	$$⊢\left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)\to \neg N\in \left\{2\right\}$$
13	4 12	eldifd	$$⊢\left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)\to N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
14	3 13	impbii	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(N\in \mathbb{P}\wedge \neg 2\parallel N\right)$$