Proof of Theorem fourierdlem114
Step | Hyp | Ref
| Expression |
1 | | fourierdlem114.f |
. 2
|
2 | | fourierdlem114.t |
. 2
|
3 | | fourierdlem114.per |
. 2
|
4 | | fourierdlem114.x |
. 2
|
5 | | fourierdlem114.l |
. 2
lim |
6 | | fourierdlem114.r |
. 2
lim |
7 | | fourierdlem114.p |
. 2
..^ |
8 | | fourierdlem114.m |
. . 3
|
9 | | 2z 11409 |
. . . . . 6
|
10 | 9 | a1i 11 |
. . . . 5
|
11 | | fourierdlem114.h |
. . . . . . . 8
|
12 | | tpfi 8236 |
. . . . . . . . . 10
|
13 | 12 | a1i 11 |
. . . . . . . . 9
|
14 | | pire 24210 |
. . . . . . . . . . . . . . 15
|
15 | 14 | renegcli 10342 |
. . . . . . . . . . . . . 14
|
16 | 15 | rexri 10097 |
. . . . . . . . . . . . 13
|
17 | 14 | rexri 10097 |
. . . . . . . . . . . . 13
|
18 | | negpilt0 39492 |
. . . . . . . . . . . . . . 15
|
19 | | pipos 24212 |
. . . . . . . . . . . . . . 15
|
20 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
|
21 | 15, 20, 14 | lttri 10163 |
. . . . . . . . . . . . . . 15
|
22 | 18, 19, 21 | mp2an 708 |
. . . . . . . . . . . . . 14
|
23 | 15, 14, 22 | ltleii 10160 |
. . . . . . . . . . . . 13
|
24 | | prunioo 12301 |
. . . . . . . . . . . . 13
|
25 | 16, 17, 23, 24 | mp3an 1424 |
. . . . . . . . . . . 12
|
26 | 25 | difeq1i 3724 |
. . . . . . . . . . 11
|
27 | | difundir 3880 |
. . . . . . . . . . 11
|
28 | 26, 27 | eqtr3i 2646 |
. . . . . . . . . 10
|
29 | | fourierdlem114.dmdv |
. . . . . . . . . . 11
|
30 | | prfi 8235 |
. . . . . . . . . . . 12
|
31 | | diffi 8192 |
. . . . . . . . . . . 12
|
32 | 30, 31 | mp1i 13 |
. . . . . . . . . . 11
|
33 | | unfi 8227 |
. . . . . . . . . . 11
|
34 | 29, 32, 33 | syl2anc 693 |
. . . . . . . . . 10
|
35 | 28, 34 | syl5eqel 2705 |
. . . . . . . . 9
|
36 | | unfi 8227 |
. . . . . . . . 9
|
37 | 13, 35, 36 | syl2anc 693 |
. . . . . . . 8
|
38 | 11, 37 | syl5eqel 2705 |
. . . . . . 7
|
39 | | hashcl 13147 |
. . . . . . 7
|
40 | 38, 39 | syl 17 |
. . . . . 6
|
41 | 40 | nn0zd 11480 |
. . . . 5
|
42 | 15, 22 | ltneii 10150 |
. . . . . . 7
|
43 | | hashprg 13182 |
. . . . . . . 8
|
44 | 15, 14, 43 | mp2an 708 |
. . . . . . 7
|
45 | 42, 44 | mpbi 220 |
. . . . . 6
|
46 | 12 | elexi 3213 |
. . . . . . . . . 10
|
47 | | ovex 6678 |
. . . . . . . . . . 11
|
48 | | difexg 4808 |
. . . . . . . . . . 11
|
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
|
50 | 46, 49 | unex 6956 |
. . . . . . . . 9
|
51 | 11, 50 | eqeltri 2697 |
. . . . . . . 8
|
52 | | negex 10279 |
. . . . . . . . . . 11
|
53 | 52 | tpid1 4303 |
. . . . . . . . . 10
|
54 | 14 | elexi 3213 |
. . . . . . . . . . 11
|
55 | 54 | tpid2 4304 |
. . . . . . . . . 10
|
56 | | prssi 4353 |
. . . . . . . . . 10
|
57 | 53, 55, 56 | mp2an 708 |
. . . . . . . . 9
|
58 | | ssun1 3776 |
. . . . . . . . . 10
|
59 | 58, 11 | sseqtr4i 3638 |
. . . . . . . . 9
|
60 | 57, 59 | sstri 3612 |
. . . . . . . 8
|
61 | | hashss 13197 |
. . . . . . . 8
|
62 | 51, 60, 61 | mp2an 708 |
. . . . . . 7
|
63 | 62 | a1i 11 |
. . . . . 6
|
64 | 45, 63 | syl5eqbrr 4689 |
. . . . 5
|
65 | | eluz2 11693 |
. . . . 5
|
66 | 10, 41, 64, 65 | syl3anbrc 1246 |
. . . 4
|
67 | | uz2m1nn 11763 |
. . . 4
|
68 | 66, 67 | syl 17 |
. . 3
|
69 | 8, 68 | syl5eqel 2705 |
. 2
|
70 | 15 | a1i 11 |
. . . . . . . . . . 11
|
71 | 14 | a1i 11 |
. . . . . . . . . . 11
|
72 | | negpitopissre 24286 |
. . . . . . . . . . . 12
|
73 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
|
74 | | picn 24211 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | 2timesi 11147 |
. . . . . . . . . . . . . . 15
|
76 | 74, 74 | subnegi 10360 |
. . . . . . . . . . . . . . 15
|
77 | 75, 2, 76 | 3eqtr4i 2654 |
. . . . . . . . . . . . . 14
|
78 | | fourierdlem114.e |
. . . . . . . . . . . . . 14
|
79 | 70, 71, 73, 77, 78 | fourierdlem4 40328 |
. . . . . . . . . . . . 13
|
80 | 79, 4 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
81 | 72, 80 | sseldi 3601 |
. . . . . . . . . . 11
|
82 | 70, 71, 81 | 3jca 1242 |
. . . . . . . . . 10
|
83 | | fvex 6201 |
. . . . . . . . . . 11
|
84 | 52, 54, 83 | tpss 4368 |
. . . . . . . . . 10
|
85 | 82, 84 | sylib 208 |
. . . . . . . . 9
|
86 | | iccssre 12255 |
. . . . . . . . . . 11
|
87 | 15, 14, 86 | mp2an 708 |
. . . . . . . . . 10
|
88 | | ssdifss 3741 |
. . . . . . . . . 10
|
89 | 87, 88 | mp1i 13 |
. . . . . . . . 9
|
90 | 85, 89 | unssd 3789 |
. . . . . . . 8
|
91 | 11, 90 | syl5eqss 3649 |
. . . . . . 7
|
92 | | fourierdlem114.q |
. . . . . . 7
|
93 | 38, 91, 92, 8 | fourierdlem36 40360 |
. . . . . 6
|
94 | | isof1o 6573 |
. . . . . 6
|
95 | | f1of 6137 |
. . . . . 6
|
96 | 93, 94, 95 | 3syl 18 |
. . . . 5
|
97 | 96, 91 | fssd 6057 |
. . . 4
|
98 | | reex 10027 |
. . . . 5
|
99 | | ovex 6678 |
. . . . 5
|
100 | 98, 99 | elmap 7886 |
. . . 4
|
101 | 97, 100 | sylibr 224 |
. . 3
|
102 | | fveq2 6191 |
. . . . . . . . . . 11
|
103 | 102 | adantl 482 |
. . . . . . . . . 10
|
104 | 97 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
105 | 104 | leidd 10594 |
. . . . . . . . . . 11
|
106 | 105 | adantr 481 |
. . . . . . . . . 10
|
107 | 103, 106 | eqbrtrd 4675 |
. . . . . . . . 9
|
108 | | elfzelz 12342 |
. . . . . . . . . . . . 13
|
109 | 108 | zred 11482 |
. . . . . . . . . . . 12
|
110 | 109 | ad2antlr 763 |
. . . . . . . . . . 11
|
111 | | elfzle1 12344 |
. . . . . . . . . . . 12
|
112 | 111 | ad2antlr 763 |
. . . . . . . . . . 11
|
113 | | neqne 2802 |
. . . . . . . . . . . . 13
|
114 | 113 | necomd 2849 |
. . . . . . . . . . . 12
|
115 | 114 | adantl 482 |
. . . . . . . . . . 11
|
116 | 110, 112,
115 | ne0gt0d 10174 |
. . . . . . . . . 10
|
117 | | nnssnn0 11295 |
. . . . . . . . . . . . . . . . 17
|
118 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . 17
|
119 | 117, 118 | sseqtri 3637 |
. . . . . . . . . . . . . . . 16
|
120 | 119, 69 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
121 | | eluzfz1 12348 |
. . . . . . . . . . . . . . 15
|
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . 14
|
123 | 96, 122 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
124 | 91, 123 | sseldd 3604 |
. . . . . . . . . . . 12
|
125 | 124 | ad2antrr 762 |
. . . . . . . . . . 11
|
126 | 104 | adantr 481 |
. . . . . . . . . . 11
|
127 | | simpr 477 |
. . . . . . . . . . . 12
|
128 | 93 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
129 | 122 | anim1i 592 |
. . . . . . . . . . . . . 14
|
130 | 129 | adantr 481 |
. . . . . . . . . . . . 13
|
131 | | isorel 6576 |
. . . . . . . . . . . . 13
|
132 | 128, 130,
131 | syl2anc 693 |
. . . . . . . . . . . 12
|
133 | 127, 132 | mpbid 222 |
. . . . . . . . . . 11
|
134 | 125, 126,
133 | ltled 10185 |
. . . . . . . . . 10
|
135 | 116, 134 | syldan 487 |
. . . . . . . . 9
|
136 | 107, 135 | pm2.61dan 832 |
. . . . . . . 8
|
137 | 136 | adantr 481 |
. . . . . . 7
|
138 | | simpr 477 |
. . . . . . 7
|
139 | 137, 138 | breqtrd 4679 |
. . . . . 6
|
140 | 70 | rexrd 10089 |
. . . . . . . 8
|
141 | 71 | rexrd 10089 |
. . . . . . . 8
|
142 | | lbicc2 12288 |
. . . . . . . . . . . . . 14
|
143 | 16, 17, 23, 142 | mp3an 1424 |
. . . . . . . . . . . . 13
|
144 | 143 | a1i 11 |
. . . . . . . . . . . 12
|
145 | | ubicc2 12289 |
. . . . . . . . . . . . . 14
|
146 | 16, 17, 23, 145 | mp3an 1424 |
. . . . . . . . . . . . 13
|
147 | 146 | a1i 11 |
. . . . . . . . . . . 12
|
148 | | iocssicc 12261 |
. . . . . . . . . . . . 13
|
149 | 148, 80 | sseldi 3601 |
. . . . . . . . . . . 12
|
150 | | tpssi 4369 |
. . . . . . . . . . . 12
|
151 | 144, 147,
149, 150 | syl3anc 1326 |
. . . . . . . . . . 11
|
152 | | difssd 3738 |
. . . . . . . . . . 11
|
153 | 151, 152 | unssd 3789 |
. . . . . . . . . 10
|
154 | 11, 153 | syl5eqss 3649 |
. . . . . . . . 9
|
155 | 154, 123 | sseldd 3604 |
. . . . . . . 8
|
156 | | iccgelb 12230 |
. . . . . . . 8
|
157 | 140, 141,
155, 156 | syl3anc 1326 |
. . . . . . 7
|
158 | 157 | ad2antrr 762 |
. . . . . 6
|
159 | 124 | ad2antrr 762 |
. . . . . . 7
|
160 | 15 | a1i 11 |
. . . . . . 7
|
161 | 159, 160 | letri3d 10179 |
. . . . . 6
|
162 | 139, 158,
161 | mpbir2and 957 |
. . . . 5
|
163 | 59, 53 | sselii 3600 |
. . . . . . 7
|
164 | | f1ofo 6144 |
. . . . . . . . 9
|
165 | 94, 164 | syl 17 |
. . . . . . . 8
|
166 | | forn 6118 |
. . . . . . . 8
|
167 | 93, 165, 166 | 3syl 18 |
. . . . . . 7
|
168 | 163, 167 | syl5eleqr 2708 |
. . . . . 6
|
169 | | ffn 6045 |
. . . . . . 7
|
170 | | fvelrnb 6243 |
. . . . . . 7
|
171 | 96, 169, 170 | 3syl 18 |
. . . . . 6
|
172 | 168, 171 | mpbid 222 |
. . . . 5
|
173 | 162, 172 | r19.29a 3078 |
. . . 4
|
174 | 59, 55 | sselii 3600 |
. . . . . . 7
|
175 | 174, 167 | syl5eleqr 2708 |
. . . . . 6
|
176 | | fvelrnb 6243 |
. . . . . . 7
|
177 | 96, 169, 176 | 3syl 18 |
. . . . . 6
|
178 | 175, 177 | mpbid 222 |
. . . . 5
|
179 | 96, 154 | fssd 6057 |
. . . . . . . . . 10
|
180 | | eluzfz2 12349 |
. . . . . . . . . . 11
|
181 | 120, 180 | syl 17 |
. . . . . . . . . 10
|
182 | 179, 181 | ffvelrnd 6360 |
. . . . . . . . 9
|
183 | | iccleub 12229 |
. . . . . . . . 9
|
184 | 140, 141,
182, 183 | syl3anc 1326 |
. . . . . . . 8
|
185 | 184 | 3ad2ant1 1082 |
. . . . . . 7
|
186 | | id 22 |
. . . . . . . . . 10
|
187 | 186 | eqcomd 2628 |
. . . . . . . . 9
|
188 | 187 | 3ad2ant3 1084 |
. . . . . . . 8
|
189 | 105 | adantr 481 |
. . . . . . . . . . 11
|
190 | | fveq2 6191 |
. . . . . . . . . . . 12
|
191 | 190 | adantl 482 |
. . . . . . . . . . 11
|
192 | 189, 191 | breqtrd 4679 |
. . . . . . . . . 10
|
193 | 109 | ad2antlr 763 |
. . . . . . . . . . . 12
|
194 | | elfzel2 12340 |
. . . . . . . . . . . . . 14
|
195 | 194 | zred 11482 |
. . . . . . . . . . . . 13
|
196 | 195 | ad2antlr 763 |
. . . . . . . . . . . 12
|
197 | | elfzle2 12345 |
. . . . . . . . . . . . 13
|
198 | 197 | ad2antlr 763 |
. . . . . . . . . . . 12
|
199 | | neqne 2802 |
. . . . . . . . . . . . . 14
|
200 | 199 | necomd 2849 |
. . . . . . . . . . . . 13
|
201 | 200 | adantl 482 |
. . . . . . . . . . . 12
|
202 | 193, 196,
198, 201 | leneltd 10191 |
. . . . . . . . . . 11
|
203 | 104 | adantr 481 |
. . . . . . . . . . . 12
|
204 | 87, 182 | sseldi 3601 |
. . . . . . . . . . . . 13
|
205 | 204 | ad2antrr 762 |
. . . . . . . . . . . 12
|
206 | | simpr 477 |
. . . . . . . . . . . . 13
|
207 | 93 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
208 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
209 | 181 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
210 | 208, 209 | jca 554 |
. . . . . . . . . . . . . . 15
|
211 | 210 | adantr 481 |
. . . . . . . . . . . . . 14
|
212 | | isorel 6576 |
. . . . . . . . . . . . . 14
|
213 | 207, 211,
212 | syl2anc 693 |
. . . . . . . . . . . . 13
|
214 | 206, 213 | mpbid 222 |
. . . . . . . . . . . 12
|
215 | 203, 205,
214 | ltled 10185 |
. . . . . . . . . . 11
|
216 | 202, 215 | syldan 487 |
. . . . . . . . . 10
|
217 | 192, 216 | pm2.61dan 832 |
. . . . . . . . 9
|
218 | 217 | 3adant3 1081 |
. . . . . . . 8
|
219 | 188, 218 | eqbrtrd 4675 |
. . . . . . 7
|
220 | 204 | 3ad2ant1 1082 |
. . . . . . . 8
|
221 | 14 | a1i 11 |
. . . . . . . 8
|
222 | 220, 221 | letri3d 10179 |
. . . . . . 7
|
223 | 185, 219,
222 | mpbir2and 957 |
. . . . . 6
|
224 | 223 | rexlimdv3a 3033 |
. . . . 5
|
225 | 178, 224 | mpd 15 |
. . . 4
|
226 | | elfzoelz 12470 |
. . . . . . . . 9
..^
|
227 | 226 | zred 11482 |
. . . . . . . 8
..^
|
228 | 227 | ltp1d 10954 |
. . . . . . 7
..^
|
229 | 228 | adantl 482 |
. . . . . 6
..^ |
230 | | elfzofz 12485 |
. . . . . . . 8
..^
|
231 | | fzofzp1 12565 |
. . . . . . . 8
..^
|
232 | 230, 231 | jca 554 |
. . . . . . 7
..^
|
233 | | isorel 6576 |
. . . . . . 7
|
234 | 93, 232, 233 | syl2an 494 |
. . . . . 6
..^ |
235 | 229, 234 | mpbid 222 |
. . . . 5
..^ |
236 | 235 | ralrimiva 2966 |
. . . 4
..^ |
237 | 173, 225,
236 | jca31 557 |
. . 3
..^ |
238 | 7 | fourierdlem2 40326 |
. . . 4
..^ |
239 | 69, 238 | syl 17 |
. . 3
..^ |
240 | 101, 237,
239 | mpbir2and 957 |
. 2
|
241 | | fourierdlem114.g |
. . . . 5
|
242 | 241 | reseq1i 5392 |
. . . 4
|
243 | 16 | a1i 11 |
. . . . . 6
..^ |
244 | 17 | a1i 11 |
. . . . . 6
..^ |
245 | 179 | adantr 481 |
. . . . . 6
..^ |
246 | | simpr 477 |
. . . . . 6
..^ ..^ |
247 | 243, 244,
245, 246 | fourierdlem27 40351 |
. . . . 5
..^ |
248 | 247 | resabs1d 5428 |
. . . 4
..^ |
249 | 242, 248 | syl5req 2669 |
. . 3
..^
|
250 | | fourierdlem114.gcn |
. . . 4
|
251 | 250, 7, 69, 240, 11, 167 | fourierdlem38 40362 |
. . 3
..^ |
252 | 249, 251 | eqeltrd 2701 |
. 2
..^ |
253 | 249 | oveq1d 6665 |
. . 3
..^ lim
lim |
254 | 250 | adantr 481 |
. . . . 5
..^ |
255 | | fourierdlem114.rlim |
. . . . . 6
lim
|
256 | 255 | adantlr 751 |
. . . . 5
..^
lim
|
257 | | fourierdlem114.llim |
. . . . . 6
lim |
258 | 257 | adantlr 751 |
. . . . 5
..^ lim |
259 | 93 | adantr 481 |
. . . . 5
..^ |
260 | 259, 94, 95 | 3syl 18 |
. . . . 5
..^ |
261 | 81 | adantr 481 |
. . . . 5
..^ |
262 | 259, 165,
166 | 3syl 18 |
. . . . 5
..^
|
263 | 254, 256,
258, 259, 260, 246, 235, 247, 261, 11, 262 | fourierdlem46 40369 |
. . . 4
..^
lim lim |
264 | 263 | simpld 475 |
. . 3
..^ lim |
265 | 253, 264 | eqnetrd 2861 |
. 2
..^ lim |
266 | 249 | oveq1d 6665 |
. . 3
..^ lim
lim |
267 | 263 | simprd 479 |
. . 3
..^ lim |
268 | 266, 267 | eqnetrd 2861 |
. 2
..^ lim |
269 | | fourierdlem114.a |
. 2
|
270 | | fourierdlem114.b |
. 2
|
271 | | fourierdlem114.s |
. 2
|
272 | 83 | tpid3 4307 |
. . . . 5
|
273 | | elun1 3780 |
. . . . 5
|
274 | 272, 273 | mp1i 13 |
. . . 4
|
275 | 274, 11 | syl6eleqr 2712 |
. . 3
|
276 | 275, 167 | eleqtrrd 2704 |
. 2
|
277 | 1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276 | fourierdlem113 40436 |
1
|