This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmlem1

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)

Ref Expression
Hypotheses prmlem1.n 
|- N e. NN
prmlem1.gt 
|- 1 < N
prmlem1.2 
|- -. 2 || N
prmlem1.3 
|- -. 3 || N
prmlem1.lt 
|- N < ; 2 5
Assertion prmlem1 
|- N e. Prime

Proof

Step Hyp Ref Expression
1 prmlem1.n 
 |-  N e. NN
2 prmlem1.gt 
 |-  1 < N
3 prmlem1.2 
 |-  -. 2 || N
4 prmlem1.3 
 |-  -. 3 || N
5 prmlem1.lt 
 |-  N < ; 2 5
6 eluzelre 
 |-  ( x e. ( ZZ>= ` 5 ) -> x e. RR )
7 6 resqcld 
 |-  ( x e. ( ZZ>= ` 5 ) -> ( x ^ 2 ) e. RR )
8 eluzle 
 |-  ( x e. ( ZZ>= ` 5 ) -> 5 <_ x )
9 5re 
 |-  5 e. RR
10 5nn0 
 |-  5 e. NN0
11 10 nn0ge0i 
 |-  0 <_ 5
12 le2sq2 
 |-  ( ( ( 5 e. RR /\ 0 <_ 5 ) /\ ( x e. RR /\ 5 <_ x ) ) -> ( 5 ^ 2 ) <_ ( x ^ 2 ) )
13 9 11 12 mpanl12 
 |-  ( ( x e. RR /\ 5 <_ x ) -> ( 5 ^ 2 ) <_ ( x ^ 2 ) )
14 6 8 13 syl2anc 
 |-  ( x e. ( ZZ>= ` 5 ) -> ( 5 ^ 2 ) <_ ( x ^ 2 ) )
15 1 nnrei 
 |-  N e. RR
16 9 resqcli 
 |-  ( 5 ^ 2 ) e. RR
17 5cn 
 |-  5 e. CC
18 17 sqvali 
 |-  ( 5 ^ 2 ) = ( 5 x. 5 )
19 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
20 18 19 eqtri 
 |-  ( 5 ^ 2 ) = ; 2 5
21 5 20 breqtrri 
 |-  N < ( 5 ^ 2 )
22 ltletr 
 |-  ( ( N e. RR /\ ( 5 ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( N < ( 5 ^ 2 ) /\ ( 5 ^ 2 ) <_ ( x ^ 2 ) ) -> N < ( x ^ 2 ) ) )
23 21 22 mpani 
 |-  ( ( N e. RR /\ ( 5 ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( 5 ^ 2 ) <_ ( x ^ 2 ) -> N < ( x ^ 2 ) ) )
24 15 16 23 mp3an12 
 |-  ( ( x ^ 2 ) e. RR -> ( ( 5 ^ 2 ) <_ ( x ^ 2 ) -> N < ( x ^ 2 ) ) )
25 7 14 24 sylc 
 |-  ( x e. ( ZZ>= ` 5 ) -> N < ( x ^ 2 ) )
26 ltnle 
 |-  ( ( N e. RR /\ ( x ^ 2 ) e. RR ) -> ( N < ( x ^ 2 ) <-> -. ( x ^ 2 ) <_ N ) )
27 15 7 26 sylancr 
 |-  ( x e. ( ZZ>= ` 5 ) -> ( N < ( x ^ 2 ) <-> -. ( x ^ 2 ) <_ N ) )
28 25 27 mpbid 
 |-  ( x e. ( ZZ>= ` 5 ) -> -. ( x ^ 2 ) <_ N )
29 28 pm2.21d 
 |-  ( x e. ( ZZ>= ` 5 ) -> ( ( x ^ 2 ) <_ N -> -. x || N ) )
30 29 adantld 
 |-  ( x e. ( ZZ>= ` 5 ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
31 30 adantl 
 |-  ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
32 1 2 3 4 31 prmlem1a 
 |-  N e. Prime