Metamath Proof Explorer

Theorem proththd

Description: Proth's theorem (1878). If P is aProth number, i.e. a number of the form k2^n+1 with k less than 2^n, and if there exists an integer x for which x^((P-1)/2) is -1 modulo P, then P is prime. Such a prime is called aProth prime. Like Pocklington's theorem (see pockthg ), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020)

Ref Expression
Hypotheses proththd.n 
|- ( ph -> N e. NN )
proththd.k 
|- ( ph -> K e. NN )
proththd.p 
|- ( ph -> P = ( ( K x. ( 2 ^ N ) ) + 1 ) )
proththd.l 
|- ( ph -> K < ( 2 ^ N ) )
proththd.x 
|- ( ph -> E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )
Assertion proththd 
|- ( ph -> P e. Prime )

Proof

Step Hyp Ref Expression
1 proththd.n 
 |-  ( ph -> N e. NN )
2 proththd.k 
 |-  ( ph -> K e. NN )
3 proththd.p 
 |-  ( ph -> P = ( ( K x. ( 2 ^ N ) ) + 1 ) )
4 proththd.l 
 |-  ( ph -> K < ( 2 ^ N ) )
5 proththd.x 
 |-  ( ph -> E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )
6 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( ph -> 2 e. NN )
8 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
9 7 8 nnexpcld 
 |-  ( ph -> ( 2 ^ N ) e. NN )
10 2 nncnd 
 |-  ( ph -> K e. CC )
11 9 nncnd 
 |-  ( ph -> ( 2 ^ N ) e. CC )
12 10 11 mulcomd 
 |-  ( ph -> ( K x. ( 2 ^ N ) ) = ( ( 2 ^ N ) x. K ) )
13 12 oveq1d 
 |-  ( ph -> ( ( K x. ( 2 ^ N ) ) + 1 ) = ( ( ( 2 ^ N ) x. K ) + 1 ) )
14 3 13 eqtrd 
 |-  ( ph -> P = ( ( ( 2 ^ N ) x. K ) + 1 ) )
15 simpr 
 |-  ( ( ph /\ p e. Prime ) -> p e. Prime )
16 2prm 
 |-  2 e. Prime
17 16 a1i 
 |-  ( ( ph /\ p e. Prime ) -> 2 e. Prime )
18 1 adantr 
 |-  ( ( ph /\ p e. Prime ) -> N e. NN )
19 prmdvdsexpb 
 |-  ( ( p e. Prime /\ 2 e. Prime /\ N e. NN ) -> ( p || ( 2 ^ N ) <-> p = 2 ) )
20 15 17 18 19 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( 2 ^ N ) <-> p = 2 ) )
21 1 2 3 proththdlem 
 |-  ( ph -> ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) )
22 21 simp1d 
 |-  ( ph -> P e. NN )
23 22 nncnd 
 |-  ( ph -> P e. CC )
24 peano2cnm 
 |-  ( P e. CC -> ( P - 1 ) e. CC )
25 23 24 syl 
 |-  ( ph -> ( P - 1 ) e. CC )
26 25 adantr 
 |-  ( ( ph /\ x e. ZZ ) -> ( P - 1 ) e. CC )
27 2cnd 
 |-  ( ( ph /\ x e. ZZ ) -> 2 e. CC )
28 2ne0 
 |-  2 =/= 0
29 28 a1i 
 |-  ( ( ph /\ x e. ZZ ) -> 2 =/= 0 )
30 26 27 29 divcan1d 
 |-  ( ( ph /\ x e. ZZ ) -> ( ( ( P - 1 ) / 2 ) x. 2 ) = ( P - 1 ) )
31 30 eqcomd 
 |-  ( ( ph /\ x e. ZZ ) -> ( P - 1 ) = ( ( ( P - 1 ) / 2 ) x. 2 ) )
