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	$$⊢23\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		3nn	$$⊢3\in \mathbb{N}$$
3	1 2	decnncl	$$⊢23\in \mathbb{N}$$
4		2nn	$$⊢2\in \mathbb{N}$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		1lt10	$$⊢1<10$$
8	4 5 6 7	declti	$$⊢1<23$$
9	4	nncni	$$⊢2\in ℂ$$
10	9	mulid2i	$$⊢1\cdot 2=2$$
11		df-3	$$⊢3=2+1$$
12	1 6 10 11	dec2dvds	$$⊢\neg 2\parallel 23$$
13		7nn0	$$⊢7\in {\mathbb{N}}_0$$
14		7cn	$$⊢7\in ℂ$$
15	2	nncni	$$⊢3\in ℂ$$
16		7t3e21	$$⊢7\cdot 3=21$$
17	14 15 16	mulcomli	$$⊢3\cdot 7=21$$
18		1p2e3	$$⊢1+2=3$$
19	1 6 1 17 18	decaddi	$$⊢3\cdot 7+2=23$$
20		2lt3	$$⊢2<3$$
21	2 13 4 19 20	ndvdsi	$$⊢\neg 3\parallel 23$$
22		5nn	$$⊢5\in \mathbb{N}$$
23		3lt5	$$⊢3<5$$
24	1 5 22 23	declt	$$⊢23<25$$
25	3 8 12 21 24	prmlem1	$$⊢23\in \mathbb{P}$$