Metamath Proof Explorer

Theorem pockthi

Description: Pocklington's theorem, which gives a sufficient criterion for a number N to be prime. This is the preferred method for verifying large primes, being much more efficient to compute than trial division. This form has been optimized for application to specific large primes; see pockthg for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014)

Ref Expression
Hypotheses pockthi.p 
|- P e. Prime
pockthi.g 
|- G e. NN
pockthi.m 
|- M = ( G x. P )
pockthi.n 
|- N = ( M + 1 )
pockthi.d 
|- D e. NN
pockthi.e 
|- E e. NN
pockthi.a 
|- A e. NN
pockthi.fac 
|- M = ( D x. ( P ^ E ) )
pockthi.gt 
|- D < ( P ^ E )
pockthi.mod 
|- ( ( A ^ M ) mod N ) = ( 1 mod N )
pockthi.gcd 
|- ( ( ( A ^ G ) - 1 ) gcd N ) = 1
Assertion pockthi 
|- N e. Prime

Proof

Step Hyp Ref Expression
1 pockthi.p 
 |-  P e. Prime
2 pockthi.g 
 |-  G e. NN
3 pockthi.m 
 |-  M = ( G x. P )
4 pockthi.n 
 |-  N = ( M + 1 )
5 pockthi.d 
 |-  D e. NN
6 pockthi.e 
 |-  E e. NN
7 pockthi.a 
 |-  A e. NN
8 pockthi.fac 
 |-  M = ( D x. ( P ^ E ) )
9 pockthi.gt 
 |-  D < ( P ^ E )
10 pockthi.mod 
 |-  ( ( A ^ M ) mod N ) = ( 1 mod N )
11 pockthi.gcd 
 |-  ( ( ( A ^ G ) - 1 ) gcd N ) = 1
12 prmnn 
 |-  ( P e. Prime -> P e. NN )
13 1 12 ax-mp 
 |-  P e. NN
14 6 nnnn0i 
 |-  E e. NN0
15 nnexpcl 
 |-  ( ( P e. NN /\ E e. NN0 ) -> ( P ^ E ) e. NN )
16 13 14 15 mp2an 
 |-  ( P ^ E ) e. NN
17 16 a1i 
 |-  ( D e. NN -> ( P ^ E ) e. NN )
18 id 
 |-  ( D e. NN -> D e. NN )
19 9 a1i 
 |-  ( D e. NN -> D < ( P ^ E ) )
20 5 nncni 
 |-  D e. CC
21 16 nncni 
 |-  ( P ^ E ) e. CC
22 20 21 mulcomi 
 |-  ( D x. ( P ^ E ) ) = ( ( P ^ E ) x. D )
23 8 22 eqtri 
 |-  M = ( ( P ^ E ) x. D )
24 23 oveq1i 
 |-  ( M + 1 ) = ( ( ( P ^ E ) x. D ) + 1 )
25 4 24 eqtri 
 |-  N = ( ( ( P ^ E ) x. D ) + 1 )
26 25 a1i 
 |-  ( D e. NN -> N = ( ( ( P ^ E ) x. D ) + 1 ) )
27 prmdvdsexpb 
 |-  ( ( x e. Prime /\ P e. Prime /\ E e. NN ) -> ( x || ( P ^ E ) <-> x = P ) )
28 1 6 27 mp3an23 
 |-  ( x e. Prime -> ( x || ( P ^ E ) <-> x = P ) )
29 2 13 nnmulcli 
 |-  ( G x. P ) e. NN
30 3 29 eqeltri 
 |-  M e. NN
31 30 nncni 
 |-  M e. CC
32 ax-1cn 
 |-  1 e. CC
33 31 32 4 mvrraddi 
 |-  ( N - 1 ) = M
34 33 oveq2i 
 |-  ( A ^ ( N - 1 ) ) = ( A ^ M )
35 34 oveq1i 
 |-  ( ( A ^ ( N - 1 ) ) mod N ) = ( ( A ^ M ) mod N )
36 peano2nn 
 |-  ( M e. NN -> ( M + 1 ) e. NN )
37 30 36 ax-mp 
 |-  ( M + 1 ) e. NN
38 4 37 eqeltri 
 |-  N e. NN
39 38 nnrei 
 |-  N e. RR
40 30 nngt0i 
 |-  0 < M