32 31 oveq2d 
 |-  ( ( ph /\ x e. ZZ ) -> ( x ^ ( P - 1 ) ) = ( x ^ ( ( ( P - 1 ) / 2 ) x. 2 ) ) )
33 zcn 
 |-  ( x e. ZZ -> x e. CC )
34 33 adantl 
 |-  ( ( ph /\ x e. ZZ ) -> x e. CC )
35 2nn0 
 |-  2 e. NN0
36 35 a1i 
 |-  ( ( ph /\ x e. ZZ ) -> 2 e. NN0 )
37 21 simp3d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
38 37 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
39 38 adantr 
 |-  ( ( ph /\ x e. ZZ ) -> ( ( P - 1 ) / 2 ) e. NN0 )
40 34 36 39 expmuld 
 |-  ( ( ph /\ x e. ZZ ) -> ( x ^ ( ( ( P - 1 ) / 2 ) x. 2 ) ) = ( ( x ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) )
41 32 40 eqtrd 
 |-  ( ( ph /\ x e. ZZ ) -> ( x ^ ( P - 1 ) ) = ( ( x ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) )
42 41 ad4ant13 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( x ^ ( P - 1 ) ) = ( ( x ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) )
43 42 oveq1d 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( x ^ ( P - 1 ) ) mod P ) = ( ( ( x ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) mod P ) )
44 38 adantr 
 |-  ( ( ph /\ p = 2 ) -> ( ( P - 1 ) / 2 ) e. NN0 )
45 44 anim1i 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( ( ( P - 1 ) / 2 ) e. NN0 /\ x e. ZZ ) )
46 45 ancomd 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( x e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) )
47 zexpcl 
 |-  ( ( x e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( x ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
48 46 47 syl 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( x ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
49 48 adantr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( x ^ ( ( P - 1 ) / 2 ) ) e. ZZ )
50 22 nnrpd 
 |-  ( ph -> P e. RR+ )
51 50 ad3antrrr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> P e. RR+ )
52 21 simp2d 
 |-  ( ph -> 1 < P )
53 52 ad3antrrr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> 1 < P )
54 simpr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) )
55 49 51 53 54 modexp2m1d 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) ^ 2 ) mod P ) = 1 )
56 43 55 eqtrd 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( x ^ ( P - 1 ) ) mod P ) = 1 )
57 oveq2 
 |-  ( p = 2 -> ( ( P - 1 ) / p ) = ( ( P - 1 ) / 2 ) )
58 57 eleq1d 
 |-  ( p = 2 -> ( ( ( P - 1 ) / p ) e. NN0 <-> ( ( P - 1 ) / 2 ) e. NN0 ) )
59 58 adantl 
 |-  ( ( ph /\ p = 2 ) -> ( ( ( P - 1 ) / p ) e. NN0 <-> ( ( P - 1 ) / 2 ) e. NN0 ) )
60 44 59 mpbird 
 |-  ( ( ph /\ p = 2 ) -> ( ( P - 1 ) / p ) e. NN0 )
61 60 anim2i 
 |-  ( ( x e. ZZ /\ ( ph /\ p = 2 ) ) -> ( x e. ZZ /\ ( ( P - 1 ) / p ) e. NN0 ) )
62 61 ancoms 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( x e. ZZ /\ ( ( P - 1 ) / p ) e. NN0 ) )
63 zexpcl 
 |-  ( ( x e. ZZ /\ ( ( P - 1 ) / p ) e. NN0 ) -> ( x ^ ( ( P - 1 ) / p ) ) e. ZZ )
64 62 63 syl 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( x ^ ( ( P - 1 ) / p ) ) e. ZZ )
65 64 zred 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( x ^ ( ( P - 1 ) / p ) ) e. RR )
66 65 adantr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( x ^ ( ( P - 1 ) / p ) ) e. RR )
67 1red 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> 1 e. RR )
68 67 renegcld 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> -u 1 e. RR )
69 oveq2 
 |-  ( 2 = p -> ( ( P - 1 ) / 2 ) = ( ( P - 1 ) / p ) )
