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 ⊢ 𝑃 ∈ ℙ
pockthi.g ⊢ 𝐺 ∈ ℕ
pockthi.m ⊢ 𝑀 = ( 𝐺 · 𝑃 )
pockthi.n ⊢ 𝑁 = ( 𝑀 + 1 )
pockthi.d ⊢ 𝐷 ∈ ℕ
pockthi.e ⊢ 𝐸 ∈ ℕ
pockthi.a ⊢ 𝐴 ∈ ℕ
pockthi.fac ⊢ 𝑀 = ( 𝐷 · ( 𝑃 ↑ 𝐸 ) )
pockthi.gt ⊢ 𝐷 < ( 𝑃 ↑ 𝐸 )
pockthi.mod ⊢ ( ( 𝐴 ↑ 𝑀 ) mod 𝑁 ) = ( 1 mod 𝑁 )
pockthi.gcd ⊢ ( ( ( 𝐴 ↑ 𝐺 ) − 1 ) gcd 𝑁 ) = 1
Assertion pockthi 𝑁 ∈ ℙ

Proof

Step Hyp Ref Expression
1 pockthi.p ⊢ 𝑃 ∈ ℙ
2 pockthi.g ⊢ 𝐺 ∈ ℕ
3 pockthi.m ⊢ 𝑀 = ( 𝐺 · 𝑃 )
4 pockthi.n ⊢ 𝑁 = ( 𝑀 + 1 )
5 pockthi.d ⊢ 𝐷 ∈ ℕ
6 pockthi.e ⊢ 𝐸 ∈ ℕ
7 pockthi.a ⊢ 𝐴 ∈ ℕ
8 pockthi.fac ⊢ 𝑀 = ( 𝐷 · ( 𝑃 ↑ 𝐸 ) )
9 pockthi.gt ⊢ 𝐷 < ( 𝑃 ↑ 𝐸 )
10 pockthi.mod ⊢ ( ( 𝐴 ↑ 𝑀 ) mod 𝑁 ) = ( 1 mod 𝑁 )
11 pockthi.gcd ⊢ ( ( ( 𝐴 ↑ 𝐺 ) − 1 ) gcd 𝑁 ) = 1
12 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
13 1 12 ax-mp ⊢ 𝑃 ∈ ℕ
14 6 nnnn0i ⊢ 𝐸 ∈ ℕ0
15 nnexpcl ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐸 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐸 ) ∈ ℕ )
16 13 14 15 mp2an ⊢ ( 𝑃 ↑ 𝐸 ) ∈ ℕ
17 16 a1i ⊢ ( 𝐷 ∈ ℕ → ( 𝑃 ↑ 𝐸 ) ∈ ℕ )
18 id ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℕ )
19 9 a1i ⊢ ( 𝐷 ∈ ℕ → 𝐷 < ( 𝑃 ↑ 𝐸 ) )
20 5 nncni ⊢ 𝐷 ∈ ℂ
21 16 nncni ⊢ ( 𝑃 ↑ 𝐸 ) ∈ ℂ
22 20 21 mulcomi ⊢ ( 𝐷 · ( 𝑃 ↑ 𝐸 ) ) = ( ( 𝑃 ↑ 𝐸 ) · 𝐷 )
23 8 22 eqtri ⊢ 𝑀 = ( ( 𝑃 ↑ 𝐸 ) · 𝐷 )
24 23 oveq1i ⊢ ( 𝑀 + 1 ) = ( ( ( 𝑃 ↑ 𝐸 ) · 𝐷 ) + 1 )
25 4 24 eqtri ⊢ 𝑁 = ( ( ( 𝑃 ↑ 𝐸 ) · 𝐷 ) + 1 )
26 25 a1i ⊢ ( 𝐷 ∈ ℕ → 𝑁 = ( ( ( 𝑃 ↑ 𝐸 ) · 𝐷 ) + 1 ) )
27 prmdvdsexpb ⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝐸 ∈ ℕ ) → ( 𝑥 ∥ ( 𝑃 ↑ 𝐸 ) ↔ 𝑥 = 𝑃 ) )
28 1 6 27 mp3an23 ⊢ ( 𝑥 ∈ ℙ → ( 𝑥 ∥ ( 𝑃 ↑ 𝐸 ) ↔ 𝑥 = 𝑃 ) )
29 2 13 nnmulcli ⊢ ( 𝐺 · 𝑃 ) ∈ ℕ
30 3 29 eqeltri ⊢ 𝑀 ∈ ℕ
31 30 nncni ⊢ 𝑀 ∈ ℂ
32 ax-1cn ⊢ 1 ∈ ℂ
33 31 32 4 mvrraddi ⊢ ( 𝑁 − 1 ) = 𝑀
34 33 oveq2i ⊢ ( 𝐴 ↑ ( 𝑁 − 1 ) ) = ( 𝐴 ↑ 𝑀 )
35 34 oveq1i ⊢ ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( ( 𝐴 ↑ 𝑀 ) mod 𝑁 )
36 peano2nn ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℕ )
37 30 36 ax-mp ⊢ ( 𝑀 + 1 ) ∈ ℕ
38 4 37 eqeltri ⊢ 𝑁 ∈ ℕ
39 38 nnrei ⊢ 𝑁 ∈ ℝ
40 30 nngt0i ⊢ 0 < 𝑀
41 30 nnrei ⊢ 𝑀 ∈ ℝ
42 1re ⊢ 1 ∈ ℝ
43 ltaddpos2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 < 𝑀 ↔ 1 < ( 𝑀 + 1 ) ) )
44 41 42 43 mp2an ⊢ ( 0 < 𝑀 ↔ 1 < ( 𝑀 + 1 ) )
45 40 44 mpbi ⊢ 1 < ( 𝑀 + 1 )
46 45 4 breqtrri ⊢ 1 < 𝑁
47 1mod ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )
48 39 46 47 mp2an ⊢ ( 1 mod 𝑁 ) = 1
49 10 48 eqtri ⊢ ( ( 𝐴 ↑ 𝑀 ) mod 𝑁 ) = 1
50 35 49 eqtri ⊢ ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1
51 oveq2 ⊢ ( 𝑥 = 𝑃 → ( ( 𝑁 − 1 ) / 𝑥 ) = ( ( 𝑁 − 1 ) / 𝑃 ) )
52 2 nncni ⊢ 𝐺 ∈ ℂ
53 13 nncni ⊢ 𝑃 ∈ ℂ
54 52 53 mulcomi ⊢ ( 𝐺 · 𝑃 ) = ( 𝑃 · 𝐺 )
55 33 3 54 3eqtrri ⊢ ( 𝑃 · 𝐺 ) = ( 𝑁 − 1 )
56 38 nncni ⊢ 𝑁 ∈ ℂ
57 56 32 subcli ⊢ ( 𝑁 − 1 ) ∈ ℂ
58 13 nnne0i ⊢ 𝑃 ≠ 0
59 57 53 52 58 divmuli ⊢ ( ( ( 𝑁 − 1 ) / 𝑃 ) = 𝐺 ↔ ( 𝑃 · 𝐺 ) = ( 𝑁 − 1 ) )
60 55 59 mpbir ⊢ ( ( 𝑁 − 1 ) / 𝑃 ) = 𝐺
61 51 60 eqtrdi ⊢ ( 𝑥 = 𝑃 → ( ( 𝑁 − 1 ) / 𝑥 ) = 𝐺 )
62 61 oveq2d ⊢ ( 𝑥 = 𝑃 → ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) = ( 𝐴 ↑ 𝐺 ) )
63 62 oveq1d ⊢ ( 𝑥 = 𝑃 → ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) = ( ( 𝐴 ↑ 𝐺 ) − 1 ) )
64 63 oveq1d ⊢ ( 𝑥 = 𝑃 → ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = ( ( ( 𝐴 ↑ 𝐺 ) − 1 ) gcd 𝑁 ) )
65 64 11 eqtrdi ⊢ ( 𝑥 = 𝑃 → ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 )
66 7 nnzi ⊢ 𝐴 ∈ ℤ
67 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ↑ ( 𝑁 − 1 ) ) = ( 𝐴 ↑ ( 𝑁 − 1 ) ) )
68 67 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) )
69 68 eqeq1d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ↔ ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ) )
70 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) = ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) )
71 70 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) = ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) )
72 71 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) )
73 72 eqeq1d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ↔ ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) )
74 69 73 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) ↔ ( ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) ) )
75 74 rspcev ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) ) → ∃ 𝑦 ∈ ℤ ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) )
76 66 75 mpan ⊢ ( ( ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝐴 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) → ∃ 𝑦 ∈ ℤ ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) )
77 50 65 76 sylancr ⊢ ( 𝑥 = 𝑃 → ∃ 𝑦 ∈ ℤ ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) )
78 28 77 syl6bi ⊢ ( 𝑥 ∈ ℙ → ( 𝑥 ∥ ( 𝑃 ↑ 𝐸 ) → ∃ 𝑦 ∈ ℤ ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) ) )
79 78 rgen ⊢ ∀ 𝑥 ∈ ℙ ( 𝑥 ∥ ( 𝑃 ↑ 𝐸 ) → ∃ 𝑦 ∈ ℤ ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) )
80 79 a1i ⊢ ( 𝐷 ∈ ℕ → ∀ 𝑥 ∈ ℙ ( 𝑥 ∥ ( 𝑃 ↑ 𝐸 ) → ∃ 𝑦 ∈ ℤ ( ( ( 𝑦 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 ∧ ( ( ( 𝑦 ↑ ( ( 𝑁 − 1 ) / 𝑥 ) ) − 1 ) gcd 𝑁 ) = 1 ) ) )
81 17 18 19 26 80 pockthg ⊢ ( 𝐷 ∈ ℕ → 𝑁 ∈ ℙ )
82 5 81 ax-mp ⊢ 𝑁 ∈ ℙ