Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmlem1 Structured version   Unicode version

Theorem prmlem1 13430
 Description: A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
Hypotheses
Ref Expression
prmlem1.n
prmlem1.gt
prmlem1.2
prmlem1.3
prmlem1.lt ;
Assertion
Ref Expression
prmlem1

Proof of Theorem prmlem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 prmlem1.n . 2
2 prmlem1.gt . 2
3 prmlem1.2 . 2
4 prmlem1.3 . 2
5 eluzelre 10497 . . . . . . . 8
65resqcld 11549 . . . . . . 7
7 eluzle 10498 . . . . . . . 8
8 5re 10075 . . . . . . . . 9
9 5nn0 10241 . . . . . . . . . 10
109nn0ge0i 10249 . . . . . . . . 9
11 le2sq2 11457 . . . . . . . . 9
128, 10, 11mpanl12 664 . . . . . . . 8
135, 7, 12syl2anc 643 . . . . . . 7
141nnrei 10009 . . . . . . . 8
158resqcli 11467 . . . . . . . 8
16 prmlem1.lt . . . . . . . . . 10 ;
178recni 9102 . . . . . . . . . . . 12
1817sqvali 11461 . . . . . . . . . . 11
19 5t5e25 10458 . . . . . . . . . . 11 ;
2018, 19eqtri 2456 . . . . . . . . . 10 ;
2116, 20breqtrri 4237 . . . . . . . . 9
22 ltletr 9166 . . . . . . . . 9
2321, 22mpani 658 . . . . . . . 8
2414, 15, 23mp3an12 1269 . . . . . . 7
256, 13, 24sylc 58 . . . . . 6
26 ltnle 9155 . . . . . . 7
2714, 6, 26sylancr 645 . . . . . 6
2825, 27mpbid 202 . . . . 5
2928pm2.21d 100 . . . 4