Theorem 13prm

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

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

Proof

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