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
pockthi.g G
pockthi.m M = G P
pockthi.n N = M + 1
pockthi.d D
pockthi.e E
pockthi.a A
pockthi.fac M = D 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

Proof

Step Hyp Ref Expression
1 pockthi.p P
2 pockthi.g G
3 pockthi.m M = G P
4 pockthi.n N = M + 1
5 pockthi.d D
6 pockthi.e E
7 pockthi.a A
8 pockthi.fac M = D 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 P
13 1 12 ax-mp P
14 6 nnnn0i E 0
15 nnexpcl P E 0 P E
16 13 14 15 mp2an P E
17 16 a1i D P E
18 id D D
19 9 a1i D D < P E
20 5 nncni D
21 16 nncni P E
22 20 21 mulcomi D P E = P E D
23 8 22 eqtri M = P E D
24 23 oveq1i M + 1 = P E D + 1
25 4 24 eqtri N = P E D + 1
26 25 a1i D N = P E D + 1
27 prmdvdsexpb x P E x P E x = P
28 1 6 27 mp3an23 x x P E x = P
29 2 13 nnmulcli G P
30 3 29 eqeltri M
31 30 nncni M
32 ax-1cn 1
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 M + 1
37 30 36 ax-mp M + 1
38 4 37 eqeltri N
39 38 nnrei N
40 30 nngt0i 0 < M
41 30 nnrei M
42 1re 1
43 ltaddpos2 M 1 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 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
53 13 nncni P
54 52 53 mulcomi G P = P G
55 33 3 54 3eqtrri P G = N 1
56 38 nncni N
57 56 32 subcli N 1
58 13 nnne0i P 0
59 57 53 52 58 divmuli N 1 P = G P 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
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 A N 1 mod N = 1 A N 1 x 1 gcd N = 1 y 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 y y N 1 mod N = 1 y N 1 x 1 gcd N = 1
77 50 65 76 sylancr x = P y y N 1 mod N = 1 y N 1 x 1 gcd N = 1
78 28 77 syl6bi x x P E y y N 1 mod N = 1 y N 1 x 1 gcd N = 1
79 78 rgen x x P E y y N 1 mod N = 1 y N 1 x 1 gcd N = 1
80 79 a1i D x x P E y y N 1 mod N = 1 y N 1 x 1 gcd N = 1
81 17 18 19 26 80 pockthg D N
82 5 81 ax-mp N