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 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		9nn	⊢ 9 ∈ ℕ
3	1 2	decnncl	⊢ ; 1 9 ∈ ℕ
4		1nn	⊢ 1 ∈ ℕ
5		9nn0	⊢ 9 ∈ ℕ0
6		1lt10	⊢ 1 < ; 1 0
7	4 5 1 6	declti	⊢ 1 < ; 1 9
8		4nn0	⊢ 4 ∈ ℕ0
9		4t2e8	⊢ ( 4 · 2 ) = 8
10		df-9	⊢ 9 = ( 8 + 1 )
11	1 8 9 10	dec2dvds	⊢ ¬ 2 ∥ ; 1 9
12		3nn	⊢ 3 ∈ ℕ
13		6nn0	⊢ 6 ∈ ℕ0
14		8nn0	⊢ 8 ∈ ℕ0
15		8p1e9	⊢ ( 8 + 1 ) = 9
16		6cn	⊢ 6 ∈ ℂ
17		3cn	⊢ 3 ∈ ℂ
18		6t3e18	⊢ ( 6 · 3 ) = ; 1 8
19	16 17 18	mulcomli	⊢ ( 3 · 6 ) = ; 1 8
20	1 14 15 19	decsuc	⊢ ( ( 3 · 6 ) + 1 ) = ; 1 9
21		1lt3	⊢ 1 < 3
22	12 13 4 20 21	ndvdsi	⊢ ¬ 3 ∥ ; 1 9
23		2nn0	⊢ 2 ∈ ℕ0
24		5nn0	⊢ 5 ∈ ℕ0
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 ∈ ℙ