41 30 nnrei 
 |-  M e. RR
42 1re 
 |-  1 e. RR
43 ltaddpos2 
 |-  ( ( M e. RR /\ 1 e. RR ) -> ( 0 < M <-> 1 < ( M + 1 ) ) )
44 41 42 43 mp2an 
 |-  ( 0 < M <-> 1 < ( M + 1 ) )
45 40 44 mpbi 
 |-  1 < ( M + 1 )
46 45 4 breqtrri 
 |-  1 < N
47 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
48 39 46 47 mp2an 
 |-  ( 1 mod N ) = 1
49 10 48 eqtri 
 |-  ( ( A ^ M ) mod N ) = 1
50 35 49 eqtri 
 |-  ( ( A ^ ( N - 1 ) ) mod N ) = 1
51 oveq2 
 |-  ( x = P -> ( ( N - 1 ) / x ) = ( ( N - 1 ) / P ) )
52 2 nncni 
 |-  G e. CC
53 13 nncni 
 |-  P e. CC
54 52 53 mulcomi 
 |-  ( G x. P ) = ( P x. G )
55 33 3 54 3eqtrri 
 |-  ( P x. G ) = ( N - 1 )
56 38 nncni 
 |-  N e. CC
57 56 32 subcli 
 |-  ( N - 1 ) e. CC
58 13 nnne0i 
 |-  P =/= 0
59 57 53 52 58 divmuli 
 |-  ( ( ( N - 1 ) / P ) = G <-> ( P x. G ) = ( N - 1 ) )
60 55 59 mpbir 
 |-  ( ( N - 1 ) / P ) = G
61 51 60 eqtrdi 
 |-  ( x = P -> ( ( N - 1 ) / x ) = G )
62 61 oveq2d 
 |-  ( x = P -> ( A ^ ( ( N - 1 ) / x ) ) = ( A ^ G ) )
63 62 oveq1d 
 |-  ( x = P -> ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) = ( ( A ^ G ) - 1 ) )
64 63 oveq1d 
 |-  ( x = P -> ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = ( ( ( A ^ G ) - 1 ) gcd N ) )
65 64 11 eqtrdi 
 |-  ( x = P -> ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 )
66 7 nnzi 
 |-  A e. ZZ
67 oveq1 
 |-  ( y = A -> ( y ^ ( N - 1 ) ) = ( A ^ ( N - 1 ) ) )
68 67 oveq1d 
 |-  ( y = A -> ( ( y ^ ( N - 1 ) ) mod N ) = ( ( A ^ ( N - 1 ) ) mod N ) )
69 68 eqeq1d 
 |-  ( y = A -> ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 <-> ( ( A ^ ( N - 1 ) ) mod N ) = 1 ) )
70 oveq1 
 |-  ( y = A -> ( y ^ ( ( N - 1 ) / x ) ) = ( A ^ ( ( N - 1 ) / x ) ) )
71 70 oveq1d 
 |-  ( y = A -> ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) = ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) )
72 71 oveq1d 
 |-  ( y = A -> ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) )
73 72 eqeq1d 
 |-  ( y = A -> ( ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 <-> ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) )
74 69 73 anbi12d 
 |-  ( y = A -> ( ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) <-> ( ( ( A ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) ) )
75 74 rspcev 
 |-  ( ( A e. ZZ /\ ( ( ( A ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) ) -> E. y e. ZZ ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) )
76 66 75 mpan 
 |-  ( ( ( ( A ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( A ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) -> E. y e. ZZ ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) )
77 50 65 76 sylancr 
 |-  ( x = P -> E. y e. ZZ ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) )
78 28 77 syl6bi 
 |-  ( x e. Prime -> ( x || ( P ^ E ) -> E. y e. ZZ ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) ) )
79 78 rgen 
 |-  A. x e. Prime ( x || ( P ^ E ) -> E. y e. ZZ ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) )
80 79 a1i 
 |-  ( D e. NN -> A. x e. Prime ( x || ( P ^ E ) -> E. y e. ZZ ( ( ( y ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( y ^ ( ( N - 1 ) / x ) ) - 1 ) gcd N ) = 1 ) ) )
81 17 18 19 26 80 pockthg 
 |-  ( D e. NN -> N e. Prime )
82 5 81 ax-mp 
 |-  N e. Prime