70 69 eqcoms 
 |-  ( p = 2 -> ( ( P - 1 ) / 2 ) = ( ( P - 1 ) / p ) )
71 70 oveq2d 
 |-  ( p = 2 -> ( x ^ ( ( P - 1 ) / 2 ) ) = ( x ^ ( ( P - 1 ) / p ) ) )
72 71 oveq1d 
 |-  ( p = 2 -> ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( x ^ ( ( P - 1 ) / p ) ) mod P ) )
73 72 eqeq1d 
 |-  ( p = 2 -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) <-> ( ( x ^ ( ( P - 1 ) / p ) ) mod P ) = ( -u 1 mod P ) ) )
74 73 adantl 
 |-  ( ( ph /\ p = 2 ) -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) <-> ( ( x ^ ( ( P - 1 ) / p ) ) mod P ) = ( -u 1 mod P ) ) )
75 74 adantr 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) <-> ( ( x ^ ( ( P - 1 ) / p ) ) mod P ) = ( -u 1 mod P ) ) )
76 75 biimpa 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( x ^ ( ( P - 1 ) / p ) ) mod P ) = ( -u 1 mod P ) )
77 eqidd 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( 1 mod P ) = ( 1 mod P ) )
78 66 68 67 67 51 76 77 modsub12d 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) mod P ) = ( ( -u 1 - 1 ) mod P ) )
79 78 oveq1d 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) mod P ) gcd P ) = ( ( ( -u 1 - 1 ) mod P ) gcd P ) )
80 peano2zm 
 |-  ( ( x ^ ( ( P - 1 ) / p ) ) e. ZZ -> ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) e. ZZ )
81 64 80 syl 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) e. ZZ )
82 22 ad2antrr 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> P e. NN )
83 modgcd 
 |-  ( ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) e. ZZ /\ P e. NN ) -> ( ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) mod P ) gcd P ) = ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) )
84 81 82 83 syl2anc 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) mod P ) gcd P ) = ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) )
85 84 adantr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) mod P ) gcd P ) = ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) )
86 ax-1cn 
 |-  1 e. CC
87 negdi2 
 |-  ( ( 1 e. CC /\ 1 e. CC ) -> -u ( 1 + 1 ) = ( -u 1 - 1 ) )
88 87 eqcomd 
 |-  ( ( 1 e. CC /\ 1 e. CC ) -> ( -u 1 - 1 ) = -u ( 1 + 1 ) )
89 86 86 88 mp2an 
 |-  ( -u 1 - 1 ) = -u ( 1 + 1 )
90 1p1e2 
 |-  ( 1 + 1 ) = 2
91 90 negeqi 
 |-  -u ( 1 + 1 ) = -u 2
92 89 91 eqtri 
 |-  ( -u 1 - 1 ) = -u 2
93 92 a1i 
 |-  ( ph -> ( -u 1 - 1 ) = -u 2 )
94 93 oveq1d 
 |-  ( ph -> ( ( -u 1 - 1 ) mod P ) = ( -u 2 mod P ) )
95 94 oveq1d 
 |-  ( ph -> ( ( ( -u 1 - 1 ) mod P ) gcd P ) = ( ( -u 2 mod P ) gcd P ) )
96 nnnegz 
 |-  ( 2 e. NN -> -u 2 e. ZZ )
97 7 96 syl 
 |-  ( ph -> -u 2 e. ZZ )
98 modgcd 
 |-  ( ( -u 2 e. ZZ /\ P e. NN ) -> ( ( -u 2 mod P ) gcd P ) = ( -u 2 gcd P ) )
99 97 22 98 syl2anc 
 |-  ( ph -> ( ( -u 2 mod P ) gcd P ) = ( -u 2 gcd P ) )
