Metamath Proof Explorer


Theorem lgseisenlem1

Description: Lemma for lgseisen . If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ) , then for any even 1 <_ u <_ P - 1 , M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1 . To simplify these statements, we divide all the even numbers by 2 , so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2 . (Contributed by Mario Carneiro, 17-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 φ P 2
lgseisen.2 φ Q 2
lgseisen.3 φ P Q
lgseisen.4 R = Q 2 x mod P
lgseisen.5 M = x 1 P 1 2 1 R R mod P 2
Assertion lgseisenlem1 φ M : 1 P 1 2 1 P 1 2

Proof

Step Hyp Ref Expression
1 lgseisen.1 φ P 2
2 lgseisen.2 φ Q 2
3 lgseisen.3 φ P Q
4 lgseisen.4 R = Q 2 x mod P
5 lgseisen.5 M = x 1 P 1 2 1 R R mod P 2
6 1zzd φ x 1 P 1 2 1
7 1 adantr φ x 1 P 1 2 P 2
8 oddprm P 2 P 1 2
9 7 8 syl φ x 1 P 1 2 P 1 2
10 9 nnzd φ x 1 P 1 2 P 1 2
11 neg1cn 1
12 11 a1i φ x 1 P 1 2 R 2 1
13 neg1ne0 1 0
14 13 a1i φ x 1 P 1 2 R 2 1 0
15 2z 2
16 15 a1i φ x 1 P 1 2 R 2 2
17 simpr φ x 1 P 1 2 R 2 R 2
18 expmulz 1 1 0 2 R 2 1 2 R 2 = -1 2 R 2
19 12 14 16 17 18 syl22anc φ x 1 P 1 2 R 2 1 2 R 2 = -1 2 R 2
20 2 adantr φ x 1 P 1 2 Q 2
21 20 eldifad φ x 1 P 1 2 Q
22 prmz Q Q
23 21 22 syl φ x 1 P 1 2 Q
24 elfzelz x 1 P 1 2 x
25 24 adantl φ x 1 P 1 2 x
26 zmulcl 2 x 2 x
27 15 25 26 sylancr φ x 1 P 1 2 2 x
28 23 27 zmulcld φ x 1 P 1 2 Q 2 x
29 7 eldifad φ x 1 P 1 2 P
30 prmnn P P
31 29 30 syl φ x 1 P 1 2 P
32 zmodfz Q 2 x P Q 2 x mod P 0 P 1
33 28 31 32 syl2anc φ x 1 P 1 2 Q 2 x mod P 0 P 1
34 4 33 eqeltrid φ x 1 P 1 2 R 0 P 1
35 elfznn0 R 0 P 1 R 0
36 34 35 syl φ x 1 P 1 2 R 0
37 36 nn0zd φ x 1 P 1 2 R
38 37 zcnd φ x 1 P 1 2 R
39 38 adantr φ x 1 P 1 2 R 2 R
40 2cnd φ x 1 P 1 2 R 2 2
41 2ne0 2 0
42 41 a1i φ x 1 P 1 2 R 2 2 0
43 39 40 42 divcan2d φ x 1 P 1 2 R 2 2 R 2 = R
44 43 oveq2d φ x 1 P 1 2 R 2 1 2 R 2 = 1 R
45 neg1sqe1 1 2 = 1
46 45 oveq1i -1 2 R 2 = 1 R 2
47 1exp R 2 1 R 2 = 1
48 47 adantl φ x 1 P 1 2 R 2 1 R 2 = 1
49 46 48 syl5eq φ x 1 P 1 2 R 2 -1 2 R 2 = 1
50 19 44 49 3eqtr3d φ x 1 P 1 2 R 2 1 R = 1
51 50 oveq1d φ x 1 P 1 2 R 2 1 R R = 1 R
52 39 mulid2d φ x 1 P 1 2 R 2 1 R = R
53 51 52 eqtrd φ x 1 P 1 2 R 2 1 R R = R
54 53 oveq1d φ x 1 P 1 2 R 2 1 R R mod P = R mod P
55 36 nn0red φ x 1 P 1 2 R
56 31 nnrpd φ x 1 P 1 2 P +
57 36 nn0ge0d φ x 1 P 1 2 0 R
58 28 zred φ x 1 P 1 2 Q 2 x
59 modlt Q 2 x P + Q 2 x mod P < P
60 58 56 59 syl2anc φ x 1 P 1 2 Q 2 x mod P < P
61 4 60 eqbrtrid φ x 1 P 1 2 R < P
62 modid R P + 0 R R < P R mod P = R
63 55 56 57 61 62 syl22anc φ x 1 P 1 2 R mod P = R
64 63 adantr φ x 1 P 1 2 R 2 R mod P = R
65 54 64 eqtrd φ x 1 P 1 2 R 2 1 R R mod P = R
66 65 oveq1d φ x 1 P 1 2 R 2 1 R R mod P 2 = R 2
67 66 17 eqeltrd φ x 1 P 1 2 R 2 1 R R mod P 2
68 31 nncnd φ x 1 P 1 2 P
69 68 mulid2d φ x 1 P 1 2 1 P = P
70 69 oveq2d φ x 1 P 1 2 - R + 1 P = - R + P
71 55 renegcld φ x 1 P 1 2 R
72 71 recnd φ x 1 P 1 2 R
73 68 72 addcomd φ x 1 P 1 2 P + R = - R + P
74 68 38 negsubd φ x 1 P 1 2 P + R = P R
75 70 73 74 3eqtr2d φ x 1 P 1 2 - R + 1 P = P R
76 75 oveq1d φ x 1 P 1 2 - R + 1 P mod P = P R mod P
77 modcyc R P + 1 - R + 1 P mod P = R mod P
78 71 56 6 77 syl3anc φ x 1 P 1 2 - R + 1 P mod P = R mod P
79 31 nnred φ x 1 P 1 2 P
80 79 55 resubcld φ x 1 P 1 2 P R
81 55 79 61 ltled φ x 1 P 1 2 R P
82 79 55 subge0d φ x 1 P 1 2 0 P R R P
83 81 82 mpbird φ x 1 P 1 2 0 P R
84 2nn 2
85 elfznn x 1 P 1 2 x
86 85 adantl φ x 1 P 1 2 x
87 nnmulcl 2 x 2 x
88 84 86 87 sylancr φ x 1 P 1 2 2 x
89 elfzle2 x 1 P 1 2 x P 1 2
90 89 adantl φ x 1 P 1 2 x P 1 2
91 86 nnred φ x 1 P 1 2 x
92 prmuz2 P P 2
93 uz2m1nn P 2 P 1
94 29 92 93 3syl φ x 1 P 1 2 P 1
95 94 nnred φ x 1 P 1 2 P 1
96 2re 2
97 96 a1i φ x 1 P 1 2 2
98 2pos 0 < 2
99 98 a1i φ x 1 P 1 2 0 < 2
100 lemuldiv2 x P 1 2 0 < 2 2 x P 1 x P 1 2
101 91 95 97 99 100 syl112anc φ x 1 P 1 2 2 x P 1 x P 1 2
102 90 101 mpbird φ x 1 P 1 2 2 x P 1
103 prmz P P
104 29 103 syl φ x 1 P 1 2 P
105 peano2zm P P 1
106 fznn P 1 2 x 1 P 1 2 x 2 x P 1
107 104 105 106 3syl φ x 1 P 1 2 2 x 1 P 1 2 x 2 x P 1
108 88 102 107 mpbir2and φ x 1 P 1 2 2 x 1 P 1
109 fzm1ndvds P 2 x 1 P 1 ¬ P 2 x
110 31 108 109 syl2anc φ x 1 P 1 2 ¬ P 2 x
111 3 adantr φ x 1 P 1 2 P Q
112 prmrp P Q P gcd Q = 1 P Q
113 29 21 112 syl2anc φ x 1 P 1 2 P gcd Q = 1 P Q
114 111 113 mpbird φ x 1 P 1 2 P gcd Q = 1
115 coprmdvds P Q 2 x P Q 2 x P gcd Q = 1 P 2 x
116 104 23 27 115 syl3anc φ x 1 P 1 2 P Q 2 x P gcd Q = 1 P 2 x
117 114 116 mpan2d φ x 1 P 1 2 P Q 2 x P 2 x
118 110 117 mtod φ x 1 P 1 2 ¬ P Q 2 x
119 dvdsval3 P Q 2 x P Q 2 x Q 2 x mod P = 0
120 31 28 119 syl2anc φ x 1 P 1 2 P Q 2 x Q 2 x mod P = 0
121 118 120 mtbid φ x 1 P 1 2 ¬ Q 2 x mod P = 0
122 4 eqeq1i R = 0 Q 2 x mod P = 0
123 121 122 sylnibr φ x 1 P 1 2 ¬ R = 0
124 94 nnnn0d φ x 1 P 1 2 P 1 0
125 nn0uz 0 = 0
126 124 125 eleqtrdi φ x 1 P 1 2 P 1 0
127 elfzp12 P 1 0 R 0 P 1 R = 0 R 0 + 1 P 1
128 126 127 syl φ x 1 P 1 2 R 0 P 1 R = 0 R 0 + 1 P 1
129 34 128 mpbid φ x 1 P 1 2 R = 0 R 0 + 1 P 1
130 129 ord φ x 1 P 1 2 ¬ R = 0 R 0 + 1 P 1
131 123 130 mpd φ x 1 P 1 2 R 0 + 1 P 1
132 1e0p1 1 = 0 + 1
133 132 oveq1i 1 P 1 = 0 + 1 P 1
134 131 133 eleqtrrdi φ x 1 P 1 2 R 1 P 1
135 elfznn R 1 P 1 R
136 134 135 syl φ x 1 P 1 2 R
137 136 nnrpd φ x 1 P 1 2 R +
138 79 137 ltsubrpd φ x 1 P 1 2 P R < P
139 modid P R P + 0 P R P R < P P R mod P = P R
140 80 56 83 138 139 syl22anc φ x 1 P 1 2 P R mod P = P R
141 76 78 140 3eqtr3d φ x 1 P 1 2 R mod P = P R
142 141 adantr φ x 1 P 1 2 R + 1 2 R mod P = P R
143 ax-1cn 1
144 143 a1i φ x 1 P 1 2 R + 1 2 1
145 136 adantr φ x 1 P 1 2 R + 1 2 R
146 37 peano2zd φ x 1 P 1 2 R + 1
147 dvdsval2 2 2 0 R + 1 2 R + 1 R + 1 2
148 15 41 146 147 mp3an12i φ x 1 P 1 2 2 R + 1 R + 1 2
149 148 biimpar φ x 1 P 1 2 R + 1 2 2 R + 1
150 37 adantr φ x 1 P 1 2 R + 1 2 R
151 84 a1i φ x 1 P 1 2 R + 1 2 2
152 1lt2 1 < 2
153 152 a1i φ x 1 P 1 2 R + 1 2 1 < 2
154 ndvdsp1 R 2 1 < 2 2 R ¬ 2 R + 1
155 150 151 153 154 syl3anc φ x 1 P 1 2 R + 1 2 2 R ¬ 2 R + 1
156 149 155 mt2d φ x 1 P 1 2 R + 1 2 ¬ 2 R
157 oexpneg 1 R ¬ 2 R 1 R = 1 R
158 144 145 156 157 syl3anc φ x 1 P 1 2 R + 1 2 1 R = 1 R
159 1exp R 1 R = 1
160 150 159 syl φ x 1 P 1 2 R + 1 2 1 R = 1
161 160 negeqd φ x 1 P 1 2 R + 1 2 1 R = 1
162 158 161 eqtrd φ x 1 P 1 2 R + 1 2 1 R = 1
163 162 oveq1d φ x 1 P 1 2 R + 1 2 1 R R = -1 R
164 38 adantr φ x 1 P 1 2 R + 1 2 R
165 164 mulm1d φ x 1 P 1 2 R + 1 2 -1 R = R
166 163 165 eqtrd φ x 1 P 1 2 R + 1 2 1 R R = R
167 166 oveq1d φ x 1 P 1 2 R + 1 2 1 R R mod P = R mod P
168 68 adantr φ x 1 P 1 2 R + 1 2 P
169 168 164 144 pnpcan2d φ x 1 P 1 2 R + 1 2 P + 1 - R + 1 = P R
170 142 167 169 3eqtr4d φ x 1 P 1 2 R + 1 2 1 R R mod P = P + 1 - R + 1
171 170 oveq1d φ x 1 P 1 2 R + 1 2 1 R R mod P 2 = P + 1 - R + 1 2
172 peano2cn P P + 1
173 168 172 syl φ x 1 P 1 2 R + 1 2 P + 1
174 peano2cn R R + 1
175 164 174 syl φ x 1 P 1 2 R + 1 2 R + 1
176 2cnd φ x 1 P 1 2 R + 1 2 2
177 41 a1i φ x 1 P 1 2 R + 1 2 2 0
178 173 175 176 177 divsubdird φ x 1 P 1 2 R + 1 2 P + 1 - R + 1 2 = P + 1 2 R + 1 2
179 171 178 eqtrd φ x 1 P 1 2 R + 1 2 1 R R mod P 2 = P + 1 2 R + 1 2
180 168 144 176 subadd23d φ x 1 P 1 2 R + 1 2 P - 1 + 2 = P + 2 - 1
181 2m1e1 2 1 = 1
182 181 oveq2i P + 2 - 1 = P + 1
183 180 182 eqtr2di φ x 1 P 1 2 R + 1 2 P + 1 = P - 1 + 2
184 183 oveq1d φ x 1 P 1 2 R + 1 2 P + 1 2 = P - 1 + 2 2
185 94 nncnd φ x 1 P 1 2 P 1
186 185 adantr φ x 1 P 1 2 R + 1 2 P 1
187 186 176 176 177 divdird φ x 1 P 1 2 R + 1 2 P - 1 + 2 2 = P 1 2 + 2 2
188 2div2e1 2 2 = 1
189 188 oveq2i P 1 2 + 2 2 = P 1 2 + 1
190 187 189 eqtrdi φ x 1 P 1 2 R + 1 2 P - 1 + 2 2 = P 1 2 + 1
191 184 190 eqtrd φ x 1 P 1 2 R + 1 2 P + 1 2 = P 1 2 + 1
192 10 adantr φ x 1 P 1 2 R + 1 2 P 1 2
193 192 peano2zd φ x 1 P 1 2 R + 1 2 P 1 2 + 1
194 191 193 eqeltrd φ x 1 P 1 2 R + 1 2 P + 1 2
195 simpr φ x 1 P 1 2 R + 1 2 R + 1 2
196 194 195 zsubcld φ x 1 P 1 2 R + 1 2 P + 1 2 R + 1 2
197 179 196 eqeltrd φ x 1 P 1 2 R + 1 2 1 R R mod P 2
198 zeo R R 2 R + 1 2
199 37 198 syl φ x 1 P 1 2 R 2 R + 1 2
200 67 197 199 mpjaodan φ x 1 P 1 2 1 R R mod P 2
201 m1expcl R 1 R
202 37 201 syl φ x 1 P 1 2 1 R
203 202 37 zmulcld φ x 1 P 1 2 1 R R
204 203 31 zmodcld φ x 1 P 1 2 1 R R mod P 0
205 204 nn0red φ x 1 P 1 2 1 R R mod P
206 fzm1ndvds P R 1 P 1 ¬ P R
207 31 134 206 syl2anc φ x 1 P 1 2 ¬ P R
208 ax-1ne0 1 0
209 divneg2 1 1 1 0 1 1 = 1 1
210 143 143 208 209 mp3an 1 1 = 1 1
211 1div1e1 1 1 = 1
212 211 negeqi 1 1 = 1
213 210 212 eqtr3i 1 1 = 1
214 213 oveq1i 1 1 R = 1 R
215 11 a1i φ x 1 P 1 2 1
216 13 a1i φ x 1 P 1 2 1 0
217 215 216 37 exprecd φ x 1 P 1 2 1 1 R = 1 1 R
218 214 217 eqtr3id φ x 1 P 1 2 1 R = 1 1 R
219 218 oveq2d φ x 1 P 1 2 1 R 1 R = 1 R 1 1 R
220 202 zcnd φ x 1 P 1 2 1 R
221 215 216 37 expne0d φ x 1 P 1 2 1 R 0
222 220 221 recidd φ x 1 P 1 2 1 R 1 1 R = 1
223 219 222 eqtrd φ x 1 P 1 2 1 R 1 R = 1
224 223 oveq1d φ x 1 P 1 2 1 R 1 R R = 1 R
225 220 220 38 mulassd φ x 1 P 1 2 1 R 1 R R = 1 R 1 R R
226 38 mulid2d φ x 1 P 1 2 1 R = R
227 224 225 226 3eqtr3d φ x 1 P 1 2 1 R 1 R R = R
228 227 breq2d φ x 1 P 1 2 P 1 R 1 R R P R
229 207 228 mtbird φ x 1 P 1 2 ¬ P 1 R 1 R R
230 dvdsmultr2 P 1 R 1 R R P 1 R R P 1 R 1 R R
231 104 202 203 230 syl3anc φ x 1 P 1 2 P 1 R R P 1 R 1 R R
232 229 231 mtod φ x 1 P 1 2 ¬ P 1 R R
233 dvdsval3 P 1 R R P 1 R R 1 R R mod P = 0
234 31 203 233 syl2anc φ x 1 P 1 2 P 1 R R 1 R R mod P = 0
235 232 234 mtbid φ x 1 P 1 2 ¬ 1 R R mod P = 0
236 elnn0 1 R R mod P 0 1 R R mod P 1 R R mod P = 0
237 204 236 sylib φ x 1 P 1 2 1 R R mod P 1 R R mod P = 0
238 237 ord φ x 1 P 1 2 ¬ 1 R R mod P 1 R R mod P = 0
239 235 238 mt3d φ x 1 P 1 2 1 R R mod P
240 239 nngt0d φ x 1 P 1 2 0 < 1 R R mod P
241 205 97 240 99 divgt0d φ x 1 P 1 2 0 < 1 R R mod P 2
242 elnnz 1 R R mod P 2 1 R R mod P 2 0 < 1 R R mod P 2
243 200 241 242 sylanbrc φ x 1 P 1 2 1 R R mod P 2
244 243 nnge1d φ x 1 P 1 2 1 1 R R mod P 2
245 zmodfz 1 R R P 1 R R mod P 0 P 1
246 203 31 245 syl2anc φ x 1 P 1 2 1 R R mod P 0 P 1
247 elfzle2 1 R R mod P 0 P 1 1 R R mod P P 1
248 246 247 syl φ x 1 P 1 2 1 R R mod P P 1
249 lediv1 1 R R mod P P 1 2 0 < 2 1 R R mod P P 1 1 R R mod P 2 P 1 2
250 205 95 97 99 249 syl112anc φ x 1 P 1 2 1 R R mod P P 1 1 R R mod P 2 P 1 2
251 248 250 mpbid φ x 1 P 1 2 1 R R mod P 2 P 1 2
252 6 10 200 244 251 elfzd φ x 1 P 1 2 1 R R mod P 2 1 P 1 2
253 252 5 fmptd φ M : 1 P 1 2 1 P 1 2