Theorem 17prm

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

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

Proof

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