Theorem prm2orodd

Description: A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021)

	Ref	Expression
Assertion	prm2orodd	$$⊢P\in \mathbb{P}\to \left(P=2\vee \neg 2\parallel P\right)$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		dvdsprime	$$⊢\left(P\in \mathbb{P}\wedge 2\in \mathbb{N}\right)\to \left(2\parallel P\leftrightarrow \left(2=P\vee 2=1\right)\right)$$
3	1 2	mpan2	$$⊢P\in \mathbb{P}\to \left(2\parallel P\leftrightarrow \left(2=P\vee 2=1\right)\right)$$
4		eqcom	$$⊢2=P\leftrightarrow P=2$$
5	4	biimpi	$$⊢2=P\to P=2$$
6		1ne2	$$⊢1\ne 2$$
7		necom	$$⊢1\ne 2\leftrightarrow 2\ne 1$$
8		eqneqall	$$⊢2=1\to \left(2\ne 1\to P=2\right)$$
9	8	com12	$$⊢2\ne 1\to \left(2=1\to P=2\right)$$
10	7 9	sylbi	$$⊢1\ne 2\to \left(2=1\to P=2\right)$$
11	6 10	ax-mp	$$⊢2=1\to P=2$$
12	5 11	jaoi	$$⊢\left(2=P\vee 2=1\right)\to P=2$$
13	3 12	biimtrdi	$$⊢P\in \mathbb{P}\to \left(2\parallel P\to P=2\right)$$
14	13	con3d	$$⊢P\in \mathbb{P}\to \left(\neg P=2\to \neg 2\parallel P\right)$$
15	14	orrd	$$⊢P\in \mathbb{P}\to \left(P=2\vee \neg 2\parallel P\right)$$