Step | Hyp | Ref
| Expression |
1 | | fourierdlem39.a |
. 2
|
2 | | fourierdlem39.b |
. 2
|
3 | | fourierdlem39.aleb |
. 2
|
4 | | fourierdlem39.f |
. . . . . 6
|
5 | | cncff 22696 |
. . . . . 6
|
6 | 4, 5 | syl 17 |
. . . . 5
|
7 | 6 | feqmptd 6249 |
. . . 4
|
8 | 7 | eqcomd 2628 |
. . 3
|
9 | 8, 4 | eqeltrd 2701 |
. 2
|
10 | | coscn 24199 |
. . . . . 6
|
11 | 10 | a1i 11 |
. . . . 5
|
12 | 1, 2 | iccssred 39727 |
. . . . . . . 8
|
13 | | ax-resscn 9993 |
. . . . . . . 8
|
14 | 12, 13 | syl6ss 3615 |
. . . . . . 7
|
15 | | fourierdlem39.r |
. . . . . . . . 9
|
16 | 15 | rpred 11872 |
. . . . . . . 8
|
17 | 16 | recnd 10068 |
. . . . . . 7
|
18 | | ssid 3624 |
. . . . . . . 8
|
19 | 18 | a1i 11 |
. . . . . . 7
|
20 | 14, 17, 19 | constcncfg 40084 |
. . . . . 6
|
21 | 14, 19 | idcncfg 40085 |
. . . . . 6
|
22 | 20, 21 | mulcncf 23215 |
. . . . 5
|
23 | 11, 22 | cncfmpt1f 22716 |
. . . 4
|
24 | 15 | rpcnne0d 11881 |
. . . . . 6
|
25 | | eldifsn 4317 |
. . . . . 6
|
26 | 24, 25 | sylibr 224 |
. . . . 5
|
27 | | difssd 3738 |
. . . . 5
|
28 | 14, 26, 27 | constcncfg 40084 |
. . . 4
|
29 | 23, 28 | divcncf 23216 |
. . 3
|
30 | 29 | negcncfg 40094 |
. 2
|
31 | | fourierdlem39.gcn |
. . . . . 6
|
32 | | cncff 22696 |
. . . . . 6
|
33 | 31, 32 | syl 17 |
. . . . 5
|
34 | 33 | feqmptd 6249 |
. . . 4
|
35 | 34 | eqcomd 2628 |
. . 3
|
36 | 35, 31 | eqeltrd 2701 |
. 2
|
37 | | sincn 24198 |
. . . 4
|
38 | 37 | a1i 11 |
. . 3
|
39 | | ioosscn 39716 |
. . . . . 6
|
40 | 39 | a1i 11 |
. . . . 5
|
41 | 40, 17, 19 | constcncfg 40084 |
. . . 4
|
42 | 40, 19 | idcncfg 40085 |
. . . 4
|
43 | 41, 42 | mulcncf 23215 |
. . 3
|
44 | 38, 43 | cncfmpt1f 22716 |
. 2
|
45 | | ioombl 23333 |
. . . 4
|
46 | 45 | a1i 11 |
. . 3
|
47 | | volioo 23337 |
. . . . 5
|
48 | 1, 2, 3, 47 | syl3anc 1326 |
. . . 4
|
49 | 2, 1 | resubcld 10458 |
. . . 4
|
50 | 48, 49 | eqeltrd 2701 |
. . 3
|
51 | | eqid 2622 |
. . . . 5
|
52 | | ioossicc 12259 |
. . . . . 6
|
53 | 52 | a1i 11 |
. . . . 5
|
54 | 6 | adantr 481 |
. . . . . 6
|
55 | 53 | sselda 3603 |
. . . . . 6
|
56 | 54, 55 | ffvelrnd 6360 |
. . . . 5
|
57 | 51, 9, 53, 19, 56 | cncfmptssg 40083 |
. . . 4
|
58 | 57, 44 | mulcncf 23215 |
. . 3
|
59 | | cniccbdd 23230 |
. . . . . 6
|
60 | 1, 2, 4, 59 | syl3anc 1326 |
. . . . 5
|
61 | | nfra1 2941 |
. . . . . . . 8
|
62 | 52 | sseli 3599 |
. . . . . . . . . 10
|
63 | | rspa 2930 |
. . . . . . . . . 10
|
64 | 62, 63 | sylan2 491 |
. . . . . . . . 9
|
65 | 64 | ex 450 |
. . . . . . . 8
|
66 | 61, 65 | ralrimi 2957 |
. . . . . . 7
|
67 | 66 | a1i 11 |
. . . . . 6
|
68 | 67 | reximdva 3017 |
. . . . 5
|
69 | 60, 68 | mpd 15 |
. . . 4
|
70 | | nfv 1843 |
. . . . . . . 8
|
71 | | nfra1 2941 |
. . . . . . . 8
|
72 | 70, 71 | nfan 1828 |
. . . . . . 7
|
73 | | simpll 790 |
. . . . . . . . 9
|
74 | | simpr 477 |
. . . . . . . . . . 11
|
75 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
76 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
78 | 75, 77 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
|
79 | 78 | resincld 14873 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
81 | 56, 80 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
82 | 81 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
83 | | dmmptg 5632 |
. . . . . . . . . . . . 13
|
84 | 82, 83 | syl 17 |
. . . . . . . . . . . 12
|
85 | 84 | adantr 481 |
. . . . . . . . . . 11
|
86 | 74, 85 | eleqtrd 2703 |
. . . . . . . . . 10
|
87 | 86 | ad4ant14 1293 |
. . . . . . . . 9
|
88 | | simplr 792 |
. . . . . . . . . . 11
|
89 | 86 | adantlr 751 |
. . . . . . . . . . 11
|
90 | | rspa 2930 |
. . . . . . . . . . 11
|
91 | 88, 89, 90 | syl2anc 693 |
. . . . . . . . . 10
|
92 | 91 | adantllr 755 |
. . . . . . . . 9
|
93 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
94 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
95 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
97 | 94, 96 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
99 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
100 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
101 | 52, 99 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
|
102 | 100, 101 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
103 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 39, 99 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 103, 104 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
106 | 105 | sincld 14860 |
. . . . . . . . . . . . . . . . 17
|
107 | 102, 106 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
108 | 93, 98, 99, 107 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
|
109 | 108 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
110 | 102, 106 | absmuld 14193 |
. . . . . . . . . . . . . 14
|
111 | 109, 110 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
112 | 111 | adantlr 751 |
. . . . . . . . . . . 12
|
113 | 112 | adantr 481 |
. . . . . . . . . . 11
|
114 | | simplll 798 |
. . . . . . . . . . . . . . 15
|
115 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
116 | 114, 115,
102 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
117 | 116 | abscld 14175 |
. . . . . . . . . . . . 13
|
118 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
119 | 39, 115 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
|
120 | 118, 119 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
121 | 120 | sincld 14860 |
. . . . . . . . . . . . . 14
|
122 | 121 | abscld 14175 |
. . . . . . . . . . . . 13
|
123 | 117, 122 | remulcld 10070 |
. . . . . . . . . . . 12
|
124 | | 1red 10055 |
. . . . . . . . . . . . 13
|
125 | 117, 124 | remulcld 10070 |
. . . . . . . . . . . 12
|
126 | | simpllr 799 |
. . . . . . . . . . . . 13
|
127 | 126, 124 | remulcld 10070 |
. . . . . . . . . . . 12
|
128 | 106 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
129 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
130 | 102 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
131 | 102 | absge0d 14183 |
. . . . . . . . . . . . . . 15
|
132 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
133 | | elioore 12205 |
. . . . . . . . . . . . . . . . . 18
|
134 | 133 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
135 | 132, 134 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
136 | | abssinbd 39509 |
. . . . . . . . . . . . . . . 16
|
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . 15
|
138 | 128, 129,
130, 131, 137 | lemul2ad 10964 |
. . . . . . . . . . . . . 14
|
139 | 138 | adantlr 751 |
. . . . . . . . . . . . 13
|
140 | 139 | adantr 481 |
. . . . . . . . . . . 12
|
141 | | 0le1 10551 |
. . . . . . . . . . . . . 14
|
142 | 141 | a1i 11 |
. . . . . . . . . . . . 13
|
143 | | simpr 477 |
. . . . . . . . . . . . 13
|
144 | 117, 126,
124, 142, 143 | lemul1ad 10963 |
. . . . . . . . . . . 12
|
145 | 123, 125,
127, 140, 144 | letrd 10194 |
. . . . . . . . . . 11
|
146 | 113, 145 | eqbrtrd 4675 |
. . . . . . . . . 10
|
147 | 126 | recnd 10068 |
. . . . . . . . . . 11
|
148 | 147 | mulid1d 10057 |
. . . . . . . . . 10
|
149 | 146, 148 | breqtrd 4679 |
. . . . . . . . 9
|
150 | 73, 87, 92, 149 | syl21anc 1325 |
. . . . . . . 8
|
151 | 150 | ex 450 |
. . . . . . 7
|
152 | 72, 151 | ralrimi 2957 |
. . . . . 6
|
153 | 152 | ex 450 |
. . . . 5
|
154 | 153 | reximdva 3017 |
. . . 4
|
155 | 69, 154 | mpd 15 |
. . 3
|
156 | 46, 50, 58, 155 | cnbdibl 40178 |
. 2
|
157 | 11, 43 | cncfmpt1f 22716 |
. . . . . 6
|
158 | 40, 26, 27 | constcncfg 40084 |
. . . . . 6
|
159 | 157, 158 | divcncf 23216 |
. . . . 5
|
160 | 159 | negcncfg 40094 |
. . . 4
|
161 | 36, 160 | mulcncf 23215 |
. . 3
|
162 | | simpr 477 |
. . . . . . 7
|
163 | 16 | adantr 481 |
. . . . . . 7
|
164 | 15 | rpne0d 11877 |
. . . . . . . 8
|
165 | 164 | adantr 481 |
. . . . . . 7
|
166 | 162, 163,
165 | redivcld 10853 |
. . . . . 6
|
167 | 166 | adantr 481 |
. . . . 5
|
168 | | simpr 477 |
. . . . . . . . 9
|
169 | 33 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
170 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
171 | 76 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
173 | 170, 172 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
174 | 173 | coscld 14861 |
. . . . . . . . . . . . . . 15
|
175 | 164 | adantr 481 |
. . . . . . . . . . . . . . 15
|
176 | 174, 170,
175 | divcld 10801 |
. . . . . . . . . . . . . 14
|
177 | 176 | negcld 10379 |
. . . . . . . . . . . . 13
|
178 | 169, 177 | mulcld 10060 |
. . . . . . . . . . . 12
|
179 | 178 | ralrimiva 2966 |
. . . . . . . . . . 11
|
180 | 179 | adantr 481 |
. . . . . . . . . 10
|
181 | | dmmptg 5632 |
. . . . . . . . . 10
|
182 | 180, 181 | syl 17 |
. . . . . . . . 9
|
183 | 168, 182 | eleqtrd 2703 |
. . . . . . . 8
|
184 | 183 | ad4ant14 1293 |
. . . . . . 7
|
185 | | eqidd 2623 |
. . . . . . . . . . 11
|
186 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
187 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
188 | 187 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
189 | 188 | negeqd 10275 |
. . . . . . . . . . . . 13
|
190 | 186, 189 | oveq12d 6668 |
. . . . . . . . . . . 12
|
191 | 190 | adantl 482 |
. . . . . . . . . . 11
|
192 | 33 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
193 | 105 | coscld 14861 |
. . . . . . . . . . . . . 14
|
194 | 164 | adantr 481 |
. . . . . . . . . . . . . 14
|
195 | 193, 103,
194 | divcld 10801 |
. . . . . . . . . . . . 13
|
196 | 195 | negcld 10379 |
. . . . . . . . . . . 12
|
197 | 192, 196 | mulcld 10060 |
. . . . . . . . . . 11
|
198 | 185, 191,
99, 197 | fvmptd 6288 |
. . . . . . . . . 10
|
199 | 198 | fveq2d 6195 |
. . . . . . . . 9
|
200 | 199 | ad4ant14 1293 |
. . . . . . . 8
|
201 | 33 | ad2antrr 762 |
. . . . . . . . . . . 12
|
202 | 201 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
203 | 202 | abscld 14175 |
. . . . . . . . . 10
|
204 | | simpllr 799 |
. . . . . . . . . 10
|
205 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
206 | 104 | ad4ant14 1293 |
. . . . . . . . . . . . . . 15
|
207 | 205, 206 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
208 | 207 | coscld 14861 |
. . . . . . . . . . . . 13
|
209 | 164 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
210 | 208, 205,
209 | divcld 10801 |
. . . . . . . . . . . 12
|
211 | 210 | negcld 10379 |
. . . . . . . . . . 11
|
212 | 211 | abscld 14175 |
. . . . . . . . . 10
|
213 | 15 | rprecred 11883 |
. . . . . . . . . . 11
|
214 | 213 | ad3antrrr 766 |
. . . . . . . . . 10
|
215 | 202 | absge0d 14183 |
. . . . . . . . . 10
|
216 | 211 | absge0d 14183 |
. . . . . . . . . 10
|
217 | 186 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
218 | 217 | breq1d 4663 |
. . . . . . . . . . . 12
|
219 | 218 | rspccva 3308 |
. . . . . . . . . . 11
|
220 | 219 | adantll 750 |
. . . . . . . . . 10
|
221 | 195 | absnegd 14188 |
. . . . . . . . . . . . 13
|
222 | 193, 103,
194 | absdivd 14194 |
. . . . . . . . . . . . 13
|
223 | 15 | rpge0d 11876 |
. . . . . . . . . . . . . . . 16
|
224 | 16, 223 | absidd 14161 |
. . . . . . . . . . . . . . 15
|
225 | 224 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
226 | 225 | adantr 481 |
. . . . . . . . . . . . 13
|
227 | 221, 222,
226 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
228 | 193 | abscld 14175 |
. . . . . . . . . . . . 13
|
229 | 15 | adantr 481 |
. . . . . . . . . . . . 13
|
230 | | abscosbd 39490 |
. . . . . . . . . . . . . 14
|
231 | 135, 230 | syl 17 |
. . . . . . . . . . . . 13
|
232 | 228, 129,
229, 231 | lediv1dd 11930 |
. . . . . . . . . . . 12
|
233 | 227, 232 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
234 | 233 | ad4ant14 1293 |
. . . . . . . . . 10
|
235 | 203, 204,
212, 214, 215, 216, 220, 234 | lemul12ad 10966 |
. . . . . . . . 9
|
236 | 192, 196 | absmuld 14193 |
. . . . . . . . . 10
|
237 | 236 | ad4ant14 1293 |
. . . . . . . . 9
|
238 | 204 | recnd 10068 |
. . . . . . . . . 10
|
239 | 238, 205,
209 | divrecd 10804 |
. . . . . . . . 9
|
240 | 235, 237,
239 | 3brtr4d 4685 |
. . . . . . . 8
|
241 | 200, 240 | eqbrtrd 4675 |
. . . . . . 7
|
242 | 184, 241 | syldan 487 |
. . . . . 6
|
243 | 242 | ralrimiva 2966 |
. . . . 5
|
244 | | breq2 4657 |
. . . . . . 7
|
245 | 244 | ralbidv 2986 |
. . . . . 6
|
246 | 245 | rspcev 3309 |
. . . . 5
|
247 | 167, 243,
246 | syl2anc 693 |
. . . 4
|
248 | | fourierdlem39.gbd |
. . . 4
|
249 | 247, 248 | r19.29a 3078 |
. . 3
|
250 | 46, 50, 161, 249 | cnbdibl 40178 |
. 2
|
251 | 8 | oveq2d 6666 |
. . 3
|
252 | | fourierdlem39.g |
. . . . 5
|
253 | 252 | eqcomi 2631 |
. . . 4
|
254 | 253 | a1i 11 |
. . 3
|
255 | 251, 254,
34 | 3eqtrd 2660 |
. 2
|
256 | | reelprrecn 10028 |
. . . . 5
|
257 | 256 | a1i 11 |
. . . 4
|
258 | 17 | adantr 481 |
. . . . . . . 8
|
259 | | recn 10026 |
. . . . . . . . 9
|
260 | 259 | adantl 482 |
. . . . . . . 8
|
261 | 258, 260 | mulcld 10060 |
. . . . . . 7
|
262 | 261 | coscld 14861 |
. . . . . 6
|
263 | 164 | adantr 481 |
. . . . . 6
|
264 | 262, 258,
263 | divcld 10801 |
. . . . 5
|
265 | 264 | negcld 10379 |
. . . 4
|
266 | 16 | adantr 481 |
. . . . . . . . . 10
|
267 | | simpr 477 |
. . . . . . . . . 10
|
268 | 266, 267 | remulcld 10070 |
. . . . . . . . 9
|
269 | 268 | resincld 14873 |
. . . . . . . 8
|
270 | 269 | renegcld 10457 |
. . . . . . 7
|
271 | 270, 266 | remulcld 10070 |
. . . . . 6
|
272 | 271, 266,
263 | redivcld 10853 |
. . . . 5
|
273 | 272 | renegcld 10457 |
. . . 4
|
274 | | recoscl 14871 |
. . . . . . . . 9
|
275 | 274 | adantl 482 |
. . . . . . . 8
|
276 | 275 | recnd 10068 |
. . . . . . 7
|
277 | | resincl 14870 |
. . . . . . . . 9
|
278 | 277 | renegcld 10457 |
. . . . . . . 8
|
279 | 278 | adantl 482 |
. . . . . . 7
|
280 | | 1red 10055 |
. . . . . . . . 9
|
281 | 257 | dvmptid 23720 |
. . . . . . . . 9
|
282 | 257, 260,
280, 281, 17 | dvmptcmul 23727 |
. . . . . . . 8
|
283 | 258 | mulid1d 10057 |
. . . . . . . . 9
|
284 | 283 | mpteq2dva 4744 |
. . . . . . . 8
|
285 | 282, 284 | eqtrd 2656 |
. . . . . . 7
|
286 | | dvcosre 40126 |
. . . . . . . 8
|
287 | 286 | a1i 11 |
. . . . . . 7
|
288 | | fveq2 6191 |
. . . . . . 7
|
289 | | fveq2 6191 |
. . . . . . . 8
|
290 | 289 | negeqd 10275 |
. . . . . . 7
|
291 | 257, 257,
268, 266, 276, 279, 285, 287, 288, 290 | dvmptco 23735 |
. . . . . 6
|
292 | 257, 262,
271, 291, 17, 164 | dvmptdivc 23728 |
. . . . 5
|
293 | 257, 264,
272, 292 | dvmptneg 23729 |
. . . 4
|
294 | | eqid 2622 |
. . . . 5
ℂfld ℂfld |
295 | 294 | tgioo2 22606 |
. . . 4
ℂfld
↾t |
296 | | iccntr 22624 |
. . . . 5
|
297 | 1, 2, 296 | syl2anc 693 |
. . . 4
|
298 | 257, 265,
273, 293, 12, 295, 294, 297 | dvmptres2 23725 |
. . 3
|
299 | 80, 170 | mulneg1d 10483 |
. . . . . . . 8
|
300 | 299 | oveq1d 6665 |
. . . . . . 7
|
301 | 80, 170 | mulcld 10060 |
. . . . . . . 8
|
302 | 301, 170,
175 | divnegd 10814 |
. . . . . . 7
|
303 | 300, 302 | eqtr4d 2659 |
. . . . . 6
|
304 | 303 | negeqd 10275 |
. . . . 5
|
305 | 301, 170,
175 | divcld 10801 |
. . . . . 6
|
306 | 305 | negnegd 10383 |
. . . . 5
|
307 | 80, 170, 175 | divcan4d 10807 |
. . . . 5
|
308 | 304, 306,
307 | 3eqtrd 2660 |
. . . 4
|
309 | 308 | mpteq2dva 4744 |
. . 3
|
310 | 298, 309 | eqtrd 2656 |
. 2
|
311 | | fveq2 6191 |
. . . 4
|
312 | | oveq2 6658 |
. . . . . . 7
|
313 | 312 | fveq2d 6195 |
. . . . . 6
|
314 | 313 | oveq1d 6665 |
. . . . 5
|
315 | 314 | negeqd 10275 |
. . . 4
|
316 | 311, 315 | oveq12d 6668 |
. . 3
|
317 | 316 | adantl 482 |
. 2
|
318 | | fveq2 6191 |
. . . 4
|
319 | | oveq2 6658 |
. . . . . . 7
|
320 | 319 | fveq2d 6195 |
. . . . . 6
|
321 | 320 | oveq1d 6665 |
. . . . 5
|
322 | 321 | negeqd 10275 |
. . . 4
|
323 | 318, 322 | oveq12d 6668 |
. . 3
|
324 | 323 | adantl 482 |
. 2
|
325 | 1, 2, 3, 9, 30, 36, 44, 156, 250, 255, 310, 317, 324 | itgparts 23810 |
1
|