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	⊢ ; 1 3 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		3nn	⊢ 3 ∈ ℕ
3	1 2	decnncl	⊢ ; 1 3 ∈ ℕ
4		1nn	⊢ 1 ∈ ℕ
5		3nn0	⊢ 3 ∈ ℕ0
6		1lt10	⊢ 1 < ; 1 0
7	4 5 1 6	declti	⊢ 1 < ; 1 3
8		2cn	⊢ 2 ∈ ℂ
9	8	mulid2i	⊢ ( 1 · 2 ) = 2
10		df-3	⊢ 3 = ( 2 + 1 )
11	1 1 9 10	dec2dvds	⊢ ¬ 2 ∥ ; 1 3
12		4nn0	⊢ 4 ∈ ℕ0
13		2nn0	⊢ 2 ∈ ℕ0
14		2p1e3	⊢ ( 2 + 1 ) = 3
15		4cn	⊢ 4 ∈ ℂ
16		3cn	⊢ 3 ∈ ℂ
17		4t3e12	⊢ ( 4 · 3 ) = ; 1 2
18	15 16 17	mulcomli	⊢ ( 3 · 4 ) = ; 1 2
19	1 13 14 18	decsuc	⊢ ( ( 3 · 4 ) + 1 ) = ; 1 3
20		1lt3	⊢ 1 < 3
21	2 12 4 19 20	ndvdsi	⊢ ¬ 3 ∥ ; 1 3
22		5nn0	⊢ 5 ∈ ℕ0
23		3lt10	⊢ 3 < ; 1 0
24		1lt2	⊢ 1 < 2
25	1 13 5 22 23 24	decltc	⊢ ; 1 3 < ; 2 5
26	3 7 11 21 25	prmlem1	⊢ ; 1 3 ∈ ℙ