Step | Hyp | Ref
| Expression |
1 | | fourierdlem75.xre |
. . . . 5
|
2 | 1 | ad2antrr 762 |
. . . 4
..^ |
3 | | fourierdlem75.v |
. . . . . . . . . 10
|
4 | | fourierdlem75.m |
. . . . . . . . . . 11
|
5 | | fourierdlem75.p |
. . . . . . . . . . . 12
..^ |
6 | 5 | fourierdlem2 40326 |
. . . . . . . . . . 11
..^ |
7 | 4, 6 | syl 17 |
. . . . . . . . . 10
..^ |
8 | 3, 7 | mpbid 222 |
. . . . . . . . 9
..^ |
9 | 8 | simpld 475 |
. . . . . . . 8
|
10 | | elmapi 7879 |
. . . . . . . 8
|
11 | 9, 10 | syl 17 |
. . . . . . 7
|
12 | 11 | adantr 481 |
. . . . . 6
..^ |
13 | | fzofzp1 12565 |
. . . . . . 7
..^
|
14 | 13 | adantl 482 |
. . . . . 6
..^ |
15 | 12, 14 | ffvelrnd 6360 |
. . . . 5
..^ |
16 | 15 | adantr 481 |
. . . 4
..^ |
17 | | eqcom 2629 |
. . . . . . 7
|
18 | 17 | biimpi 206 |
. . . . . 6
|
19 | 18 | adantl 482 |
. . . . 5
..^ |
20 | 8 | simprrd 797 |
. . . . . . 7
..^ |
21 | 20 | r19.21bi 2932 |
. . . . . 6
..^ |
22 | 21 | adantr 481 |
. . . . 5
..^ |
23 | 19, 22 | eqbrtrd 4675 |
. . . 4
..^ |
24 | | fourierdlem75.f |
. . . . . . 7
|
25 | 24 | adantr 481 |
. . . . . 6
..^ |
26 | | ioossre 12235 |
. . . . . . 7
|
27 | 26 | a1i 11 |
. . . . . 6
..^
|
28 | 25, 27 | fssresd 6071 |
. . . . 5
..^ |
29 | 28 | adantr 481 |
. . . 4
..^ |
30 | | limcresi 23649 |
. . . . . . . 8
lim lim |
31 | | fourierdlem75.y |
. . . . . . . 8
lim |
32 | 30, 31 | sseldi 3601 |
. . . . . . 7
lim |
33 | 32 | adantr 481 |
. . . . . 6
..^ lim |
34 | | pnfxr 10092 |
. . . . . . . . . 10
|
35 | 34 | a1i 11 |
. . . . . . . . 9
..^
|
36 | 15 | rexrd 10089 |
. . . . . . . . . 10
..^ |
37 | 15 | ltpnfd 11955 |
. . . . . . . . . 10
..^ |
38 | 36, 35, 37 | xrltled 39486 |
. . . . . . . . 9
..^ |
39 | | iooss2 12211 |
. . . . . . . . 9
|
40 | 35, 38, 39 | syl2anc 693 |
. . . . . . . 8
..^
|
41 | 40 | resabs1d 5428 |
. . . . . . 7
..^ |
42 | 41 | oveq1d 6665 |
. . . . . 6
..^
lim lim |
43 | 33, 42 | eleqtrd 2703 |
. . . . 5
..^ lim |
44 | 43 | adantr 481 |
. . . 4
..^ lim |
45 | | eqid 2622 |
. . . 4
|
46 | | ax-resscn 9993 |
. . . . . . . . . . 11
|
47 | 46 | a1i 11 |
. . . . . . . . . 10
|
48 | 24, 47 | fssd 6057 |
. . . . . . . . . 10
|
49 | | ssid 3624 |
. . . . . . . . . . 11
|
50 | 49 | a1i 11 |
. . . . . . . . . 10
|
51 | 26 | a1i 11 |
. . . . . . . . . 10
|
52 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld ℂfld |
53 | 52 | tgioo2 22606 |
. . . . . . . . . . 11
ℂfld
↾t |
54 | 52, 53 | dvres 23675 |
. . . . . . . . . 10
|
55 | 47, 48, 50, 51, 54 | syl22anc 1327 |
. . . . . . . . 9
|
56 | | fourierdlem75.g |
. . . . . . . . . . 11
|
57 | 56 | eqcomi 2631 |
. . . . . . . . . 10
|
58 | | ioontr 39736 |
. . . . . . . . . 10
|
59 | 57, 58 | reseq12i 5394 |
. . . . . . . . 9
|
60 | 55, 59 | syl6eq 2672 |
. . . . . . . 8
|
61 | 60 | adantr 481 |
. . . . . . 7
|
62 | 61 | dmeqd 5326 |
. . . . . 6
|
63 | 62 | adantlr 751 |
. . . . 5
..^
|
64 | | fourierdlem75.gcn |
. . . . . . . . 9
..^ |
65 | 64 | adantr 481 |
. . . . . . . 8
..^ |
66 | | oveq1 6657 |
. . . . . . . . . . 11
|
67 | 66 | reseq2d 5396 |
. . . . . . . . . 10
|
68 | 67 | feq1d 6030 |
. . . . . . . . 9
|
69 | 68 | adantl 482 |
. . . . . . . 8
..^
|
70 | 65, 69 | mpbid 222 |
. . . . . . 7
..^ |
71 | 66 | adantl 482 |
. . . . . . . 8
..^ |
72 | 71 | feq2d 6031 |
. . . . . . 7
..^
|
73 | 70, 72 | mpbid 222 |
. . . . . 6
..^ |
74 | | fdm 6051 |
. . . . . 6
|
75 | 73, 74 | syl 17 |
. . . . 5
..^
|
76 | 63, 75 | eqtrd 2656 |
. . . 4
..^
|
77 | | limcresi 23649 |
. . . . . . . 8
lim lim |
78 | | fourierdlem75.e |
. . . . . . . 8
lim |
79 | 77, 78 | sseldi 3601 |
. . . . . . 7
lim |
80 | 79 | adantr 481 |
. . . . . 6
..^ lim |
81 | 40 | resabs1d 5428 |
. . . . . . . 8
..^ |
82 | 60 | adantr 481 |
. . . . . . . 8
..^
|
83 | 81, 82 | eqtr4d 2659 |
. . . . . . 7
..^
|
84 | 83 | oveq1d 6665 |
. . . . . 6
..^
lim lim |
85 | 80, 84 | eleqtrd 2703 |
. . . . 5
..^ lim |
86 | 85 | adantr 481 |
. . . 4
..^
lim |
87 | | eqid 2622 |
. . . 4
|
88 | | oveq2 6658 |
. . . . . . 7
|
89 | 88 | fveq2d 6195 |
. . . . . 6
|
90 | 89 | oveq1d 6665 |
. . . . 5
|
91 | 90 | cbvmptv 4750 |
. . . 4
|
92 | | id 22 |
. . . . 5
|
93 | 92 | cbvmptv 4750 |
. . . 4
|
94 | 2, 16, 23, 29, 44, 45, 76, 86, 87, 91, 93 | fourierdlem61 40384 |
. . 3
..^ lim |
95 | | fourierdlem75.a |
. . . . 5
|
96 | | iftrue 4092 |
. . . . 5
|
97 | 95, 96 | syl5eq 2668 |
. . . 4
|
98 | 97 | adantl 482 |
. . 3
..^ |
99 | | fourierdlem75.h |
. . . . . . 7
|
100 | 99 | reseq1i 5392 |
. . . . . 6
|
101 | 100 | a1i 11 |
. . . . 5
..^
|
102 | | ioossicc 12259 |
. . . . . . . 8
|
103 | | pire 24210 |
. . . . . . . . . . . 12
|
104 | 103 | renegcli 10342 |
. . . . . . . . . . 11
|
105 | 104 | rexri 10097 |
. . . . . . . . . 10
|
106 | 105 | a1i 11 |
. . . . . . . . 9
..^ |
107 | 103 | rexri 10097 |
. . . . . . . . . 10
|
108 | 107 | a1i 11 |
. . . . . . . . 9
..^ |
109 | 104 | a1i 11 |
. . . . . . . . . . . 12
|
110 | 103 | a1i 11 |
. . . . . . . . . . . 12
|
111 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
112 | 111, 1 | readdcld 10069 |
. . . . . . . . . . . . . . . 16
|
113 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
114 | 113, 1 | readdcld 10069 |
. . . . . . . . . . . . . . . 16
|
115 | 112, 114 | iccssred 39727 |
. . . . . . . . . . . . . . 15
|
116 | 115 | adantr 481 |
. . . . . . . . . . . . . 14
|
117 | 5, 4, 3 | fourierdlem15 40339 |
. . . . . . . . . . . . . . 15
|
118 | 117 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
119 | 116, 118 | sseldd 3604 |
. . . . . . . . . . . . 13
|
120 | 1 | adantr 481 |
. . . . . . . . . . . . 13
|
121 | 119, 120 | resubcld 10458 |
. . . . . . . . . . . 12
|
122 | 111 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
123 | 1 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
124 | 122, 123 | pncand 10393 |
. . . . . . . . . . . . . . 15
|
125 | 124 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
126 | 125 | adantr 481 |
. . . . . . . . . . . . 13
|
127 | 112 | adantr 481 |
. . . . . . . . . . . . . 14
|
128 | 114 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
129 | | elicc2 12238 |
. . . . . . . . . . . . . . . . 17
|
130 | 127, 128,
129 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
131 | 118, 130 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
132 | 131 | simp2d 1074 |
. . . . . . . . . . . . . 14
|
133 | 127, 119,
120, 132 | lesub1dd 10643 |
. . . . . . . . . . . . 13
|
134 | 126, 133 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
135 | 131 | simp3d 1075 |
. . . . . . . . . . . . . 14
|
136 | 119, 128,
120, 135 | lesub1dd 10643 |
. . . . . . . . . . . . 13
|
137 | 110 | recnd 10068 |
. . . . . . . . . . . . . 14
|
138 | 123 | adantr 481 |
. . . . . . . . . . . . . 14
|
139 | 137, 138 | pncand 10393 |
. . . . . . . . . . . . 13
|
140 | 136, 139 | breqtrd 4679 |
. . . . . . . . . . . 12
|
141 | 109, 110,
121, 134, 140 | eliccd 39726 |
. . . . . . . . . . 11
|
142 | | fourierdlem75.q |
. . . . . . . . . . 11
|
143 | 141, 142 | fmptd 6385 |
. . . . . . . . . 10
|
144 | 143 | adantr 481 |
. . . . . . . . 9
..^ |
145 | | simpr 477 |
. . . . . . . . 9
..^ ..^ |
146 | 106, 108,
144, 145 | fourierdlem8 40332 |
. . . . . . . 8
..^ |
147 | 102, 146 | syl5ss 3614 |
. . . . . . 7
..^ |
148 | 147 | resmptd 5452 |
. . . . . 6
..^
|
149 | 148 | adantr 481 |
. . . . 5
..^
|
150 | | elfzofz 12485 |
. . . . . . . 8
..^
|
151 | | simpr 477 |
. . . . . . . . . . 11
|
152 | 142 | fvmpt2 6291 |
. . . . . . . . . . 11
|
153 | 151, 141,
152 | syl2anc 693 |
. . . . . . . . . 10
|
154 | 153 | adantr 481 |
. . . . . . . . 9
|
155 | | oveq1 6657 |
. . . . . . . . . 10
|
156 | 155 | adantl 482 |
. . . . . . . . 9
|
157 | 123 | ad2antrr 762 |
. . . . . . . . . 10
|
158 | 157 | subidd 10380 |
. . . . . . . . 9
|
159 | 154, 156,
158 | 3eqtrd 2660 |
. . . . . . . 8
|
160 | 150, 159 | sylanl2 683 |
. . . . . . 7
..^ |
161 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
162 | 161 | oveq1d 6665 |
. . . . . . . . . . . 12
|
163 | 162 | cbvmptv 4750 |
. . . . . . . . . . 11
|
164 | 142, 163 | eqtri 2644 |
. . . . . . . . . 10
|
165 | 164 | a1i 11 |
. . . . . . . . 9
..^ |
166 | | fveq2 6191 |
. . . . . . . . . . 11
|
167 | 166 | oveq1d 6665 |
. . . . . . . . . 10
|
168 | 167 | adantl 482 |
. . . . . . . . 9
..^ |
169 | 1 | adantr 481 |
. . . . . . . . . 10
..^ |
170 | 15, 169 | resubcld 10458 |
. . . . . . . . 9
..^ |
171 | 165, 168,
14, 170 | fvmptd 6288 |
. . . . . . . 8
..^ |
172 | 171 | adantr 481 |
. . . . . . 7
..^ |
173 | 160, 172 | oveq12d 6668 |
. . . . . 6
..^ |
174 | | simplr 792 |
. . . . . . . . . 10
..^
|
175 | | fourierdlem75.o |
. . . . . . . . . . . . 13
..^ |
176 | 4 | adantr 481 |
. . . . . . . . . . . . 13
|
177 | 111, 113,
1, 5, 175, 4, 3, 142 | fourierdlem14 40338 |
. . . . . . . . . . . . . 14
|
178 | 177 | adantr 481 |
. . . . . . . . . . . . 13
|
179 | | simpr 477 |
. . . . . . . . . . . . . 14
|
180 | | fourierdlem75.x |
. . . . . . . . . . . . . . . . . 18
|
181 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
182 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . . . 19
|
183 | 117, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
184 | 180, 183 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
185 | 159 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
186 | 185 | reximdva 3017 |
. . . . . . . . . . . . . . . . 17
|
187 | 184, 186 | mpd 15 |
. . . . . . . . . . . . . . . 16
|
188 | 121, 142 | fmptd 6385 |
. . . . . . . . . . . . . . . . 17
|
189 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
|
190 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . 17
|
191 | 188, 189,
190 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
192 | 187, 191 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
193 | 192 | adantr 481 |
. . . . . . . . . . . . . 14
|
194 | 179, 193 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
195 | 175, 176,
178, 194 | fourierdlem12 40336 |
. . . . . . . . . . . 12
..^
|
196 | 195 | an32s 846 |
. . . . . . . . . . 11
..^
|
197 | 196 | adantlr 751 |
. . . . . . . . . 10
..^
|
198 | 174, 197 | pm2.65da 600 |
. . . . . . . . 9
..^
|
199 | 198 | adantlr 751 |
. . . . . . . 8
..^
|
200 | 199 | iffalsed 4097 |
. . . . . . 7
..^
|
201 | 160 | eqcomd 2628 |
. . . . . . . . . . . 12
..^ |
202 | 201 | adantr 481 |
. . . . . . . . . . 11
..^
|
203 | | elioo3g 12204 |
. . . . . . . . . . . . . 14
|
204 | 203 | biimpi 206 |
. . . . . . . . . . . . 13
|
205 | 204 | simprld 795 |
. . . . . . . . . . . 12
|
206 | 205 | adantl 482 |
. . . . . . . . . . 11
..^
|
207 | 202, 206 | eqbrtrd 4675 |
. . . . . . . . . 10
..^
|
208 | 207 | iftrued 4094 |
. . . . . . . . 9
..^
|
209 | 208 | oveq2d 6666 |
. . . . . . . 8
..^
|
210 | 209 | oveq1d 6665 |
. . . . . . 7
..^
|
211 | 1 | rexrd 10089 |
. . . . . . . . . . . . 13
|
212 | 211 | ad3antrrr 766 |
. . . . . . . . . . . 12
..^
|
213 | 36 | ad2antrr 762 |
. . . . . . . . . . . 12
..^
|
214 | 169 | ad2antrr 762 |
. . . . . . . . . . . . 13
..^
|
215 | | elioore 12205 |
. . . . . . . . . . . . . 14
|
216 | 215 | adantl 482 |
. . . . . . . . . . . . 13
..^
|
217 | 214, 216 | readdcld 10069 |
. . . . . . . . . . . 12
..^
|
218 | 216, 207 | elrpd 11869 |
. . . . . . . . . . . . 13
..^
|
219 | 214, 218 | ltaddrpd 11905 |
. . . . . . . . . . . 12
..^
|
220 | 215 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ |
221 | 188 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
222 | 221, 14 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
..^ |
223 | 222 | adantr 481 |
. . . . . . . . . . . . . . 15
..^ |
224 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
..^ |
225 | 204 | simprrd 797 |
. . . . . . . . . . . . . . . 16
|
226 | 225 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ |
227 | 220, 223,
224, 226 | ltadd2dd 10196 |
. . . . . . . . . . . . . 14
..^
|
228 | 171 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
..^ |
229 | 123 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
230 | 15 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
..^ |
231 | 229, 230 | pncan3d 10395 |
. . . . . . . . . . . . . . . 16
..^ |
232 | 228, 231 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
..^ |
233 | 232 | adantr 481 |
. . . . . . . . . . . . . 14
..^
|
234 | 227, 233 | breqtrd 4679 |
. . . . . . . . . . . . 13
..^
|
235 | 234 | adantlr 751 |
. . . . . . . . . . . 12
..^
|
236 | 212, 213,
217, 219, 235 | eliood 39720 |
. . . . . . . . . . 11
..^
|
237 | | fvres 6207 |
. . . . . . . . . . 11
|
238 | 236, 237 | syl 17 |
. . . . . . . . . 10
..^
|
239 | 238 | eqcomd 2628 |
. . . . . . . . 9
..^
|
240 | 239 | oveq1d 6665 |
. . . . . . . 8
..^
|
241 | 240 | oveq1d 6665 |
. . . . . . 7
..^
|
242 | 200, 210,
241 | 3eqtrd 2660 |
. . . . . 6
..^
|
243 | 173, 242 | mpteq12dva 4732 |
. . . . 5
..^
|
244 | 101, 149,
243 | 3eqtrd 2660 |
. . . 4
..^
|
245 | 244, 160 | oveq12d 6668 |
. . 3
..^ lim lim |
246 | 94, 98, 245 | 3eltr4d 2716 |
. 2
..^ lim |
247 | | eqid 2622 |
. . . . 5
|
248 | | eqid 2622 |
. . . . 5
|
249 | | eqid 2622 |
. . . . 5
|
250 | 24 | adantr 481 |
. . . . . . . . . 10
|
251 | 1 | adantr 481 |
. . . . . . . . . . 11
|
252 | 215 | adantl 482 |
. . . . . . . . . . 11
|
253 | 251, 252 | readdcld 10069 |
. . . . . . . . . 10
|
254 | 250, 253 | ffvelrnd 6360 |
. . . . . . . . 9
|
255 | 254 | recnd 10068 |
. . . . . . . 8
|
256 | 255 | adantlr 751 |
. . . . . . 7
..^ |
257 | 256 | 3adantl3 1219 |
. . . . . 6
..^ |
258 | | limccl 23639 |
. . . . . . . . . 10
lim |
259 | 258, 31 | sseldi 3601 |
. . . . . . . . 9
|
260 | | fourierdlem75.w |
. . . . . . . . . 10
|
261 | 260 | recnd 10068 |
. . . . . . . . 9
|
262 | 259, 261 | ifcld 4131 |
. . . . . . . 8
|
263 | 262 | adantr 481 |
. . . . . . 7
|
264 | 263 | 3ad2antl1 1223 |
. . . . . 6
..^ |
265 | 257, 264 | subcld 10392 |
. . . . 5
..^
|
266 | 215 | recnd 10068 |
. . . . . . 7
|
267 | 266 | adantl 482 |
. . . . . 6
..^ |
268 | | velsn 4193 |
. . . . . . . 8
|
269 | 198, 268 | sylnibr 319 |
. . . . . . 7
..^
|
270 | 269 | 3adantl3 1219 |
. . . . . 6
..^
|
271 | 267, 270 | eldifd 3585 |
. . . . 5
..^ |
272 | | eqid 2622 |
. . . . . . . . . 10
|
273 | | eqid 2622 |
. . . . . . . . . 10
|
274 | | eqid 2622 |
. . . . . . . . . 10
|
275 | 261 | ad2antrr 762 |
. . . . . . . . . 10
..^ |
276 | | ioossre 12235 |
. . . . . . . . . . . 12
|
277 | 276 | a1i 11 |
. . . . . . . . . . 11
..^ |
278 | 150, 119 | sylan2 491 |
. . . . . . . . . . . . . 14
..^ |
279 | 278 | rexrd 10089 |
. . . . . . . . . . . . 13
..^ |
280 | 279 | adantr 481 |
. . . . . . . . . . . 12
..^ |
281 | 36 | adantr 481 |
. . . . . . . . . . . 12
..^ |
282 | 253 | adantlr 751 |
. . . . . . . . . . . 12
..^
|
283 | | iccssre 12255 |
. . . . . . . . . . . . . . . . . . 19
|
284 | 104, 103,
283 | mp2an 708 |
. . . . . . . . . . . . . . . . . 18
|
285 | 284, 46 | sstri 3612 |
. . . . . . . . . . . . . . . . 17
|
286 | 153, 141 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
287 | 150, 286 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
..^ |
288 | 285, 287 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
..^ |
289 | 229, 288 | addcomd 10238 |
. . . . . . . . . . . . . . 15
..^ |
290 | 150 | adantl 482 |
. . . . . . . . . . . . . . . . 17
..^ |
291 | 150, 121 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
..^ |
292 | 142 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . 17
|
293 | 290, 291,
292 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
..^ |
294 | 293 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
..^ |
295 | 278 | recnd 10068 |
. . . . . . . . . . . . . . . 16
..^ |
296 | 295, 229 | npcand 10396 |
. . . . . . . . . . . . . . 15
..^ |
297 | 289, 294,
296 | 3eqtrrd 2661 |
. . . . . . . . . . . . . 14
..^ |
298 | 297 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
299 | 293, 291 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
..^ |
300 | 299 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
301 | 205 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
302 | 300, 220,
224, 301 | ltadd2dd 10196 |
. . . . . . . . . . . . 13
..^
|
303 | 298, 302 | eqbrtrd 4675 |
. . . . . . . . . . . 12
..^ |
304 | 280, 281,
282, 303, 234 | eliood 39720 |
. . . . . . . . . . 11
..^
|
305 | | ioossre 12235 |
. . . . . . . . . . . 12
|
306 | 305 | a1i 11 |
. . . . . . . . . . 11
..^ |
307 | 300, 301 | gtned 10172 |
. . . . . . . . . . 11
..^ |
308 | | fourierdlem75.r |
. . . . . . . . . . . 12
..^ lim |
309 | 297 | oveq2d 6666 |
. . . . . . . . . . . 12
..^ lim
lim
|
310 | 308, 309 | eleqtrd 2703 |
. . . . . . . . . . 11
..^ lim |
311 | 25, 169, 277, 272, 304, 306, 307, 310, 288 | fourierdlem53 40376 |
. . . . . . . . . 10
..^
lim |
312 | | ioosscn 39716 |
. . . . . . . . . . . 12
|
313 | 312 | a1i 11 |
. . . . . . . . . . 11
..^ |
314 | 261 | adantr 481 |
. . . . . . . . . . 11
..^ |
315 | 273, 313,
314, 288 | constlimc 39856 |
. . . . . . . . . 10
..^ lim |
316 | 272, 273,
274, 256, 275, 311, 315 | sublimc 39884 |
. . . . . . . . 9
..^
lim |
317 | 316 | adantr 481 |
. . . . . . . 8
..^
lim |
318 | | iftrue 4092 |
. . . . . . . . . 10
|
319 | 318 | oveq2d 6666 |
. . . . . . . . 9
|
320 | 319 | adantl 482 |
. . . . . . . 8
..^
|
321 | 215 | adantl 482 |
. . . . . . . . . . . . 13
..^
|
322 | | 0red 10041 |
. . . . . . . . . . . . 13
..^
|
323 | 222 | ad2antrr 762 |
. . . . . . . . . . . . . 14
..^
|
324 | 225 | adantl 482 |
. . . . . . . . . . . . . 14
..^
|
325 | 171 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^ |
326 | 279 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
..^
|
327 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
..^
|
328 | 169 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
..^
|
329 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
..^
|
330 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
331 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
332 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
333 | 331, 332 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
334 | 330, 333 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
335 | 334 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
..^
|
336 | 326, 327,
328, 329, 335 | eliood 39720 |
. . . . . . . . . . . . . . . . . 18
..^
|
337 | 5, 4, 3, 180 | fourierdlem12 40336 |
. . . . . . . . . . . . . . . . . . 19
..^
|
338 | 337 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
..^
|
339 | 336, 338 | condan 835 |
. . . . . . . . . . . . . . . . 17
..^ |
340 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^ |
341 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
..^ |
342 | 340, 341 | suble0d 10618 |
. . . . . . . . . . . . . . . . 17
..^
|
343 | 339, 342 | mpbird 247 |
. . . . . . . . . . . . . . . 16
..^ |
344 | 325, 343 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
..^ |
345 | 344 | adantr 481 |
. . . . . . . . . . . . . 14
..^
|
346 | 321, 323,
322, 324, 345 | ltletrd 10197 |
. . . . . . . . . . . . 13
..^
|
347 | 321, 322,
346 | ltnsymd 10186 |
. . . . . . . . . . . 12
..^
|
348 | 347 | iffalsed 4097 |
. . . . . . . . . . 11
..^
|
349 | 348 | oveq2d 6666 |
. . . . . . . . . 10
..^
|
350 | 349 | mpteq2dva 4744 |
. . . . . . . . 9
..^
|
351 | 350 | oveq1d 6665 |
. . . . . . . 8
..^
lim
lim |
352 | 317, 320,
351 | 3eltr4d 2716 |
. . . . . . 7
..^
lim |
353 | 352 | 3adantl3 1219 |
. . . . . 6
..^
lim |
354 | | eqid 2622 |
. . . . . . . . . 10
|
355 | | eqid 2622 |
. . . . . . . . . 10
|
356 | 259 | ad2antrr 762 |
. . . . . . . . . 10
..^ |
357 | 259 | adantr 481 |
. . . . . . . . . . 11
..^ |
358 | 354, 313,
357, 288 | constlimc 39856 |
. . . . . . . . . 10
..^ lim |
359 | 272, 354,
355, 256, 356, 311, 358 | sublimc 39884 |
. . . . . . . . 9
..^
lim |
360 | 359 | adantr 481 |
. . . . . . . 8
..^
lim |
361 | | iffalse 4095 |
. . . . . . . . . 10
|
362 | 361 | oveq2d 6666 |
. . . . . . . . 9
|
363 | 362 | adantl 482 |
. . . . . . . 8
..^
|
364 | | 0red 10041 |
. . . . . . . . . . . . 13
..^
|
365 | 299 | ad2antrr 762 |
. . . . . . . . . . . . 13
..^
|
366 | 215 | adantl 482 |
. . . . . . . . . . . . 13
..^
|
367 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
..^ |
368 | 278 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
369 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
..^ |
370 | 367, 368,
369 | nltled 10187 |
. . . . . . . . . . . . . . . 16
..^ |
371 | 368, 367 | subge0d 10617 |
. . . . . . . . . . . . . . . 16
..^
|
372 | 370, 371 | mpbird 247 |
. . . . . . . . . . . . . . 15
..^ |
373 | 293 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
..^ |
374 | 373 | adantr 481 |
. . . . . . . . . . . . . . 15
..^ |
375 | 372, 374 | breqtrd 4679 |
. . . . . . . . . . . . . 14
..^ |
376 | 375 | adantr 481 |
. . . . . . . . . . . . 13
..^
|
377 | 205 | adantl 482 |
. . . . . . . . . . . . 13
..^
|
378 | 364, 365,
366, 376, 377 | lelttrd 10195 |
. . . . . . . . . . . 12
..^
|
379 | 378 | iftrued 4094 |
. . . . . . . . . . 11
..^
|
380 | 379 | oveq2d 6666 |
. . . . . . . . . 10
..^
|
381 | 380 | mpteq2dva 4744 |
. . . . . . . . 9
..^
|
382 | 381 | oveq1d 6665 |
. . . . . . . 8
..^
lim
lim |
383 | 360, 363,
382 | 3eltr4d 2716 |
. . . . . . 7
..^
lim |
384 | 383 | 3adantl3 1219 |
. . . . . 6
..^
lim |
385 | 353, 384 | pm2.61dan 832 |
. . . . 5
..^
lim |
386 | 313, 248,
288 | idlimc 39858 |
. . . . . 6
..^ lim |
387 | 386 | 3adant3 1081 |
. . . . 5
..^ lim |
388 | 293 | 3adant3 1081 |
. . . . . 6
..^ |
389 | 295 | 3adant3 1081 |
. . . . . . 7
..^ |
390 | 229 | 3adant3 1081 |
. . . . . . 7
..^ |
391 | | neqne 2802 |
. . . . . . . 8
|
392 | 391 | 3ad2ant3 1084 |
. . . . . . 7
..^ |
393 | 389, 390,
392 | subne0d 10401 |
. . . . . 6
..^ |
394 | 388, 393 | eqnetrd 2861 |
. . . . 5
..^ |
395 | 198 | 3adantl3 1219 |
. . . . . 6
..^
|
396 | 395 | neqned 2801 |
. . . . 5
..^ |
397 | 247, 248,
249, 265, 271, 385, 387, 394, 396 | divlimc 39888 |
. . . 4
..^ lim |
398 | | iffalse 4095 |
. . . . . 6
|
399 | 95, 398 | syl5eq 2668 |
. . . . 5
|
400 | 399 | 3ad2ant3 1084 |
. . . 4
..^ |
401 | | ioossre 12235 |
. . . . . . . . . . . . 13
|
402 | 401 | a1i 11 |
. . . . . . . . . . . 12
|
403 | 24, 402 | fssresd 6071 |
. . . . . . . . . . 11
|
404 | 401, 47 | syl5ss 3614 |
. . . . . . . . . . 11
|
405 | 34 | a1i 11 |
. . . . . . . . . . . 12
|
406 | 1 | ltpnfd 11955 |
. . . . . . . . . . . 12
|
407 | 52, 405, 1, 406 | lptioo1cn 39878 |
. . . . . . . . . . 11
ℂfld |
408 | 403, 404,
407, 31 | limcrecl 39861 |
. . . . . . . . . 10
|
409 | 24, 1, 408, 260, 99 | fourierdlem9 40333 |
. . . . . . . . 9
|
410 | 409 | adantr 481 |
. . . . . . . 8
..^ |
411 | 410, 147 | feqresmpt 6250 |
. . . . . . 7
..^ |
412 | 147 | sselda 3603 |
. . . . . . . . . 10
..^ |
413 | | 0cnd 10033 |
. . . . . . . . . . 11
..^ |
414 | 262 | ad2antrr 762 |
. . . . . . . . . . . . 13
..^ |
415 | 256, 414 | subcld 10392 |
. . . . . . . . . . . 12
..^
|
416 | 266 | adantl 482 |
. . . . . . . . . . . 12
..^ |
417 | 198 | neqned 2801 |
. . . . . . . . . . . 12
..^ |
418 | 415, 416,
417 | divcld 10801 |
. . . . . . . . . . 11
..^
|
419 | 413, 418 | ifcld 4131 |
. . . . . . . . . 10
..^
|
420 | 99 | fvmpt2 6291 |
. . . . . . . . . 10
|
421 | 412, 419,
420 | syl2anc 693 |
. . . . . . . . 9
..^ |
422 | 198 | iffalsed 4097 |
. . . . . . . . 9
..^
|
423 | 421, 422 | eqtrd 2656 |
. . . . . . . 8
..^ |
424 | 423 | mpteq2dva 4744 |
. . . . . . 7
..^ |
425 | 411, 424 | eqtrd 2656 |
. . . . . 6
..^
|
426 | 425 | 3adant3 1081 |
. . . . 5
..^
|
427 | 426 | oveq1d 6665 |
. . . 4
..^ lim
lim |
428 | 397, 400,
427 | 3eltr4d 2716 |
. . 3
..^ lim |
429 | 428 | 3expa 1265 |
. 2
..^ lim |
430 | 246, 429 | pm2.61dan 832 |
1
..^ lim |