Theorem 5prm

Description: 5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by Mario Carneiro, 20-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		5nn	$$⊢5\in \mathbb{N}$$
2		1lt5	$$⊢1<5$$
3		2nn	$$⊢2\in \mathbb{N}$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		2t2e4	$$⊢2\cdot 2=4$$
7	6	oveq1i	$$⊢2\cdot 2+1=4+1$$
8		df-5	$$⊢5=4+1$$
9	7 8	eqtr4i	$$⊢2\cdot 2+1=5$$
10		1lt2	$$⊢1<2$$
11	3 4 5 9 10	ndvdsi	$$⊢\neg 2\parallel 5$$
12		3nn	$$⊢3\in \mathbb{N}$$
13		1nn0	$$⊢1\in {\mathbb{N}}_0$$
14		3t1e3	$$⊢3\cdot 1=3$$
15	14	oveq1i	$$⊢3\cdot 1+2=3+2$$
16		3p2e5	$$⊢3+2=5$$
17	15 16	eqtri	$$⊢3\cdot 1+2=5$$
18		2lt3	$$⊢2<3$$
19	12 13 3 17 18	ndvdsi	$$⊢\neg 3\parallel 5$$
20		5nn0	$$⊢5\in {\mathbb{N}}_0$$
21		5lt10	$$⊢5<10$$
22	3 20 20 21	declti	$$⊢5<25$$
23	1 2 11 19 22	prmlem1	$$⊢5\in \mathbb{P}$$