Theorem 17prm

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

	Ref	Expression
Assertion	17prm	⊢ ; 1 7 ∈ ℙ

Proof

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