Metamath Proof Explorer


Theorem fourierdlem73

Description: A version of the Riemann Lebesgue lemma: as r increases, the integral in S goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem73.a φ A
fourierdlem73.b φ B
fourierdlem73.f φ F : A B
fourierdlem73.m φ M
fourierdlem73.qf φ Q : 0 M A B
fourierdlem73.q0 φ Q 0 = A
fourierdlem73.qm φ Q M = B
fourierdlem73.qilt φ i 0 ..^ M Q i < Q i + 1
fourierdlem73.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem73.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
fourierdlem73.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
fourierdlem73.g G = D F
fourierdlem73.gcn φ i 0 ..^ M G Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem73.gbd φ y x dom G G x y
fourierdlem73.s S = r + A B F x sin r x dx
fourierdlem73.d D = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x
Assertion fourierdlem73 φ e + n r n +∞ A B F x sin r x dx < e

Proof

Step Hyp Ref Expression
1 fourierdlem73.a φ A
2 fourierdlem73.b φ B
3 fourierdlem73.f φ F : A B
4 fourierdlem73.m φ M
5 fourierdlem73.qf φ Q : 0 M A B
6 fourierdlem73.q0 φ Q 0 = A
7 fourierdlem73.qm φ Q M = B
8 fourierdlem73.qilt φ i 0 ..^ M Q i < Q i + 1
9 fourierdlem73.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
10 fourierdlem73.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
11 fourierdlem73.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
12 fourierdlem73.g G = D F
13 fourierdlem73.gcn φ i 0 ..^ M G Q i Q i + 1 : Q i Q i + 1 cn
14 fourierdlem73.gbd φ y x dom G G x y
15 fourierdlem73.s S = r + A B F x sin r x dx
16 fourierdlem73.d D = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x
17 cncff G Q i Q i + 1 : Q i Q i + 1 cn G Q i Q i + 1 : Q i Q i + 1
18 13 17 syl φ i 0 ..^ M G Q i Q i + 1 : Q i Q i + 1
19 ax-resscn
20 19 a1i φ i 0 ..^ M
21 1 2 iccssred φ A B
22 5 21 fssd φ Q : 0 M
23 22 adantr φ i 0 ..^ M Q : 0 M
24 elfzofz i 0 ..^ M i 0 M
25 24 adantl φ i 0 ..^ M i 0 M
26 23 25 ffvelcdmd φ i 0 ..^ M Q i
27 fzofzp1 i 0 ..^ M i + 1 0 M
28 27 adantl φ i 0 ..^ M i + 1 0 M
29 23 28 ffvelcdmd φ i 0 ..^ M Q i + 1
30 26 29 iccssred φ i 0 ..^ M Q i Q i + 1
31 limccl F Q i Q i + 1 lim Q i
32 31 11 sselid φ i 0 ..^ M R
33 32 adantr φ i 0 ..^ M x Q i Q i + 1 R
34 limccl F Q i Q i + 1 lim Q i + 1
35 34 10 sselid φ i 0 ..^ M L
36 35 adantr φ i 0 ..^ M x Q i Q i + 1 L
37 3 ad2antrr φ i 0 ..^ M x Q i Q i + 1 F : A B
38 1 ad2antrr φ i 0 ..^ M x Q i Q i + 1 A
39 2 ad2antrr φ i 0 ..^ M x Q i Q i + 1 B
40 26 adantr φ i 0 ..^ M x Q i Q i + 1 Q i
41 29 adantr φ i 0 ..^ M x Q i Q i + 1 Q i + 1
42 simpr φ i 0 ..^ M x Q i Q i + 1 x Q i Q i + 1
43 eliccre Q i Q i + 1 x Q i Q i + 1 x
44 40 41 42 43 syl3anc φ i 0 ..^ M x Q i Q i + 1 x
45 1 rexrd φ A *
46 45 adantr φ i 0 ..^ M A *
47 2 rexrd φ B *
48 47 adantr φ i 0 ..^ M B *
49 5 adantr φ i 0 ..^ M Q : 0 M A B
50 49 25 ffvelcdmd φ i 0 ..^ M Q i A B
51 iccgelb A * B * Q i A B A Q i
52 46 48 50 51 syl3anc φ i 0 ..^ M A Q i
53 52 adantr φ i 0 ..^ M x Q i Q i + 1 A Q i
54 40 rexrd φ i 0 ..^ M x Q i Q i + 1 Q i *
55 41 rexrd φ i 0 ..^ M x Q i Q i + 1 Q i + 1 *
56 iccgelb Q i * Q i + 1 * x Q i Q i + 1 Q i x
57 54 55 42 56 syl3anc φ i 0 ..^ M x Q i Q i + 1 Q i x
58 38 40 44 53 57 letrd φ i 0 ..^ M x Q i Q i + 1 A x
59 iccleub Q i * Q i + 1 * x Q i Q i + 1 x Q i + 1
60 54 55 42 59 syl3anc φ i 0 ..^ M x Q i Q i + 1 x Q i + 1
61 45 ad2antrr φ i 0 ..^ M x Q i Q i + 1 A *
62 47 ad2antrr φ i 0 ..^ M x Q i Q i + 1 B *
63 49 28 ffvelcdmd φ i 0 ..^ M Q i + 1 A B
64 63 adantr φ i 0 ..^ M x Q i Q i + 1 Q i + 1 A B
65 iccleub A * B * Q i + 1 A B Q i + 1 B
66 61 62 64 65 syl3anc φ i 0 ..^ M x Q i Q i + 1 Q i + 1 B
67 44 41 39 60 66 letrd φ i 0 ..^ M x Q i Q i + 1 x B
68 38 39 44 58 67 eliccd φ i 0 ..^ M x Q i Q i + 1 x A B
69 37 68 ffvelcdmd φ i 0 ..^ M x Q i Q i + 1 F x
70 36 69 ifcld φ i 0 ..^ M x Q i Q i + 1 if x = Q i + 1 L F x
71 33 70 ifcld φ i 0 ..^ M x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x
72 71 16 fmptd φ i 0 ..^ M D : Q i Q i + 1
73 eqid TopOpen fld = TopOpen fld
74 73 tgioo2 topGen ran . = TopOpen fld 𝑡
75 iccntr Q i Q i + 1 int topGen ran . Q i Q i + 1 = Q i Q i + 1
76 26 29 75 syl2anc φ i 0 ..^ M int topGen ran . Q i Q i + 1 = Q i Q i + 1
77 20 30 72 74 73 76 dvresntr φ i 0 ..^ M D D = D D Q i Q i + 1
78 ioossicc Q i Q i + 1 Q i Q i + 1
79 78 sseli x Q i Q i + 1 x Q i Q i + 1
80 79 adantl φ i 0 ..^ M x Q i Q i + 1 x Q i Q i + 1
81 fvres x Q i Q i + 1 F Q i Q i + 1 x = F x
82 80 81 syl φ i 0 ..^ M x Q i Q i + 1 F Q i Q i + 1 x = F x
83 80 71 syldan φ i 0 ..^ M x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x
84 16 fvmpt2 x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x D x = if x = Q i R if x = Q i + 1 L F x
85 80 83 84 syl2anc φ i 0 ..^ M x Q i Q i + 1 D x = if x = Q i R if x = Q i + 1 L F x
86 26 adantr φ i 0 ..^ M x Q i Q i + 1 Q i
87 80 54 syldan φ i 0 ..^ M x Q i Q i + 1 Q i *
88 80 55 syldan φ i 0 ..^ M x Q i Q i + 1 Q i + 1 *
89 simpr φ i 0 ..^ M x Q i Q i + 1 x Q i Q i + 1
90 ioogtlb Q i * Q i + 1 * x Q i Q i + 1 Q i < x
91 87 88 89 90 syl3anc φ i 0 ..^ M x Q i Q i + 1 Q i < x
92 86 91 gtned φ i 0 ..^ M x Q i Q i + 1 x Q i
93 92 neneqd φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i
94 93 iffalsed φ i 0 ..^ M x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x = if x = Q i + 1 L F x
95 elioore x Q i Q i + 1 x
96 95 adantl φ i 0 ..^ M x Q i Q i + 1 x
97 iooltub Q i * Q i + 1 * x Q i Q i + 1 x < Q i + 1
98 87 88 89 97 syl3anc φ i 0 ..^ M x Q i Q i + 1 x < Q i + 1
99 96 98 ltned φ i 0 ..^ M x Q i Q i + 1 x Q i + 1
100 99 neneqd φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i + 1
101 100 iffalsed φ i 0 ..^ M x Q i Q i + 1 if x = Q i + 1 L F x = F x
102 85 94 101 3eqtrrd φ i 0 ..^ M x Q i Q i + 1 F x = D x
103 82 102 eqtr2d φ i 0 ..^ M x Q i Q i + 1 D x = F Q i Q i + 1 x
104 103 ralrimiva φ i 0 ..^ M x Q i Q i + 1 D x = F Q i Q i + 1 x
105 ffn D : Q i Q i + 1 D Fn Q i Q i + 1
106 72 105 syl φ i 0 ..^ M D Fn Q i Q i + 1
107 ffn F : A B F Fn A B
108 3 107 syl φ F Fn A B
109 108 adantr φ i 0 ..^ M F Fn A B
110 simpr φ i 0 ..^ M i 0 ..^ M
111 46 48 49 110 fourierdlem8 φ i 0 ..^ M Q i Q i + 1 A B
112 fnssres F Fn A B Q i Q i + 1 A B F Q i Q i + 1 Fn Q i Q i + 1
113 109 111 112 syl2anc φ i 0 ..^ M F Q i Q i + 1 Fn Q i Q i + 1
114 78 a1i φ i 0 ..^ M Q i Q i + 1 Q i Q i + 1
115 fvreseq D Fn Q i Q i + 1 F Q i Q i + 1 Fn Q i Q i + 1 Q i Q i + 1 Q i Q i + 1 D Q i Q i + 1 = F Q i Q i + 1 Q i Q i + 1 x Q i Q i + 1 D x = F Q i Q i + 1 x
116 106 113 114 115 syl21anc φ i 0 ..^ M D Q i Q i + 1 = F Q i Q i + 1 Q i Q i + 1 x Q i Q i + 1 D x = F Q i Q i + 1 x
117 104 116 mpbird φ i 0 ..^ M D Q i Q i + 1 = F Q i Q i + 1 Q i Q i + 1
118 114 resabs1d φ i 0 ..^ M F Q i Q i + 1 Q i Q i + 1 = F Q i Q i + 1
119 117 118 eqtrd φ i 0 ..^ M D Q i Q i + 1 = F Q i Q i + 1
120 119 oveq2d φ i 0 ..^ M D D Q i Q i + 1 = D F Q i Q i + 1
121 3 adantr φ i 0 ..^ M F : A B
122 21 adantr φ i 0 ..^ M A B
123 114 30 sstrd φ i 0 ..^ M Q i Q i + 1
124 73 74 dvres F : A B A B Q i Q i + 1 D F Q i Q i + 1 = F int topGen ran . Q i Q i + 1
125 20 121 122 123 124 syl22anc φ i 0 ..^ M D F Q i Q i + 1 = F int topGen ran . Q i Q i + 1
126 12 eqcomi D F = G
127 126 a1i φ i 0 ..^ M D F = G
128 iooretop Q i Q i + 1 topGen ran .
129 retop topGen ran . Top
130 uniretop = topGen ran .
131 130 isopn3 topGen ran . Top Q i Q i + 1 Q i Q i + 1 topGen ran . int topGen ran . Q i Q i + 1 = Q i Q i + 1
132 129 123 131 sylancr φ i 0 ..^ M Q i Q i + 1 topGen ran . int topGen ran . Q i Q i + 1 = Q i Q i + 1
133 128 132 mpbii φ i 0 ..^ M int topGen ran . Q i Q i + 1 = Q i Q i + 1
134 127 133 reseq12d φ i 0 ..^ M F int topGen ran . Q i Q i + 1 = G Q i Q i + 1
135 125 134 eqtrd φ i 0 ..^ M D F Q i Q i + 1 = G Q i Q i + 1
136 77 120 135 3eqtrd φ i 0 ..^ M D D = G Q i Q i + 1
137 136 feq1d φ i 0 ..^ M D : Q i Q i + 1 G Q i Q i + 1 : Q i Q i + 1
138 18 137 mpbird φ i 0 ..^ M D : Q i Q i + 1
139 138 feqmptd φ i 0 ..^ M D D = x Q i Q i + 1 D x
140 139 136 eqtr3d φ i 0 ..^ M x Q i Q i + 1 D x = G Q i Q i + 1
141 ioombl Q i Q i + 1 dom vol
142 141 a1i φ i 0 ..^ M Q i Q i + 1 dom vol
143 26 29 8 ltled φ i 0 ..^ M Q i Q i + 1
144 volioo Q i Q i + 1 Q i Q i + 1 vol Q i Q i + 1 = Q i + 1 Q i
145 26 29 143 144 syl3anc φ i 0 ..^ M vol Q i Q i + 1 = Q i + 1 Q i
146 29 26 resubcld φ i 0 ..^ M Q i + 1 Q i
147 145 146 eqeltrd φ i 0 ..^ M vol Q i Q i + 1
148 14 adantr φ i 0 ..^ M y x dom G G x y
149 nfv x φ i 0 ..^ M y
150 nfra1 x x dom G G x y
151 149 150 nfan x φ i 0 ..^ M y x dom G G x y
152 simpr φ i 0 ..^ M x dom G Q i Q i + 1 x dom G Q i Q i + 1
153 fdm G Q i Q i + 1 : Q i Q i + 1 dom G Q i Q i + 1 = Q i Q i + 1
154 18 153 syl φ i 0 ..^ M dom G Q i Q i + 1 = Q i Q i + 1
155 154 adantr φ i 0 ..^ M x dom G Q i Q i + 1 dom G Q i Q i + 1 = Q i Q i + 1
156 152 155 eleqtrd φ i 0 ..^ M x dom G Q i Q i + 1 x Q i Q i + 1
157 fvres x Q i Q i + 1 G Q i Q i + 1 x = G x
158 156 157 syl φ i 0 ..^ M x dom G Q i Q i + 1 G Q i Q i + 1 x = G x
159 158 fveq2d φ i 0 ..^ M x dom G Q i Q i + 1 G Q i Q i + 1 x = G x
160 159 ad4ant14 φ i 0 ..^ M y x dom G G x y x dom G Q i Q i + 1 G Q i Q i + 1 x = G x
161 simplr φ i 0 ..^ M x dom G G x y x dom G Q i Q i + 1 x dom G G x y
162 ssdmres Q i Q i + 1 dom G dom G Q i Q i + 1 = Q i Q i + 1
163 154 162 sylibr φ i 0 ..^ M Q i Q i + 1 dom G
164 163 sselda φ i 0 ..^ M x Q i Q i + 1 x dom G
165 156 164 syldan φ i 0 ..^ M x dom G Q i Q i + 1 x dom G
166 165 adantlr φ i 0 ..^ M x dom G G x y x dom G Q i Q i + 1 x dom G
167 rsp x dom G G x y x dom G G x y
168 161 166 167 sylc φ i 0 ..^ M x dom G G x y x dom G Q i Q i + 1 G x y
169 168 adantllr φ i 0 ..^ M y x dom G G x y x dom G Q i Q i + 1 G x y
170 160 169 eqbrtrd φ i 0 ..^ M y x dom G G x y x dom G Q i Q i + 1 G Q i Q i + 1 x y
171 170 ex φ i 0 ..^ M y x dom G G x y x dom G Q i Q i + 1 G Q i Q i + 1 x y
172 151 171 ralrimi φ i 0 ..^ M y x dom G G x y x dom G Q i Q i + 1 G Q i Q i + 1 x y
173 172 ex φ i 0 ..^ M y x dom G G x y x dom G Q i Q i + 1 G Q i Q i + 1 x y
174 173 reximdva φ i 0 ..^ M y x dom G G x y y x dom G Q i Q i + 1 G Q i Q i + 1 x y
175 148 174 mpd φ i 0 ..^ M y x dom G Q i Q i + 1 G Q i Q i + 1 x y
176 142 147 13 175 cnbdibl φ i 0 ..^ M G Q i Q i + 1 𝐿 1
177 140 176 eqeltrd φ i 0 ..^ M x Q i Q i + 1 D x 𝐿 1
178 177 adantr φ i 0 ..^ M e + x Q i Q i + 1 D x 𝐿 1
179 141 a1i φ i 0 ..^ M r Q i Q i + 1 dom vol
180 147 adantr φ i 0 ..^ M r vol Q i Q i + 1
181 140 13 eqeltrd φ i 0 ..^ M x Q i Q i + 1 D x : Q i Q i + 1 cn
182 181 adantr φ i 0 ..^ M r x Q i Q i + 1 D x : Q i Q i + 1 cn
183 coscn cos : cn
184 183 a1i φ i 0 ..^ M r cos : cn
185 ioosscn Q i Q i + 1
186 185 a1i φ i 0 ..^ M r Q i Q i + 1
187 simpr φ i 0 ..^ M r r
188 187 recnd φ i 0 ..^ M r r
189 ssid
190 189 a1i φ i 0 ..^ M r
191 186 188 190 constcncfg φ i 0 ..^ M r x Q i Q i + 1 r : Q i Q i + 1 cn
192 185 a1i φ Q i Q i + 1
193 189 a1i φ
194 192 193 idcncfg φ x Q i Q i + 1 x : Q i Q i + 1 cn
195 194 ad2antrr φ i 0 ..^ M r x Q i Q i + 1 x : Q i Q i + 1 cn
196 191 195 mulcncf φ i 0 ..^ M r x Q i Q i + 1 r x : Q i Q i + 1 cn
197 184 196 cncfmpt1f φ i 0 ..^ M r x Q i Q i + 1 cos r x : Q i Q i + 1 cn
198 197 negcncfg φ i 0 ..^ M r x Q i Q i + 1 cos r x : Q i Q i + 1 cn
199 182 198 mulcncf φ i 0 ..^ M r x Q i Q i + 1 D x cos r x : Q i Q i + 1 cn
200 nfv x φ i 0 ..^ M
201 200 150 nfan x φ i 0 ..^ M x dom G G x y
202 136 fveq1d φ i 0 ..^ M D x = G Q i Q i + 1 x
203 202 157 sylan9eq φ i 0 ..^ M x Q i Q i + 1 D x = G x
204 203 fveq2d φ i 0 ..^ M x Q i Q i + 1 D x = G x
205 204 adantlr φ i 0 ..^ M x dom G G x y x Q i Q i + 1 D x = G x
206 simplr φ i 0 ..^ M x dom G G x y x Q i Q i + 1 x dom G G x y
207 164 adantlr φ i 0 ..^ M x dom G G x y x Q i Q i + 1 x dom G
208 206 207 167 sylc φ i 0 ..^ M x dom G G x y x Q i Q i + 1 G x y
209 205 208 eqbrtrd φ i 0 ..^ M x dom G G x y x Q i Q i + 1 D x y
210 209 ex φ i 0 ..^ M x dom G G x y x Q i Q i + 1 D x y
211 201 210 ralrimi φ i 0 ..^ M x dom G G x y x Q i Q i + 1 D x y
212 211 ex φ i 0 ..^ M x dom G G x y x Q i Q i + 1 D x y
213 212 reximdv φ i 0 ..^ M y x dom G G x y y x Q i Q i + 1 D x y
214 148 213 mpd φ i 0 ..^ M y x Q i Q i + 1 D x y
215 214 adantr φ i 0 ..^ M r y x Q i Q i + 1 D x y
216 eqidd φ i 0 ..^ M r z Q i Q i + 1 x Q i Q i + 1 D x cos r x = x Q i Q i + 1 D x cos r x
217 fveq2 x = z D x = D z
218 eleq1w x = z x Q i Q i + 1 z Q i Q i + 1
219 218 anbi2d x = z φ i 0 ..^ M x Q i Q i + 1 φ i 0 ..^ M z Q i Q i + 1
220 fveq2 x = z G x = G z
221 217 220 eqeq12d x = z D x = G x D z = G z
222 219 221 imbi12d x = z φ i 0 ..^ M x Q i Q i + 1 D x = G x φ i 0 ..^ M z Q i Q i + 1 D z = G z
223 222 203 chvarvv φ i 0 ..^ M z Q i Q i + 1 D z = G z
224 217 223 sylan9eqr φ i 0 ..^ M z Q i Q i + 1 x = z D x = G z
225 oveq2 x = z r x = r z
226 225 fveq2d x = z cos r x = cos r z
227 226 negeqd x = z cos r x = cos r z
228 227 adantl φ i 0 ..^ M z Q i Q i + 1 x = z cos r x = cos r z
229 224 228 oveq12d φ i 0 ..^ M z Q i Q i + 1 x = z D x cos r x = G z cos r z
230 229 adantllr φ i 0 ..^ M r z Q i Q i + 1 x = z D x cos r x = G z cos r z
231 simpr φ i 0 ..^ M r z Q i Q i + 1 z Q i Q i + 1
232 fvres z Q i Q i + 1 G Q i Q i + 1 z = G z
233 232 adantl φ i 0 ..^ M z Q i Q i + 1 G Q i Q i + 1 z = G z
234 18 ffvelcdmda φ i 0 ..^ M z Q i Q i + 1 G Q i Q i + 1 z
235 233 234 eqeltrrd φ i 0 ..^ M z Q i Q i + 1 G z
236 235 adantlr φ i 0 ..^ M r z Q i Q i + 1 G z
237 simpl r z Q i Q i + 1 r
238 elioore z Q i Q i + 1 z
239 238 adantl r z Q i Q i + 1 z
240 237 239 remulcld r z Q i Q i + 1 r z
241 240 recnd r z Q i Q i + 1 r z
242 241 coscld r z Q i Q i + 1 cos r z
243 242 negcld r z Q i Q i + 1 cos r z
244 243 adantll φ i 0 ..^ M r z Q i Q i + 1 cos r z
245 236 244 mulcld φ i 0 ..^ M r z Q i Q i + 1 G z cos r z
246 216 230 231 245 fvmptd φ i 0 ..^ M r z Q i Q i + 1 x Q i Q i + 1 D x cos r x z = G z cos r z
247 246 fveq2d φ i 0 ..^ M r z Q i Q i + 1 x Q i Q i + 1 D x cos r x z = G z cos r z
248 247 ad4ant14 φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 x Q i Q i + 1 D x cos r x z = G z cos r z
249 245 abscld φ i 0 ..^ M r z Q i Q i + 1 G z cos r z
250 249 ad4ant14 φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 G z cos r z
251 236 abscld φ i 0 ..^ M r z Q i Q i + 1 G z
252 251 ad4ant14 φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 G z
253 simpllr φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 y
254 244 abscld φ i 0 ..^ M r z Q i Q i + 1 cos r z
255 1red φ i 0 ..^ M r z Q i Q i + 1 1
256 236 absge0d φ i 0 ..^ M r z Q i Q i + 1 0 G z
257 242 absnegd r z Q i Q i + 1 cos r z = cos r z
258 abscosbd r z cos r z 1
259 240 258 syl r z Q i Q i + 1 cos r z 1
260 257 259 eqbrtrd r z Q i Q i + 1 cos r z 1
261 260 adantll φ i 0 ..^ M r z Q i Q i + 1 cos r z 1
262 254 255 251 256 261 lemul2ad φ i 0 ..^ M r z Q i Q i + 1 G z cos r z G z 1
263 236 244 absmuld φ i 0 ..^ M r z Q i Q i + 1 G z cos r z = G z cos r z
264 251 recnd φ i 0 ..^ M r z Q i Q i + 1 G z
265 264 mulridd φ i 0 ..^ M r z Q i Q i + 1 G z 1 = G z
266 265 eqcomd φ i 0 ..^ M r z Q i Q i + 1 G z = G z 1
267 262 263 266 3brtr4d φ i 0 ..^ M r z Q i Q i + 1 G z cos r z G z
268 267 ad4ant14 φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 G z cos r z G z
269 simpr φ i 0 ..^ M x Q i Q i + 1 D x y x Q i Q i + 1 D x y
270 nfra1 x x Q i Q i + 1 D x y
271 200 270 nfan x φ i 0 ..^ M x Q i Q i + 1 D x y
272 204 eqcomd φ i 0 ..^ M x Q i Q i + 1 G x = D x
273 272 adantr φ i 0 ..^ M x Q i Q i + 1 D x y G x = D x
274 simpr φ i 0 ..^ M x Q i Q i + 1 D x y D x y
275 273 274 eqbrtrd φ i 0 ..^ M x Q i Q i + 1 D x y G x y
276 275 ex φ i 0 ..^ M x Q i Q i + 1 D x y G x y
277 276 adantlr φ i 0 ..^ M x Q i Q i + 1 D x y x Q i Q i + 1 D x y G x y
278 271 277 ralimdaa φ i 0 ..^ M x Q i Q i + 1 D x y x Q i Q i + 1 D x y x Q i Q i + 1 G x y
279 269 278 mpd φ i 0 ..^ M x Q i Q i + 1 D x y x Q i Q i + 1 G x y
280 220 fveq2d x = z G x = G z
281 280 breq1d x = z G x y G z y
282 281 cbvralvw x Q i Q i + 1 G x y z Q i Q i + 1 G z y
283 279 282 sylib φ i 0 ..^ M x Q i Q i + 1 D x y z Q i Q i + 1 G z y
284 283 ad4ant14 φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 G z y
285 284 r19.21bi φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 G z y
286 250 252 253 268 285 letrd φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 G z cos r z y
287 248 286 eqbrtrd φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 x Q i Q i + 1 D x cos r x z y
288 287 ralrimiva φ i 0 ..^ M r y x Q i Q i + 1 D x y z Q i Q i + 1 x Q i Q i + 1 D x cos r x z y
289 138 ffvelcdmda φ i 0 ..^ M x Q i Q i + 1 D x
290 289 adantlr φ i 0 ..^ M r x Q i Q i + 1 D x
291 simpl r x Q i Q i + 1 r
292 95 adantl r x Q i Q i + 1 x
293 291 292 remulcld r x Q i Q i + 1 r x
294 293 recnd r x Q i Q i + 1 r x
295 294 coscld r x Q i Q i + 1 cos r x
296 295 negcld r x Q i Q i + 1 cos r x
297 296 adantll φ i 0 ..^ M r x Q i Q i + 1 cos r x
298 290 297 mulcld φ i 0 ..^ M r x Q i Q i + 1 D x cos r x
299 298 ralrimiva φ i 0 ..^ M r x Q i Q i + 1 D x cos r x
300 dmmptg x Q i Q i + 1 D x cos r x dom x Q i Q i + 1 D x cos r x = Q i Q i + 1
301 299 300 syl φ i 0 ..^ M r dom x Q i Q i + 1 D x cos r x = Q i Q i + 1
302 301 ad2antrr φ i 0 ..^ M r y x Q i Q i + 1 D x y dom x Q i Q i + 1 D x cos r x = Q i Q i + 1
303 288 302 raleqtrrdv φ i 0 ..^ M r y x Q i Q i + 1 D x y z dom x Q i Q i + 1 D x cos r x x Q i Q i + 1 D x cos r x z y
304 303 ex φ i 0 ..^ M r y x Q i Q i + 1 D x y z dom x Q i Q i + 1 D x cos r x x Q i Q i + 1 D x cos r x z y
305 304 reximdva φ i 0 ..^ M r y x Q i Q i + 1 D x y y z dom x Q i Q i + 1 D x cos r x x Q i Q i + 1 D x cos r x z y
306 215 305 mpd φ i 0 ..^ M r y z dom x Q i Q i + 1 D x cos r x x Q i Q i + 1 D x cos r x z y
307 179 180 199 306 cnbdibl φ i 0 ..^ M r x Q i Q i + 1 D x cos r x 𝐿 1
308 307 adantlr φ i 0 ..^ M e + r x Q i Q i + 1 D x cos r x 𝐿 1
309 289 adantlr φ i 0 ..^ M e + x Q i Q i + 1 D x
310 simpr φ i 0 ..^ M e + x Q i Q i + 1 r r
311 185 sseli x Q i Q i + 1 x
312 311 ad2antlr φ i 0 ..^ M e + x Q i Q i + 1 r x
313 310 312 mulcld φ i 0 ..^ M e + x Q i Q i + 1 r r x
314 313 coscld φ i 0 ..^ M e + x Q i Q i + 1 r cos r x
315 293 ancoms x Q i Q i + 1 r r x
316 abscosbd r x cos r x 1
317 315 316 syl x Q i Q i + 1 r cos r x 1
318 317 adantll φ i 0 ..^ M e + x Q i Q i + 1 r cos r x 1
319 16 a1i φ i 0 ..^ M D = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x
320 26 adantr φ i 0 ..^ M x = Q i + 1 Q i
321 8 adantr φ i 0 ..^ M x = Q i + 1 Q i < Q i + 1
322 eqcom Q i + 1 = x x = Q i + 1
323 322 biimpri x = Q i + 1 Q i + 1 = x
324 323 adantl φ i 0 ..^ M x = Q i + 1 Q i + 1 = x
325 321 324 breqtrd φ i 0 ..^ M x = Q i + 1 Q i < x
326 320 325 gtned φ i 0 ..^ M x = Q i + 1 x Q i
327 326 neneqd φ i 0 ..^ M x = Q i + 1 ¬ x = Q i
328 327 iffalsed φ i 0 ..^ M x = Q i + 1 if x = Q i R if x = Q i + 1 L F x = if x = Q i + 1 L F x
329 iftrue x = Q i + 1 if x = Q i + 1 L F x = L
330 329 adantl φ i 0 ..^ M x = Q i + 1 if x = Q i + 1 L F x = L
331 328 330 eqtrd φ i 0 ..^ M x = Q i + 1 if x = Q i R if x = Q i + 1 L F x = L
332 29 leidd φ i 0 ..^ M Q i + 1 Q i + 1
333 26 29 29 143 332 eliccd φ i 0 ..^ M Q i + 1 Q i Q i + 1
334 319 331 333 10 fvmptd φ i 0 ..^ M D Q i + 1 = L
335 334 35 eqeltrd φ i 0 ..^ M D Q i + 1
336 335 adantr φ i 0 ..^ M e + D Q i + 1
337 eqid D Q i + 1 = D Q i + 1
338 iftrue x = Q i if x = Q i R if x = Q i + 1 L F x = R
339 338 adantl φ i 0 ..^ M x = Q i if x = Q i R if x = Q i + 1 L F x = R
340 26 rexrd φ i 0 ..^ M Q i *
341 29 rexrd φ i 0 ..^ M Q i + 1 *
342 lbicc2 Q i * Q i + 1 * Q i Q i + 1 Q i Q i Q i + 1
343 340 341 143 342 syl3anc φ i 0 ..^ M Q i Q i Q i + 1
344 319 339 343 11 fvmptd φ i 0 ..^ M D Q i = R
345 344 32 eqeltrd φ i 0 ..^ M D Q i
346 345 adantr φ i 0 ..^ M e + D Q i
347 eqid D Q i = D Q i
348 eqid Q i Q i + 1 D x dx = Q i Q i + 1 D x dx
349 simpr φ e + e +
350 4 nnrpd φ M +
351 350 adantr φ e + M +
352 349 351 rpdivcld φ e + e M +
353 352 adantlr φ i 0 ..^ M e + e M +
354 simpr φ i 0 ..^ M e + r r
355 29 recnd φ i 0 ..^ M Q i + 1
356 355 ad2antrr φ i 0 ..^ M e + r Q i + 1
357 354 356 mulcld φ i 0 ..^ M e + r r Q i + 1
358 357 coscld φ i 0 ..^ M e + r cos r Q i + 1
359 29 adantr φ i 0 ..^ M r Q i + 1
360 187 359 remulcld φ i 0 ..^ M r r Q i + 1
361 abscosbd r Q i + 1 cos r Q i + 1 1
362 360 361 syl φ i 0 ..^ M r cos r Q i + 1 1
363 362 adantlr φ i 0 ..^ M e + r cos r Q i + 1 1
364 26 recnd φ i 0 ..^ M Q i
365 364 ad2antrr φ i 0 ..^ M e + r Q i
366 354 365 mulcld φ i 0 ..^ M e + r r Q i
367 366 coscld φ i 0 ..^ M e + r cos r Q i
368 26 adantr φ i 0 ..^ M r Q i
369 187 368 remulcld φ i 0 ..^ M r r Q i
370 abscosbd r Q i cos r Q i 1
371 369 370 syl φ i 0 ..^ M r cos r Q i 1
372 371 adantlr φ i 0 ..^ M e + r cos r Q i 1
373 fveq2 z = x D z = D x
374 373 fveq2d z = x D z = D x
375 374 cbvitgv Q i Q i + 1 D z dz = Q i Q i + 1 D x dx
376 375 oveq2i D Q i + 1 + D Q i + Q i Q i + 1 D z dz = D Q i + 1 + D Q i + Q i Q i + 1 D x dx
377 376 oveq1i D Q i + 1 + D Q i + Q i Q i + 1 D z dz e M = D Q i + 1 + D Q i + Q i Q i + 1 D x dx e M
378 377 oveq1i D Q i + 1 + D Q i + Q i Q i + 1 D z dz e M + 1 = D Q i + 1 + D Q i + Q i Q i + 1 D x dx e M + 1
379 378 fveq2i D Q i + 1 + D Q i + Q i Q i + 1 D z dz e M + 1 = D Q i + 1 + D Q i + Q i Q i + 1 D x dx e M + 1
380 379 oveq1i D Q i + 1 + D Q i + Q i Q i + 1 D z dz e M + 1 + 1 = D Q i + 1 + D Q i + Q i Q i + 1 D x dx e M + 1 + 1
381 178 308 309 314 318 336 337 346 347 348 353 358 363 367 372 380 fourierdlem47 φ i 0 ..^ M e + m r m +∞ D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx < e M
382 simplll φ i 0 ..^ M m r m +∞ φ
383 simpllr φ i 0 ..^ M m r m +∞ i 0 ..^ M
384 elioore r m +∞ r
385 384 adantl m r m +∞ r
386 0red m r m +∞ 0
387 nnre m m
388 387 adantr m r m +∞ m
389 nngt0 m 0 < m
390 389 adantr m r m +∞ 0 < m
391 388 rexrd m r m +∞ m *
392 pnfxr +∞ *
393 392 a1i m r m +∞ +∞ *
394 simpr m r m +∞ r m +∞
395 ioogtlb m * +∞ * r m +∞ m < r
396 391 393 394 395 syl3anc m r m +∞ m < r
397 386 388 385 390 396 lttrd m r m +∞ 0 < r
398 385 397 elrpd m r m +∞ r +
399 398 adantll φ i 0 ..^ M m r m +∞ r +
400 26 adantr φ i 0 ..^ M r + Q i
401 29 adantr φ i 0 ..^ M r + Q i + 1
402 72 ffvelcdmda φ i 0 ..^ M x Q i Q i + 1 D x
403 402 adantlr φ i 0 ..^ M r + x Q i Q i + 1 D x
404 rpcn r + r
405 404 ad2antlr φ i 0 ..^ M r + x Q i Q i + 1 r
406 44 recnd φ i 0 ..^ M x Q i Q i + 1 x
407 406 adantlr φ i 0 ..^ M r + x Q i Q i + 1 x
408 405 407 mulcld φ i 0 ..^ M r + x Q i Q i + 1 r x
409 408 sincld φ i 0 ..^ M r + x Q i Q i + 1 sin r x
410 403 409 mulcld φ i 0 ..^ M r + x Q i Q i + 1 D x sin r x
411 400 401 410 itgioo φ i 0 ..^ M r + Q i Q i + 1 D x sin r x dx = Q i Q i + 1 D x sin r x dx
412 143 adantr φ i 0 ..^ M r + Q i Q i + 1
413 72 feqmptd φ i 0 ..^ M D = x Q i Q i + 1 D x
414 iftrue x = Q i + 1 if x = Q i + 1 L F Q i Q i + 1 x = L
415 329 414 eqtr4d x = Q i + 1 if x = Q i + 1 L F x = if x = Q i + 1 L F Q i Q i + 1 x
416 415 adantl φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i x = Q i + 1 if x = Q i + 1 L F x = if x = Q i + 1 L F Q i Q i + 1 x
417 iffalse ¬ x = Q i + 1 if x = Q i + 1 L F Q i Q i + 1 x = F Q i Q i + 1 x
418 417 adantl φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 if x = Q i + 1 L F Q i Q i + 1 x = F Q i Q i + 1 x
419 54 ad2antrr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 Q i *
420 55 ad2antrr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 Q i + 1 *
421 44 ad2antrr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 x
422 26 ad2antrr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i Q i
423 44 adantr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i x
424 57 adantr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i Q i x
425 neqne ¬ x = Q i x Q i
426 425 adantl φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i x Q i
427 422 423 424 426 leneltd φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i Q i < x
428 427 adantr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 Q i < x
429 44 adantr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i + 1 x
430 29 ad2antrr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i + 1 Q i + 1
431 60 adantr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i + 1 x Q i + 1
432 322 biimpi Q i + 1 = x x = Q i + 1
433 432 necon3bi ¬ x = Q i + 1 Q i + 1 x
434 433 adantl φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i + 1 Q i + 1 x
435 429 430 431 434 leneltd φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i + 1 x < Q i + 1
436 435 adantlr φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 x < Q i + 1
437 419 420 421 428 436 eliood φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 x Q i Q i + 1
438 fvres x Q i Q i + 1 F Q i Q i + 1 x = F x
439 437 438 syl φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 F Q i Q i + 1 x = F x
440 iffalse ¬ x = Q i + 1 if x = Q i + 1 L F x = F x
441 440 eqcomd ¬ x = Q i + 1 F x = if x = Q i + 1 L F x
442 441 adantl φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 F x = if x = Q i + 1 L F x
443 418 439 442 3eqtrrd φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i ¬ x = Q i + 1 if x = Q i + 1 L F x = if x = Q i + 1 L F Q i Q i + 1 x
444 416 443 pm2.61dan φ i 0 ..^ M x Q i Q i + 1 ¬ x = Q i if x = Q i + 1 L F x = if x = Q i + 1 L F Q i Q i + 1 x
445 444 ifeq2da φ i 0 ..^ M x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x = if x = Q i R if x = Q i + 1 L F Q i Q i + 1 x
446 445 mpteq2dva φ i 0 ..^ M x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F x = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 x
447 319 413 446 3eqtr3d φ i 0 ..^ M x Q i Q i + 1 D x = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 x
448 eqid x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 x = x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 x
449 200 448 26 29 9 10 11 cncfiooicc φ i 0 ..^ M x Q i Q i + 1 if x = Q i R if x = Q i + 1 L F Q i Q i + 1 x : Q i Q i + 1 cn
450 447 449 eqeltrd φ i 0 ..^ M x Q i Q i + 1 D x : Q i Q i + 1 cn
451 413 450 eqeltrd φ i 0 ..^ M D : Q i Q i + 1 cn
452 451 adantr φ i 0 ..^ M r + D : Q i Q i + 1 cn
453 eqid D D = D D
454 136 13 eqeltrd φ i 0 ..^ M D : Q i Q i + 1 cn
455 454 adantr φ i 0 ..^ M r + D : Q i Q i + 1 cn
456 214 adantr φ i 0 ..^ M r + y x Q i Q i + 1 D x y
457 simpr φ i 0 ..^ M r + r +
458 400 401 412 452 453 455 456 457 fourierdlem39 φ i 0 ..^ M r + Q i Q i + 1 D x sin r x dx = D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx
459 411 458 eqtr3d φ i 0 ..^ M r + Q i Q i + 1 D x sin r x dx = D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx
460 382 383 399 459 syl21anc φ i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx = D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx
461 460 fveq2d φ i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx = D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx
462 461 breq1d φ i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx < e M D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx < e M
463 462 ralbidva φ i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx < e M r m +∞ D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx < e M
464 463 rexbidva φ i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx < e M m r m +∞ D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx < e M
465 464 adantr φ i 0 ..^ M e + m r m +∞ Q i Q i + 1 D x sin r x dx < e M m r m +∞ D Q i + 1 cos r Q i + 1 r - D Q i cos r Q i r - Q i Q i + 1 D x cos r x r dx < e M
466 381 465 mpbird φ i 0 ..^ M e + m r m +∞ Q i Q i + 1 D x sin r x dx < e M
467 466 an32s φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx < e M
468 102 oveq1d φ i 0 ..^ M x Q i Q i + 1 F x sin r x = D x sin r x
469 468 itgeq2dv φ i 0 ..^ M Q i Q i + 1 F x sin r x dx = Q i Q i + 1 D x sin r x dx
470 469 eqcomd φ i 0 ..^ M Q i Q i + 1 D x sin r x dx = Q i Q i + 1 F x sin r x dx
471 470 adantr φ i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx = Q i Q i + 1 F x sin r x dx
472 26 adantr φ i 0 ..^ M r m +∞ Q i
473 29 adantr φ i 0 ..^ M r m +∞ Q i + 1
474 402 adantlr φ i 0 ..^ M r m +∞ x Q i Q i + 1 D x
475 384 recnd r m +∞ r
476 475 ad2antlr φ i 0 ..^ M r m +∞ x Q i Q i + 1 r
477 406 adantlr φ i 0 ..^ M r m +∞ x Q i Q i + 1 x
478 476 477 mulcld φ i 0 ..^ M r m +∞ x Q i Q i + 1 r x
479 478 sincld φ i 0 ..^ M r m +∞ x Q i Q i + 1 sin r x
480 474 479 mulcld φ i 0 ..^ M r m +∞ x Q i Q i + 1 D x sin r x
481 472 473 480 itgioo φ i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx = Q i Q i + 1 D x sin r x dx
482 69 adantlr φ i 0 ..^ M r m +∞ x Q i Q i + 1 F x
483 482 479 mulcld φ i 0 ..^ M r m +∞ x Q i Q i + 1 F x sin r x
484 472 473 483 itgioo φ i 0 ..^ M r m +∞ Q i Q i + 1 F x sin r x dx = Q i Q i + 1 F x sin r x dx
485 471 481 484 3eqtr3d φ i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx = Q i Q i + 1 F x sin r x dx
486 485 fveq2d φ i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx = Q i Q i + 1 F x sin r x dx
487 486 breq1d φ i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx < e M Q i Q i + 1 F x sin r x dx < e M
488 487 ralbidva φ i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx < e M r m +∞ Q i Q i + 1 F x sin r x dx < e M
489 488 adantlr φ e + i 0 ..^ M r m +∞ Q i Q i + 1 D x sin r x dx < e M r m +∞ Q i Q i + 1 F x sin r x dx < e M
490 489 rexbidv φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 D x sin r x dx < e M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
491 467 490 mpbid φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
492 491 ralrimiva φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
493 492 ralrimiva φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
494 nfv i φ e +
495 nfra1 i i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
496 494 495 nfan i φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
497 nfv r φ e +
498 nfcv _ r 0 ..^ M
499 nfcv _ r
500 nfra1 r r m +∞ Q i Q i + 1 F x sin r x dx < e M
501 499 500 nfrexw r m r m +∞ Q i Q i + 1 F x sin r x dx < e M
502 498 501 nfralw r i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
503 497 502 nfan r φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
504 nfmpt1 _ i i 0 ..^ M inf m | r m +∞ Q i Q i + 1 F x sin r x dx < e M <
505 fzofi 0 ..^ M Fin
506 505 a1i φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M 0 ..^ M Fin
507 simpr φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M
508 eqid m | r m +∞ Q i Q i + 1 F x sin r x dx < e M = m | r m +∞ Q i Q i + 1 F x sin r x dx < e M
509 eqid i 0 ..^ M inf m | r m +∞ Q i Q i + 1 F x sin r x dx < e M < = i 0 ..^ M inf m | r m +∞ Q i Q i + 1 F x sin r x dx < e M <
510 eqid sup ran i 0 ..^ M inf m | r m +∞ Q i Q i + 1 F x sin r x dx < e M < < = sup ran i 0 ..^ M inf m | r m +∞ Q i Q i + 1 F x sin r x dx < e M < <
511 496 503 504 506 507 508 509 510 fourierdlem31 φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
512 simpr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
513 nfv n φ e +
514 nfre1 n n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
515 513 514 nfan n φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
516 nfv r n
517 nfra1 r r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
518 497 516 517 nf3an r φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
519 simpll φ n r n +∞ φ
520 elioore r n +∞ r
521 520 adantl n r n +∞ r
522 0red n r n +∞ 0
523 nnre n n
524 523 adantr n r n +∞ n
525 nngt0 n 0 < n
526 525 adantr n r n +∞ 0 < n
527 524 rexrd n r n +∞ n *
528 392 a1i n r n +∞ +∞ *
529 simpr n r n +∞ r n +∞
530 ioogtlb n * +∞ * r n +∞ n < r
531 527 528 529 530 syl3anc n r n +∞ n < r
532 522 524 521 526 531 lttrd n r n +∞ 0 < r
533 521 532 elrpd n r n +∞ r +
534 533 adantll φ n r n +∞ r +
535 1 adantr φ r + A
536 2 adantr φ r + B
537 3 ffvelcdmda φ x A B F x
538 537 adantlr φ r + x A B F x
539 404 ad2antlr φ r + x A B r
540 21 sselda φ x A B x
541 540 recnd φ x A B x
542 541 adantlr φ r + x A B x
543 539 542 mulcld φ r + x A B r x
544 543 sincld φ r + x A B sin r x
545 538 544 mulcld φ r + x A B F x sin r x
546 535 536 545 itgioo φ r + A B F x sin r x dx = A B F x sin r x dx
547 6 eqcomd φ A = Q 0
548 7 eqcomd φ B = Q M
549 547 548 oveq12d φ A B = Q 0 Q M
550 549 adantr φ r + A B = Q 0 Q M
551 550 itgeq1d φ r + A B F x sin r x dx = Q 0 Q M F x sin r x dx
552 0zd φ r + 0
553 nnuz = 1
554 0p1e1 0 + 1 = 1
555 554 fveq2i 0 + 1 = 1
556 553 555 eqtr4i = 0 + 1
557 4 556 eleqtrdi φ M 0 + 1
558 557 adantr φ r + M 0 + 1
559 22 adantr φ r + Q : 0 M
560 8 adantlr φ r + i 0 ..^ M Q i < Q i + 1
561 simpr φ x Q 0 Q M x Q 0 Q M
562 549 eqcomd φ Q 0 Q M = A B
563 562 adantr φ x Q 0 Q M Q 0 Q M = A B
564 561 563 eleqtrd φ x Q 0 Q M x A B
565 564 adantlr φ r + x Q 0 Q M x A B
566 565 545 syldan φ r + x Q 0 Q M F x sin r x
567 26 adantlr φ r + i 0 ..^ M Q i
568 29 adantlr φ r + i 0 ..^ M Q i + 1
569 114 111 sstrd φ i 0 ..^ M Q i Q i + 1 A B
570 121 569 feqresmpt φ i 0 ..^ M F Q i Q i + 1 = x Q i Q i + 1 F x
571 570 9 eqeltrrd φ i 0 ..^ M x Q i Q i + 1 F x : Q i Q i + 1 cn
572 571 adantlr φ r + i 0 ..^ M x Q i Q i + 1 F x : Q i Q i + 1 cn
573 sincn sin : cn
574 573 a1i φ r + i 0 ..^ M sin : cn
575 185 a1i φ r + Q i Q i + 1
576 404 adantl φ r + r
577 189 a1i φ r +
578 575 576 577 constcncfg φ r + x Q i Q i + 1 r : Q i Q i + 1 cn
579 194 adantr φ r + x Q i Q i + 1 x : Q i Q i + 1 cn
580 578 579 mulcncf φ r + x Q i Q i + 1 r x : Q i Q i + 1 cn
581 580 adantr φ r + i 0 ..^ M x Q i Q i + 1 r x : Q i Q i + 1 cn
582 574 581 cncfmpt1f φ r + i 0 ..^ M x Q i Q i + 1 sin r x : Q i Q i + 1 cn
583 572 582 mulcncf φ r + i 0 ..^ M x Q i Q i + 1 F x sin r x : Q i Q i + 1 cn
584 eqid x Q i Q i + 1 F x = x Q i Q i + 1 F x
585 eqid x Q i Q i + 1 sin r x = x Q i Q i + 1 sin r x
586 eqid x Q i Q i + 1 F x sin r x = x Q i Q i + 1 F x sin r x
587 3 ad2antrr φ i 0 ..^ M x Q i Q i + 1 F : A B
588 45 ad2antrr φ i 0 ..^ M x Q i Q i + 1 A *
589 47 ad2antrr φ i 0 ..^ M x Q i Q i + 1 B *
590 5 ad2antrr φ i 0 ..^ M x Q i Q i + 1 Q : 0 M A B
591 simplr φ i 0 ..^ M x Q i Q i + 1 i 0 ..^ M
592 588 589 590 591 80 fourierdlem1 φ i 0 ..^ M x Q i Q i + 1 x A B
593 587 592 ffvelcdmd φ i 0 ..^ M x Q i Q i + 1 F x
594 593 adantllr φ r + i 0 ..^ M x Q i Q i + 1 F x
595 576 ad2antrr φ r + i 0 ..^ M x Q i Q i + 1 r
596 311 adantl φ r + i 0 ..^ M x Q i Q i + 1 x
597 595 596 mulcld φ r + i 0 ..^ M x Q i Q i + 1 r x
598 597 sincld φ r + i 0 ..^ M x Q i Q i + 1 sin r x
599 570 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1 = x Q i Q i + 1 F x lim Q i + 1
600 10 599 eleqtrd φ i 0 ..^ M L x Q i Q i + 1 F x lim Q i + 1
601 600 adantlr φ r + i 0 ..^ M L x Q i Q i + 1 F x lim Q i + 1
602 rpre r + r
603 602 adantr r + x Q i Q i + 1 r
604 95 adantl r + x Q i Q i + 1 x
605 603 604 remulcld r + x Q i Q i + 1 r x
606 605 adantll φ r + x Q i Q i + 1 r x
607 606 ad2ant2r φ r + i 0 ..^ M x Q i Q i + 1 r x r Q i + 1 r x
608 recn y y
609 608 sincld y sin y
610 609 adantl φ r + i 0 ..^ M y sin y
611 eqid x Q i Q i + 1 r = x Q i Q i + 1 r
612 eqid x Q i Q i + 1 x = x Q i Q i + 1 x
613 eqid x Q i Q i + 1 r x = x Q i Q i + 1 r x
614 185 a1i φ r + i 0 ..^ M Q i Q i + 1
615 576 adantr φ r + i 0 ..^ M r
616 568 recnd φ r + i 0 ..^ M Q i + 1
617 611 614 615 616 constlimc φ r + i 0 ..^ M r x Q i Q i + 1 r lim Q i + 1
618 614 612 616 idlimc φ r + i 0 ..^ M Q i + 1 x Q i Q i + 1 x lim Q i + 1
619 611 612 613 595 596 617 618 mullimc φ r + i 0 ..^ M r Q i + 1 x Q i Q i + 1 r x lim Q i + 1
620 eqid y sin y = y sin y
621 sinf sin :
622 621 a1i sin :
623 622 feqmptd sin = y sin y
624 623 573 eqeltrrdi y sin y : cn
625 19 a1i
626 resincl y sin y
627 626 adantl y sin y
628 620 624 625 625 627 cncfmptssg y sin y : cn
629 628 mptru y sin y : cn
630 629 a1i φ r + i 0 ..^ M y sin y : cn
631 602 ad2antlr φ r + i 0 ..^ M r
632 631 568 remulcld φ r + i 0 ..^ M r Q i + 1
633 fveq2 y = r Q i + 1 sin y = sin r Q i + 1
634 630 632 633 cnmptlimc φ r + i 0 ..^ M sin r Q i + 1 y sin y lim r Q i + 1
635 fveq2 y = r x sin y = sin r x
636 fveq2 r x = r Q i + 1 sin r x = sin r Q i + 1
637 636 ad2antll φ r + i 0 ..^ M x Q i Q i + 1 r x = r Q i + 1 sin r x = sin r Q i + 1
638 607 610 619 634 635 637 limcco φ r + i 0 ..^ M sin r Q i + 1 x Q i Q i + 1 sin r x lim Q i + 1
639 584 585 586 594 598 601 638 mullimc φ r + i 0 ..^ M L sin r Q i + 1 x Q i Q i + 1 F x sin r x lim Q i + 1
640 570 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i = x Q i Q i + 1 F x lim Q i
641 11 640 eleqtrd φ i 0 ..^ M R x Q i Q i + 1 F x lim Q i
642 641 adantlr φ r + i 0 ..^ M R x Q i Q i + 1 F x lim Q i
643 606 ad2ant2r φ r + i 0 ..^ M x Q i Q i + 1 r x r Q i r x
644 567 recnd φ r + i 0 ..^ M Q i
645 611 614 615 644 constlimc φ r + i 0 ..^ M r x Q i Q i + 1 r lim Q i
646 614 612 644 idlimc φ r + i 0 ..^ M Q i x Q i Q i + 1 x lim Q i
647 611 612 613 595 596 645 646 mullimc φ r + i 0 ..^ M r Q i x Q i Q i + 1 r x lim Q i
648 631 567 remulcld φ r + i 0 ..^ M r Q i
649 fveq2 y = r Q i sin y = sin r Q i
650 630 648 649 cnmptlimc φ r + i 0 ..^ M sin r Q i y sin y lim r Q i
651 fveq2 r x = r Q i sin r x = sin r Q i
652 651 ad2antll φ r + i 0 ..^ M x Q i Q i + 1 r x = r Q i sin r x = sin r Q i
653 643 610 647 650 635 652 limcco φ r + i 0 ..^ M sin r Q i x Q i Q i + 1 sin r x lim Q i
654 584 585 586 594 598 642 653 mullimc φ r + i 0 ..^ M R sin r Q i x Q i Q i + 1 F x sin r x lim Q i
655 567 568 583 639 654 iblcncfioo φ r + i 0 ..^ M x Q i Q i + 1 F x sin r x 𝐿 1
656 simpll φ r + i 0 ..^ M x Q i Q i + 1 φ r +
657 68 adantllr φ r + i 0 ..^ M x Q i Q i + 1 x A B
658 656 657 545 syl2anc φ r + i 0 ..^ M x Q i Q i + 1 F x sin r x
659 567 568 655 658 ibliooicc φ r + i 0 ..^ M x Q i Q i + 1 F x sin r x 𝐿 1
660 552 558 559 560 566 659 itgspltprt φ r + Q 0 Q M F x sin r x dx = i 0 ..^ M Q i Q i + 1 F x sin r x dx
661 546 551 660 3eqtrd φ r + A B F x sin r x dx = i 0 ..^ M Q i Q i + 1 F x sin r x dx
662 519 534 661 syl2anc φ n r n +∞ A B F x sin r x dx = i 0 ..^ M Q i Q i + 1 F x sin r x dx
663 505 a1i φ n r n +∞ 0 ..^ M Fin
664 69 adantllr φ r n +∞ i 0 ..^ M x Q i Q i + 1 F x
665 520 recnd r n +∞ r
666 665 adantl φ r n +∞ r
667 666 ad2antrr φ r n +∞ i 0 ..^ M x Q i Q i + 1 r
668 406 adantllr φ r n +∞ i 0 ..^ M x Q i Q i + 1 x
669 667 668 mulcld φ r n +∞ i 0 ..^ M x Q i Q i + 1 r x
670 669 sincld φ r n +∞ i 0 ..^ M x Q i Q i + 1 sin r x
671 664 670 mulcld φ r n +∞ i 0 ..^ M x Q i Q i + 1 F x sin r x
672 671 adantl3r φ n r n +∞ i 0 ..^ M x Q i Q i + 1 F x sin r x
673 simplll φ n r n +∞ i 0 ..^ M φ
674 534 adantr φ n r n +∞ i 0 ..^ M r +
675 simpr φ n r n +∞ i 0 ..^ M i 0 ..^ M
676 673 674 675 659 syl21anc φ n r n +∞ i 0 ..^ M x Q i Q i + 1 F x sin r x 𝐿 1
677 672 676 itgcl φ n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx
678 663 677 fsumcl φ n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx
679 662 678 eqeltrd φ n r n +∞ A B F x sin r x dx
680 679 adantllr φ e + n r n +∞ A B F x sin r x dx
681 680 3adantl3 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx
682 681 abscld φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx
683 677 abscld φ n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx
684 663 683 fsumrecl φ n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx
685 684 adantllr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx
686 685 3adantl3 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx
687 rpre e + e
688 687 ad2antlr φ e + r n +∞ e
689 688 3ad2antl1 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ e
690 662 fveq2d φ n r n +∞ A B F x sin r x dx = i 0 ..^ M Q i Q i + 1 F x sin r x dx
691 663 677 fsumabs φ n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx i 0 ..^ M Q i Q i + 1 F x sin r x dx
692 690 691 eqbrtrd φ n r n +∞ A B F x sin r x dx i 0 ..^ M Q i Q i + 1 F x sin r x dx
693 692 adantllr φ e + n r n +∞ A B F x sin r x dx i 0 ..^ M Q i Q i + 1 F x sin r x dx
694 693 3adantl3 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx i 0 ..^ M Q i Q i + 1 F x sin r x dx
695 505 a1i φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ 0 ..^ M Fin
696 0zd φ 0
697 4 nnzd φ M
698 4 nngt0d φ 0 < M
699 fzolb 0 0 ..^ M 0 M 0 < M
700 696 697 698 699 syl3anbrc φ 0 0 ..^ M
701 ne0i 0 0 ..^ M 0 ..^ M
702 700 701 syl φ 0 ..^ M
703 702 ad2antrr φ e + r n +∞ 0 ..^ M
704 703 3ad2antl1 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ 0 ..^ M
705 simp1l φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M φ
706 705 ad2antrr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M φ
707 simpll2 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M n
708 706 707 jca φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M φ n
709 simplr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M r n +∞
710 simpr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M j 0 ..^ M
711 eleq1w i = j i 0 ..^ M j 0 ..^ M
712 711 anbi2d i = j φ n r n +∞ i 0 ..^ M φ n r n +∞ j 0 ..^ M
713 fveq2 i = j Q i = Q j
714 oveq1 i = j i + 1 = j + 1
715 714 fveq2d i = j Q i + 1 = Q j + 1
716 713 715 oveq12d i = j Q i Q i + 1 = Q j Q j + 1
717 716 itgeq1d i = j Q i Q i + 1 F x sin r x dx = Q j Q j + 1 F x sin r x dx
718 717 eleq1d i = j Q i Q i + 1 F x sin r x dx Q j Q j + 1 F x sin r x dx
719 712 718 imbi12d i = j φ n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx φ n r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx
720 719 677 chvarvv φ n r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx
721 708 709 710 720 syl21anc φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx
722 721 abscld φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx
723 352 rpred φ e + e M
724 723 3ad2ant1 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M e M
725 724 ad2antrr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M e M
726 simpll3 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
727 rspa r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
728 727 adantr r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M
729 717 fveq2d i = j Q i Q i + 1 F x sin r x dx = Q j Q j + 1 F x sin r x dx
730 729 breq1d i = j Q i Q i + 1 F x sin r x dx < e M Q j Q j + 1 F x sin r x dx < e M
731 730 cbvralvw i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M j 0 ..^ M Q j Q j + 1 F x sin r x dx < e M
732 728 731 sylib r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M j 0 ..^ M Q j Q j + 1 F x sin r x dx < e M
733 rspa j 0 ..^ M Q j Q j + 1 F x sin r x dx < e M j 0 ..^ M Q j Q j + 1 F x sin r x dx < e M
734 732 733 sylancom r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx < e M
735 726 709 710 734 syl21anc φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx < e M
736 695 704 722 725 735 fsumlt φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx < j 0 ..^ M e M
737 fveq2 j = i Q j = Q i
738 oveq1 j = i j + 1 = i + 1
739 738 fveq2d j = i Q j + 1 = Q i + 1
740 737 739 oveq12d j = i Q j Q j + 1 = Q i Q i + 1
741 740 itgeq1d j = i Q j Q j + 1 F x sin r x dx = Q i Q i + 1 F x sin r x dx
742 741 fveq2d j = i Q j Q j + 1 F x sin r x dx = Q i Q i + 1 F x sin r x dx
743 742 cbvsumv j 0 ..^ M Q j Q j + 1 F x sin r x dx = i 0 ..^ M Q i Q i + 1 F x sin r x dx
744 743 a1i φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M Q j Q j + 1 F x sin r x dx = i 0 ..^ M Q i Q i + 1 F x sin r x dx
745 352 rpcnd φ e + e M
746 fsumconst 0 ..^ M Fin e M j 0 ..^ M e M = 0 ..^ M e M
747 505 745 746 sylancr φ e + j 0 ..^ M e M = 0 ..^ M e M
748 4 nnnn0d φ M 0
749 hashfzo0 M 0 0 ..^ M = M
750 748 749 syl φ 0 ..^ M = M
751 750 oveq1d φ 0 ..^ M e M = M e M
752 751 adantr φ e + 0 ..^ M e M = M e M
753 349 rpcnd φ e + e
754 351 rpcnd φ e + M
755 351 rpne0d φ e + M 0
756 753 754 755 divcan2d φ e + M e M = e
757 747 752 756 3eqtrd φ e + j 0 ..^ M e M = e
758 757 adantr φ e + r n +∞ j 0 ..^ M e M = e
759 758 3ad2antl1 φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ j 0 ..^ M e M = e
760 736 744 759 3brtr3d φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e
761 682 686 689 694 760 lelttrd φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx < e
762 761 ex φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx < e
763 518 762 ralrimi φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx < e
764 763 3exp φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx < e
765 764 adantr φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M r n +∞ A B F x sin r x dx < e
766 515 765 reximdai φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M n r n +∞ A B F x sin r x dx < e
767 512 766 mpd φ e + n r n +∞ i 0 ..^ M Q i Q i + 1 F x sin r x dx < e M n r n +∞ A B F x sin r x dx < e
768 511 767 syldan φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M n r n +∞ A B F x sin r x dx < e
769 768 ex φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M n r n +∞ A B F x sin r x dx < e
770 769 ralimdva φ e + i 0 ..^ M m r m +∞ Q i Q i + 1 F x sin r x dx < e M e + n r n +∞ A B F x sin r x dx < e
771 493 770 mpd φ e + n r n +∞ A B F x sin r x dx < e