Theorem 2prm

Description: 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Fan Zheng, 16-Jun-2016)

	Ref	Expression
Assertion	2prm	$$⊢2\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		1lt2	$$⊢1<2$$
3		eluz2b1	$$⊢2\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 1<2\right)$$
4	1 2 3	mpbir2an	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
5		ral0	$$⊢\forall z\in \varnothing \neg z\parallel 2$$
6		fzssuz	$$⊢\left(2\dots 2-1\right)\subseteq {\mathbb{Z}}_{\ge 2}$$
7		df-ss	$$⊢\left(2\dots 2-1\right)\subseteq {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\dots 2-1\right)\cap {\mathbb{Z}}_{\ge 2}=\left(2\dots 2-1\right)$$
8	6 7	mpbi	$$⊢\left(2\dots 2-1\right)\cap {\mathbb{Z}}_{\ge 2}=\left(2\dots 2-1\right)$$
9		uzdisj	$$⊢\left(2\dots 2-1\right)\cap {\mathbb{Z}}_{\ge 2}=\varnothing$$
10	8 9	eqtr3i	$$⊢\left(2\dots 2-1\right)=\varnothing$$
11	10	raleqi	$$⊢\forall z\in \left(2\dots 2-1\right)\neg z\parallel 2\leftrightarrow \forall z\in \varnothing \neg z\parallel 2$$
12	5 11	mpbir	$$⊢\forall z\in \left(2\dots 2-1\right)\neg z\parallel 2$$
13		isprm3	$$⊢2\in \mathbb{P}\leftrightarrow \left(2\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in \left(2\dots 2-1\right)\neg z\parallel 2\right)$$
14	4 12 13	mpbir2an	$$⊢2\in \mathbb{P}$$