Metamath Proof Explorer

Theorem prmlem1a

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
prmlem1a.x 
|- ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
Assertion prmlem1a 
|- 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 prmlem1a.x 
 |-  ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
6 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
7 1 2 6 mpbir2an 
 |-  N e. ( ZZ>= ` 2 )
8 breq1 
 |-  ( x = 2 -> ( x || N <-> 2 || N ) )
9 8 notbid 
 |-  ( x = 2 -> ( -. x || N <-> -. 2 || N ) )
10 9 imbi2d 
 |-  ( x = 2 -> ( ( ( x ^ 2 ) <_ N -> -. x || N ) <-> ( ( x ^ 2 ) <_ N -> -. 2 || N ) ) )
11 prmnn 
 |-  ( x e. Prime -> x e. NN )
12 11 adantr 
 |-  ( ( x e. Prime /\ x =/= 2 ) -> x e. NN )
13 eldifsn 
 |-  ( x e. ( Prime \ { 2 } ) <-> ( x e. Prime /\ x =/= 2 ) )
14 n2dvds1 
 |-  -. 2 || 1
15 4 a1i 
 |-  ( 3 e. Prime -> -. 3 || N )
16 3p2e5 
 |-  ( 3 + 2 ) = 5
17 5 15 16 prmlem0 
 |-  ( ( -. 2 || 3 /\ x e. ( ZZ>= ` 3 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
18 1nprm 
 |-  -. 1 e. Prime
19 18 pm2.21i 
 |-  ( 1 e. Prime -> -. 1 || N )
20 1p2e3 
 |-  ( 1 + 2 ) = 3
21 17 19 20 prmlem0 
 |-  ( ( -. 2 || 1 /\ x e. ( ZZ>= ` 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
22 14 21 mpan 
 |-  ( x e. ( ZZ>= ` 1 ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 22 23 eleq2s 
 |-  ( x e. NN -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
25 24 expd 
 |-  ( x e. NN -> ( x e. ( Prime \ { 2 } ) -> ( ( x ^ 2 ) <_ N -> -. x || N ) ) )
26 13 25 syl5bir 
 |-  ( x e. NN -> ( ( x e. Prime /\ x =/= 2 ) -> ( ( x ^ 2 ) <_ N -> -. x || N ) ) )
27 12 26 mpcom 
 |-  ( ( x e. Prime /\ x =/= 2 ) -> ( ( x ^ 2 ) <_ N -> -. x || N ) )
28 3 2a1i 
 |-  ( x e. Prime -> ( ( x ^ 2 ) <_ N -> -. 2 || N ) )
29 10 27 28 pm2.61ne 
 |-  ( x e. Prime -> ( ( x ^ 2 ) <_ N -> -. x || N ) )
30 29 rgen 
 |-  A. x e. Prime ( ( x ^ 2 ) <_ N -> -. x || N )
31 isprm5 
 |-  ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ A. x e. Prime ( ( x ^ 2 ) <_ N -> -. x || N ) ) )
32 7 30 31 mpbir2an 
 |-  N e. Prime