Description: 23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by Mario Carneiro, 20-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 23prm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nn0 | ||
2 | 3nn | ||
3 | 1 2 | decnncl | |
4 | 2nn | ||
5 | 3nn0 | ||
6 | 1nn0 | ||
7 | 1lt10 | ||
8 | 4 5 6 7 | declti | |
9 | 4 | nncni | |
10 | 9 | mulid2i | |
11 | df-3 | ||
12 | 1 6 10 11 | dec2dvds | |
13 | 7nn0 | ||
14 | 7cn | ||
15 | 2 | nncni | |
16 | 7t3e21 | ||
17 | 14 15 16 | mulcomli | |
18 | 1p2e3 | ||
19 | 1 6 1 17 18 | decaddi | |
20 | 2lt3 | ||
21 | 2 13 4 19 20 | ndvdsi | |
22 | 5nn | ||
23 | 3lt5 | ||
24 | 1 5 22 23 | declt | |
25 | 3 8 12 21 24 | prmlem1 |