Theorem 5prm

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

	Ref	Expression
Assertion	5prm	⊢ 5 ∈ ℙ

Proof

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