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	|- ; 1 9 e. Prime

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		9nn	|- 9 e. NN
3	1 2	decnncl	|- ; 1 9 e. NN
4		1nn	|- 1 e. NN
5		9nn0	|- 9 e. NN0
6		1lt10	|- 1 < ; 1 0
7	4 5 1 6	declti	|- 1 < ; 1 9
8		4nn0	|- 4 e. NN0
9		4t2e8	|- ( 4 x. 2 ) = 8
10		df-9	|- 9 = ( 8 + 1 )
11	1 8 9 10	dec2dvds	|- -. 2 || ; 1 9
12		3nn	|- 3 e. NN
13		6nn0	|- 6 e. NN0
14		8nn0	|- 8 e. NN0
15		8p1e9	|- ( 8 + 1 ) = 9
16		6cn	|- 6 e. CC
17		3cn	|- 3 e. CC
18		6t3e18	|- ( 6 x. 3 ) = ; 1 8
19	16 17 18	mulcomli	|- ( 3 x. 6 ) = ; 1 8
20	1 14 15 19	decsuc	|- ( ( 3 x. 6 ) + 1 ) = ; 1 9
21		1lt3	|- 1 < 3
22	12 13 4 20 21	ndvdsi	|- -. 3 || ; 1 9
23		2nn0	|- 2 e. NN0
24		5nn0	|- 5 e. NN0
25		9lt10	|- 9 < ; 1 0
26		1lt2	|- 1 < 2
27	1 23 5 24 25 26	decltc	|- ; 1 9 < ; 2 5
28	3 7 11 22 27	prmlem1	|- ; 1 9 e. Prime