Step | Hyp | Ref
| Expression |
1 | | fourierdlem113.f |
. 2
|
2 | | oveq1 6657 |
. . . . . . 7
|
3 | 2 | eqeq1d 2624 |
. . . . . 6
|
4 | | oveq2 6658 |
. . . . . . . 8
|
5 | 4 | fveq2d 6195 |
. . . . . . 7
|
6 | | oveq1 6657 |
. . . . . . . . 9
|
7 | 6 | fveq2d 6195 |
. . . . . . . 8
|
8 | 7 | oveq2d 6666 |
. . . . . . 7
|
9 | 5, 8 | oveq12d 6668 |
. . . . . 6
|
10 | 3, 9 | ifbieq2d 4111 |
. . . . 5
|
11 | 10 | cbvmptv 4750 |
. . . 4
|
12 | | oveq2 6658 |
. . . . . . . 8
|
13 | 12 | oveq1d 6665 |
. . . . . . 7
|
14 | 13 | oveq1d 6665 |
. . . . . 6
|
15 | | oveq1 6657 |
. . . . . . . . 9
|
16 | 15 | oveq1d 6665 |
. . . . . . . 8
|
17 | 16 | fveq2d 6195 |
. . . . . . 7
|
18 | 17 | oveq1d 6665 |
. . . . . 6
|
19 | 14, 18 | ifeq12d 4106 |
. . . . 5
|
20 | 19 | mpteq2dv 4745 |
. . . 4
|
21 | 11, 20 | syl5eq 2668 |
. . 3
|
22 | 21 | cbvmptv 4750 |
. 2
|
23 | | fourierdlem113.p |
. 2
..^ |
24 | | fourierdlem113.m |
. 2
|
25 | | fourierdlem113.q |
. 2
|
26 | | oveq1 6657 |
. . . . . . . 8
|
27 | 26 | eleq1d 2686 |
. . . . . . 7
|
28 | 27 | rexbidv 3052 |
. . . . . 6
|
29 | 28 | cbvrabv 3199 |
. . . . 5
|
30 | 29 | uneq2i 3764 |
. . . 4
|
31 | 30 | fveq2i 6194 |
. . 3
|
32 | 31 | oveq1i 6660 |
. 2
|
33 | | oveq1 6657 |
. . . . . . . . . . . 12
|
34 | 33 | oveq2d 6666 |
. . . . . . . . . . 11
|
35 | 34 | eleq1d 2686 |
. . . . . . . . . 10
|
36 | 35 | cbvrexv 3172 |
. . . . . . . . 9
|
37 | 36 | a1i 11 |
. . . . . . . 8
|
38 | 37 | rabbiia 3185 |
. . . . . . 7
|
39 | 38 | uneq2i 3764 |
. . . . . 6
|
40 | | isoeq5 6571 |
. . . . . 6
|
41 | 39, 40 | ax-mp 5 |
. . . . 5
|
42 | 41 | a1i 11 |
. . . 4
|
43 | 33 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
44 | 43 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
45 | 44 | cbvrexv 3172 |
. . . . . . . . . . . 12
|
46 | 45 | a1i 11 |
. . . . . . . . . . 11
|
47 | 46 | rabbiia 3185 |
. . . . . . . . . 10
|
48 | 47 | uneq2i 3764 |
. . . . . . . . 9
|
49 | 48 | fveq2i 6194 |
. . . . . . . 8
|
50 | 49 | oveq1i 6660 |
. . . . . . 7
|
51 | 50 | oveq2i 6661 |
. . . . . 6
|
52 | | isoeq4 6570 |
. . . . . 6
|
53 | 51, 52 | ax-mp 5 |
. . . . 5
|
54 | 53 | a1i 11 |
. . . 4
|
55 | | isoeq1 6567 |
. . . 4
|
56 | 42, 54, 55 | 3bitrd 294 |
. . 3
|
57 | 56 | cbviotav 5857 |
. 2
|
58 | | fourierdlem113.x |
. 2
|
59 | | pire 24210 |
. . . . 5
|
60 | 59 | renegcli 10342 |
. . . 4
|
61 | 60 | a1i 11 |
. . 3
|
62 | 59 | a1i 11 |
. . 3
|
63 | | negpilt0 39492 |
. . . 4
|
64 | 63 | a1i 11 |
. . 3
|
65 | | pipos 24212 |
. . . 4
|
66 | 65 | a1i 11 |
. . 3
|
67 | | picn 24211 |
. . . . 5
|
68 | 67 | 2timesi 11147 |
. . . 4
|
69 | | fourierdlem113.t |
. . . 4
|
70 | 67, 67 | subnegi 10360 |
. . . 4
|
71 | 68, 69, 70 | 3eqtr4i 2654 |
. . 3
|
72 | 23 | fourierdlem2 40326 |
. . . . . . . 8
..^ |
73 | 24, 72 | syl 17 |
. . . . . . 7
..^ |
74 | 25, 73 | mpbid 222 |
. . . . . 6
..^ |
75 | 74 | simpld 475 |
. . . . 5
|
76 | | elmapi 7879 |
. . . . 5
|
77 | 75, 76 | syl 17 |
. . . 4
|
78 | | fzfid 12772 |
. . . 4
|
79 | | rnffi 39356 |
. . . 4
|
80 | 77, 78, 79 | syl2anc 693 |
. . 3
|
81 | 23, 24, 25 | fourierdlem15 40339 |
. . . 4
|
82 | | frn 6053 |
. . . 4
|
83 | 81, 82 | syl 17 |
. . 3
|
84 | 74 | simprd 479 |
. . . . 5
..^ |
85 | 84 | simplrd 793 |
. . . 4
|
86 | | ffun 6048 |
. . . . . 6
|
87 | 81, 86 | syl 17 |
. . . . 5
|
88 | 24 | nnnn0d 11351 |
. . . . . . . 8
|
89 | | nn0uz 11722 |
. . . . . . . 8
|
90 | 88, 89 | syl6eleq 2711 |
. . . . . . 7
|
91 | | eluzfz2 12349 |
. . . . . . 7
|
92 | 90, 91 | syl 17 |
. . . . . 6
|
93 | | fdm 6051 |
. . . . . . . 8
|
94 | 81, 93 | syl 17 |
. . . . . . 7
|
95 | 94 | eqcomd 2628 |
. . . . . 6
|
96 | 92, 95 | eleqtrd 2703 |
. . . . 5
|
97 | | fvelrn 6352 |
. . . . 5
|
98 | 87, 96, 97 | syl2anc 693 |
. . . 4
|
99 | 85, 98 | eqeltrrd 2702 |
. . 3
|
100 | | fourierdlem113.e |
. . 3
|
101 | | fourierdlem113.exq |
. . 3
|
102 | | eqid 2622 |
. . 3
|
103 | | isoeq1 6567 |
. . . . 5
|
104 | 30, 48, 39 | 3eqtr4ri 2655 |
. . . . . 6
|
105 | | isoeq5 6571 |
. . . . . 6
|
106 | 104, 105 | ax-mp 5 |
. . . . 5
|
107 | 103, 106 | syl6bb 276 |
. . . 4
|
108 | 107 | cbviotav 5857 |
. . 3
|
109 | | eqid 2622 |
. . 3
|
110 | 61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109 | fourierdlem51 40374 |
. 2
|
111 | | fourierdlem113.per |
. 2
|
112 | | ax-resscn 9993 |
. . . 4
|
113 | 112 | a1i 11 |
. . 3
..^ |
114 | | ioossre 12235 |
. . . . . . 7
|
115 | 114 | a1i 11 |
. . . . . 6
|
116 | 1, 115 | fssresd 6071 |
. . . . 5
|
117 | 112 | a1i 11 |
. . . . 5
|
118 | 116, 117 | fssd 6057 |
. . . 4
|
119 | 118 | adantr 481 |
. . 3
..^ |
120 | 114 | a1i 11 |
. . 3
..^ |
121 | 1, 117 | fssd 6057 |
. . . . . . 7
|
122 | 121 | adantr 481 |
. . . . . 6
..^ |
123 | | ssid 3624 |
. . . . . . 7
|
124 | 123 | a1i 11 |
. . . . . 6
..^ |
125 | | eqid 2622 |
. . . . . . 7
ℂfld ℂfld |
126 | 125 | tgioo2 22606 |
. . . . . . 7
ℂfld
↾t |
127 | 125, 126 | dvres 23675 |
. . . . . 6
|
128 | 113, 122,
124, 120, 127 | syl22anc 1327 |
. . . . 5
..^
|
129 | 128 | dmeqd 5326 |
. . . 4
..^
|
130 | | ioontr 39736 |
. . . . . . 7
|
131 | 130 | reseq2i 5393 |
. . . . . 6
|
132 | 131 | dmeqi 5325 |
. . . . 5
|
133 | 132 | a1i 11 |
. . . 4
..^
|
134 | | fourierdlem113.dvcn |
. . . . 5
..^ |
135 | | cncff 22696 |
. . . . 5
|
136 | | fdm 6051 |
. . . . 5
|
137 | 134, 135,
136 | 3syl 18 |
. . . 4
..^
|
138 | 129, 133,
137 | 3eqtrd 2660 |
. . 3
..^
|
139 | | dvcn 23684 |
. . 3
|
140 | 113, 119,
120, 138, 139 | syl31anc 1329 |
. 2
..^ |
141 | 120, 113 | sstrd 3613 |
. . 3
..^ |
142 | 77 | adantr 481 |
. . . . . 6
..^ |
143 | | fzofzp1 12565 |
. . . . . . 7
..^
|
144 | 143 | adantl 482 |
. . . . . 6
..^ |
145 | 142, 144 | ffvelrnd 6360 |
. . . . 5
..^ |
146 | 145 | rexrd 10089 |
. . . 4
..^ |
147 | | elfzofz 12485 |
. . . . . 6
..^
|
148 | 147 | adantl 482 |
. . . . 5
..^ |
149 | 142, 148 | ffvelrnd 6360 |
. . . 4
..^ |
150 | 74 | simprrd 797 |
. . . . 5
..^ |
151 | 150 | r19.21bi 2932 |
. . . 4
..^ |
152 | 125, 146,
149, 151 | lptioo1cn 39878 |
. . 3
..^ ℂfld |
153 | 116 | adantr 481 |
. . . 4
..^ |
154 | 123 | a1i 11 |
. . . . . . . 8
|
155 | 117, 121,
154 | dvbss 23665 |
. . . . . . 7
|
156 | | dvfre 23714 |
. . . . . . . 8
|
157 | 1, 154, 156 | syl2anc 693 |
. . . . . . 7
|
158 | | 0re 10040 |
. . . . . . . . . 10
|
159 | 60, 158, 59 | lttri 10163 |
. . . . . . . . 9
|
160 | 63, 65, 159 | mp2an 708 |
. . . . . . . 8
|
161 | 160 | a1i 11 |
. . . . . . 7
|
162 | 84 | simplld 791 |
. . . . . . 7
|
163 | 134, 135 | syl 17 |
. . . . . . . 8
..^ |
164 | | fourierdlem113.dvlb |
. . . . . . . 8
..^ lim |
165 | 163, 141,
152, 164, 125 | ellimciota 39846 |
. . . . . . 7
..^
lim lim |
166 | 149 | rexrd 10089 |
. . . . . . . . 9
..^ |
167 | 125, 166,
145, 151 | lptioo2cn 39877 |
. . . . . . . 8
..^ ℂfld |
168 | | fourierdlem113.dvub |
. . . . . . . 8
..^ lim |
169 | 163, 141,
167, 168, 125 | ellimciota 39846 |
. . . . . . 7
..^
lim lim |
170 | 121 | adantr 481 |
. . . . . . . . . 10
|
171 | | zre 11381 |
. . . . . . . . . . . 12
|
172 | 171 | adantl 482 |
. . . . . . . . . . 11
|
173 | | 2re 11090 |
. . . . . . . . . . . . . . 15
|
174 | 173, 59 | remulcli 10054 |
. . . . . . . . . . . . . 14
|
175 | 174 | a1i 11 |
. . . . . . . . . . . . 13
|
176 | 69, 175 | syl5eqel 2705 |
. . . . . . . . . . . 12
|
177 | 176 | adantr 481 |
. . . . . . . . . . 11
|
178 | 172, 177 | remulcld 10070 |
. . . . . . . . . 10
|
179 | 170 | adantr 481 |
. . . . . . . . . . 11
|
180 | 177 | adantr 481 |
. . . . . . . . . . 11
|
181 | | simplr 792 |
. . . . . . . . . . 11
|
182 | | simpr 477 |
. . . . . . . . . . 11
|
183 | 111 | ad4ant14 1293 |
. . . . . . . . . . 11
|
184 | 179, 180,
181, 182, 183 | fperiodmul 39518 |
. . . . . . . . . 10
|
185 | | eqid 2622 |
. . . . . . . . . 10
|
186 | 170, 178,
184, 185 | fperdvper 40133 |
. . . . . . . . 9
|
187 | 186 | an32s 846 |
. . . . . . . 8
|
188 | 187 | simpld 475 |
. . . . . . 7
|
189 | 187 | simprd 479 |
. . . . . . 7
|
190 | | fveq2 6191 |
. . . . . . . . 9
|
191 | | oveq1 6657 |
. . . . . . . . . 10
|
192 | 191 | fveq2d 6195 |
. . . . . . . . 9
|
193 | 190, 192 | oveq12d 6668 |
. . . . . . . 8
|
194 | 193 | cbvmptv 4750 |
. . . . . . 7
..^ ..^ |
195 | | eqid 2622 |
. . . . . . 7
|
196 | 155, 157,
61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195 | fourierdlem71 40394 |
. . . . . 6
|
197 | 196 | adantr 481 |
. . . . 5
..^ |
198 | | nfv 1843 |
. . . . . . . . 9
..^ |
199 | | nfra1 2941 |
. . . . . . . . 9
|
200 | 198, 199 | nfan 1828 |
. . . . . . . 8
..^ |
201 | 128, 131 | syl6eq 2672 |
. . . . . . . . . . . . . 14
..^
|
202 | 201 | fveq1d 6193 |
. . . . . . . . . . . . 13
..^ |
203 | | fvres 6207 |
. . . . . . . . . . . . 13
|
204 | 202, 203 | sylan9eq 2676 |
. . . . . . . . . . . 12
..^ |
205 | 204 | fveq2d 6195 |
. . . . . . . . . . 11
..^ |
206 | 205 | adantlr 751 |
. . . . . . . . . 10
..^
|
207 | | simplr 792 |
. . . . . . . . . . 11
..^
|
208 | | ssdmres 5420 |
. . . . . . . . . . . . . 14
|
209 | 137, 208 | sylibr 224 |
. . . . . . . . . . . . 13
..^
|
210 | 209 | ad2antrr 762 |
. . . . . . . . . . . 12
..^
|
211 | | simpr 477 |
. . . . . . . . . . . 12
..^
|
212 | 210, 211 | sseldd 3604 |
. . . . . . . . . . 11
..^
|
213 | | rspa 2930 |
. . . . . . . . . . 11
|
214 | 207, 212,
213 | syl2anc 693 |
. . . . . . . . . 10
..^
|
215 | 206, 214 | eqbrtrd 4675 |
. . . . . . . . 9
..^
|
216 | 215 | ex 450 |
. . . . . . . 8
..^
|
217 | 200, 216 | ralrimi 2957 |
. . . . . . 7
..^
|
218 | 217 | ex 450 |
. . . . . 6
..^ |
219 | 218 | reximdv 3016 |
. . . . 5
..^ |
220 | 197, 219 | mpd 15 |
. . . 4
..^ |
221 | 149, 145,
153, 138, 220 | ioodvbdlimc1 40148 |
. . 3
..^ lim |
222 | 119, 141,
152, 221, 125 | ellimciota 39846 |
. 2
..^
lim lim |
223 | 149, 145,
153, 138, 220 | ioodvbdlimc2 40150 |
. . 3
..^ lim |
224 | 119, 141,
167, 223, 125 | ellimciota 39846 |
. 2
..^
lim lim |
225 | | frel 6050 |
. . . . . . 7
|
226 | 157, 225 | syl 17 |
. . . . . 6
|
227 | | resindm 5444 |
. . . . . 6
|
228 | 226, 227 | syl 17 |
. . . . 5
|
229 | | inss2 3834 |
. . . . . . 7
|
230 | 229 | a1i 11 |
. . . . . 6
|
231 | 157, 230 | fssresd 6071 |
. . . . 5
|
232 | 228, 231 | feq1dd 39347 |
. . . 4
|
233 | 232, 117 | fssd 6057 |
. . 3
|
234 | | ioosscn 39716 |
. . . . 5
|
235 | | ssinss1 3841 |
. . . . 5
|
236 | 234, 235 | ax-mp 5 |
. . . 4
|
237 | 236 | a1i 11 |
. . 3
|
238 | | 3simpb 1059 |
. . . . . . . 8
|
239 | | simp2 1062 |
. . . . . . . 8
|
240 | 170 | adantr 481 |
. . . . . . . . . 10
|
241 | 177 | adantr 481 |
. . . . . . . . . 10
|
242 | | simplr 792 |
. . . . . . . . . 10
|
243 | | simpr 477 |
. . . . . . . . . 10
|
244 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
245 | 244 | anbi2d 740 |
. . . . . . . . . . . . 13
|
246 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
247 | 246 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
248 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
249 | 247, 248 | eqeq12d 2637 |
. . . . . . . . . . . . 13
|
250 | 245, 249 | imbi12d 334 |
. . . . . . . . . . . 12
|
251 | 250, 111 | chvarv 2263 |
. . . . . . . . . . 11
|
252 | 251 | ad4ant14 1293 |
. . . . . . . . . 10
|
253 | 240, 241,
242, 243, 252 | fperiodmul 39518 |
. . . . . . . . 9
|
254 | 170, 178,
253, 185 | fperdvper 40133 |
. . . . . . . 8
|
255 | 238, 239,
254 | syl2anc 693 |
. . . . . . 7
|
256 | 255 | simpld 475 |
. . . . . 6
|
257 | | oveq2 6658 |
. . . . . . . . . 10
|
258 | 257 | oveq1d 6665 |
. . . . . . . . 9
|
259 | 258 | fveq2d 6195 |
. . . . . . . 8
|
260 | 259 | oveq1d 6665 |
. . . . . . 7
|
261 | 260 | cbvmptv 4750 |
. . . . . 6
|
262 | | eqid 2622 |
. . . . . 6
|
263 | 61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209 | fourierdlem41 40365 |
. . . . 5
|
264 | 263 | simpld 475 |
. . . 4
|
265 | 125 | cnfldtop 22587 |
. . . . . . . . 9
ℂfld |
266 | 265 | a1i 11 |
. . . . . . . 8
ℂfld |
267 | 236 | a1i 11 |
. . . . . . . 8
|
268 | | mnfxr 10096 |
. . . . . . . . . . . 12
|
269 | 268 | a1i 11 |
. . . . . . . . . . 11
|
270 | | rexr 10085 |
. . . . . . . . . . . 12
|
271 | | mnflt 11957 |
. . . . . . . . . . . 12
|
272 | 269, 270,
271 | xrltled 39486 |
. . . . . . . . . . 11
|
273 | | iooss1 12210 |
. . . . . . . . . . 11
|
274 | 269, 272,
273 | syl2anc 693 |
. . . . . . . . . 10
|
275 | 274 | 3ad2ant2 1083 |
. . . . . . . . 9
|
276 | | simp3 1063 |
. . . . . . . . 9
|
277 | 275, 276 | ssind 3837 |
. . . . . . . 8
|
278 | | unicntop 22589 |
. . . . . . . . 9
ℂfld |
279 | 278 | lpss3 20948 |
. . . . . . . 8
ℂfld
ℂfld
ℂfld
|
280 | 266, 267,
277, 279 | syl3anc 1326 |
. . . . . . 7
ℂfld
ℂfld
|
281 | 280 | 3adant3l 1322 |
. . . . . 6
ℂfld
ℂfld
|
282 | 270 | 3ad2ant2 1083 |
. . . . . . 7
|
283 | 58 | 3ad2ant1 1082 |
. . . . . . 7
|
284 | | simp3l 1089 |
. . . . . . 7
|
285 | 125, 282,
283, 284 | lptioo2cn 39877 |
. . . . . 6
ℂfld |
286 | 281, 285 | sseldd 3604 |
. . . . 5
ℂfld
|
287 | 286 | rexlimdv3a 3033 |
. . . 4
ℂfld
|
288 | 264, 287 | mpd 15 |
. . 3
ℂfld
|
289 | 255 | simprd 479 |
. . . 4
|
290 | | oveq2 6658 |
. . . . . . . 8
|
291 | 290 | oveq1d 6665 |
. . . . . . 7
|
292 | 291 | fveq2d 6195 |
. . . . . 6
|
293 | 292 | oveq1d 6665 |
. . . . 5
|
294 | 293 | cbvmptv 4750 |
. . . 4
|
295 | | id 22 |
. . . . . 6
|
296 | | fveq2 6191 |
. . . . . 6
|
297 | 295, 296 | oveq12d 6668 |
. . . . 5
|
298 | 297 | cbvmptv 4750 |
. . . 4
|
299 | 61, 62, 161, 23, 71, 24, 25, 155, 157, 256, 289, 134, 169, 58, 294, 298 | fourierdlem49 40372 |
. . 3
lim |
300 | 233, 237,
288, 299, 125 | ellimciota 39846 |
. 2
lim lim |
301 | | resindm 5444 |
. . . . . 6
|
302 | 226, 301 | syl 17 |
. . . . 5
|
303 | | inss2 3834 |
. . . . . . 7
|
304 | 303 | a1i 11 |
. . . . . 6
|
305 | 157, 304 | fssresd 6071 |
. . . . 5
|
306 | 302, 305 | feq1dd 39347 |
. . . 4
|
307 | 306, 117 | fssd 6057 |
. . 3
|
308 | | ioosscn 39716 |
. . . . 5
|
309 | | ssinss1 3841 |
. . . . 5
|
310 | 308, 309 | ax-mp 5 |
. . . 4
|
311 | 310 | a1i 11 |
. . 3
|
312 | 263 | simprd 479 |
. . . 4
|
313 | 265 | a1i 11 |
. . . . . . . 8
ℂfld |
314 | 310 | a1i 11 |
. . . . . . . 8
|
315 | | pnfxr 10092 |
. . . . . . . . . . . 12
|
316 | 315 | a1i 11 |
. . . . . . . . . . 11
|
317 | | ltpnf 11954 |
. . . . . . . . . . . 12
|
318 | 270, 316,
317 | xrltled 39486 |
. . . . . . . . . . 11
|
319 | | iooss2 12211 |
. . . . . . . . . . 11
|
320 | 316, 318,
319 | syl2anc 693 |
. . . . . . . . . 10
|
321 | 320 | 3ad2ant2 1083 |
. . . . . . . . 9
|
322 | | simp3 1063 |
. . . . . . . . 9
|
323 | 321, 322 | ssind 3837 |
. . . . . . . 8
|
324 | 278 | lpss3 20948 |
. . . . . . . 8
ℂfld
ℂfld ℂfld
|
325 | 313, 314,
323, 324 | syl3anc 1326 |
. . . . . . 7
ℂfld ℂfld
|
326 | 325 | 3adant3l 1322 |
. . . . . 6
ℂfld ℂfld
|
327 | 270 | 3ad2ant2 1083 |
. . . . . . 7
|
328 | 58 | 3ad2ant1 1082 |
. . . . . . 7
|
329 | | simp3l 1089 |
. . . . . . 7
|
330 | 125, 327,
328, 329 | lptioo1cn 39878 |
. . . . . 6
ℂfld |
331 | 326, 330 | sseldd 3604 |
. . . . 5
ℂfld
|
332 | 331 | rexlimdv3a 3033 |
. . . 4
ℂfld
|
333 | 312, 332 | mpd 15 |
. . 3
ℂfld
|
334 | | biid 251 |
. . . 4
..^
..^ |
335 | 61, 62, 161, 23, 71, 24, 25, 157, 256, 289, 134, 165, 58, 294, 298, 334 | fourierdlem48 40371 |
. . 3
lim
|
336 | 307, 311,
333, 335, 125 | ellimciota 39846 |
. 2
lim lim |
337 | | fourierdlem113.l |
. 2
lim |
338 | | fourierdlem113.r |
. 2
lim |
339 | | fourierdlem113.a |
. 2
|
340 | | fourierdlem113.b |
. 2
|
341 | | fveq2 6191 |
. . . . . . . 8
|
342 | | oveq1 6657 |
. . . . . . . . 9
|
343 | 342 | fveq2d 6195 |
. . . . . . . 8
|
344 | 341, 343 | oveq12d 6668 |
. . . . . . 7
|
345 | | fveq2 6191 |
. . . . . . . 8
|
346 | 342 | fveq2d 6195 |
. . . . . . . 8
|
347 | 345, 346 | oveq12d 6668 |
. . . . . . 7
|
348 | 344, 347 | oveq12d 6668 |
. . . . . 6
|
349 | 348 | cbvsumv 14426 |
. . . . 5
|
350 | | oveq2 6658 |
. . . . . . 7
|
351 | 350 | eqcomd 2628 |
. . . . . 6
|
352 | 351 | sumeq1d 14431 |
. . . . 5
|
353 | 349, 352 | syl5req 2669 |
. . . 4
|
354 | 353 | oveq2d 6666 |
. . 3
|
355 | 354 | cbvmptv 4750 |
. 2
|
356 | | fourierdlem113.15 |
. 2
|
357 | | fdm 6051 |
. . . . . 6
|
358 | 1, 357 | syl 17 |
. . . . 5
|
359 | 358, 154 | eqsstrd 3639 |
. . . 4
|
360 | 358 | feq2d 6031 |
. . . . 5
|
361 | 1, 360 | mpbird 247 |
. . . 4
|
362 | 359 | sselda 3603 |
. . . . . . 7
|
363 | 362 | adantr 481 |
. . . . . 6
|
364 | 171 | adantl 482 |
. . . . . . 7
|
365 | 177 | adantlr 751 |
. . . . . . 7
|
366 | 364, 365 | remulcld 10070 |
. . . . . 6
|
367 | 363, 366 | readdcld 10069 |
. . . . 5
|
368 | 358 | eqcomd 2628 |
. . . . . 6
|
369 | 368 | ad2antrr 762 |
. . . . 5
|
370 | 367, 369 | eleqtrd 2703 |
. . . 4
|
371 | | id 22 |
. . . . . 6
|
372 | 371 | adantlr 751 |
. . . . 5
|
373 | 372, 363,
184 | syl2anc 693 |
. . . 4
|
374 | 359, 361,
61, 62, 161, 71, 24, 77, 162, 85, 140, 222, 224, 370, 373, 194, 195 | fourierdlem71 40394 |
. . 3
|
375 | 358 | raleqdv 3144 |
. . . 4
|
376 | 375 | rexbidv 3052 |
. . 3
|
377 | 374, 376 | mpbid 222 |
. 2
|
378 | 1, 22, 23, 24, 25, 32, 57, 58, 110, 69, 111, 140, 222, 224, 134, 300, 336, 337, 338, 339, 340, 355, 356, 377, 196, 58 | fourierdlem112 40435 |
1
|