Step | Hyp | Ref
| Expression |
1 | | fourierdlem76.ch |
. . 3
..^
..^
|
2 | | eqid 2622 |
. . . . 5
|
3 | | eqid 2622 |
. . . . 5
|
4 | | eqid 2622 |
. . . . 5
|
5 | | simplll 798 |
. . . . . . . . . . 11
..^
..^
|
6 | 1, 5 | sylbi 207 |
. . . . . . . . . 10
|
7 | 6 | adantr 481 |
. . . . . . . . 9
|
8 | | ioossicc 12259 |
. . . . . . . . . 10
|
9 | | fourierdlem76.a |
. . . . . . . . . . . . . 14
|
10 | 9 | rexrd 10089 |
. . . . . . . . . . . . 13
|
11 | 6, 10 | syl 17 |
. . . . . . . . . . . 12
|
12 | 11 | adantr 481 |
. . . . . . . . . . 11
|
13 | | fourierdlem76.b |
. . . . . . . . . . . . . 14
|
14 | 13 | rexrd 10089 |
. . . . . . . . . . . . 13
|
15 | 6, 14 | syl 17 |
. . . . . . . . . . . 12
|
16 | 15 | adantr 481 |
. . . . . . . . . . 11
|
17 | | elioore 12205 |
. . . . . . . . . . . 12
|
18 | 17 | adantl 482 |
. . . . . . . . . . 11
|
19 | 6, 9 | syl 17 |
. . . . . . . . . . . . 13
|
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
|
21 | | fourierdlem76.t |
. . . . . . . . . . . . . . . . . . 19
|
22 | | prfi 8235 |
. . . . . . . . . . . . . . . . . . . . 21
|
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
24 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | | fourierdlem76.q |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 25 | rnmptfi 39351 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | | infi 8184 |
. . . . . . . . . . . . . . . . . . . . 21
|
28 | 24, 26, 27 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | | unfi 8227 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 23, 28, 29 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 21, 30 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
|
32 | | prssg 4350 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 9, 13, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 9, 13, 33 | mpbi2and 956 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | 35, 36 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 34, 38 | unssd 3789 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 21, 39 | syl5eqss 3649 |
. . . . . . . . . . . . . . . . . 18
|
41 | | fourierdlem76.s |
. . . . . . . . . . . . . . . . . 18
|
42 | | fourierdlem76.n |
. . . . . . . . . . . . . . . . . 18
|
43 | 31, 40, 41, 42 | fourierdlem36 40360 |
. . . . . . . . . . . . . . . . 17
|
44 | 6, 43 | syl 17 |
. . . . . . . . . . . . . . . 16
|
45 | | isof1o 6573 |
. . . . . . . . . . . . . . . 16
|
46 | | f1of 6137 |
. . . . . . . . . . . . . . . 16
|
47 | 44, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . 15
|
48 | 6, 40 | syl 17 |
. . . . . . . . . . . . . . 15
|
49 | 47, 48 | fssd 6057 |
. . . . . . . . . . . . . 14
|
50 | 49 | adantr 481 |
. . . . . . . . . . . . 13
|
51 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
..^
..^
..^ |
52 | 1, 51 | sylbi 207 |
. . . . . . . . . . . . . . 15
..^ |
53 | | elfzofz 12485 |
. . . . . . . . . . . . . . 15
..^
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14
|
55 | 54 | adantr 481 |
. . . . . . . . . . . . 13
|
56 | 50, 55 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
57 | 43, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
58 | | frn 6053 |
. . . . . . . . . . . . . . . . . 18
|
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
60 | 9 | leidd 10594 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | | fourierdlem76.altb |
. . . . . . . . . . . . . . . . . . . . . 22
|
62 | 9, 13, 61 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | 9, 13, 9, 60, 62 | eliccd 39726 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | 13 | leidd 10594 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | 9, 13, 13, 62, 64 | eliccd 39726 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | | prssg 4350 |
. . . . . . . . . . . . . . . . . . . . 21
|
67 | 9, 13, 66 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | 63, 65, 67 | mpbi2and 956 |
. . . . . . . . . . . . . . . . . . 19
|
69 | 35, 8 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . 20
|
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 68, 70 | unssd 3789 |
. . . . . . . . . . . . . . . . . 18
|
72 | 21, 71 | syl5eqss 3649 |
. . . . . . . . . . . . . . . . 17
|
73 | 59, 72 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
|
74 | 6, 73 | syl 17 |
. . . . . . . . . . . . . . 15
|
75 | | ffun 6048 |
. . . . . . . . . . . . . . . . 17
|
76 | 49, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
|
77 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . 19
|
78 | 49, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
79 | 78 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
80 | 54, 79 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
|
81 | | fvelrn 6352 |
. . . . . . . . . . . . . . . 16
|
82 | 76, 80, 81 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
83 | 74, 82 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
84 | | iccgelb 12230 |
. . . . . . . . . . . . . 14
|
85 | 11, 15, 83, 84 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
86 | 85 | adantr 481 |
. . . . . . . . . . . 12
|
87 | 56 | rexrd 10089 |
. . . . . . . . . . . . 13
|
88 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . . 17
..^
|
89 | 52, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
|
90 | 49, 89 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
|
91 | 90 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
92 | 91 | adantr 481 |
. . . . . . . . . . . . 13
|
93 | | simpr 477 |
. . . . . . . . . . . . 13
|
94 | | ioogtlb 39717 |
. . . . . . . . . . . . 13
|
95 | 87, 92, 93, 94 | syl3anc 1326 |
. . . . . . . . . . . 12
|
96 | 20, 56, 18, 86, 95 | lelttrd 10195 |
. . . . . . . . . . 11
|
97 | 90 | adantr 481 |
. . . . . . . . . . . 12
|
98 | 6, 13 | syl 17 |
. . . . . . . . . . . . 13
|
99 | 98 | adantr 481 |
. . . . . . . . . . . 12
|
100 | | iooltub 39735 |
. . . . . . . . . . . . 13
|
101 | 87, 92, 93, 100 | syl3anc 1326 |
. . . . . . . . . . . 12
|
102 | 89, 79 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
|
103 | | fvelrn 6352 |
. . . . . . . . . . . . . . . 16
|
104 | 76, 102, 103 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
105 | 74, 104 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
106 | | iccleub 12229 |
. . . . . . . . . . . . . 14
|
107 | 11, 15, 105, 106 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
108 | 107 | adantr 481 |
. . . . . . . . . . . 12
|
109 | 18, 97, 99, 101, 108 | ltletrd 10197 |
. . . . . . . . . . 11
|
110 | 12, 16, 18, 96, 109 | eliood 39720 |
. . . . . . . . . 10
|
111 | 8, 110 | sseldi 3601 |
. . . . . . . . 9
|
112 | | fourierdlem76.f |
. . . . . . . . . . 11
|
113 | 112 | adantr 481 |
. . . . . . . . . 10
|
114 | | fourierdlem76.xre |
. . . . . . . . . . . 12
|
115 | 114 | adantr 481 |
. . . . . . . . . . 11
|
116 | 9, 13 | iccssred 39727 |
. . . . . . . . . . . 12
|
117 | 116 | sselda 3603 |
. . . . . . . . . . 11
|
118 | 115, 117 | readdcld 10069 |
. . . . . . . . . 10
|
119 | 113, 118 | ffvelrnd 6360 |
. . . . . . . . 9
|
120 | 7, 111, 119 | syl2anc 693 |
. . . . . . . 8
|
121 | 120 | recnd 10068 |
. . . . . . 7
|
122 | | fourierdlem76.c |
. . . . . . . . . 10
|
123 | 122 | recnd 10068 |
. . . . . . . . 9
|
124 | 6, 123 | syl 17 |
. . . . . . . 8
|
125 | 124 | adantr 481 |
. . . . . . 7
|
126 | 121, 125 | subcld 10392 |
. . . . . 6
|
127 | | ioossre 12235 |
. . . . . . . . 9
|
128 | 127 | a1i 11 |
. . . . . . . 8
|
129 | 128 | sselda 3603 |
. . . . . . 7
|
130 | 129 | recnd 10068 |
. . . . . 6
|
131 | | nne 2798 |
. . . . . . . . . . . 12
|
132 | 131 | biimpi 206 |
. . . . . . . . . . 11
|
133 | 132 | eqcomd 2628 |
. . . . . . . . . 10
|
134 | 133 | adantl 482 |
. . . . . . . . 9
|
135 | | simpr 477 |
. . . . . . . . . 10
|
136 | 135 | adantr 481 |
. . . . . . . . 9
|
137 | 134, 136 | eqeltrd 2701 |
. . . . . . . 8
|
138 | | fourierdlem76.n0 |
. . . . . . . . 9
|
139 | 138 | ad2antrr 762 |
. . . . . . . 8
|
140 | 137, 139 | condan 835 |
. . . . . . 7
|
141 | 7, 111, 140 | syl2anc 693 |
. . . . . 6
|
142 | 126, 130,
141 | divcld 10801 |
. . . . 5
|
143 | | 2cnd 11093 |
. . . . . . 7
|
144 | 130 | halfcld 11277 |
. . . . . . . 8
|
145 | 144 | sincld 14860 |
. . . . . . 7
|
146 | 143, 145 | mulcld 10060 |
. . . . . 6
|
147 | 17 | recnd 10068 |
. . . . . . . . . 10
|
148 | 147 | adantl 482 |
. . . . . . . . 9
|
149 | 148 | halfcld 11277 |
. . . . . . . 8
|
150 | 149 | sincld 14860 |
. . . . . . 7
|
151 | | 2ne0 11113 |
. . . . . . . 8
|
152 | 151 | a1i 11 |
. . . . . . 7
|
153 | | fourierdlem76.ab |
. . . . . . . . . . 11
|
154 | 6, 153 | syl 17 |
. . . . . . . . . 10
|
155 | 154 | adantr 481 |
. . . . . . . . 9
|
156 | 155, 111 | sseldd 3604 |
. . . . . . . 8
|
157 | | fourierdlem44 40368 |
. . . . . . . 8
|
158 | 156, 141,
157 | syl2anc 693 |
. . . . . . 7
|
159 | 143, 150,
152, 158 | mulne0d 10679 |
. . . . . 6
|
160 | 130, 146,
159 | divcld 10801 |
. . . . 5
|
161 | | eqid 2622 |
. . . . . 6
|
162 | | eqid 2622 |
. . . . . 6
|
163 | 141 | neneqd 2799 |
. . . . . . . 8
|
164 | | velsn 4193 |
. . . . . . . 8
|
165 | 163, 164 | sylnibr 319 |
. . . . . . 7
|
166 | 130, 165 | eldifd 3585 |
. . . . . 6
|
167 | | eqid 2622 |
. . . . . . 7
|
168 | | eqid 2622 |
. . . . . . 7
|
169 | | elfzofz 12485 |
. . . . . . . . . . . . . . 15
..^
|
170 | 169 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
171 | | pire 24210 |
. . . . . . . . . . . . . . . . . . . . 21
|
172 | 171 | renegcli 10342 |
. . . . . . . . . . . . . . . . . . . 20
|
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
174 | 173, 114 | readdcld 10069 |
. . . . . . . . . . . . . . . . . 18
|
175 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
176 | 175, 114 | readdcld 10069 |
. . . . . . . . . . . . . . . . . 18
|
177 | 174, 176 | iccssred 39727 |
. . . . . . . . . . . . . . . . 17
|
178 | 177 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^ |
179 | | fourierdlem76.p |
. . . . . . . . . . . . . . . . . . 19
..^ |
180 | | fourierdlem76.m |
. . . . . . . . . . . . . . . . . . 19
|
181 | | fourierdlem76.v |
. . . . . . . . . . . . . . . . . . 19
|
182 | 179, 180,
181 | fourierdlem15 40339 |
. . . . . . . . . . . . . . . . . 18
|
183 | 182 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
184 | 183, 170 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
..^ |
185 | 178, 184 | sseldd 3604 |
. . . . . . . . . . . . . . 15
..^ |
186 | 114 | adantr 481 |
. . . . . . . . . . . . . . 15
..^ |
187 | 185, 186 | resubcld 10458 |
. . . . . . . . . . . . . 14
..^ |
188 | 25 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
189 | 170, 187,
188 | syl2anc 693 |
. . . . . . . . . . . . 13
..^ |
190 | 189, 187 | eqeltrd 2701 |
. . . . . . . . . . . 12
..^ |
191 | 190 | adantlr 751 |
. . . . . . . . . . 11
..^ ..^
|
192 | 191 | adantr 481 |
. . . . . . . . . 10
..^
..^
|
193 | 1, 192 | sylbi 207 |
. . . . . . . . 9
|
194 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
195 | 194 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
196 | 195 | cbvmptv 4750 |
. . . . . . . . . . . . . . . 16
|
197 | 25, 196 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
198 | 197 | a1i 11 |
. . . . . . . . . . . . . 14
..^ |
199 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
200 | 199 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
201 | 200 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
202 | | fzofzp1 12565 |
. . . . . . . . . . . . . . 15
..^
|
203 | 202 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
204 | 183, 203 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
..^ |
205 | 178, 204 | sseldd 3604 |
. . . . . . . . . . . . . . 15
..^ |
206 | 205, 186 | resubcld 10458 |
. . . . . . . . . . . . . 14
..^ |
207 | 198, 201,
203, 206 | fvmptd 6288 |
. . . . . . . . . . . . 13
..^ |
208 | 207, 206 | eqeltrd 2701 |
. . . . . . . . . . . 12
..^ |
209 | 208 | adantlr 751 |
. . . . . . . . . . 11
..^ ..^
|
210 | 209 | adantr 481 |
. . . . . . . . . 10
..^
..^
|
211 | 1, 210 | sylbi 207 |
. . . . . . . . 9
|
212 | 179 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . . 18
..^ |
213 | 180, 212 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
214 | 181, 213 | mpbid 222 |
. . . . . . . . . . . . . . . 16
..^ |
215 | 214 | simprrd 797 |
. . . . . . . . . . . . . . 15
..^ |
216 | 215 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
..^ |
217 | 185, 205,
186, 216 | ltsub1dd 10639 |
. . . . . . . . . . . . 13
..^ |
218 | 217, 189,
207 | 3brtr4d 4685 |
. . . . . . . . . . . 12
..^ |
219 | 218 | adantlr 751 |
. . . . . . . . . . 11
..^ ..^
|
220 | 219 | adantr 481 |
. . . . . . . . . 10
..^
..^
|
221 | 1, 220 | sylbi 207 |
. . . . . . . . 9
|
222 | 1 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
..^
..^
|
223 | 222 | simplrd 793 |
. . . . . . . . . . . . . . . . 17
..^ |
224 | 6, 223, 185 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
225 | 224 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
226 | 225 | adantr 481 |
. . . . . . . . . . . . . 14
|
227 | 6, 223, 205 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
228 | 227 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
229 | 228 | adantr 481 |
. . . . . . . . . . . . . 14
|
230 | 6, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
|
231 | 230 | adantr 481 |
. . . . . . . . . . . . . . 15
|
232 | | elioore 12205 |
. . . . . . . . . . . . . . . 16
|
233 | 232 | adantl 482 |
. . . . . . . . . . . . . . 15
|
234 | 231, 233 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
235 | 6, 223, 189 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
236 | 235 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
237 | 230 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
238 | 224 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
239 | 237, 238 | pncan3d 10395 |
. . . . . . . . . . . . . . . . 17
|
240 | 236, 239 | eqtr2d 2657 |
. . . . . . . . . . . . . . . 16
|
241 | 240 | adantr 481 |
. . . . . . . . . . . . . . 15
|
242 | 193 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
243 | 193 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
244 | 243 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
245 | 211 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
246 | 245 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
247 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
248 | | ioogtlb 39717 |
. . . . . . . . . . . . . . . . 17
|
249 | 244, 246,
247, 248 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
250 | 242, 233,
231, 249 | ltadd2dd 10196 |
. . . . . . . . . . . . . . 15
|
251 | 241, 250 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
|
252 | 211 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
253 | | iooltub 39735 |
. . . . . . . . . . . . . . . . 17
|
254 | 244, 246,
247, 253 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
255 | 233, 252,
231, 254 | ltadd2dd 10196 |
. . . . . . . . . . . . . . 15
|
256 | 6, 223, 207 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
257 | 256 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
258 | 227 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
259 | 237, 258 | pncan3d 10395 |
. . . . . . . . . . . . . . . . 17
|
260 | 257, 259 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
261 | 260 | adantr 481 |
. . . . . . . . . . . . . . 15
|
262 | 255, 261 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
263 | 226, 229,
234, 251, 262 | eliood 39720 |
. . . . . . . . . . . . 13
|
264 | | fvres 6207 |
. . . . . . . . . . . . 13
|
265 | 263, 264 | syl 17 |
. . . . . . . . . . . 12
|
266 | 265 | eqcomd 2628 |
. . . . . . . . . . 11
|
267 | 266 | mpteq2dva 4744 |
. . . . . . . . . 10
|
268 | | ioosscn 39716 |
. . . . . . . . . . . 12
|
269 | 268 | a1i 11 |
. . . . . . . . . . 11
|
270 | | fourierdlem76.fcn |
. . . . . . . . . . . 12
..^ |
271 | 6, 223, 270 | syl2anc 693 |
. . . . . . . . . . 11
|
272 | | ioosscn 39716 |
. . . . . . . . . . . 12
|
273 | 272 | a1i 11 |
. . . . . . . . . . 11
|
274 | 269, 271,
273, 237, 263 | fourierdlem23 40347 |
. . . . . . . . . 10
|
275 | 267, 274 | eqeltrd 2701 |
. . . . . . . . 9
|
276 | 6, 112 | syl 17 |
. . . . . . . . . 10
|
277 | | ioossre 12235 |
. . . . . . . . . . 11
|
278 | 277 | a1i 11 |
. . . . . . . . . 10
|
279 | | eqid 2622 |
. . . . . . . . . 10
|
280 | | ioossre 12235 |
. . . . . . . . . . 11
|
281 | 280 | a1i 11 |
. . . . . . . . . 10
|
282 | 233, 254 | ltned 10173 |
. . . . . . . . . 10
|
283 | | fourierdlem76.l |
. . . . . . . . . . . 12
..^ lim |
284 | 6, 223, 283 | syl2anc 693 |
. . . . . . . . . . 11
lim |
285 | 260 | eqcomd 2628 |
. . . . . . . . . . . 12
|
286 | 285 | oveq2d 6666 |
. . . . . . . . . . 11
lim
lim
|
287 | 284, 286 | eleqtrd 2703 |
. . . . . . . . . 10
lim |
288 | 211 | recnd 10068 |
. . . . . . . . . 10
|
289 | 276, 230,
278, 279, 263, 281, 282, 287, 288 | fourierdlem53 40376 |
. . . . . . . . 9
lim |
290 | 49, 54 | ffvelrnd 6360 |
. . . . . . . . 9
|
291 | | elfzoelz 12470 |
. . . . . . . . . . . 12
..^
|
292 | | zre 11381 |
. . . . . . . . . . . 12
|
293 | 52, 291, 292 | 3syl 18 |
. . . . . . . . . . 11
|
294 | 293 | ltp1d 10954 |
. . . . . . . . . 10
|
295 | | isorel 6576 |
. . . . . . . . . . 11
|
296 | 44, 54, 89, 295 | syl12anc 1324 |
. . . . . . . . . 10
|
297 | 294, 296 | mpbid 222 |
. . . . . . . . 9
|
298 | 1 | simprbi 480 |
. . . . . . . . 9
|
299 | | eqid 2622 |
. . . . . . . . 9
|
300 | | eqid 2622 |
. . . . . . . . 9
ℂfld ↾t ℂfld ↾t |
301 | 193, 211,
221, 275, 289, 290, 90, 297, 298, 299, 300 | fourierdlem33 40357 |
. . . . . . . 8
lim |
302 | | eqidd 2623 |
. . . . . . . . . 10
|
303 | | simpr 477 |
. . . . . . . . . . . 12
|
304 | 303 | oveq2d 6666 |
. . . . . . . . . . 11
|
305 | 304 | fveq2d 6195 |
. . . . . . . . . 10
|
306 | 243 | adantr 481 |
. . . . . . . . . . 11
|
307 | 245 | adantr 481 |
. . . . . . . . . . 11
|
308 | 90 | adantr 481 |
. . . . . . . . . . 11
|
309 | 193, 211,
290, 90, 297, 298 | fourierdlem10 40334 |
. . . . . . . . . . . . . 14
|
310 | 309 | simpld 475 |
. . . . . . . . . . . . 13
|
311 | 193, 290,
90, 310, 297 | lelttrd 10195 |
. . . . . . . . . . . 12
|
312 | 311 | adantr 481 |
. . . . . . . . . . 11
|
313 | 211 | adantr 481 |
. . . . . . . . . . . 12
|
314 | 309 | simprd 479 |
. . . . . . . . . . . . 13
|
315 | 314 | adantr 481 |
. . . . . . . . . . . 12
|
316 | | neqne 2802 |
. . . . . . . . . . . . . 14
|
317 | 316 | necomd 2849 |
. . . . . . . . . . . . 13
|
318 | 317 | adantl 482 |
. . . . . . . . . . . 12
|
319 | 308, 313,
315, 318 | leneltd 10191 |
. . . . . . . . . . 11
|
320 | 306, 307,
308, 312, 319 | eliood 39720 |
. . . . . . . . . 10
|
321 | 230, 90 | readdcld 10069 |
. . . . . . . . . . . 12
|
322 | 276, 321 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
323 | 322 | adantr 481 |
. . . . . . . . . 10
|
324 | 302, 305,
320, 323 | fvmptd 6288 |
. . . . . . . . 9
|
325 | 324 | ifeq2da 4117 |
. . . . . . . 8
|
326 | 298 | resmptd 5452 |
. . . . . . . . 9
|
327 | 326 | oveq1d 6665 |
. . . . . . . 8
lim lim |
328 | 301, 325,
327 | 3eltr3d 2715 |
. . . . . . 7
lim |
329 | | ax-resscn 9993 |
. . . . . . . . 9
|
330 | 128, 329 | syl6ss 3615 |
. . . . . . . 8
|
331 | 90 | recnd 10068 |
. . . . . . . 8
|
332 | 168, 330,
124, 331 | constlimc 39856 |
. . . . . . 7
lim |
333 | 167, 168,
161, 121, 125, 328, 332 | sublimc 39884 |
. . . . . 6
lim |
334 | 330, 162,
331 | idlimc 39858 |
. . . . . 6
lim |
335 | 6, 105 | jca 554 |
. . . . . . 7
|
336 | | eleq1 2689 |
. . . . . . . . . 10
|
337 | 336 | anbi2d 740 |
. . . . . . . . 9
|
338 | | neeq1 2856 |
. . . . . . . . 9
|
339 | 337, 338 | imbi12d 334 |
. . . . . . . 8
|
340 | 339, 140 | vtoclg 3266 |
. . . . . . 7
|
341 | 90, 335, 340 | sylc 65 |
. . . . . 6
|
342 | 161, 162,
2, 126, 166, 333, 334, 341, 141 | divlimc 39888 |
. . . . 5
lim |
343 | | eqid 2622 |
. . . . . 6
|
344 | 143, 150 | mulcld 10060 |
. . . . . . 7
|
345 | 159 | neneqd 2799 |
. . . . . . . 8
|
346 | | 2re 11090 |
. . . . . . . . . . 11
|
347 | 346 | a1i 11 |
. . . . . . . . . 10
|
348 | 17 | rehalfcld 11279 |
. . . . . . . . . . . 12
|
349 | 348 | resincld 14873 |
. . . . . . . . . . 11
|
350 | 349 | adantl 482 |
. . . . . . . . . 10
|
351 | 347, 350 | remulcld 10070 |
. . . . . . . . 9
|
352 | | elsng 4191 |
. . . . . . . . 9
|
353 | 351, 352 | syl 17 |
. . . . . . . 8
|
354 | 345, 353 | mtbird 315 |
. . . . . . 7
|
355 | 344, 354 | eldifd 3585 |
. . . . . 6
|
356 | | eqid 2622 |
. . . . . . 7
|
357 | | eqid 2622 |
. . . . . . 7
|
358 | | 2cnd 11093 |
. . . . . . . 8
|
359 | 356, 330,
358, 331 | constlimc 39856 |
. . . . . . 7
lim |
360 | 348 | ad2antrl 764 |
. . . . . . . 8
|
361 | | recn 10026 |
. . . . . . . . . 10
|
362 | 361 | sincld 14860 |
. . . . . . . . 9
|
363 | 362 | adantl 482 |
. . . . . . . 8
|
364 | | eqid 2622 |
. . . . . . . . 9
|
365 | | 2cn 11091 |
. . . . . . . . . . 11
|
366 | | eldifsn 4317 |
. . . . . . . . . . 11
|
367 | 365, 151,
366 | mpbir2an 955 |
. . . . . . . . . 10
|
368 | 367 | a1i 11 |
. . . . . . . . 9
|
369 | 151 | a1i 11 |
. . . . . . . . 9
|
370 | 162, 356,
364, 148, 368, 334, 359, 369, 152 | divlimc 39888 |
. . . . . . . 8
lim |
371 | | sinf 14854 |
. . . . . . . . . . . . . 14
|
372 | 371 | a1i 11 |
. . . . . . . . . . . . 13
|
373 | 329 | a1i 11 |
. . . . . . . . . . . . 13
|
374 | 372, 373 | feqresmpt 6250 |
. . . . . . . . . . . 12
|
375 | 374 | trud 1493 |
. . . . . . . . . . 11
|
376 | | resincncf 40088 |
. . . . . . . . . . 11
|
377 | 375, 376 | eqeltrri 2698 |
. . . . . . . . . 10
|
378 | 377 | a1i 11 |
. . . . . . . . 9
|
379 | 90 | rehalfcld 11279 |
. . . . . . . . 9
|
380 | | fveq2 6191 |
. . . . . . . . 9
|
381 | 378, 379,
380 | cnmptlimc 23654 |
. . . . . . . 8
lim |
382 | | fveq2 6191 |
. . . . . . . 8
|
383 | | fveq2 6191 |
. . . . . . . . 9
|
384 | 383 | ad2antll 765 |
. . . . . . . 8
|
385 | 360, 363,
370, 381, 382, 384 | limcco 23657 |
. . . . . . 7
lim |
386 | 356, 357,
343, 143, 150, 359, 385 | mullimc 39848 |
. . . . . 6
lim |
387 | 331 | halfcld 11277 |
. . . . . . . 8
|
388 | 387 | sincld 14860 |
. . . . . . 7
|
389 | 154, 105 | sseldd 3604 |
. . . . . . . 8
|
390 | | fourierdlem44 40368 |
. . . . . . . 8
|
391 | 389, 341,
390 | syl2anc 693 |
. . . . . . 7
|
392 | 358, 388,
369, 391 | mulne0d 10679 |
. . . . . 6
|
393 | 162, 343,
3, 148, 355, 334, 386, 392, 159 | divlimc 39888 |
. . . . 5
lim |
394 | 2, 3, 4, 142, 160, 342, 393 | mullimc 39848 |
. . . 4
lim |
395 | | fourierdlem76.d |
. . . . 5
|
396 | 395 | a1i 11 |
. . . 4
|
397 | | fourierdlem76.o |
. . . . . . 7
|
398 | 397 | reseq1i 5392 |
. . . . . 6
|
399 | | ioossicc 12259 |
. . . . . . . 8
|
400 | | iccss 12241 |
. . . . . . . . 9
|
401 | 19, 98, 85, 107, 400 | syl22anc 1327 |
. . . . . . . 8
|
402 | 399, 401 | syl5ss 3614 |
. . . . . . 7
|
403 | 402 | resmptd 5452 |
. . . . . 6
|
404 | 398, 403 | syl5eq 2668 |
. . . . 5
|
405 | 404 | oveq1d 6665 |
. . . 4
lim lim |
406 | 394, 396,
405 | 3eltr4d 2716 |
. . 3
lim |
407 | 1, 406 | sylbir 225 |
. 2
..^
..^
lim |
408 | 242, 249 | gtned 10172 |
. . . . . . . . . 10
|
409 | | fourierdlem76.r |
. . . . . . . . . . . 12
..^ lim |
410 | 6, 223, 409 | syl2anc 693 |
. . . . . . . . . . 11
lim |
411 | 240 | oveq2d 6666 |
. . . . . . . . . . 11
lim
lim
|
412 | 410, 411 | eleqtrd 2703 |
. . . . . . . . . 10
lim |
413 | 193 | recnd 10068 |
. . . . . . . . . 10
|
414 | 276, 230,
278, 279, 263, 281, 408, 412, 413 | fourierdlem53 40376 |
. . . . . . . . 9
lim |
415 | | eqid 2622 |
. . . . . . . . 9
|
416 | | eqid 2622 |
. . . . . . . . 9
ℂfld ↾t ℂfld
↾t |
417 | 193, 211,
221, 275, 414, 290, 90, 297, 298, 415, 416 | fourierdlem32 40356 |
. . . . . . . 8
lim |
418 | | eqidd 2623 |
. . . . . . . . . 10
|
419 | | oveq2 6658 |
. . . . . . . . . . . 12
|
420 | 419 | fveq2d 6195 |
. . . . . . . . . . 11
|
421 | 420 | adantl 482 |
. . . . . . . . . 10
|
422 | 243 | adantr 481 |
. . . . . . . . . . 11
|
423 | 245 | adantr 481 |
. . . . . . . . . . 11
|
424 | 290 | adantr 481 |
. . . . . . . . . . 11
|
425 | 193 | adantr 481 |
. . . . . . . . . . . 12
|
426 | 310 | adantr 481 |
. . . . . . . . . . . 12
|
427 | | neqne 2802 |
. . . . . . . . . . . . 13
|
428 | 427 | adantl 482 |
. . . . . . . . . . . 12
|
429 | 425, 424,
426, 428 | leneltd 10191 |
. . . . . . . . . . 11
|
430 | 90 | adantr 481 |
. . . . . . . . . . . 12
|
431 | 211 | adantr 481 |
. . . . . . . . . . . 12
|
432 | 297 | adantr 481 |
. . . . . . . . . . . 12
|
433 | 314 | adantr 481 |
. . . . . . . . . . . 12
|
434 | 424, 430,
431, 432, 433 | ltletrd 10197 |
. . . . . . . . . . 11
|
435 | 422, 423,
424, 429, 434 | eliood 39720 |
. . . . . . . . . 10
|
436 | 230, 290 | readdcld 10069 |
. . . . . . . . . . . 12
|
437 | 276, 436 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
438 | 437 | adantr 481 |
. . . . . . . . . 10
|
439 | 418, 421,
435, 438 | fvmptd 6288 |
. . . . . . . . 9
|
440 | 439 | ifeq2da 4117 |
. . . . . . . 8
|
441 | 326 | oveq1d 6665 |
. . . . . . . 8
lim lim |
442 | 417, 440,
441 | 3eltr3d 2715 |
. . . . . . 7
lim |
443 | 290 | recnd 10068 |
. . . . . . . 8
|
444 | 168, 330,
124, 443 | constlimc 39856 |
. . . . . . 7
lim |
445 | 167, 168,
161, 121, 125, 442, 444 | sublimc 39884 |
. . . . . 6
lim |
446 | 330, 162,
443 | idlimc 39858 |
. . . . . 6
lim |
447 | 6, 83 | jca 554 |
. . . . . . 7
|
448 | | eleq1 2689 |
. . . . . . . . . 10
|
449 | 448 | anbi2d 740 |
. . . . . . . . 9
|
450 | | neeq1 2856 |
. . . . . . . . 9
|
451 | 449, 450 | imbi12d 334 |
. . . . . . . 8
|
452 | 451, 140 | vtoclg 3266 |
. . . . . . 7
|
453 | 83, 447, 452 | sylc 65 |
. . . . . 6
|
454 | 161, 162,
2, 126, 166, 445, 446, 453, 141 | divlimc 39888 |
. . . . 5
lim |
455 | 356, 330,
358, 443 | constlimc 39856 |
. . . . . . 7
lim |
456 | 348 | ad2antrl 764 |
. . . . . . . 8
|
457 | 162, 356,
364, 148, 368, 446, 455, 369, 152 | divlimc 39888 |
. . . . . . . 8
lim |
458 | 290 | rehalfcld 11279 |
. . . . . . . . 9
|
459 | | fveq2 6191 |
. . . . . . . . 9
|
460 | 378, 458,
459 | cnmptlimc 23654 |
. . . . . . . 8
lim |
461 | | fveq2 6191 |
. . . . . . . . 9
|
462 | 461 | ad2antll 765 |
. . . . . . . 8
|
463 | 456, 363,
457, 460, 382, 462 | limcco 23657 |
. . . . . . 7
lim |
464 | 356, 357,
343, 143, 150, 455, 463 | mullimc 39848 |
. . . . . 6
lim |
465 | 443 | halfcld 11277 |
. . . . . . . 8
|
466 | 465 | sincld 14860 |
. . . . . . 7
|
467 | 154, 83 | sseldd 3604 |
. . . . . . . 8
|
468 | | fourierdlem44 40368 |
. . . . . . . 8
|
469 | 467, 453,
468 | syl2anc 693 |
. . . . . . 7
|
470 | 358, 466,
369, 469 | mulne0d 10679 |
. . . . . 6
|
471 | 162, 343,
3, 148, 355, 446, 464, 470, 159 | divlimc 39888 |
. . . . 5
lim |
472 | 2, 3, 4, 142, 160, 454, 471 | mullimc 39848 |
. . . 4
lim |
473 | | fourierdlem76.e |
. . . . 5
|
474 | 473 | a1i 11 |
. . . 4
|
475 | 404 | oveq1d 6665 |
. . . 4
lim lim |
476 | 472, 474,
475 | 3eltr4d 2716 |
. . 3
lim |
477 | 1, 476 | sylbir 225 |
. 2
..^
..^
lim |
478 | 298 | sselda 3603 |
. . . . . . . . . 10
|
479 | 478, 266 | syldan 487 |
. . . . . . . . 9
|
480 | 479 | mpteq2dva 4744 |
. . . . . . . 8
|
481 | 225 | adantr 481 |
. . . . . . . . . 10
|
482 | 228 | adantr 481 |
. . . . . . . . . 10
|
483 | 230 | adantr 481 |
. . . . . . . . . . 11
|
484 | 483, 129 | readdcld 10069 |
. . . . . . . . . 10
|
485 | 240 | adantr 481 |
. . . . . . . . . . 11
|
486 | 193 | adantr 481 |
. . . . . . . . . . . 12
|
487 | 243 | adantr 481 |
. . . . . . . . . . . . 13
|
488 | 245 | adantr 481 |
. . . . . . . . . . . . 13
|
489 | 487, 488,
478, 248 | syl3anc 1326 |
. . . . . . . . . . . 12
|
490 | 486, 18, 483, 489 | ltadd2dd 10196 |
. . . . . . . . . . 11
|
491 | 485, 490 | eqbrtrd 4675 |
. . . . . . . . . 10
|
492 | 211 | adantr 481 |
. . . . . . . . . . . 12
|
493 | 487, 488,
478, 253 | syl3anc 1326 |
. . . . . . . . . . . 12
|
494 | 18, 492, 483, 493 | ltadd2dd 10196 |
. . . . . . . . . . 11
|
495 | 260 | adantr 481 |
. . . . . . . . . . 11
|
496 | 494, 495 | breqtrd 4679 |
. . . . . . . . . 10
|
497 | 481, 482,
484, 491, 496 | eliood 39720 |
. . . . . . . . 9
|
498 | 269, 271,
330, 237, 497 | fourierdlem23 40347 |
. . . . . . . 8
|
499 | 480, 498 | eqeltrd 2701 |
. . . . . . 7
|
500 | | ssid 3624 |
. . . . . . . . 9
|
501 | 500 | a1i 11 |
. . . . . . . 8
|
502 | 330, 124,
501 | constcncfg 40084 |
. . . . . . 7
|
503 | 499, 502 | subcncf 40082 |
. . . . . 6
|
504 | 166 | ralrimiva 2966 |
. . . . . . . 8
|
505 | | dfss3 3592 |
. . . . . . . 8
|
506 | 504, 505 | sylibr 224 |
. . . . . . 7
|
507 | | difssd 3738 |
. . . . . . 7
|
508 | 506, 507 | idcncfg 40085 |
. . . . . 6
|
509 | 503, 508 | divcncf 23216 |
. . . . 5
|
510 | 330, 501 | idcncfg 40085 |
. . . . . 6
|
511 | 355, 343 | fmptd 6385 |
. . . . . . 7
|
512 | 330, 358,
501 | constcncfg 40084 |
. . . . . . . . 9
|
513 | | sincn 24198 |
. . . . . . . . . . 11
|
514 | 513 | a1i 11 |
. . . . . . . . . 10
|
515 | 367 | a1i 11 |
. . . . . . . . . . . 12
|
516 | 330, 515,
507 | constcncfg 40084 |
. . . . . . . . . . 11
|
517 | 510, 516 | divcncf 23216 |
. . . . . . . . . 10
|
518 | 514, 517 | cncfmpt1f 22716 |
. . . . . . . . 9
|
519 | 512, 518 | mulcncf 23215 |
. . . . . . . 8
|
520 | | cncffvrn 22701 |
. . . . . . . 8
|
521 | 507, 519,
520 | syl2anc 693 |
. . . . . . 7
|
522 | 511, 521 | mpbird 247 |
. . . . . 6
|
523 | 510, 522 | divcncf 23216 |
. . . . 5
|
524 | 509, 523 | mulcncf 23215 |
. . . 4
|
525 | 404, 524 | eqeltrd 2701 |
. . 3
|
526 | 1, 525 | sylbir 225 |
. 2
..^
..^
|
527 | 407, 477,
526 | jca31 557 |
1
..^
..^
lim lim |