Step | Hyp | Ref
| Expression |
1 | | fourierdlem91.q |
. . . . . . . . . . . 12
|
2 | | fourierdlem91.m |
. . . . . . . . . . . . 13
|
3 | | fourierdlem91.p |
. . . . . . . . . . . . . 14
..^ |
4 | 3 | fourierdlem2 40326 |
. . . . . . . . . . . . 13
..^ |
5 | 2, 4 | syl 17 |
. . . . . . . . . . . 12
..^ |
6 | 1, 5 | mpbid 222 |
. . . . . . . . . . 11
..^ |
7 | 6 | simpld 475 |
. . . . . . . . . 10
|
8 | | elmapi 7879 |
. . . . . . . . . 10
|
9 | 7, 8 | syl 17 |
. . . . . . . . 9
|
10 | | fzossfz 12488 |
. . . . . . . . . 10
..^ |
11 | | fourierdlem91.t |
. . . . . . . . . . . . 13
|
12 | | fourierdlem91.e |
. . . . . . . . . . . . 13
|
13 | | fourierdlem91.J |
. . . . . . . . . . . . 13
|
14 | | fourierdlem91.i |
. . . . . . . . . . . . 13
..^ |
15 | 3, 2, 1, 11, 12, 13, 14 | fourierdlem37 40361 |
. . . . . . . . . . . 12
..^
..^ ..^ |
16 | 15 | simpld 475 |
. . . . . . . . . . 11
..^ |
17 | | fourierdlem91.c |
. . . . . . . . . . . . . . . . . 18
|
18 | | fourierdlem91.d |
. . . . . . . . . . . . . . . . . . 19
|
19 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
21 | | elioo4g 12234 |
. . . . . . . . . . . . . . . . . . . . 21
|
22 | 18, 21 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
|
23 | 22 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
|
24 | 23 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
25 | | fourierdlem91.o |
. . . . . . . . . . . . . . . . . 18
..^ |
26 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
27 | 26 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
|
28 | 27 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 28 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | uneq2i 3764 |
. . . . . . . . . . . . . . . . . 18
|
31 | | fourierdlem91.n |
. . . . . . . . . . . . . . . . . . 19
|
32 | | fourierdlem91.h |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | 32 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 33 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 31, 34 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
36 | | fourierdlem91.s |
. . . . . . . . . . . . . . . . . . 19
|
37 | | isoeq5 6571 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 32, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 38 | iotabii 5873 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 36, 39 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
41 | 11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40 | fourierdlem54 40377 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | simpld 475 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | simprd 479 |
. . . . . . . . . . . . . . 15
|
44 | 42 | simpld 475 |
. . . . . . . . . . . . . . . 16
|
45 | 25 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . 16
..^ |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
47 | 43, 46 | mpbid 222 |
. . . . . . . . . . . . . 14
..^ |
48 | 47 | simpld 475 |
. . . . . . . . . . . . 13
|
49 | | elmapi 7879 |
. . . . . . . . . . . . 13
|
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
|
51 | | fourierdlem91.17 |
. . . . . . . . . . . . 13
..^ |
52 | | elfzofz 12485 |
. . . . . . . . . . . . 13
..^
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
|
54 | 50, 53 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
55 | 16, 54 | ffvelrnd 6360 |
. . . . . . . . . 10
..^ |
56 | 10, 55 | sseldi 3601 |
. . . . . . . . 9
|
57 | 9, 56 | ffvelrnd 6360 |
. . . . . . . 8
|
58 | 57 | rexrd 10089 |
. . . . . . 7
|
59 | 58 | adantr 481 |
. . . . . 6
|
60 | | fzofzp1 12565 |
. . . . . . . . . 10
..^
|
61 | 55, 60 | syl 17 |
. . . . . . . . 9
|
62 | 9, 61 | ffvelrnd 6360 |
. . . . . . . 8
|
63 | 62 | rexrd 10089 |
. . . . . . 7
|
64 | 63 | adantr 481 |
. . . . . 6
|
65 | 3, 2, 1 | fourierdlem11 40335 |
. . . . . . . . . . 11
|
66 | 65 | simp1d 1073 |
. . . . . . . . . 10
|
67 | 66 | rexrd 10089 |
. . . . . . . . 9
|
68 | 65 | simp2d 1074 |
. . . . . . . . 9
|
69 | | iocssre 12253 |
. . . . . . . . 9
|
70 | 67, 68, 69 | syl2anc 693 |
. . . . . . . 8
|
71 | 65 | simp3d 1075 |
. . . . . . . . . 10
|
72 | 66, 68, 71, 11, 12 | fourierdlem4 40328 |
. . . . . . . . 9
|
73 | | fzofzp1 12565 |
. . . . . . . . . . 11
..^
|
74 | 51, 73 | syl 17 |
. . . . . . . . . 10
|
75 | 50, 74 | ffvelrnd 6360 |
. . . . . . . . 9
|
76 | 72, 75 | ffvelrnd 6360 |
. . . . . . . 8
|
77 | 70, 76 | sseldd 3604 |
. . . . . . 7
|
78 | 77 | adantr 481 |
. . . . . 6
|
79 | 66, 68 | iccssred 39727 |
. . . . . . . . 9
|
80 | 66, 68, 71, 13 | fourierdlem17 40341 |
. . . . . . . . . 10
|
81 | 72, 54 | ffvelrnd 6360 |
. . . . . . . . . 10
|
82 | 80, 81 | ffvelrnd 6360 |
. . . . . . . . 9
|
83 | 79, 82 | sseldd 3604 |
. . . . . . . 8
|
84 | 47 | simprrd 797 |
. . . . . . . . . . . . . 14
..^ |
85 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
86 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
87 | 86 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
88 | 85, 87 | breq12d 4666 |
. . . . . . . . . . . . . . 15
|
89 | 88 | rspccva 3308 |
. . . . . . . . . . . . . 14
..^ ..^
|
90 | 84, 51, 89 | syl2anc 693 |
. . . . . . . . . . . . 13
|
91 | 54, 75 | posdifd 10614 |
. . . . . . . . . . . . 13
|
92 | 90, 91 | mpbid 222 |
. . . . . . . . . . . 12
|
93 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
94 | 93 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
..^
..^ |
95 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
97 | 96 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
98 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
101 | 97, 100 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
102 | 96, 98 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
103 | 101, 102 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
104 | 94, 103 | imbi12d 334 |
. . . . . . . . . . . . . . 15
..^
..^
|
105 | 11 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
106 | 105 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
107 | 106 | eleq1i 2692 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
108 | 107 | rexbii 3041 |
. . . . . . . . . . . . . . . . . . . . . 22
|
109 | 108 | rgenw 2924 |
. . . . . . . . . . . . . . . . . . . . 21
|
110 | | rabbi 3120 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | 109, 110 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 111 | uneq2i 3764 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 112 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . 18
|
114 | 113 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
115 | 35, 114 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
|
116 | | isoeq5 6571 |
. . . . . . . . . . . . . . . . . . 19
|
117 | 112, 116 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
118 | 117 | iotabii 5873 |
. . . . . . . . . . . . . . . . 17
|
119 | 40, 118 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
|
120 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
121 | 3, 11, 2, 1, 17, 18, 25, 115, 119, 12, 13, 120 | fourierdlem65 40388 |
. . . . . . . . . . . . . . 15
..^ |
122 | 104, 121 | vtoclg 3266 |
. . . . . . . . . . . . . 14
..^
..^
|
123 | 122 | anabsi7 860 |
. . . . . . . . . . . . 13
..^
|
124 | 51, 123 | mpdan 702 |
. . . . . . . . . . . 12
|
125 | 92, 124 | breqtrrd 4681 |
. . . . . . . . . . 11
|
126 | 83, 77 | posdifd 10614 |
. . . . . . . . . . 11
|
127 | 125, 126 | mpbird 247 |
. . . . . . . . . 10
|
128 | 100, 97 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
129 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
130 | 129 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
131 | 129 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
133 | 130, 132 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
134 | 128, 133 | sseq12d 3634 |
. . . . . . . . . . . . . 14
|
135 | 94, 134 | imbi12d 334 |
. . . . . . . . . . . . 13
..^ ..^
|
136 | 32, 30 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
137 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
138 | 11, 3, 2, 1, 17, 20, 24, 25, 136, 31, 36, 12, 13, 137, 14 | fourierdlem79 40402 |
. . . . . . . . . . . . 13
..^ |
139 | 135, 138 | vtoclg 3266 |
. . . . . . . . . . . 12
..^
..^ |
140 | 139 | anabsi7 860 |
. . . . . . . . . . 11
..^ |
141 | 51, 140 | mpdan 702 |
. . . . . . . . . 10
|
142 | 57, 62, 83, 77, 127, 141 | fourierdlem10 40334 |
. . . . . . . . 9
|
143 | 142 | simpld 475 |
. . . . . . . 8
|
144 | 57, 83, 77, 143, 127 | lelttrd 10195 |
. . . . . . 7
|
145 | 144 | adantr 481 |
. . . . . 6
|
146 | 62 | adantr 481 |
. . . . . . 7
|
147 | 142 | simprd 479 |
. . . . . . . 8
|
148 | 147 | adantr 481 |
. . . . . . 7
|
149 | | neqne 2802 |
. . . . . . . . 9
|
150 | 149 | necomd 2849 |
. . . . . . . 8
|
151 | 150 | adantl 482 |
. . . . . . 7
|
152 | 78, 146, 148, 151 | leneltd 10191 |
. . . . . 6
|
153 | 59, 64, 78, 145, 152 | eliood 39720 |
. . . . 5
|
154 | | fvres 6207 |
. . . . 5
|
155 | 153, 154 | syl 17 |
. . . 4
|
156 | 155 | eqcomd 2628 |
. . 3
|
157 | 156 | ifeq2da 4117 |
. 2
|
158 | | fourierdlem91.f |
. . . . . 6
|
159 | | fdm 6051 |
. . . . . . . 8
|
160 | 158, 159 | syl 17 |
. . . . . . 7
|
161 | 160 | feq2d 6031 |
. . . . . 6
|
162 | 158, 161 | mpbird 247 |
. . . . 5
|
163 | | ioosscn 39716 |
. . . . . 6
|
164 | 163 | a1i 11 |
. . . . 5
|
165 | | ioossre 12235 |
. . . . . 6
|
166 | 165, 160 | syl5sseqr 3654 |
. . . . 5
|
167 | | fourierdlem91.u |
. . . . . . 7
|
168 | 75, 77 | resubcld 10458 |
. . . . . . 7
|
169 | 167, 168 | syl5eqel 2705 |
. . . . . 6
|
170 | 169 | recnd 10068 |
. . . . 5
|
171 | | eqid 2622 |
. . . . 5
|
172 | 83, 77, 169 | iooshift 39748 |
. . . . . 6
|
173 | | ioossre 12235 |
. . . . . . 7
|
174 | 173, 160 | syl5sseqr 3654 |
. . . . . 6
|
175 | 172, 174 | eqsstr3d 3640 |
. . . . 5
|
176 | | elioore 12205 |
. . . . . 6
|
177 | 68, 66 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
178 | 11, 177 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
179 | 178 | recnd 10068 |
. . . . . . . . . . . 12
|
180 | 66, 68 | posdifd 10614 |
. . . . . . . . . . . . . . 15
|
181 | 71, 180 | mpbid 222 |
. . . . . . . . . . . . . 14
|
182 | 181, 11 | syl6breqr 4695 |
. . . . . . . . . . . . 13
|
183 | 182 | gt0ne0d 10592 |
. . . . . . . . . . . 12
|
184 | 170, 179,
183 | divcan1d 10802 |
. . . . . . . . . . 11
|
185 | 184 | eqcomd 2628 |
. . . . . . . . . 10
|
186 | 185 | oveq2d 6666 |
. . . . . . . . 9
|
187 | 186 | adantr 481 |
. . . . . . . 8
|
188 | 187 | fveq2d 6195 |
. . . . . . 7
|
189 | 158 | adantr 481 |
. . . . . . . 8
|
190 | 178 | adantr 481 |
. . . . . . . 8
|
191 | 77 | recnd 10068 |
. . . . . . . . . . . . . 14
|
192 | 75 | recnd 10068 |
. . . . . . . . . . . . . 14
|
193 | 191, 192 | negsubdi2d 10408 |
. . . . . . . . . . . . 13
|
194 | 193 | eqcomd 2628 |
. . . . . . . . . . . 12
|
195 | 194 | oveq1d 6665 |
. . . . . . . . . . 11
|
196 | 167 | oveq1i 6660 |
. . . . . . . . . . . 12
|
197 | 196 | a1i 11 |
. . . . . . . . . . 11
|
198 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
199 | | id 22 |
. . . . . . . . . . . . . . . . . 18
|
200 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
|
201 | 200 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
202 | 201 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
203 | 202 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
204 | 199, 203 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
205 | 204 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
206 | 68, 75 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . 21
|
207 | 206, 178,
183 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . . 20
|
208 | 207 | flcld 12599 |
. . . . . . . . . . . . . . . . . . 19
|
209 | 208 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
210 | 209, 178 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
|
211 | 75, 210 | readdcld 10069 |
. . . . . . . . . . . . . . . 16
|
212 | 198, 205,
75, 211 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
|
213 | 212 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
214 | 208 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
215 | 214, 179 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
216 | 192, 215 | pncan2d 10394 |
. . . . . . . . . . . . . 14
|
217 | 213, 216 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
218 | 217, 215 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
219 | 218, 179,
183 | divnegd 10814 |
. . . . . . . . . . 11
|
220 | 195, 197,
219 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
221 | 217 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
222 | 214, 179,
183 | divcan4d 10807 |
. . . . . . . . . . . . 13
|
223 | 221, 222 | eqtrd 2656 |
. . . . . . . . . . . 12
|
224 | 223, 208 | eqeltrd 2701 |
. . . . . . . . . . 11
|
225 | 224 | znegcld 11484 |
. . . . . . . . . 10
|
226 | 220, 225 | eqeltrd 2701 |
. . . . . . . . 9
|
227 | 226 | adantr 481 |
. . . . . . . 8
|
228 | | simpr 477 |
. . . . . . . 8
|
229 | | fourierdlem91.6 |
. . . . . . . . 9
|
230 | 229 | adantlr 751 |
. . . . . . . 8
|
231 | 189, 190,
227, 228, 230 | fperiodmul 39518 |
. . . . . . 7
|
232 | 188, 231 | eqtrd 2656 |
. . . . . 6
|
233 | 176, 232 | sylan2 491 |
. . . . 5
|
234 | 6 | simprrd 797 |
. . . . . . . 8
..^ |
235 | | fveq2 6191 |
. . . . . . . . . 10
|
236 | | oveq1 6657 |
. . . . . . . . . . 11
|
237 | 236 | fveq2d 6195 |
. . . . . . . . . 10
|
238 | 235, 237 | breq12d 4666 |
. . . . . . . . 9
|
239 | 238 | rspccva 3308 |
. . . . . . . 8
..^ ..^
|
240 | 234, 55, 239 | syl2anc 693 |
. . . . . . 7
|
241 | 55 | ancli 574 |
. . . . . . . 8
..^ |
242 | | eleq1 2689 |
. . . . . . . . . . 11
..^ ..^ |
243 | 242 | anbi2d 740 |
. . . . . . . . . 10
..^
..^ |
244 | 235, 237 | oveq12d 6668 |
. . . . . . . . . . . 12
|
245 | 244 | reseq2d 5396 |
. . . . . . . . . . 11
|
246 | 244 | oveq1d 6665 |
. . . . . . . . . . 11
|
247 | 245, 246 | eleq12d 2695 |
. . . . . . . . . 10
|
248 | 243, 247 | imbi12d 334 |
. . . . . . . . 9
..^
..^ |
249 | | fourierdlem91.fcn |
. . . . . . . . 9
..^ |
250 | 248, 249 | vtoclg 3266 |
. . . . . . . 8
..^
..^ |
251 | 55, 241, 250 | sylc 65 |
. . . . . . 7
|
252 | | nfv 1843 |
. . . . . . . . . 10
..^ |
253 | | fourierdlem91.w |
. . . . . . . . . . . . 13
..^ |
254 | | nfmpt1 4747 |
. . . . . . . . . . . . 13
..^ |
255 | 253, 254 | nfcxfr 2762 |
. . . . . . . . . . . 12
|
256 | | nfcv 2764 |
. . . . . . . . . . . 12
|
257 | 255, 256 | nffv 6198 |
. . . . . . . . . . 11
|
258 | 257 | nfel1 2779 |
. . . . . . . . . 10
lim |
259 | 252, 258 | nfim 1825 |
. . . . . . . . 9
..^ lim |
260 | 243 | biimpar 502 |
. . . . . . . . . . . . . 14
..^ ..^ |
261 | 260 | 3adant2 1080 |
. . . . . . . . . . . . 13
..^
lim ..^
..^ |
262 | | fourierdlem91.l |
. . . . . . . . . . . . 13
..^ lim |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . 12
..^
lim ..^ lim |
264 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
265 | 264 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
266 | 265 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
267 | 260 | simprd 479 |
. . . . . . . . . . . . . . 15
..^ ..^ |
268 | | elex 3212 |
. . . . . . . . . . . . . . . 16
lim
|
269 | 260, 262,
268 | 3syl 18 |
. . . . . . . . . . . . . . 15
..^ |
270 | 253 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
..^ |
271 | 267, 269,
270 | syl2anc 693 |
. . . . . . . . . . . . . 14
..^ |
272 | 266, 271 | eqtrd 2656 |
. . . . . . . . . . . . 13
..^ |
273 | 272 | 3adant2 1080 |
. . . . . . . . . . . 12
..^
lim ..^ |
274 | 245, 237 | oveq12d 6668 |
. . . . . . . . . . . . . 14
lim
lim |
275 | 274 | eqcomd 2628 |
. . . . . . . . . . . . 13
lim lim |
276 | 275 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
..^
lim ..^ lim lim |
277 | 263, 273,
276 | 3eltr4d 2716 |
. . . . . . . . . . 11
..^
lim ..^ lim |
278 | 277 | 3exp 1264 |
. . . . . . . . . 10
..^
lim
..^
lim |
279 | 262 | 2a1i 12 |
. . . . . . . . . 10
..^
lim
..^
lim |
280 | 278, 279 | impbid 202 |
. . . . . . . . 9
..^
lim
..^ lim |
281 | 259, 280,
262 | vtoclg1f 3265 |
. . . . . . . 8
..^
..^ lim |
282 | 55, 241, 281 | sylc 65 |
. . . . . . 7
lim |
283 | | eqid 2622 |
. . . . . . 7
|
284 | | eqid 2622 |
. . . . . . 7
ℂfld ↾t ℂfld
↾t |
285 | 57, 62, 240, 251, 282, 83, 77, 127, 141, 283, 284 | fourierdlem33 40357 |
. . . . . 6
lim |
286 | 141 | resabs1d 5428 |
. . . . . . 7
|
287 | 286 | oveq1d 6665 |
. . . . . 6
lim
lim |
288 | 285, 287 | eleqtrd 2703 |
. . . . 5
lim |
289 | 162, 164,
166, 170, 171, 175, 233, 288 | limcperiod 39860 |
. . . 4
lim |
290 | 167 | oveq2i 6661 |
. . . . . 6
|
291 | 191, 192 | pncan3d 10395 |
. . . . . 6
|
292 | 290, 291 | syl5eq 2668 |
. . . . 5
|
293 | 292 | oveq2d 6666 |
. . . 4
lim
lim |
294 | 289, 293 | eleqtrd 2703 |
. . 3
lim |
295 | 167 | oveq2i 6661 |
. . . . . . . . 9
|
296 | 295 | a1i 11 |
. . . . . . . 8
|
297 | 17, 20 | iccssred 39727 |
. . . . . . . . . . . . . . 15
|
298 | | ax-resscn 9993 |
. . . . . . . . . . . . . . 15
|
299 | 297, 298 | syl6ss 3615 |
. . . . . . . . . . . . . 14
|
300 | 25, 44, 43 | fourierdlem15 40339 |
. . . . . . . . . . . . . . 15
|
301 | 300, 53 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
302 | 299, 301 | sseldd 3604 |
. . . . . . . . . . . . 13
|
303 | 192, 302 | subcld 10392 |
. . . . . . . . . . . 12
|
304 | 83 | recnd 10068 |
. . . . . . . . . . . 12
|
305 | 191, 303,
304 | subsub23d 39499 |
. . . . . . . . . . 11
|
306 | 124, 305 | mpbird 247 |
. . . . . . . . . 10
|
307 | 306 | eqcomd 2628 |
. . . . . . . . 9
|
308 | 307 | oveq1d 6665 |
. . . . . . . 8
|
309 | 191, 303 | subcld 10392 |
. . . . . . . . . 10
|
310 | 309, 192,
191 | addsub12d 10415 |
. . . . . . . . 9
|
311 | 191, 303,
191 | sub32d 10424 |
. . . . . . . . . . 11
|
312 | 191 | subidd 10380 |
. . . . . . . . . . . 12
|
313 | 312 | oveq1d 6665 |
. . . . . . . . . . 11
|
314 | | df-neg 10269 |
. . . . . . . . . . . 12
|
315 | 192, 302 | negsubdi2d 10408 |
. . . . . . . . . . . 12
|
316 | 314, 315 | syl5eqr 2670 |
. . . . . . . . . . 11
|
317 | 311, 313,
316 | 3eqtrd 2660 |
. . . . . . . . . 10
|
318 | 317 | oveq2d 6666 |
. . . . . . . . 9
|
319 | 192, 302 | pncan3d 10395 |
. . . . . . . . 9
|
320 | 310, 318,
319 | 3eqtrd 2660 |
. . . . . . . 8
|
321 | 296, 308,
320 | 3eqtrd 2660 |
. . . . . . 7
|
322 | 321, 292 | oveq12d 6668 |
. . . . . 6
|
323 | 172, 322 | eqtr3d 2658 |
. . . . 5
|
324 | 323 | reseq2d 5396 |
. . . 4
|
325 | 324 | oveq1d 6665 |
. . 3
lim
lim |
326 | 294, 325 | eleqtrd 2703 |
. 2
lim |
327 | 157, 326 | eqeltrd 2701 |
1
lim |