Step | Hyp | Ref
| Expression |
1 | | fourierdlem88.o |
. 2
..^ |
2 | | fourierdlem88.m |
. 2
|
3 | | pire 24210 |
. . . . 5
|
4 | 3 | a1i 11 |
. . . 4
|
5 | 4 | renegcld 10457 |
. . 3
|
6 | | fourierdlem88.v |
. . . . . . 7
|
7 | | fourierdlem88.1 |
. . . . . . . . 9
..^ |
8 | 7 | fourierdlem2 40326 |
. . . . . . . 8
..^ |
9 | 2, 8 | syl 17 |
. . . . . . 7
..^ |
10 | 6, 9 | mpbid 222 |
. . . . . 6
..^ |
11 | 10 | simpld 475 |
. . . . 5
|
12 | | elmapi 7879 |
. . . . 5
|
13 | | frn 6053 |
. . . . 5
|
14 | 11, 12, 13 | 3syl 18 |
. . . 4
|
15 | | fourierdlem88.x |
. . . 4
|
16 | 14, 15 | sseldd 3604 |
. . 3
|
17 | | fourierdlem88.q |
. . 3
|
18 | 5, 4, 16, 7, 1, 2,
6, 17 | fourierdlem14 40338 |
. 2
|
19 | | fourierdlem88.f |
. . . . . . 7
|
20 | | ioossre 12235 |
. . . . . . . . . 10
|
21 | 20 | a1i 11 |
. . . . . . . . 9
|
22 | 19, 21 | fssresd 6071 |
. . . . . . . 8
|
23 | | ax-resscn 9993 |
. . . . . . . . 9
|
24 | 21, 23 | syl6ss 3615 |
. . . . . . . 8
|
25 | | eqid 2622 |
. . . . . . . . 9
ℂfld ℂfld |
26 | | pnfxr 10092 |
. . . . . . . . . 10
|
27 | 26 | a1i 11 |
. . . . . . . . 9
|
28 | 16 | ltpnfd 11955 |
. . . . . . . . 9
|
29 | 25, 27, 16, 28 | lptioo1cn 39878 |
. . . . . . . 8
ℂfld |
30 | | fourierdlem88.y |
. . . . . . . 8
lim |
31 | 22, 24, 29, 30 | limcrecl 39861 |
. . . . . . 7
|
32 | | ioossre 12235 |
. . . . . . . . . 10
|
33 | 32 | a1i 11 |
. . . . . . . . 9
|
34 | 19, 33 | fssresd 6071 |
. . . . . . . 8
|
35 | 33, 23 | syl6ss 3615 |
. . . . . . . 8
|
36 | | mnfxr 10096 |
. . . . . . . . . 10
|
37 | 36 | a1i 11 |
. . . . . . . . 9
|
38 | 16 | mnfltd 11958 |
. . . . . . . . 9
|
39 | 25, 37, 16, 38 | lptioo2cn 39877 |
. . . . . . . 8
ℂfld |
40 | | fourierdlem88.w |
. . . . . . . 8
lim |
41 | 34, 35, 39, 40 | limcrecl 39861 |
. . . . . . 7
|
42 | | fourierdlem88.h |
. . . . . . 7
|
43 | | fourierdlem88.k |
. . . . . . 7
|
44 | | fourierdlem88.u |
. . . . . . 7
|
45 | 19, 16, 31, 41, 42, 43, 44 | fourierdlem55 40378 |
. . . . . 6
|
46 | 45 | ffvelrnda 6359 |
. . . . 5
|
47 | | fourierdlem88.n |
. . . . . . 7
|
48 | | fourierdlem88.s |
. . . . . . . 8
|
49 | 48 | fourierdlem5 40329 |
. . . . . . 7
|
50 | 47, 49 | syl 17 |
. . . . . 6
|
51 | 50 | ffvelrnda 6359 |
. . . . 5
|
52 | 46, 51 | remulcld 10070 |
. . . 4
|
53 | 52 | recnd 10068 |
. . 3
|
54 | | fourierdlem88.g |
. . 3
|
55 | 53, 54 | fmptd 6385 |
. 2
|
56 | | ssid 3624 |
. . . 4
|
57 | | cncfss 22702 |
. . . 4
|
58 | 23, 56, 57 | mp2an 708 |
. . 3
|
59 | 19 | adantr 481 |
. . . 4
..^ |
60 | 1, 2, 18 | fourierdlem15 40339 |
. . . . . 6
|
61 | 60 | adantr 481 |
. . . . 5
..^ |
62 | | elfzofz 12485 |
. . . . . 6
..^
|
63 | 62 | adantl 482 |
. . . . 5
..^ |
64 | 61, 63 | ffvelrnd 6360 |
. . . 4
..^ |
65 | | fzofzp1 12565 |
. . . . . 6
..^
|
66 | 65 | adantl 482 |
. . . . 5
..^ |
67 | 61, 66 | ffvelrnd 6360 |
. . . 4
..^ |
68 | 16 | adantr 481 |
. . . 4
..^ |
69 | 7, 2, 6, 15 | fourierdlem12 40336 |
. . . . . 6
..^
|
70 | 68 | recnd 10068 |
. . . . . . . 8
..^ |
71 | 70 | addid2d 10237 |
. . . . . . 7
..^ |
72 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^ |
73 | 72 | renegcld 10457 |
. . . . . . . . . . . . . . 15
..^ |
74 | 73, 68 | readdcld 10069 |
. . . . . . . . . . . . . 14
..^ |
75 | 72, 68 | readdcld 10069 |
. . . . . . . . . . . . . 14
..^ |
76 | 74, 75 | iccssred 39727 |
. . . . . . . . . . . . 13
..^ |
77 | 7, 2, 6 | fourierdlem15 40339 |
. . . . . . . . . . . . . . 15
|
78 | 77 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
79 | 78, 63 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
..^ |
80 | 76, 79 | sseldd 3604 |
. . . . . . . . . . . 12
..^ |
81 | 80, 68 | resubcld 10458 |
. . . . . . . . . . 11
..^ |
82 | 17 | fvmpt2 6291 |
. . . . . . . . . . 11
|
83 | 63, 81, 82 | syl2anc 693 |
. . . . . . . . . 10
..^ |
84 | 83 | oveq1d 6665 |
. . . . . . . . 9
..^ |
85 | 80 | recnd 10068 |
. . . . . . . . . 10
..^ |
86 | 85, 70 | npcand 10396 |
. . . . . . . . 9
..^ |
87 | 84, 86 | eqtrd 2656 |
. . . . . . . 8
..^ |
88 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
89 | 88 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
90 | 89 | cbvmptv 4750 |
. . . . . . . . . . . . 13
|
91 | 17, 90 | eqtri 2644 |
. . . . . . . . . . . 12
|
92 | 91 | a1i 11 |
. . . . . . . . . . 11
..^ |
93 | | simpr 477 |
. . . . . . . . . . . . 13
..^ |
94 | 93 | fveq2d 6195 |
. . . . . . . . . . . 12
..^ |
95 | 94 | oveq1d 6665 |
. . . . . . . . . . 11
..^ |
96 | 78, 66 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
..^ |
97 | 76, 96 | sseldd 3604 |
. . . . . . . . . . . 12
..^ |
98 | 97, 68 | resubcld 10458 |
. . . . . . . . . . 11
..^ |
99 | 92, 95, 66, 98 | fvmptd 6288 |
. . . . . . . . . 10
..^ |
100 | 99 | oveq1d 6665 |
. . . . . . . . 9
..^ |
101 | 97 | recnd 10068 |
. . . . . . . . . 10
..^ |
102 | 101, 70 | npcand 10396 |
. . . . . . . . 9
..^ |
103 | 100, 102 | eqtrd 2656 |
. . . . . . . 8
..^ |
104 | 87, 103 | oveq12d 6668 |
. . . . . . 7
..^ |
105 | 71, 104 | eleq12d 2695 |
. . . . . 6
..^
|
106 | 69, 105 | mtbird 315 |
. . . . 5
..^
|
107 | | 0red 10041 |
. . . . . 6
..^ |
108 | 83, 81 | eqeltrd 2701 |
. . . . . 6
..^ |
109 | 99, 98 | eqeltrd 2701 |
. . . . . 6
..^ |
110 | 107, 108,
109, 68 | eliooshift 39729 |
. . . . 5
..^ |
111 | 106, 110 | mtbird 315 |
. . . 4
..^
|
112 | | fourierdlem88.fcn |
. . . . 5
..^ |
113 | 104 | reseq2d 5396 |
. . . . 5
..^
|
114 | 104 | oveq1d 6665 |
. . . . 5
..^ |
115 | 112, 113,
114 | 3eltr4d 2716 |
. . . 4
..^ |
116 | 31 | adantr 481 |
. . . 4
..^ |
117 | 41 | adantr 481 |
. . . 4
..^ |
118 | 47 | adantr 481 |
. . . 4
..^ |
119 | 59, 64, 67, 68, 111, 115, 116, 117, 42, 43, 44, 118, 48, 54 | fourierdlem78 40401 |
. . 3
..^ |
120 | 58, 119 | sseldi 3601 |
. 2
..^ |
121 | | eqid 2622 |
. . . 4
|
122 | | eqid 2622 |
. . . 4
|
123 | | eqid 2622 |
. . . 4
|
124 | 3 | renegcli 10342 |
. . . . . . . . . . 11
|
125 | 124 | rexri 10097 |
. . . . . . . . . 10
|
126 | 125 | a1i 11 |
. . . . . . . . 9
..^ |
127 | 3 | rexri 10097 |
. . . . . . . . . 10
|
128 | 127 | a1i 11 |
. . . . . . . . 9
..^ |
129 | 61 | adantr 481 |
. . . . . . . . 9
..^ |
130 | | simplr 792 |
. . . . . . . . 9
..^ ..^ |
131 | 126, 128,
129, 130 | fourierdlem8 40332 |
. . . . . . . 8
..^ |
132 | | ioossicc 12259 |
. . . . . . . . . 10
|
133 | 132 | sseli 3599 |
. . . . . . . . 9
|
134 | 133 | adantl 482 |
. . . . . . . 8
..^ |
135 | 131, 134 | sseldd 3604 |
. . . . . . 7
..^ |
136 | 19, 16, 31, 41, 42 | fourierdlem9 40333 |
. . . . . . . . . 10
|
137 | 136 | ad2antrr 762 |
. . . . . . . . 9
..^ |
138 | 137, 135 | ffvelrnd 6360 |
. . . . . . . 8
..^ |
139 | 43 | fourierdlem43 40367 |
. . . . . . . . . 10
|
140 | 139 | a1i 11 |
. . . . . . . . 9
..^ |
141 | 140, 135 | ffvelrnd 6360 |
. . . . . . . 8
..^ |
142 | 138, 141 | remulcld 10070 |
. . . . . . 7
..^ |
143 | 44 | fvmpt2 6291 |
. . . . . . 7
|
144 | 135, 142,
143 | syl2anc 693 |
. . . . . 6
..^ |
145 | 144, 142 | eqeltrd 2701 |
. . . . 5
..^ |
146 | 145 | recnd 10068 |
. . . 4
..^ |
147 | 47, 48 | fourierdlem18 40342 |
. . . . . . . . 9
|
148 | | cncff 22696 |
. . . . . . . . 9
|
149 | 147, 148 | syl 17 |
. . . . . . . 8
|
150 | 149 | adantr 481 |
. . . . . . 7
..^ |
151 | 150 | adantr 481 |
. . . . . 6
..^ |
152 | 151, 135 | ffvelrnd 6360 |
. . . . 5
..^ |
153 | 152 | recnd 10068 |
. . . 4
..^ |
154 | | eqid 2622 |
. . . . . 6
|
155 | | eqid 2622 |
. . . . . 6
|
156 | | eqid 2622 |
. . . . . 6
|
157 | 138 | recnd 10068 |
. . . . . 6
..^ |
158 | 141 | recnd 10068 |
. . . . . 6
..^ |
159 | | fourierdlem88.r |
. . . . . . . 8
..^ lim |
160 | | fourierdlem88.i |
. . . . . . . 8
|
161 | | fourierdlem88.ifn |
. . . . . . . . 9
..^ |
162 | 23 | a1i 11 |
. . . . . . . . 9
..^ |
163 | 161, 162 | fssd 6057 |
. . . . . . . 8
..^ |
164 | | fourierdlem88.d |
. . . . . . . 8
lim |
165 | | eqid 2622 |
. . . . . . . 8
|
166 | 16, 7, 19, 15, 30, 41, 42, 2, 6, 159, 17, 1, 160, 163, 164, 165 | fourierdlem75 40398 |
. . . . . . 7
..^ lim |
167 | 136 | adantr 481 |
. . . . . . . . 9
..^ |
168 | 125 | a1i 11 |
. . . . . . . . . . 11
..^ |
169 | 127 | a1i 11 |
. . . . . . . . . . 11
..^ |
170 | | simpr 477 |
. . . . . . . . . . 11
..^ ..^ |
171 | 168, 169,
61, 170 | fourierdlem8 40332 |
. . . . . . . . . 10
..^ |
172 | 132, 171 | syl5ss 3614 |
. . . . . . . . 9
..^ |
173 | 167, 172 | feqresmpt 6250 |
. . . . . . . 8
..^ |
174 | 173 | oveq1d 6665 |
. . . . . . 7
..^ lim lim |
175 | 166, 174 | eleqtrd 2703 |
. . . . . 6
..^ lim |
176 | | limcresi 23649 |
. . . . . . . 8
lim lim |
177 | 43 | fourierdlem62 40385 |
. . . . . . . . . 10
|
178 | 177 | a1i 11 |
. . . . . . . . 9
..^ |
179 | 178, 64 | cnlimci 23653 |
. . . . . . . 8
..^ lim |
180 | 176, 179 | sseldi 3601 |
. . . . . . 7
..^
lim |
181 | 139 | a1i 11 |
. . . . . . . . 9
..^ |
182 | 181, 172 | feqresmpt 6250 |
. . . . . . . 8
..^ |
183 | 182 | oveq1d 6665 |
. . . . . . 7
..^ lim lim |
184 | 180, 183 | eleqtrd 2703 |
. . . . . 6
..^ lim |
185 | 154, 155,
156, 157, 158, 175, 184 | mullimc 39848 |
. . . . 5
..^
lim |
186 | 144 | eqcomd 2628 |
. . . . . . 7
..^ |
187 | 186 | mpteq2dva 4744 |
. . . . . 6
..^ |
188 | 187 | oveq1d 6665 |
. . . . 5
..^ lim lim |
189 | 185, 188 | eleqtrd 2703 |
. . . 4
..^
lim |
190 | | limcresi 23649 |
. . . . . 6
lim lim |
191 | 147 | adantr 481 |
. . . . . . 7
..^ |
192 | 191, 64 | cnlimci 23653 |
. . . . . 6
..^ lim |
193 | 190, 192 | sseldi 3601 |
. . . . 5
..^
lim |
194 | 150, 172 | feqresmpt 6250 |
. . . . . 6
..^ |
195 | 194 | oveq1d 6665 |
. . . . 5
..^ lim lim |
196 | 193, 195 | eleqtrd 2703 |
. . . 4
..^ lim |
197 | 121, 122,
123, 146, 153, 189, 196 | mullimc 39848 |
. . 3
..^ lim |
198 | 52, 54 | fmptd 6385 |
. . . . . . 7
|
199 | 198 | adantr 481 |
. . . . . 6
..^ |
200 | 199, 172 | feqresmpt 6250 |
. . . . 5
..^ |
201 | 145, 152 | remulcld 10070 |
. . . . . . 7
..^ |
202 | 54 | fvmpt2 6291 |
. . . . . . 7
|
203 | 135, 201,
202 | syl2anc 693 |
. . . . . 6
..^ |
204 | 203 | mpteq2dva 4744 |
. . . . 5
..^ |
205 | 200, 204 | eqtr2d 2657 |
. . . 4
..^ |
206 | 205 | oveq1d 6665 |
. . 3
..^ lim lim |
207 | 197, 206 | eleqtrd 2703 |
. 2
..^ lim |
208 | | fourierdlem88.l |
. . . . . . . 8
..^ lim |
209 | | fourierdlem88.c |
. . . . . . . 8
lim |
210 | | eqid 2622 |
. . . . . . . 8
|
211 | 16, 7, 19, 15, 31, 40, 42, 2, 6, 208, 17, 1, 160, 161, 209, 210 | fourierdlem74 40397 |
. . . . . . 7
..^ lim |
212 | 173 | oveq1d 6665 |
. . . . . . 7
..^ lim lim |
213 | 211, 212 | eleqtrd 2703 |
. . . . . 6
..^ lim |
214 | | limcresi 23649 |
. . . . . . . 8
lim lim |
215 | 178, 67 | cnlimci 23653 |
. . . . . . . 8
..^ lim |
216 | 214, 215 | sseldi 3601 |
. . . . . . 7
..^
lim |
217 | 182 | oveq1d 6665 |
. . . . . . 7
..^ lim lim |
218 | 216, 217 | eleqtrd 2703 |
. . . . . 6
..^ lim |
219 | 154, 155,
156, 157, 158, 213, 218 | mullimc 39848 |
. . . . 5
..^
lim |
220 | 187 | oveq1d 6665 |
. . . . 5
..^ lim lim |
221 | 219, 220 | eleqtrd 2703 |
. . . 4
..^
lim |
222 | | limcresi 23649 |
. . . . . 6
lim lim |
223 | 191, 67 | cnlimci 23653 |
. . . . . 6
..^ lim |
224 | 222, 223 | sseldi 3601 |
. . . . 5
..^
lim |
225 | 194 | oveq1d 6665 |
. . . . 5
..^ lim lim |
226 | 224, 225 | eleqtrd 2703 |
. . . 4
..^ lim |
227 | 121, 122,
123, 146, 153, 221, 226 | mullimc 39848 |
. . 3
..^ lim |
228 | 205 | oveq1d 6665 |
. . 3
..^ lim lim |
229 | 227, 228 | eleqtrd 2703 |
. 2
..^ lim |
230 | 1, 2, 18, 55, 120, 207, 229 | fourierdlem69 40392 |
1
|