100 2z 
 |-  2 e. ZZ
101 22 nnzd 
 |-  ( ph -> P e. ZZ )
102 neggcd 
 |-  ( ( 2 e. ZZ /\ P e. ZZ ) -> ( -u 2 gcd P ) = ( 2 gcd P ) )
103 100 101 102 sylancr 
 |-  ( ph -> ( -u 2 gcd P ) = ( 2 gcd P ) )
104 nnz 
 |-  ( P e. NN -> P e. ZZ )
105 oddm1d2 
 |-  ( P e. ZZ -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
106 104 105 syl 
 |-  ( P e. NN -> ( -. 2 || P <-> ( ( P - 1 ) / 2 ) e. ZZ ) )
107 106 biimprd 
 |-  ( P e. NN -> ( ( ( P - 1 ) / 2 ) e. ZZ -> -. 2 || P ) )
108 nnz 
 |-  ( ( ( P - 1 ) / 2 ) e. NN -> ( ( P - 1 ) / 2 ) e. ZZ )
109 107 108 impel 
 |-  ( ( P e. NN /\ ( ( P - 1 ) / 2 ) e. NN ) -> -. 2 || P )
110 isoddgcd1 
 |-  ( P e. ZZ -> ( -. 2 || P <-> ( 2 gcd P ) = 1 ) )
111 104 110 syl 
 |-  ( P e. NN -> ( -. 2 || P <-> ( 2 gcd P ) = 1 ) )
112 111 adantr 
 |-  ( ( P e. NN /\ ( ( P - 1 ) / 2 ) e. NN ) -> ( -. 2 || P <-> ( 2 gcd P ) = 1 ) )
113 109 112 mpbid 
 |-  ( ( P e. NN /\ ( ( P - 1 ) / 2 ) e. NN ) -> ( 2 gcd P ) = 1 )
114 113 3adant2 
 |-  ( ( P e. NN /\ 1 < P /\ ( ( P - 1 ) / 2 ) e. NN ) -> ( 2 gcd P ) = 1 )
115 21 114 syl 
 |-  ( ph -> ( 2 gcd P ) = 1 )
116 103 115 eqtrd 
 |-  ( ph -> ( -u 2 gcd P ) = 1 )
117 99 116 eqtrd 
 |-  ( ph -> ( ( -u 2 mod P ) gcd P ) = 1 )
118 95 117 eqtrd 
 |-  ( ph -> ( ( ( -u 1 - 1 ) mod P ) gcd P ) = 1 )
119 118 ad3antrrr 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( -u 1 - 1 ) mod P ) gcd P ) = 1 )
120 79 85 119 3eqtr3d 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 )
121 56 120 jca 
 |-  ( ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) /\ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) ) -> ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) )
122 121 ex 
 |-  ( ( ( ph /\ p = 2 ) /\ x e. ZZ ) -> ( ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) -> ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) )
123 122 reximdva 
 |-  ( ( ph /\ p = 2 ) -> ( E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) -> E. x e. ZZ ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) )
124 123 ex 
 |-  ( ph -> ( p = 2 -> ( E. x e. ZZ ( ( x ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( -u 1 mod P ) -> E. x e. ZZ ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) ) )
125 5 124 mpid 
 |-  ( ph -> ( p = 2 -> E. x e. ZZ ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) )
126 125 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( p = 2 -> E. x e. ZZ ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) )
127 20 126 sylbid 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( 2 ^ N ) -> E. x e. ZZ ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) )
128 127 ralrimiva 
 |-  ( ph -> A. p e. Prime ( p || ( 2 ^ N ) -> E. x e. ZZ ( ( ( x ^ ( P - 1 ) ) mod P ) = 1 /\ ( ( ( x ^ ( ( P - 1 ) / p ) ) - 1 ) gcd P ) = 1 ) ) )
129 9 2 4 14 128 pockthg 
 |-  ( ph -> P e. Prime )