Theorem 7prm

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

	Ref	Expression
Assertion	7prm	⊢ 7 ∈ ℙ

Proof

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