Theorem 3prm

Description: 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		3z	$$⊢3\in \mathbb{Z}$$
2		1lt3	$$⊢1<3$$
3		eluz2b1	$$⊢3\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(3\in \mathbb{Z}\wedge 1<3\right)$$
4	1 2 3	mpbir2an	$$⊢3\in {\mathbb{Z}}_{\ge 2}$$
5		elfz1eq	$$⊢z\in \left(2\dots 2\right)\to z=2$$
6		n2dvds3	$$⊢\neg 2\parallel 3$$
7		breq1	$$⊢z=2\to \left(z\parallel 3\leftrightarrow 2\parallel 3\right)$$
8	6 7	mtbiri	$$⊢z=2\to \neg z\parallel 3$$
9	5 8	syl	$$⊢z\in \left(2\dots 2\right)\to \neg z\parallel 3$$
10		3m1e2	$$⊢3-1=2$$
11	10	oveq2i	$$⊢\left(2\dots 3-1\right)=\left(2\dots 2\right)$$
12	9 11	eleq2s	$$⊢z\in \left(2\dots 3-1\right)\to \neg z\parallel 3$$
13	12	rgen	$$⊢\forall z\in \left(2\dots 3-1\right)\neg z\parallel 3$$
14		isprm3	$$⊢3\in \mathbb{P}\leftrightarrow \left(3\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in \left(2\dots 3-1\right)\neg z\parallel 3\right)$$
15	4 13 14	mpbir2an	$$⊢3\in \mathbb{P}$$