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 e. Prime

Proof

Step	Hyp	Ref	Expression
1		2nn0	|- 2 e. NN0
2		3nn	|- 3 e. NN
3	1 2	decnncl	|- ; 2 3 e. NN
4		2nn	|- 2 e. NN
5		3nn0	|- 3 e. NN0
6		1nn0	|- 1 e. NN0
7		1lt10	|- 1 < ; 1 0
8	4 5 6 7	declti	|- 1 < ; 2 3
9	4	nncni	|- 2 e. CC
10	9	mullidi	|- ( 1 x. 2 ) = 2
11		df-3	|- 3 = ( 2 + 1 )
12	1 6 10 11	dec2dvds	|- -. 2 || ; 2 3
13		7nn0	|- 7 e. NN0
14		7cn	|- 7 e. CC
15	2	nncni	|- 3 e. CC
16		7t3e21	|- ( 7 x. 3 ) = ; 2 1
17	14 15 16	mulcomli	|- ( 3 x. 7 ) = ; 2 1
18		1p2e3	|- ( 1 + 2 ) = 3
19	1 6 1 17 18	decaddi	|- ( ( 3 x. 7 ) + 2 ) = ; 2 3
20		2lt3	|- 2 < 3
21	2 13 4 19 20	ndvdsi	|- -. 3 || ; 2 3
22		5nn	|- 5 e. NN
23		3lt5	|- 3 < 5
24	1 5 22 23	declt	|- ; 2 3 < ; 2 5
25	3 8 12 21 24	prmlem1	|- ; 2 3 e. Prime