Theorem 19prm

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

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

Proof

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