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\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to N\in \mathrm{Odd}$$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(N\in \mathbb{P}\wedge N\ne 2\right)$$
2		prmz	$$⊢N\in \mathbb{P}\to N\in \mathbb{Z}$$
3	2	adantr	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to N\in \mathbb{Z}$$
4		necom	$$⊢N\ne 2\leftrightarrow 2\ne N$$
5		df-ne	$$⊢2\ne N\leftrightarrow \neg 2=N$$
6	4 5	sylbb	$$⊢N\ne 2\to \neg 2=N$$
7	6	adantl	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to \neg 2=N$$
8		1ne2	$$⊢1\ne 2$$
9	8	nesymi	$$⊢\neg 2=1$$
10	9	a1i	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to \neg 2=1$$
11		ioran	$$⊢\neg \left(2=N\vee 2=1\right)\leftrightarrow \left(\neg 2=N\wedge \neg 2=1\right)$$
12	7 10 11	sylanbrc	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to \neg \left(2=N\vee 2=1\right)$$
13		2nn	$$⊢2\in \mathbb{N}$$
14	13	a1i	$$⊢N\ne 2\to 2\in \mathbb{N}$$
15		dvdsprime	$$⊢\left(N\in \mathbb{P}\wedge 2\in \mathbb{N}\right)\to \left(2\parallel N\leftrightarrow \left(2=N\vee 2=1\right)\right)$$
16	14 15	sylan2	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to \left(2\parallel N\leftrightarrow \left(2=N\vee 2=1\right)\right)$$
17	12 16	mtbird	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to \neg 2\parallel N$$
18		isodd3	$$⊢N\in \mathrm{Odd}\leftrightarrow \left(N\in \mathbb{Z}\wedge \neg 2\parallel N\right)$$
19	3 17 18	sylanbrc	$$⊢\left(N\in \mathbb{P}\wedge N\ne 2\right)\to N\in \mathrm{Odd}$$
20	1 19	sylbi	$$⊢N\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to N\in \mathrm{Odd}$$