Step | Hyp | Ref
| Expression |
1 | | fourierdlem92.a |
. . . 4
|
2 | 1 | adantr 481 |
. . 3
|
3 | | fourierdlem92.b |
. . . 4
|
4 | 3 | adantr 481 |
. . 3
|
5 | | fourierdlem92.p |
. . 3
..^ |
6 | | fourierdlem92.m |
. . . 4
|
7 | 6 | adantr 481 |
. . 3
|
8 | | fourierdlem92.t |
. . . . 5
|
9 | 8 | adantr 481 |
. . . 4
|
10 | | simpr 477 |
. . . 4
|
11 | 9, 10 | elrpd 11869 |
. . 3
|
12 | | fourierdlem92.q |
. . . 4
|
13 | 12 | adantr 481 |
. . 3
|
14 | | fourierdlem92.fper |
. . . 4
|
15 | 14 | adantlr 751 |
. . 3
|
16 | | fveq2 6191 |
. . . . 5
|
17 | 16 | oveq1d 6665 |
. . . 4
|
18 | 17 | cbvmptv 4750 |
. . 3
|
19 | | fourierdlem92.f |
. . . 4
|
20 | 19 | adantr 481 |
. . 3
|
21 | | fourierdlem92.cncf |
. . . 4
..^ |
22 | 21 | adantlr 751 |
. . 3
..^
|
23 | | fourierdlem92.r |
. . . 4
..^ lim |
24 | 23 | adantlr 751 |
. . 3
..^
lim |
25 | | fourierdlem92.l |
. . . 4
..^ lim |
26 | 25 | adantlr 751 |
. . 3
..^
lim |
27 | | eqeq1 2626 |
. . . . 5
|
28 | | eqeq1 2626 |
. . . . . 6
|
29 | | fveq2 6191 |
. . . . . 6
|
30 | 28, 29 | ifbieq2d 4111 |
. . . . 5
|
31 | 27, 30 | ifbieq2d 4111 |
. . . 4
|
32 | 31 | cbvmptv 4750 |
. . 3
|
33 | | eqid 2622 |
. . 3
|
34 | 2, 4, 5, 7, 11, 13, 15, 18, 20, 22, 24, 26, 32, 33 | fourierdlem81 40404 |
. 2
|
35 | | simpr 477 |
. . . . . . . 8
|
36 | 35 | oveq2d 6666 |
. . . . . . 7
|
37 | 1 | recnd 10068 |
. . . . . . . . 9
|
38 | 37 | adantr 481 |
. . . . . . . 8
|
39 | 38 | addid1d 10236 |
. . . . . . 7
|
40 | 36, 39 | eqtrd 2656 |
. . . . . 6
|
41 | 35 | oveq2d 6666 |
. . . . . . 7
|
42 | 3 | recnd 10068 |
. . . . . . . . 9
|
43 | 42 | adantr 481 |
. . . . . . . 8
|
44 | 43 | addid1d 10236 |
. . . . . . 7
|
45 | 41, 44 | eqtrd 2656 |
. . . . . 6
|
46 | 40, 45 | oveq12d 6668 |
. . . . 5
|
47 | 46 | itgeq1d 40172 |
. . . 4
|
48 | 47 | adantlr 751 |
. . 3
|
49 | | simpll 790 |
. . . 4
|
50 | | simpr 477 |
. . . . . . 7
|
51 | | simplr 792 |
. . . . . . 7
|
52 | | ioran 511 |
. . . . . . 7
|
53 | 50, 51, 52 | sylanbrc 698 |
. . . . . 6
|
54 | 49, 8 | syl 17 |
. . . . . . 7
|
55 | | 0red 10041 |
. . . . . . 7
|
56 | 54, 55 | lttrid 10175 |
. . . . . 6
|
57 | 53, 56 | mpbird 247 |
. . . . 5
|
58 | 54 | lt0neg1d 10597 |
. . . . 5
|
59 | 57, 58 | mpbid 222 |
. . . 4
|
60 | 1, 8 | readdcld 10069 |
. . . . . . . . . . . 12
|
61 | 60 | recnd 10068 |
. . . . . . . . . . 11
|
62 | 8 | recnd 10068 |
. . . . . . . . . . 11
|
63 | 61, 62 | negsubd 10398 |
. . . . . . . . . 10
|
64 | 37, 62 | pncand 10393 |
. . . . . . . . . 10
|
65 | 63, 64 | eqtrd 2656 |
. . . . . . . . 9
|
66 | 3, 8 | readdcld 10069 |
. . . . . . . . . . . 12
|
67 | 66 | recnd 10068 |
. . . . . . . . . . 11
|
68 | 67, 62 | negsubd 10398 |
. . . . . . . . . 10
|
69 | 42, 62 | pncand 10393 |
. . . . . . . . . 10
|
70 | 68, 69 | eqtrd 2656 |
. . . . . . . . 9
|
71 | 65, 70 | oveq12d 6668 |
. . . . . . . 8
|
72 | 71 | eqcomd 2628 |
. . . . . . 7
|
73 | 72 | itgeq1d 40172 |
. . . . . 6
|
74 | 73 | adantr 481 |
. . . . 5
|
75 | 1 | adantr 481 |
. . . . . . 7
|
76 | 8 | adantr 481 |
. . . . . . 7
|
77 | 75, 76 | readdcld 10069 |
. . . . . 6
|
78 | 3 | adantr 481 |
. . . . . . 7
|
79 | 78, 76 | readdcld 10069 |
. . . . . 6
|
80 | | eqid 2622 |
. . . . . 6
..^ ..^ |
81 | 6 | adantr 481 |
. . . . . 6
|
82 | 76 | renegcld 10457 |
. . . . . . 7
|
83 | | simpr 477 |
. . . . . . 7
|
84 | 82, 83 | elrpd 11869 |
. . . . . 6
|
85 | 5 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . . 18
..^ |
86 | 6, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
87 | 12, 86 | mpbid 222 |
. . . . . . . . . . . . . . . 16
..^ |
88 | 87 | simpld 475 |
. . . . . . . . . . . . . . 15
|
89 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
|
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . 14
|
91 | 90 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
92 | 8 | adantr 481 |
. . . . . . . . . . . . 13
|
93 | 91, 92 | readdcld 10069 |
. . . . . . . . . . . 12
|
94 | | fourierdlem92.s |
. . . . . . . . . . . 12
|
95 | 93, 94 | fmptd 6385 |
. . . . . . . . . . 11
|
96 | | reex 10027 |
. . . . . . . . . . . . 13
|
97 | 96 | a1i 11 |
. . . . . . . . . . . 12
|
98 | | ovex 6678 |
. . . . . . . . . . . . 13
|
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
|
100 | 97, 99 | elmapd 7871 |
. . . . . . . . . . 11
|
101 | 95, 100 | mpbird 247 |
. . . . . . . . . 10
|
102 | 94 | a1i 11 |
. . . . . . . . . . . . 13
|
103 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
104 | 103 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
105 | 104 | adantl 482 |
. . . . . . . . . . . . 13
|
106 | | 0zd 11389 |
. . . . . . . . . . . . . . . 16
|
107 | 6 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
108 | 106, 107,
106 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
109 | | 0le0 11110 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . 15
|
111 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . 17
|
112 | 111 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . 16
|
113 | 6, 112 | syl 17 |
. . . . . . . . . . . . . . 15
|
114 | 108, 110,
113 | jca32 558 |
. . . . . . . . . . . . . 14
|
115 | | elfz2 12333 |
. . . . . . . . . . . . . 14
|
116 | 114, 115 | sylibr 224 |
. . . . . . . . . . . . 13
|
117 | 90, 116 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
118 | 117, 8 | readdcld 10069 |
. . . . . . . . . . . . 13
|
119 | 102, 105,
116, 118 | fvmptd 6288 |
. . . . . . . . . . . 12
|
120 | | simprll 802 |
. . . . . . . . . . . . . 14
..^ |
121 | 87, 120 | syl 17 |
. . . . . . . . . . . . 13
|
122 | 121 | oveq1d 6665 |
. . . . . . . . . . . 12
|
123 | 119, 122 | eqtrd 2656 |
. . . . . . . . . . 11
|
124 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
125 | 124 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
126 | 125 | adantl 482 |
. . . . . . . . . . . . 13
|
127 | 6 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
|
128 | | nn0uz 11722 |
. . . . . . . . . . . . . . 15
|
129 | 127, 128 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
|
130 | | eluzfz2 12349 |
. . . . . . . . . . . . . 14
|
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . 13
|
132 | 90, 131 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
133 | 132, 8 | readdcld 10069 |
. . . . . . . . . . . . 13
|
134 | 102, 126,
131, 133 | fvmptd 6288 |
. . . . . . . . . . . 12
|
135 | | simprlr 803 |
. . . . . . . . . . . . . 14
..^ |
136 | 87, 135 | syl 17 |
. . . . . . . . . . . . 13
|
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . 12
|
138 | 134, 137 | eqtrd 2656 |
. . . . . . . . . . 11
|
139 | 123, 138 | jca 554 |
. . . . . . . . . 10
|
140 | 90 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
141 | | elfzofz 12485 |
. . . . . . . . . . . . . . 15
..^
|
142 | 141 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
143 | 140, 142 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
..^ |
144 | | fzofzp1 12565 |
. . . . . . . . . . . . . . 15
..^
|
145 | 144 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
146 | 140, 145 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
..^ |
147 | 8 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
148 | 87 | simprrd 797 |
. . . . . . . . . . . . . 14
..^ |
149 | 148 | r19.21bi 2932 |
. . . . . . . . . . . . 13
..^ |
150 | 143, 146,
147, 149 | ltadd1dd 10638 |
. . . . . . . . . . . 12
..^ |
151 | 143, 147 | readdcld 10069 |
. . . . . . . . . . . . 13
..^ |
152 | 94 | fvmpt2 6291 |
. . . . . . . . . . . . 13
|
153 | 142, 151,
152 | syl2anc 693 |
. . . . . . . . . . . 12
..^ |
154 | 94, 18 | eqtr4i 2647 |
. . . . . . . . . . . . . 14
|
155 | 154 | a1i 11 |
. . . . . . . . . . . . 13
..^ |
156 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
157 | 156 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
158 | 157 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
159 | 146, 147 | readdcld 10069 |
. . . . . . . . . . . . 13
..^ |
160 | 155, 158,
145, 159 | fvmptd 6288 |
. . . . . . . . . . . 12
..^ |
161 | 150, 153,
160 | 3brtr4d 4685 |
. . . . . . . . . . 11
..^ |
162 | 161 | ralrimiva 2966 |
. . . . . . . . . 10
..^ |
163 | 101, 139,
162 | jca32 558 |
. . . . . . . . 9
..^ |
164 | | fourierdlem92.h |
. . . . . . . . . . 11
..^
|
165 | 164 | fourierdlem2 40326 |
. . . . . . . . . 10
..^ |
166 | 6, 165 | syl 17 |
. . . . . . . . 9
..^ |
167 | 163, 166 | mpbird 247 |
. . . . . . . 8
|
168 | 164 | fveq1i 6192 |
. . . . . . . 8
..^ |
169 | 167, 168 | syl6eleq 2711 |
. . . . . . 7
..^
|
170 | 169 | adantr 481 |
. . . . . 6
..^ |
171 | 60 | adantr 481 |
. . . . . . . . . . . 12
|
172 | 66 | adantr 481 |
. . . . . . . . . . . 12
|
173 | | simpr 477 |
. . . . . . . . . . . 12
|
174 | | eliccre 39728 |
. . . . . . . . . . . 12
|
175 | 171, 172,
173, 174 | syl3anc 1326 |
. . . . . . . . . . 11
|
176 | 175 | recnd 10068 |
. . . . . . . . . 10
|
177 | 62 | negcld 10379 |
. . . . . . . . . . 11
|
178 | 177 | adantr 481 |
. . . . . . . . . 10
|
179 | 176, 178 | addcld 10059 |
. . . . . . . . 9
|
180 | | simpl 473 |
. . . . . . . . . 10
|
181 | 1 | adantr 481 |
. . . . . . . . . . 11
|
182 | 3 | adantr 481 |
. . . . . . . . . . 11
|
183 | 8 | renegcld 10457 |
. . . . . . . . . . . . 13
|
184 | 183 | adantr 481 |
. . . . . . . . . . . 12
|
185 | 175, 184 | readdcld 10069 |
. . . . . . . . . . 11
|
186 | 63, 64 | eqtr2d 2657 |
. . . . . . . . . . . . 13
|
187 | 186 | adantr 481 |
. . . . . . . . . . . 12
|
188 | 171 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
189 | 172 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
190 | | iccgelb 12230 |
. . . . . . . . . . . . . 14
|
191 | 188, 189,
173, 190 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
192 | 171, 175,
184, 191 | leadd1dd 10641 |
. . . . . . . . . . . 12
|
193 | 187, 192 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
194 | | iccleub 12229 |
. . . . . . . . . . . . . 14
|
195 | 188, 189,
173, 194 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
196 | 175, 172,
184, 195 | leadd1dd 10641 |
. . . . . . . . . . . 12
|
197 | 172 | recnd 10068 |
. . . . . . . . . . . . . 14
|
198 | 62 | adantr 481 |
. . . . . . . . . . . . . 14
|
199 | 197, 198 | negsubd 10398 |
. . . . . . . . . . . . 13
|
200 | 69 | adantr 481 |
. . . . . . . . . . . . 13
|
201 | 199, 200 | eqtrd 2656 |
. . . . . . . . . . . 12
|
202 | 196, 201 | breqtrd 4679 |
. . . . . . . . . . 11
|
203 | 181, 182,
185, 193, 202 | eliccd 39726 |
. . . . . . . . . 10
|
204 | 180, 203 | jca 554 |
. . . . . . . . 9
|
205 | | eleq1 2689 |
. . . . . . . . . . . 12
|
206 | 205 | anbi2d 740 |
. . . . . . . . . . 11
|
207 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
208 | 207 | fveq2d 6195 |
. . . . . . . . . . . 12
|
209 | | fveq2 6191 |
. . . . . . . . . . . 12
|
210 | 208, 209 | eqeq12d 2637 |
. . . . . . . . . . 11
|
211 | 206, 210 | imbi12d 334 |
. . . . . . . . . 10
|
212 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
213 | 212 | anbi2d 740 |
. . . . . . . . . . . 12
|
214 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
215 | 214 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
216 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
217 | 215, 216 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
218 | 213, 217 | imbi12d 334 |
. . . . . . . . . . 11
|
219 | 218, 14 | chvarv 2263 |
. . . . . . . . . 10
|
220 | 211, 219 | vtoclg 3266 |
. . . . . . . . 9
|
221 | 179, 204,
220 | sylc 65 |
. . . . . . . 8
|
222 | 176, 198 | negsubd 10398 |
. . . . . . . . . . 11
|
223 | 222 | oveq1d 6665 |
. . . . . . . . . 10
|
224 | 176, 198 | npcand 10396 |
. . . . . . . . . 10
|
225 | 223, 224 | eqtrd 2656 |
. . . . . . . . 9
|
226 | 225 | fveq2d 6195 |
. . . . . . . 8
|
227 | 221, 226 | eqtr3d 2658 |
. . . . . . 7
|
228 | 227 | adantlr 751 |
. . . . . 6
|
229 | | fveq2 6191 |
. . . . . . . 8
|
230 | 229 | oveq1d 6665 |
. . . . . . 7
|
231 | 230 | cbvmptv 4750 |
. . . . . 6
|
232 | 19 | adantr 481 |
. . . . . 6
|
233 | 19 | adantr 481 |
. . . . . . . . . 10
..^ |
234 | | ioossre 12235 |
. . . . . . . . . . 11
|
235 | 234 | a1i 11 |
. . . . . . . . . 10
..^ |
236 | 233, 235 | feqresmpt 6250 |
. . . . . . . . 9
..^ |
237 | 153, 160 | oveq12d 6668 |
. . . . . . . . . . 11
..^ |
238 | 143, 146,
147 | iooshift 39748 |
. . . . . . . . . . 11
..^
|
239 | 237, 238 | eqtrd 2656 |
. . . . . . . . . 10
..^
|
240 | 239 | mpteq1d 4738 |
. . . . . . . . 9
..^
|
241 | | simpll 790 |
. . . . . . . . . . . . 13
..^
|
242 | | simplr 792 |
. . . . . . . . . . . . 13
..^
..^ |
243 | 238 | eleq2d 2687 |
. . . . . . . . . . . . . 14
..^
|
244 | 243 | biimpar 502 |
. . . . . . . . . . . . 13
..^
|
245 | 143 | rexrd 10089 |
. . . . . . . . . . . . . . 15
..^ |
246 | 245 | 3adant3 1081 |
. . . . . . . . . . . . . 14
..^
|
247 | 146 | rexrd 10089 |
. . . . . . . . . . . . . . 15
..^ |
248 | 247 | 3adant3 1081 |
. . . . . . . . . . . . . 14
..^
|
249 | | elioore 12205 |
. . . . . . . . . . . . . . . . 17
|
250 | 249 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
251 | 8 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
252 | 250, 251 | resubcld 10458 |
. . . . . . . . . . . . . . 15
|
253 | 252 | 3adant2 1080 |
. . . . . . . . . . . . . 14
..^
|
254 | 143 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
..^ |
255 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
..^ |
256 | 254, 255 | pncand 10393 |
. . . . . . . . . . . . . . . . 17
..^ |
257 | 256 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
..^ |
258 | 257 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
..^
|
259 | 151 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
..^
|
260 | 250 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
..^
|
261 | 8 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
..^
|
262 | 151 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
..^ |
263 | 262 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
..^
|
264 | 159 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
..^ |
265 | 264 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
..^
|
266 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
..^
|
267 | | ioogtlb 39717 |
. . . . . . . . . . . . . . . . 17
|
268 | 263, 265,
266, 267 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
..^
|
269 | 259, 260,
261, 268 | ltsub1dd 10639 |
. . . . . . . . . . . . . . 15
..^
|
270 | 258, 269 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
..^
|
271 | 159 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
..^
|
272 | | iooltub 39735 |
. . . . . . . . . . . . . . . . 17
|
273 | 263, 265,
266, 272 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
..^
|
274 | 260, 271,
261, 273 | ltsub1dd 10639 |
. . . . . . . . . . . . . . 15
..^
|
275 | 146 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
..^ |
276 | 275, 255 | pncand 10393 |
. . . . . . . . . . . . . . . 16
..^ |
277 | 276 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
..^
|
278 | 274, 277 | breqtrd 4679 |
. . . . . . . . . . . . . 14
..^
|
279 | 246, 248,
253, 270, 278 | eliood 39720 |
. . . . . . . . . . . . 13
..^
|
280 | 241, 242,
244, 279 | syl3anc 1326 |
. . . . . . . . . . . 12
..^
|
281 | | fvres 6207 |
. . . . . . . . . . . 12
|
282 | 280, 281 | syl 17 |
. . . . . . . . . . 11
..^
|
283 | 241, 244,
252 | syl2anc 693 |
. . . . . . . . . . . 12
..^
|
284 | 1 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
..^
|
285 | 3 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
..^
|
286 | 64 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
287 | 286 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
..^
|
288 | 60 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
..^
|
289 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
290 | 1 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
291 | 290 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
292 | 3 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
293 | 292 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
294 | 5, 6, 12 | fourierdlem15 40339 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
295 | 294 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
296 | 295, 142 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
297 | | iccgelb 12230 |
. . . . . . . . . . . . . . . . . . . . . 22
|
298 | 291, 293,
296, 297 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
299 | 289, 143,
147, 298 | leadd1dd 10641 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
300 | 299 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . 19
..^
|
301 | 288, 259,
260, 300, 268 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . 18
..^
|
302 | 288, 260,
261, 301 | ltsub1dd 10639 |
. . . . . . . . . . . . . . . . 17
..^
|
303 | 287, 302 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . 16
..^
|
304 | 284, 253,
303 | ltled 10185 |
. . . . . . . . . . . . . . 15
..^
|
305 | 146 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
..^
|
306 | 295, 145 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
..^ |
307 | | iccleub 12229 |
. . . . . . . . . . . . . . . . . . 19
|
308 | 291, 293,
306, 307 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
..^ |
309 | 308 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
..^
|
310 | 253, 305,
285, 278, 309 | ltletrd 10197 |
. . . . . . . . . . . . . . . 16
..^
|
311 | 253, 285,
310 | ltled 10185 |
. . . . . . . . . . . . . . 15
..^
|
312 | 284, 285,
253, 304, 311 | eliccd 39726 |
. . . . . . . . . . . . . 14
..^
|
313 | 241, 242,
244, 312 | syl3anc 1326 |
. . . . . . . . . . . . 13
..^
|
314 | 241, 313 | jca 554 |
. . . . . . . . . . . 12
..^
|
315 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
316 | 315 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
317 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
318 | 317 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
319 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
320 | 318, 319 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
|
321 | 316, 320 | imbi12d 334 |
. . . . . . . . . . . . 13
|
322 | 321, 219 | vtoclg 3266 |
. . . . . . . . . . . 12
|
323 | 283, 314,
322 | sylc 65 |
. . . . . . . . . . 11
..^
|
324 | 244, 249 | syl 17 |
. . . . . . . . . . . 12
..^
|
325 | | recn 10026 |
. . . . . . . . . . . . . . 15
|
326 | 325 | adantl 482 |
. . . . . . . . . . . . . 14
|
327 | 62 | adantr 481 |
. . . . . . . . . . . . . 14
|
328 | 326, 327 | npcand 10396 |
. . . . . . . . . . . . 13
|
329 | 328 | fveq2d 6195 |
. . . . . . . . . . . 12
|
330 | 241, 324,
329 | syl2anc 693 |
. . . . . . . . . . 11
..^
|
331 | 282, 323,
330 | 3eqtr2rd 2663 |
. . . . . . . . . 10
..^
|
332 | 331 | mpteq2dva 4744 |
. . . . . . . . 9
..^ |
333 | 236, 240,
332 | 3eqtrd 2660 |
. . . . . . . 8
..^ |
334 | | ioosscn 39716 |
. . . . . . . . . . 11
|
335 | 334 | a1i 11 |
. . . . . . . . . 10
..^ |
336 | | eqeq1 2626 |
. . . . . . . . . . . . 13
|
337 | 336 | rexbidv 3052 |
. . . . . . . . . . . 12
|
338 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
339 | 338 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
340 | 339 | cbvrexv 3172 |
. . . . . . . . . . . 12
|
341 | 337, 340 | syl6bb 276 |
. . . . . . . . . . 11
|
342 | 341 | cbvrabv 3199 |
. . . . . . . . . 10
|
343 | | eqid 2622 |
. . . . . . . . . 10
|
344 | 335, 255,
342, 21, 343 | cncfshift 40087 |
. . . . . . . . 9
..^ |
345 | 239 | eqcomd 2628 |
. . . . . . . . . 10
..^ |
346 | 345 | oveq1d 6665 |
. . . . . . . . 9
..^ |
347 | 344, 346 | eleqtrd 2703 |
. . . . . . . 8
..^ |
348 | 333, 347 | eqeltrd 2701 |
. . . . . . 7
..^ |
349 | 348 | adantlr 751 |
. . . . . 6
..^ |
350 | | ffdm 6062 |
. . . . . . . . . . . 12
|
351 | 19, 350 | syl 17 |
. . . . . . . . . . 11
|
352 | 351 | simpld 475 |
. . . . . . . . . 10
|
353 | 352 | adantr 481 |
. . . . . . . . 9
..^ |
354 | | ioossre 12235 |
. . . . . . . . . 10
|
355 | | fdm 6051 |
. . . . . . . . . . 11
|
356 | 233, 355 | syl 17 |
. . . . . . . . . 10
..^
|
357 | 354, 356 | syl5sseqr 3654 |
. . . . . . . . 9
..^ |
358 | 342 | eqcomi 2631 |
. . . . . . . . 9
|
359 | 235, 345,
356 | 3sstr4d 3648 |
. . . . . . . . . 10
..^
|
360 | 342, 359 | syl5eqssr 3650 |
. . . . . . . . 9
..^
|
361 | | simpll 790 |
. . . . . . . . . 10
..^ |
362 | 361, 290 | syl 17 |
. . . . . . . . . . 11
..^ |
363 | 361, 292 | syl 17 |
. . . . . . . . . . 11
..^ |
364 | 361, 294 | syl 17 |
. . . . . . . . . . 11
..^ |
365 | | simplr 792 |
. . . . . . . . . . 11
..^ ..^ |
366 | | ioossicc 12259 |
. . . . . . . . . . . . 13
|
367 | 366 | sseli 3599 |
. . . . . . . . . . . 12
|
368 | 367 | adantl 482 |
. . . . . . . . . . 11
..^ |
369 | 362, 363,
364, 365, 368 | fourierdlem1 40325 |
. . . . . . . . . 10
..^ |
370 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
371 | 370 | anbi2d 740 |
. . . . . . . . . . . 12
|
372 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
373 | 372 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
374 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
375 | 373, 374 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
376 | 371, 375 | imbi12d 334 |
. . . . . . . . . . 11
|
377 | 376, 14 | chvarv 2263 |
. . . . . . . . . 10
|
378 | 361, 369,
377 | syl2anc 693 |
. . . . . . . . 9
..^ |
379 | 353, 335,
357, 255, 358, 360, 378, 23 | limcperiod 39860 |
. . . . . . . 8
..^ lim |
380 | 358, 345 | syl5eq 2668 |
. . . . . . . . . 10
..^ |
381 | 380 | reseq2d 5396 |
. . . . . . . . 9
..^
|
382 | 153 | eqcomd 2628 |
. . . . . . . . 9
..^ |
383 | 381, 382 | oveq12d 6668 |
. . . . . . . 8
..^ lim lim |
384 | 379, 383 | eleqtrd 2703 |
. . . . . . 7
..^ lim |
385 | 384 | adantlr 751 |
. . . . . 6
..^
lim |
386 | 353, 335,
357, 255, 358, 360, 378, 25 | limcperiod 39860 |
. . . . . . . 8
..^ lim |
387 | 160 | eqcomd 2628 |
. . . . . . . . 9
..^ |
388 | 381, 387 | oveq12d 6668 |
. . . . . . . 8
..^ lim lim |
389 | 386, 388 | eleqtrd 2703 |
. . . . . . 7
..^ lim |
390 | 389 | adantlr 751 |
. . . . . 6
..^
lim |
391 | | eqeq1 2626 |
. . . . . . . 8
|
392 | | eqeq1 2626 |
. . . . . . . . 9
|
393 | 392, 29 | ifbieq2d 4111 |
. . . . . . . 8
|
394 | 391, 393 | ifbieq2d 4111 |
. . . . . . 7
|
395 | 394 | cbvmptv 4750 |
. . . . . 6
|
396 | | eqid 2622 |
. . . . . 6
|
397 | 77, 79, 80, 81, 84, 170, 228, 231, 232, 349, 385, 390, 395, 396 | fourierdlem81 40404 |
. . . . 5
|
398 | 74, 397 | eqtr2d 2657 |
. . . 4
|
399 | 49, 59, 398 | syl2anc 693 |
. . 3
|
400 | 48, 399 | pm2.61dan 832 |
. 2
|
401 | 34, 400 | pm2.61dan 832 |
1
|