Theorem 23prm

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

	Ref	Expression
Assertion	23prm	⊢ ; 2 3 ∈ ℙ

Proof

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