Metamath Proof Explorer


Theorem ostth2lem2

Description: Lemma for ostth2 . (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q Q = fld 𝑠
qabsabv.a A = AbsVal Q
padic.j J = q x if x = 0 0 q q pCnt x
ostth.k K = x if x = 0 0 1
ostth.1 φ F A
ostth2.2 φ N 2
ostth2.3 φ 1 < F N
ostth2.4 R = log F N log N
ostth2.5 φ M 2
ostth2.6 S = log F M log M
ostth2.7 T = if F M 1 1 F M
Assertion ostth2lem2 φ X 0 Y 0 M X 1 F Y M X T X

Proof

Step Hyp Ref Expression
1 qrng.q Q = fld 𝑠
2 qabsabv.a A = AbsVal Q
3 padic.j J = q x if x = 0 0 q q pCnt x
4 ostth.k K = x if x = 0 0 1
5 ostth.1 φ F A
6 ostth2.2 φ N 2
7 ostth2.3 φ 1 < F N
8 ostth2.4 R = log F N log N
9 ostth2.5 φ M 2
10 ostth2.6 S = log F M log M
11 ostth2.7 T = if F M 1 1 F M
12 oveq2 x = 0 M x = M 0
13 12 oveq1d x = 0 M x 1 = M 0 1
14 13 oveq2d x = 0 0 M x 1 = 0 M 0 1
15 oveq2 x = 0 M x = M 0
16 oveq2 x = 0 T x = T 0
17 15 16 oveq12d x = 0 M x T x = M 0 T 0
18 17 breq2d x = 0 F k M x T x F k M 0 T 0
19 14 18 raleqbidv x = 0 k 0 M x 1 F k M x T x k 0 M 0 1 F k M 0 T 0
20 19 imbi2d x = 0 φ k 0 M x 1 F k M x T x φ k 0 M 0 1 F k M 0 T 0
21 oveq2 x = n M x = M n
22 21 oveq1d x = n M x 1 = M n 1
23 22 oveq2d x = n 0 M x 1 = 0 M n 1
24 oveq2 x = n M x = M n
25 oveq2 x = n T x = T n
26 24 25 oveq12d x = n M x T x = M n T n
27 26 breq2d x = n F k M x T x F k M n T n
28 23 27 raleqbidv x = n k 0 M x 1 F k M x T x k 0 M n 1 F k M n T n
29 28 imbi2d x = n φ k 0 M x 1 F k M x T x φ k 0 M n 1 F k M n T n
30 oveq2 x = n + 1 M x = M n + 1
31 30 oveq1d x = n + 1 M x 1 = M n + 1 1
32 31 oveq2d x = n + 1 0 M x 1 = 0 M n + 1 1
33 oveq2 x = n + 1 M x = M n + 1
34 oveq2 x = n + 1 T x = T n + 1
35 33 34 oveq12d x = n + 1 M x T x = M n + 1 T n + 1
36 35 breq2d x = n + 1 F k M x T x F k M n + 1 T n + 1
37 32 36 raleqbidv x = n + 1 k 0 M x 1 F k M x T x k 0 M n + 1 1 F k M n + 1 T n + 1
38 37 imbi2d x = n + 1 φ k 0 M x 1 F k M x T x φ k 0 M n + 1 1 F k M n + 1 T n + 1
39 oveq2 x = X M x = M X
40 39 oveq1d x = X M x 1 = M X 1
41 40 oveq2d x = X 0 M x 1 = 0 M X 1
42 oveq2 x = X M x = M X
43 oveq2 x = X T x = T X
44 42 43 oveq12d x = X M x T x = M X T X
45 44 breq2d x = X F k M x T x F k M X T X
46 41 45 raleqbidv x = X k 0 M x 1 F k M x T x k 0 M X 1 F k M X T X
47 46 imbi2d x = X φ k 0 M x 1 F k M x T x φ k 0 M X 1 F k M X T X
48 eluz2nn M 2 M
49 9 48 syl φ M
50 49 nncnd φ M
51 50 exp0d φ M 0 = 1
52 51 oveq1d φ M 0 1 = 1 1
53 1m1e0 1 1 = 0
54 52 53 eqtrdi φ M 0 1 = 0
55 54 oveq2d φ 0 M 0 1 = 0 0
56 55 eleq2d φ k 0 M 0 1 k 0 0
57 0le0 0 0
58 57 a1i φ 0 0
59 1 qrng0 0 = 0 Q
60 2 59 abv0 F A F 0 = 0
61 5 60 syl φ F 0 = 0
62 50 mul01d φ M 0 = 0
63 62 oveq1d φ M 0 T 0 = 0 T 0
64 1re 1
65 nnq M M
66 49 65 syl φ M
67 1 qrngbas = Base Q
68 2 67 abvcl F A M F M
69 5 66 68 syl2anc φ F M
70 ifcl 1 F M if F M 1 1 F M
71 64 69 70 sylancr φ if F M 1 1 F M
72 11 71 eqeltrid φ T
73 72 recnd φ T
74 0nn0 0 0
75 expcl T 0 0 T 0
76 73 74 75 sylancl φ T 0
77 76 mul02d φ 0 T 0 = 0
78 63 77 eqtrd φ M 0 T 0 = 0
79 58 61 78 3brtr4d φ F 0 M 0 T 0
80 elfz1eq k 0 0 k = 0
81 80 fveq2d k 0 0 F k = F 0
82 81 breq1d k 0 0 F k M 0 T 0 F 0 M 0 T 0
83 79 82 syl5ibrcom φ k 0 0 F k M 0 T 0
84 56 83 sylbid φ k 0 M 0 1 F k M 0 T 0
85 84 ralrimiv φ k 0 M 0 1 F k M 0 T 0
86 fveq2 k = j F k = F j
87 86 breq1d k = j F k M n T n F j M n T n
88 87 cbvralvw k 0 M n 1 F k M n T n j 0 M n 1 F j M n T n
89 5 ad2antrr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F A
90 elfzelz k 0 M n + 1 1 k
91 90 ad2antrl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k
92 zq k k
93 91 92 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k
94 2 67 abvcl F A k F k
95 89 93 94 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k
96 49 ad2antrr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M
97 simplr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n 0
98 96 97 nnexpcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n
99 91 98 zmodcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n 0
100 99 nn0zd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n
101 zq k mod M n k mod M n
102 100 101 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n
103 2 67 abvcl F A k mod M n F k mod M n
104 89 102 103 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n
105 96 65 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M
106 89 105 68 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M
107 106 97 reexpcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n
108 91 zred φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k
109 108 98 nndivred φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n
110 109 flcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n
111 zq k M n k M n
112 110 111 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n
113 2 67 abvcl F A k M n F k M n
114 89 112 113 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n
115 107 114 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n F k M n
116 104 115 readdcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + F M n F k M n
117 96 nnred φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M
118 nn0p1nn n 0 n + 1
119 118 ad2antlr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n + 1
120 119 nnred φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n + 1
121 117 120 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1
122 72 ad2antrr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n T
123 peano2nn0 n 0 n + 1 0
124 123 ad2antlr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n + 1 0
125 122 124 reexpcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n T n + 1
126 121 125 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 T n + 1
127 nnq M n M n
128 98 127 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n
129 qmulcl M n k M n M n k M n
130 128 112 129 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n k M n
131 qex V
132 cnfldadd + = + fld
133 1 132 ressplusg V + = + Q
134 131 133 ax-mp + = + Q
135 2 67 134 abvtri F A k mod M n M n k M n F k mod M n + M n k M n F k mod M n + F M n k M n
136 89 102 130 135 syl3anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + M n k M n F k mod M n + F M n k M n
137 98 nnrpd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n +
138 modval k M n + k mod M n = k M n k M n
139 108 137 138 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n = k M n k M n
140 139 oveq1d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n + M n k M n = k - M n k M n + M n k M n
141 108 recnd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k
142 qcn M n k M n M n k M n
143 130 142 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n k M n
144 141 143 npcand φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k - M n k M n + M n k M n = k
145 140 144 eqtrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n + M n k M n = k
146 145 fveq2d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + M n k M n = F k
147 cnfldmul × = fld
148 1 147 ressmulr V × = Q
149 131 148 ax-mp × = Q
150 2 67 149 abvmul F A M n k M n F M n k M n = F M n F k M n
151 89 128 112 150 syl3anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n k M n = F M n F k M n
152 1 2 qabvexp F A M n 0 F M n = F M n
153 89 105 97 152 syl3anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n = F M n
154 153 oveq1d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n F k M n = F M n F k M n
155 151 154 eqtrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n k M n = F M n F k M n
156 155 oveq2d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + F M n k M n = F k mod M n + F M n F k M n
157 136 146 156 3brtr3d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k F k mod M n + F M n F k M n
158 122 97 reexpcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n T n
159 121 158 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 T n
160 nn0re n 0 n
161 160 ad2antlr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n
162 117 161 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n
163 162 158 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n T n
164 117 158 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M T n
165 fveq2 j = k mod M n F j = F k mod M n
166 165 breq1d j = k mod M n F j M n T n F k mod M n M n T n
167 simprr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n j 0 M n 1 F j M n T n
168 zmodfz k M n k mod M n 0 M n 1
169 91 98 168 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k mod M n 0 M n 1
170 166 167 169 rspcdva φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n M n T n
171 117 107 remulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M F M n
172 107 recnd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n
173 114 recnd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n
174 172 173 mulcomd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n F k M n = F k M n F M n
175 2 67 abvge0 F A M 0 F M
176 89 105 175 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 F M
177 106 97 176 expge0d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 F M n
178 110 zred φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n
179 elfzle1 k 0 M n + 1 1 0 k
180 179 ad2antrl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 k
181 98 nnred φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n
182 98 nngt0d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 < M n
183 divge0 k 0 k M n 0 < M n 0 k M n
184 108 180 181 182 183 syl22anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 k M n
185 flge0nn0 k M n 0 k M n k M n 0
186 109 184 185 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n 0
187 1 2 qabvle F A k M n 0 F k M n k M n
188 89 186 187 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n k M n
189 simprl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k 0 M n + 1 1
190 0z 0
191 96 124 nnexpcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1
192 191 nnzd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1
193 elfzm11 0 M n + 1 k 0 M n + 1 1 k 0 k k < M n + 1
194 190 192 193 sylancr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k 0 M n + 1 1 k 0 k k < M n + 1
195 189 194 mpbid φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k 0 k k < M n + 1
196 195 simp3d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k < M n + 1
197 96 nncnd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M
198 197 97 expp1d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 = M n M
199 196 198 breqtrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k < M n M
200 ltdivmul k M M n 0 < M n k M n < M k < M n M
201 108 117 181 182 200 syl112anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n < M k < M n M
202 199 201 mpbird φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n < M
203 96 nnzd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M
204 fllt k M n M k M n < M k M n < M
205 109 203 204 syl2anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n < M k M n < M
206 202 205 mpbid φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n < M
207 178 117 206 ltled φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n k M n M
208 114 178 117 188 207 letrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n M
209 114 117 107 177 208 lemul1ad φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n F M n M F M n
210 174 209 eqbrtrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n F k M n M F M n
211 96 nnnn0d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M 0
212 211 nn0ge0d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 M
213 max1 F M 1 F M if F M 1 1 F M
214 106 64 213 sylancl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M if F M 1 1 F M
215 214 11 breqtrrdi φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M T
216 leexp1a F M T n 0 0 F M F M T F M n T n
217 106 122 97 176 215 216 syl32anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n T n
218 107 158 117 212 217 lemul2ad φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M F M n M T n
219 115 171 164 210 218 letrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F M n F k M n M T n
220 104 115 163 164 170 219 le2addd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + F M n F k M n M n T n + M T n
221 nn0cn n 0 n
222 221 ad2antlr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n
223 1cnd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 1
224 197 222 223 adddid φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 = M n + M 1
225 197 mulid1d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M 1 = M
226 225 oveq2d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + M 1 = M n + M
227 224 226 eqtrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 = M n + M
228 227 oveq1d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 T n = M n + M T n
229 197 222 mulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n
230 158 recnd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n T n
231 229 197 230 adddird φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + M T n = M n T n + M T n
232 228 231 eqtrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 T n = M n T n + M T n
233 220 232 breqtrrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + F M n F k M n M n + 1 T n
234 max2 F M 1 1 if F M 1 1 F M
235 106 64 234 sylancl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 1 if F M 1 1 F M
236 235 11 breqtrrdi φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 1 T
237 nn0z n 0 n
238 237 ad2antlr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n
239 uzid n n n
240 238 239 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n n
241 peano2uz n n n + 1 n
242 240 241 syl φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n n + 1 n
243 122 236 242 leexp2ad φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n T n T n + 1
244 96 119 nnmulcld φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1
245 244 nngt0d φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n 0 < M n + 1
246 lemul2 T n T n + 1 M n + 1 0 < M n + 1 T n T n + 1 M n + 1 T n M n + 1 T n + 1
247 158 125 121 245 246 syl112anc φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n T n T n + 1 M n + 1 T n M n + 1 T n + 1
248 243 247 mpbid φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n M n + 1 T n M n + 1 T n + 1
249 116 159 126 233 248 letrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k mod M n + F M n F k M n M n + 1 T n + 1
250 95 116 126 157 249 letrd φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n + 1 T n + 1
251 250 expr φ n 0 k 0 M n + 1 1 j 0 M n 1 F j M n T n F k M n + 1 T n + 1
252 251 ralrimdva φ n 0 j 0 M n 1 F j M n T n k 0 M n + 1 1 F k M n + 1 T n + 1
253 88 252 syl5bi φ n 0 k 0 M n 1 F k M n T n k 0 M n + 1 1 F k M n + 1 T n + 1
254 253 expcom n 0 φ k 0 M n 1 F k M n T n k 0 M n + 1 1 F k M n + 1 T n + 1
255 254 a2d n 0 φ k 0 M n 1 F k M n T n φ k 0 M n + 1 1 F k M n + 1 T n + 1
256 20 29 38 47 85 255 nn0ind X 0 φ k 0 M X 1 F k M X T X
257 256 impcom φ X 0 k 0 M X 1 F k M X T X
258 fveq2 k = Y F k = F Y
259 258 breq1d k = Y F k M X T X F Y M X T X
260 259 rspccv k 0 M X 1 F k M X T X Y 0 M X 1 F Y M X T X
261 257 260 syl φ X 0 Y 0 M X 1 F Y M X T X
262 261 3impia φ X 0 Y 0 M X 1 F Y M X T X