Metamath Proof Explorer


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

Proof

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