Theorem 7prm

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

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

Proof

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