Metamath Proof Explorer


Theorem fourierdlem112

Description: Here abbreviations (local definitions) are introduced to prove the fourier theorem. ( Zm ) is the m_th partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem112.f φ F :
fourierdlem112.d D = m y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
fourierdlem112.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
fourierdlem112.m φ M
fourierdlem112.q φ Q P M
fourierdlem112.n N = - π + X π + X y - π + X π + X | k y + k T ran Q 1
fourierdlem112.v V = ι f | f Isom < , < 0 N - π + X π + X y - π + X π + X | k y + k T ran Q
fourierdlem112.x φ X
fourierdlem112.xran φ X ran V
fourierdlem112.t T = 2 π
fourierdlem112.fper φ x F x + T = F x
fourierdlem112.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem112.c φ i 0 ..^ M C F Q i Q i + 1 lim Q i
fourierdlem112.u φ i 0 ..^ M U F Q i Q i + 1 lim Q i + 1
fourierdlem112.fdvcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem112.e φ E F −∞ X lim X
fourierdlem112.i φ I F X +∞ lim X
fourierdlem112.l φ L F −∞ X lim X
fourierdlem112.r φ R F X +∞ lim X
fourierdlem112.a A = n 0 π π F x cos n x dx π
fourierdlem112.b B = n π π F x sin n x dx π
fourierdlem112.z Z = m A 0 2 + n = 1 m A n cos n X + B n sin n X
fourierdlem112.23 S = n A n cos n X + B n sin n X
fourierdlem112.fbd φ w t F t w
fourierdlem112.fdvbd φ z t dom F F t z
fourierdlem112.25 φ X
Assertion fourierdlem112 φ seq 1 + S L + R 2 A 0 2 A 0 2 + n A n cos n X + B n sin n X = L + R 2

Proof

Step Hyp Ref Expression
1 fourierdlem112.f φ F :
2 fourierdlem112.d D = m y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
3 fourierdlem112.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
4 fourierdlem112.m φ M
5 fourierdlem112.q φ Q P M
6 fourierdlem112.n N = - π + X π + X y - π + X π + X | k y + k T ran Q 1
7 fourierdlem112.v V = ι f | f Isom < , < 0 N - π + X π + X y - π + X π + X | k y + k T ran Q
8 fourierdlem112.x φ X
9 fourierdlem112.xran φ X ran V
10 fourierdlem112.t T = 2 π
11 fourierdlem112.fper φ x F x + T = F x
12 fourierdlem112.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
13 fourierdlem112.c φ i 0 ..^ M C F Q i Q i + 1 lim Q i
14 fourierdlem112.u φ i 0 ..^ M U F Q i Q i + 1 lim Q i + 1
15 fourierdlem112.fdvcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
16 fourierdlem112.e φ E F −∞ X lim X
17 fourierdlem112.i φ I F X +∞ lim X
18 fourierdlem112.l φ L F −∞ X lim X
19 fourierdlem112.r φ R F X +∞ lim X
20 fourierdlem112.a A = n 0 π π F x cos n x dx π
21 fourierdlem112.b B = n π π F x sin n x dx π
22 fourierdlem112.z Z = m A 0 2 + n = 1 m A n cos n X + B n sin n X
23 fourierdlem112.23 S = n A n cos n X + B n sin n X
24 fourierdlem112.fbd φ w t F t w
25 fourierdlem112.fdvbd φ z t dom F F t z
26 fourierdlem112.25 φ X
27 fveq2 n = j A n = A j
28 oveq1 n = j n X = j X
29 28 fveq2d n = j cos n X = cos j X
30 27 29 oveq12d n = j A n cos n X = A j cos j X
31 fveq2 n = j B n = B j
32 28 fveq2d n = j sin n X = sin j X
33 31 32 oveq12d n = j B n sin n X = B j sin j X
34 30 33 oveq12d n = j A n cos n X + B n sin n X = A j cos j X + B j sin j X
35 34 cbvmptv n A n cos n X + B n sin n X = j A j cos j X + B j sin j X
36 23 35 eqtri S = j A j cos j X + B j sin j X
37 seqeq3 S = j A j cos j X + B j sin j X seq 1 + S = seq 1 + j A j cos j X + B j sin j X
38 36 37 mp1i φ seq 1 + S = seq 1 + j A j cos j X + B j sin j X
39 nnuz = 1
40 1zzd φ 1
41 nfv n φ
42 nfcv _ n
43 nfcv _ n π 0
44 nfcv _ n F X + s
45 nfcv _ n ×
46 nfcv _ n D m s
47 44 45 46 nfov _ n F X + s D m s
48 43 47 nfitg _ n π 0 F X + s D m s ds
49 42 48 nfmpt _ n m π 0 F X + s D m s ds
50 nfcv _ n 0 π
51 50 47 nfitg _ n 0 π F X + s D m s ds
52 42 51 nfmpt _ n m 0 π F X + s D m s ds
53 nfmpt1 _ n n 0 π π F x cos n x dx π
54 20 53 nfcxfr _ n A
55 nfcv _ n 0
56 54 55 nffv _ n A 0
57 nfcv _ n ÷
58 nfcv _ n 2
59 56 57 58 nfov _ n A 0 2
60 nfcv _ n +
61 nfcv _ n 1 m
62 61 nfsum1 _ n n = 1 m A n cos n X + B n sin n X
63 59 60 62 nfov _ n A 0 2 + n = 1 m A n cos n X + B n sin n X
64 42 63 nfmpt _ n m A 0 2 + n = 1 m A n cos n X + B n sin n X
65 22 64 nfcxfr _ n Z
66 eqid n p 0 n | p 0 = - π + X p n = π + X i 0 ..^ n p i < p i + 1 = n p 0 n | p 0 = - π + X p n = π + X i 0 ..^ n p i < p i + 1
67 picn π
68 67 2timesi 2 π = π + π
69 67 67 subnegi π π = π + π
70 68 10 69 3eqtr4i T = π π
71 pire π
72 71 a1i φ π
73 72 renegcld φ π
74 73 26 readdcld φ - π + X
75 72 26 readdcld φ π + X
76 negpilt0 π < 0
77 pipos 0 < π
78 71 renegcli π
79 0re 0
80 78 79 71 lttri π < 0 0 < π π < π
81 76 77 80 mp2an π < π
82 81 a1i φ π < π
83 73 72 26 82 ltadd1dd φ - π + X < π + X
84 oveq1 y = x y + k T = x + k T
85 84 eleq1d y = x y + k T ran Q x + k T ran Q
86 85 rexbidv y = x k y + k T ran Q k x + k T ran Q
87 86 cbvrabv y - π + X π + X | k y + k T ran Q = x - π + X π + X | k x + k T ran Q
88 87 uneq2i - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X x - π + X π + X | k x + k T ran Q
89 70 3 4 5 74 75 83 66 88 6 7 fourierdlem54 φ N V n p 0 n | p 0 = - π + X p n = π + X i 0 ..^ n p i < p i + 1 N V Isom < , < 0 N - π + X π + X y - π + X π + X | k y + k T ran Q
90 89 simpld φ N V n p 0 n | p 0 = - π + X p n = π + X i 0 ..^ n p i < p i + 1 N
91 90 simpld φ N
92 90 simprd φ V n p 0 n | p 0 = - π + X p n = π + X i 0 ..^ n p i < p i + 1 N
93 1 adantr φ i 0 ..^ N F :
94 fveq2 i = j p i = p j
95 oveq1 i = j i + 1 = j + 1
96 95 fveq2d i = j p i + 1 = p j + 1
97 94 96 breq12d i = j p i < p i + 1 p j < p j + 1
98 97 cbvralvw i 0 ..^ n p i < p i + 1 j 0 ..^ n p j < p j + 1
99 98 anbi2i p 0 = π p n = π i 0 ..^ n p i < p i + 1 p 0 = π p n = π j 0 ..^ n p j < p j + 1
100 99 a1i p 0 n p 0 = π p n = π i 0 ..^ n p i < p i + 1 p 0 = π p n = π j 0 ..^ n p j < p j + 1
101 100 rabbiia p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1 = p 0 n | p 0 = π p n = π j 0 ..^ n p j < p j + 1
102 101 mpteq2i n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1 = n p 0 n | p 0 = π p n = π j 0 ..^ n p j < p j + 1
103 3 102 eqtri P = n p 0 n | p 0 = π p n = π j 0 ..^ n p j < p j + 1
104 4 adantr φ i 0 ..^ N M
105 5 adantr φ i 0 ..^ N Q P M
106 11 adantlr φ i 0 ..^ N x F x + T = F x
107 eleq1w i = j i 0 ..^ M j 0 ..^ M
108 107 anbi2d i = j φ i 0 ..^ M φ j 0 ..^ M
109 fveq2 i = j Q i = Q j
110 95 fveq2d i = j Q i + 1 = Q j + 1
111 109 110 oveq12d i = j Q i Q i + 1 = Q j Q j + 1
112 111 reseq2d i = j F Q i Q i + 1 = F Q j Q j + 1
113 111 oveq1d i = j Q i Q i + 1 cn = Q j Q j + 1 cn
114 112 113 eleq12d i = j F Q i Q i + 1 : Q i Q i + 1 cn F Q j Q j + 1 : Q j Q j + 1 cn
115 108 114 imbi12d i = j φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn φ j 0 ..^ M F Q j Q j + 1 : Q j Q j + 1 cn
116 115 12 chvarvv φ j 0 ..^ M F Q j Q j + 1 : Q j Q j + 1 cn
117 116 adantlr φ i 0 ..^ N j 0 ..^ M F Q j Q j + 1 : Q j Q j + 1 cn
118 74 adantr φ i 0 ..^ N - π + X
119 74 rexrd φ - π + X *
120 pnfxr +∞ *
121 120 a1i φ +∞ *
122 75 ltpnfd φ π + X < +∞
123 119 121 75 83 122 eliood φ π + X - π + X +∞
124 123 adantr φ i 0 ..^ N π + X - π + X +∞
125 id i 0 ..^ N i 0 ..^ N
126 6 oveq2i 0 ..^ N = 0 ..^ - π + X π + X y - π + X π + X | k y + k T ran Q 1
127 125 126 eleqtrdi i 0 ..^ N i 0 ..^ - π + X π + X y - π + X π + X | k y + k T ran Q 1
128 127 adantl φ i 0 ..^ N i 0 ..^ - π + X π + X y - π + X π + X | k y + k T ran Q 1
129 6 oveq2i 0 N = 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1
130 isoeq4 0 N = 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 f Isom < , < 0 N - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q
131 129 130 ax-mp f Isom < , < 0 N - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q
132 131 iotabii ι f | f Isom < , < 0 N - π + X π + X y - π + X π + X | k y + k T ran Q = ι f | f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q
133 7 132 eqtri V = ι f | f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q
134 93 103 70 104 105 106 117 118 124 128 133 fourierdlem98 φ i 0 ..^ N F V i V i + 1 : V i V i + 1 cn
135 24 adantr φ i 0 ..^ N w t F t w
136 nfra1 t t F t w
137 elioore t V i V i + 1 t
138 rspa t F t w t F t w
139 137 138 sylan2 t F t w t V i V i + 1 F t w
140 139 ex t F t w t V i V i + 1 F t w
141 136 140 ralrimi t F t w t V i V i + 1 F t w
142 141 reximi w t F t w w t V i V i + 1 F t w
143 135 142 syl φ i 0 ..^ N w t V i V i + 1 F t w
144 ssid
145 dvfre F : F : dom F
146 1 144 145 sylancl φ F : dom F
147 146 adantr φ i 0 ..^ N F : dom F
148 eqid D F = D F
149 71 a1i φ i 0 ..^ N π
150 78 a1i φ i 0 ..^ N π
151 111 reseq2d i = j F Q i Q i + 1 = F Q j Q j + 1
152 151 113 eleq12d i = j F Q i Q i + 1 : Q i Q i + 1 cn F Q j Q j + 1 : Q j Q j + 1 cn
153 108 152 imbi12d i = j φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn φ j 0 ..^ M F Q j Q j + 1 : Q j Q j + 1 cn
154 153 15 chvarvv φ j 0 ..^ M F Q j Q j + 1 : Q j Q j + 1 cn
155 154 adantlr φ i 0 ..^ N j 0 ..^ M F Q j Q j + 1 : Q j Q j + 1 cn
156 73 8 readdcld φ - π + X
157 156 adantr φ i 0 ..^ N - π + X
158 156 rexrd φ - π + X *
159 72 8 readdcld φ π + X
160 73 72 8 82 ltadd1dd φ - π + X < π + X
161 159 ltpnfd φ π + X < +∞
162 158 121 159 160 161 eliood φ π + X - π + X +∞
163 162 adantr φ i 0 ..^ N π + X - π + X +∞
164 oveq1 k = h k T = h T
165 164 oveq2d k = h y + k T = y + h T
166 165 eleq1d k = h y + k T ran Q y + h T ran Q
167 166 cbvrexvw k y + k T ran Q h y + h T ran Q
168 167 rgenw y - π + X π + X k y + k T ran Q h y + h T ran Q
169 rabbi y - π + X π + X k y + k T ran Q h y + h T ran Q y - π + X π + X | k y + k T ran Q = y - π + X π + X | h y + h T ran Q
170 168 169 mpbi y - π + X π + X | k y + k T ran Q = y - π + X π + X | h y + h T ran Q
171 170 uneq2i - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X y - π + X π + X | h y + h T ran Q
172 isoeq5 - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X y - π + X π + X | h y + h T ran Q f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | h y + h T ran Q
173 171 172 ax-mp f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | h y + h T ran Q
174 173 iotabii ι f | f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q = ι f | f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | h y + h T ran Q
175 133 174 eqtri V = ι f | f Isom < , < 0 - π + X π + X y - π + X π + X | k y + k T ran Q 1 - π + X π + X y - π + X π + X | h y + h T ran Q
176 eleq1w v = u v dom F u dom F
177 fveq2 v = u F v = F u
178 176 177 ifbieq1d v = u if v dom F F v 0 = if u dom F F u 0
179 178 cbvmptv v if v dom F F v 0 = u if u dom F F u 0
180 93 148 103 149 150 70 104 105 106 155 157 163 128 175 179 fourierdlem97 φ i 0 ..^ N F V i V i + 1 : V i V i + 1 cn
181 cncff F V i V i + 1 : V i V i + 1 cn F V i V i + 1 : V i V i + 1
182 fdm F V i V i + 1 : V i V i + 1 dom F V i V i + 1 = V i V i + 1
183 180 181 182 3syl φ i 0 ..^ N dom F V i V i + 1 = V i V i + 1
184 ssdmres V i V i + 1 dom F dom F V i V i + 1 = V i V i + 1
185 183 184 sylibr φ i 0 ..^ N V i V i + 1 dom F
186 147 185 fssresd φ i 0 ..^ N F V i V i + 1 : V i V i + 1
187 ax-resscn
188 187 a1i φ i 0 ..^ N
189 cncffvrn F V i V i + 1 : V i V i + 1 cn F V i V i + 1 : V i V i + 1 cn F V i V i + 1 : V i V i + 1
190 188 180 189 syl2anc φ i 0 ..^ N F V i V i + 1 : V i V i + 1 cn F V i V i + 1 : V i V i + 1
191 186 190 mpbird φ i 0 ..^ N F V i V i + 1 : V i V i + 1 cn
192 25 adantr φ i 0 ..^ N z t dom F F t z
193 nfv t φ i 0 ..^ N
194 nfra1 t t dom F F t z
195 193 194 nfan t φ i 0 ..^ N t dom F F t z
196 fvres t V i V i + 1 F V i V i + 1 t = F t
197 196 adantl φ i 0 ..^ N t V i V i + 1 F V i V i + 1 t = F t
198 197 fveq2d φ i 0 ..^ N t V i V i + 1 F V i V i + 1 t = F t
199 198 adantlr φ i 0 ..^ N t dom F F t z t V i V i + 1 F V i V i + 1 t = F t
200 simplr φ i 0 ..^ N t dom F F t z t V i V i + 1 t dom F F t z
201 185 sselda φ i 0 ..^ N t V i V i + 1 t dom F
202 201 adantlr φ i 0 ..^ N t dom F F t z t V i V i + 1 t dom F
203 rspa t dom F F t z t dom F F t z
204 200 202 203 syl2anc φ i 0 ..^ N t dom F F t z t V i V i + 1 F t z
205 199 204 eqbrtrd φ i 0 ..^ N t dom F F t z t V i V i + 1 F V i V i + 1 t z
206 205 ex φ i 0 ..^ N t dom F F t z t V i V i + 1 F V i V i + 1 t z
207 195 206 ralrimi φ i 0 ..^ N t dom F F t z t V i V i + 1 F V i V i + 1 t z
208 207 ex φ i 0 ..^ N t dom F F t z t V i V i + 1 F V i V i + 1 t z
209 208 reximdv φ i 0 ..^ N z t dom F F t z z t V i V i + 1 F V i V i + 1 t z
210 192 209 mpd φ i 0 ..^ N z t V i V i + 1 F V i V i + 1 t z
211 nfra1 t t V i V i + 1 F V i V i + 1 t z
212 196 eqcomd t V i V i + 1 F t = F V i V i + 1 t
213 212 fveq2d t V i V i + 1 F t = F V i V i + 1 t
214 213 adantl t V i V i + 1 F V i V i + 1 t z t V i V i + 1 F t = F V i V i + 1 t
215 rspa t V i V i + 1 F V i V i + 1 t z t V i V i + 1 F V i V i + 1 t z
216 214 215 eqbrtrd t V i V i + 1 F V i V i + 1 t z t V i V i + 1 F t z
217 216 ex t V i V i + 1 F V i V i + 1 t z t V i V i + 1 F t z
218 211 217 ralrimi t V i V i + 1 F V i V i + 1 t z t V i V i + 1 F t z
219 218 a1i φ i 0 ..^ N t V i V i + 1 F V i V i + 1 t z t V i V i + 1 F t z
220 219 reximdv φ i 0 ..^ N z t V i V i + 1 F V i V i + 1 t z z t V i V i + 1 F t z
221 210 220 mpd φ i 0 ..^ N z t V i V i + 1 F t z
222 nfv i φ j 0 ..^ M
223 nfcsb1v _ i j / i C
224 223 nfel1 i j / i C F Q j Q j + 1 lim Q j
225 222 224 nfim i φ j 0 ..^ M j / i C F Q j Q j + 1 lim Q j
226 csbeq1a i = j C = j / i C
227 112 109 oveq12d i = j F Q i Q i + 1 lim Q i = F Q j Q j + 1 lim Q j
228 226 227 eleq12d i = j C F Q i Q i + 1 lim Q i j / i C F Q j Q j + 1 lim Q j
229 108 228 imbi12d i = j φ i 0 ..^ M C F Q i Q i + 1 lim Q i φ j 0 ..^ M j / i C F Q j Q j + 1 lim Q j
230 225 229 13 chvarfv φ j 0 ..^ M j / i C F Q j Q j + 1 lim Q j
231 230 adantlr φ i 0 ..^ N j 0 ..^ M j / i C F Q j Q j + 1 lim Q j
232 93 103 70 104 105 106 117 231 118 124 128 133 fourierdlem96 φ i 0 ..^ N if d π π if d = π π d c c + π c T T V i = Q y sup f 0 ..^ M | Q f d π π if d = π π d c c + π c T T y < V i j 0 ..^ M j / i C y sup f 0 ..^ M | Q f d π π if d = π π d c c + π c T T y < V i F d π π if d = π π d c c + π c T T V i F V i V i + 1 lim V i
233 nfcsb1v _ i j / i U
234 233 nfel1 i j / i U F Q j Q j + 1 lim Q j + 1
235 222 234 nfim i φ j 0 ..^ M j / i U F Q j Q j + 1 lim Q j + 1
236 csbeq1a i = j U = j / i U
237 112 110 oveq12d i = j F Q i Q i + 1 lim Q i + 1 = F Q j Q j + 1 lim Q j + 1
238 236 237 eleq12d i = j U F Q i Q i + 1 lim Q i + 1 j / i U F Q j Q j + 1 lim Q j + 1
239 108 238 imbi12d i = j φ i 0 ..^ M U F Q i Q i + 1 lim Q i + 1 φ j 0 ..^ M j / i U F Q j Q j + 1 lim Q j + 1
240 235 239 14 chvarfv φ j 0 ..^ M j / i U F Q j Q j + 1 lim Q j + 1
241 240 adantlr φ i 0 ..^ N j 0 ..^ M j / i U F Q j Q j + 1 lim Q j + 1
242 93 103 70 104 105 106 117 241 157 163 128 133 fourierdlem99 φ i 0 ..^ N if e e + π e T T V i + 1 = Q y sup h 0 ..^ M | Q h g π π if g = π π g e e + π e T T y < V i + 1 j 0 ..^ M j / i U y sup h 0 ..^ M | Q h g π π if g = π π g e e + π e T T y < V i F e e + π e T T V i + 1 F V i V i + 1 lim V i + 1
243 eqeq1 g = s g = 0 s = 0
244 oveq2 g = s X + g = X + s
245 244 fveq2d g = s F X + g = F X + s
246 breq2 g = s 0 < g 0 < s
247 246 ifbid g = s if 0 < g R L = if 0 < s R L
248 245 247 oveq12d g = s F X + g if 0 < g R L = F X + s if 0 < s R L
249 id g = s g = s
250 248 249 oveq12d g = s F X + g if 0 < g R L g = F X + s if 0 < s R L s
251 243 250 ifbieq2d g = s if g = 0 0 F X + g if 0 < g R L g = if s = 0 0 F X + s if 0 < s R L s
252 251 cbvmptv g π π if g = 0 0 F X + g if 0 < g R L g = s π π if s = 0 0 F X + s if 0 < s R L s
253 eqeq1 o = s o = 0 s = 0
254 id o = s o = s
255 oveq1 o = s o 2 = s 2
256 255 fveq2d o = s sin o 2 = sin s 2
257 256 oveq2d o = s 2 sin o 2 = 2 sin s 2
258 254 257 oveq12d o = s o 2 sin o 2 = s 2 sin s 2
259 253 258 ifbieq2d o = s if o = 0 1 o 2 sin o 2 = if s = 0 1 s 2 sin s 2
260 259 cbvmptv o π π if o = 0 1 o 2 sin o 2 = s π π if s = 0 1 s 2 sin s 2
261 fveq2 r = s g π π if g = 0 0 F X + g if 0 < g R L g r = g π π if g = 0 0 F X + g if 0 < g R L g s
262 fveq2 r = s o π π if o = 0 1 o 2 sin o 2 r = o π π if o = 0 1 o 2 sin o 2 s
263 261 262 oveq12d r = s g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r = g π π if g = 0 0 F X + g if 0 < g R L g s o π π if o = 0 1 o 2 sin o 2 s
264 263 cbvmptv r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r = s π π g π π if g = 0 0 F X + g if 0 < g R L g s o π π if o = 0 1 o 2 sin o 2 s
265 oveq2 d = s k + 1 2 d = k + 1 2 s
266 265 fveq2d d = s sin k + 1 2 d = sin k + 1 2 s
267 266 cbvmptv d π π sin k + 1 2 d = s π π sin k + 1 2 s
268 fveq2 z = s r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s
269 fveq2 z = s d π π sin k + 1 2 d z = d π π sin k + 1 2 d s
270 268 269 oveq12d z = s r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s d π π sin k + 1 2 d s
271 270 cbvmptv z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z = s π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s d π π sin k + 1 2 d s
272 fveq2 m = n D m = D n
273 272 fveq1d m = n D m s = D n s
274 273 oveq2d m = n F X + s D m s = F X + s D n s
275 274 adantr m = n s π 0 F X + s D m s = F X + s D n s
276 275 itgeq2dv m = n π 0 F X + s D m s ds = π 0 F X + s D n s ds
277 276 cbvmptv m π 0 F X + s D m s ds = n π 0 F X + s D n s ds
278 oveq1 c = k c + 1 2 = k + 1 2
279 278 oveq1d c = k c + 1 2 d = k + 1 2 d
280 279 fveq2d c = k sin c + 1 2 d = sin k + 1 2 d
281 280 mpteq2dv c = k d π π sin c + 1 2 d = d π π sin k + 1 2 d
282 281 fveq1d c = k d π π sin c + 1 2 d z = d π π sin k + 1 2 d z
283 282 oveq2d c = k r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z
284 283 mpteq2dv c = k z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z = z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z
285 284 fveq1d c = k z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s = z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s
286 285 adantr c = k s π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s = z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s
287 286 itgeq2dv c = k π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s ds = π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s ds
288 287 oveq1d c = k π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s ds π = π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s ds π
289 288 cbvmptv c π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s ds π = k π 0 z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s ds π
290 oveq1 y = s y mod 2 π = s mod 2 π
291 290 eqeq1d y = s y mod 2 π = 0 s mod 2 π = 0
292 oveq2 y = s m + 1 2 y = m + 1 2 s
293 292 fveq2d y = s sin m + 1 2 y = sin m + 1 2 s
294 oveq1 y = s y 2 = s 2
295 294 fveq2d y = s sin y 2 = sin s 2
296 295 oveq2d y = s 2 π sin y 2 = 2 π sin s 2
297 293 296 oveq12d y = s sin m + 1 2 y 2 π sin y 2 = sin m + 1 2 s 2 π sin s 2
298 291 297 ifbieq2d y = s if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2 = if s mod 2 π = 0 2 m + 1 2 π sin m + 1 2 s 2 π sin s 2
299 298 cbvmptv y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2 = s if s mod 2 π = 0 2 m + 1 2 π sin m + 1 2 s 2 π sin s 2
300 simpl m = k s m = k
301 300 oveq2d m = k s 2 m = 2 k
302 301 oveq1d m = k s 2 m + 1 = 2 k + 1
303 302 oveq1d m = k s 2 m + 1 2 π = 2 k + 1 2 π
304 300 oveq1d m = k s m + 1 2 = k + 1 2
305 304 oveq1d m = k s m + 1 2 s = k + 1 2 s
306 305 fveq2d m = k s sin m + 1 2 s = sin k + 1 2 s
307 306 oveq1d m = k s sin m + 1 2 s 2 π sin s 2 = sin k + 1 2 s 2 π sin s 2
308 303 307 ifeq12d m = k s if s mod 2 π = 0 2 m + 1 2 π sin m + 1 2 s 2 π sin s 2 = if s mod 2 π = 0 2 k + 1 2 π sin k + 1 2 s 2 π sin s 2
309 308 mpteq2dva m = k s if s mod 2 π = 0 2 m + 1 2 π sin m + 1 2 s 2 π sin s 2 = s if s mod 2 π = 0 2 k + 1 2 π sin k + 1 2 s 2 π sin s 2
310 299 309 eqtrid m = k y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2 = s if s mod 2 π = 0 2 k + 1 2 π sin k + 1 2 s 2 π sin s 2
311 310 cbvmptv m y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2 = k s if s mod 2 π = 0 2 k + 1 2 π sin k + 1 2 s 2 π sin s 2
312 2 311 eqtri D = k s if s mod 2 π = 0 2 k + 1 2 π sin k + 1 2 s 2 π sin s 2
313 eqid r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r π l = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r π l
314 eqid π l ran j 0 N V j X π l = π l ran j 0 N V j X π l
315 eqid π l ran j 0 N V j X π l 1 = π l ran j 0 N V j X π l 1
316 isoeq1 u = w u Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l w Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l
317 316 cbviotavw ι u | u Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l = ι w | w Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l
318 fveq2 j = i V j = V i
319 318 oveq1d j = i V j X = V i X
320 319 cbvmptv j 0 N V j X = i 0 N V i X
321 eqid ι m 0 ..^ N | ι u | u Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l b ι u | u Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l b + 1 j 0 N V j X m j 0 N V j X m + 1 = ι m 0 ..^ N | ι u | u Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l b ι u | u Isom < , < 0 π l ran j 0 N V j X π l 1 π l ran j 0 N V j X π l b + 1 j 0 N V j X m j 0 N V j X m + 1
322 fveq2 a = s r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s
323 oveq2 a = s b + 1 2 a = b + 1 2 s
324 323 fveq2d a = s sin b + 1 2 a = sin b + 1 2 s
325 322 324 oveq12d a = s r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s
326 325 cbvitgv l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
327 326 fveq2i l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
328 327 breq1i l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < i 2 l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < i 2
329 328 anbi2i φ i + l π 0 b l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < i 2 φ i + l π 0 b l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < i 2
330 325 cbvitgv π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
331 330 fveq2i π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
332 331 breq1i π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < i 2 π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < i 2
333 329 332 anbi12i φ i + l π 0 b l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < i 2 π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < i 2 φ i + l π 0 b l 0 r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < i 2 π l r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < i 2
334 1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 277 289 19 18 16 17 312 313 314 315 317 320 321 333 fourierdlem103 φ m π 0 F X + s D m s ds L 2
335 nnex V
336 335 mptex m A 0 2 + n = 1 m A n cos n X + B n sin n X V
337 22 336 eqeltri Z V
338 337 a1i φ Z V
339 274 adantr m = n s 0 π F X + s D m s = F X + s D n s
340 339 itgeq2dv m = n 0 π F X + s D m s ds = 0 π F X + s D n s ds
341 340 cbvmptv m 0 π F X + s D m s ds = n 0 π F X + s D n s ds
342 285 adantr c = k s 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s = z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s
343 342 itgeq2dv c = k 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s ds = 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s ds
344 343 oveq1d c = k 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s ds π = 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s ds π
345 344 cbvmptv c 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin c + 1 2 d z s ds π = k 0 π z π π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r z d π π sin k + 1 2 d z s ds π
346 eqid r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r e π = r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r e π
347 eqid e π ran j 0 N V j X e π = e π ran j 0 N V j X e π
348 eqid e π ran j 0 N V j X e π 1 = e π ran j 0 N V j X e π 1
349 isoeq1 u = v u Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π v Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π
350 349 cbviotavw ι u | u Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π = ι v | v Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π
351 eqid ι a 0 ..^ N | ι u | u Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π b ι u | u Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π b + 1 j 0 N V j X a j 0 N V j X a + 1 = ι a 0 ..^ N | ι u | u Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π b ι u | u Isom < , < 0 e π ran j 0 N V j X e π 1 e π ran j 0 N V j X e π b + 1 j 0 N V j X a j 0 N V j X a + 1
352 325 cbvitgv 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
353 352 fveq2i 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
354 353 breq1i 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < q 2 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < q 2
355 354 anbi2i φ q + e 0 π b 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < q 2 φ q + e 0 π b 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < q 2
356 325 cbvitgv e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
357 356 fveq2i e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da = e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds
358 357 breq1i e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < q 2 e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < q 2
359 355 358 anbi12i φ q + e 0 π b 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < q 2 e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r a sin b + 1 2 a da < q 2 φ q + e 0 π b 0 e r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < q 2 e π r π π g π π if g = 0 0 F X + g if 0 < g R L g r o π π if o = 0 1 o 2 sin o 2 r s sin b + 1 2 s ds < q 2
360 1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 341 345 19 18 16 17 312 346 347 348 350 320 351 359 fourierdlem104 φ m 0 π F X + s D m s ds R 2
361 eqidd φ n m π 0 F X + s D m s ds = m π 0 F X + s D m s ds
362 276 adantl φ n m = n π 0 F X + s D m s ds = π 0 F X + s D n s ds
363 simpr φ n n
364 elioore s π 0 s
365 1 adantr φ s F :
366 26 adantr φ s X
367 simpr φ s s
368 366 367 readdcld φ s X + s
369 365 368 ffvelrnd φ s F X + s
370 369 adantlr φ n s F X + s
371 2 dirkerre n s D n s
372 371 adantll φ n s D n s
373 370 372 remulcld φ n s F X + s D n s
374 364 373 sylan2 φ n s π 0 F X + s D n s
375 ioossicc π 0 π 0
376 78 leidi π π
377 79 71 77 ltleii 0 π
378 iccss π π π π 0 π π 0 π π
379 78 71 376 377 378 mp4an π 0 π π
380 375 379 sstri π 0 π π
381 380 a1i φ n π 0 π π
382 ioombl π 0 dom vol
383 382 a1i φ n π 0 dom vol
384 1 adantr φ s π π F :
385 26 adantr φ s π π X
386 73 72 iccssred φ π π
387 386 sselda φ s π π s
388 385 387 readdcld φ s π π X + s
389 384 388 ffvelrnd φ s π π F X + s
390 389 adantlr φ n s π π F X + s
391 iccssre π π π π
392 78 71 391 mp2an π π
393 392 sseli s π π s
394 393 371 sylan2 n s π π D n s
395 394 adantll φ n s π π D n s
396 390 395 remulcld φ n s π π F X + s D n s
397 78 a1i φ n π
398 71 a1i φ n π
399 1 adantr φ n F :
400 26 adantr φ n X
401 91 adantr φ n N
402 92 adantr φ n V n p 0 n | p 0 = - π + X p n = π + X i 0 ..^ n p i < p i + 1 N
403 134 adantlr φ n i 0 ..^ N F V i V i + 1 : V i V i + 1 cn
404 232 adantlr φ n i 0 ..^ N if d π π if d = π π d c c + π c T T V i = Q y sup f 0 ..^ M | Q f d π π if d = π π d c c + π c T T y < V i j 0 ..^ M j / i C y sup f 0 ..^ M | Q f d π π if d = π π d c c + π c T T y < V i F d π π if d = π π d c c + π c T T V i F V i V i + 1 lim V i
405 242 adantlr φ n i 0 ..^ N if e e + π e T T V i + 1 = Q y sup h 0 ..^ M | Q h g π π if g = π π g e e + π e T T y < V i + 1 j 0 ..^ M j / i U y sup h 0 ..^ M | Q h g π π if g = π π g e e + π e T T y < V i F e e + π e T T V i + 1 F V i V i + 1 lim V i + 1
406 2 dirkercncf n D n : cn
407 406 adantl φ n D n : cn
408 eqid s π π F X + s D n s = s π π F X + s D n s
409 397 398 399 400 66 401 402 403 404 405 320 3 407 408 fourierdlem84 φ n s π π F X + s D n s 𝐿 1
410 381 383 396 409 iblss φ n s π 0 F X + s D n s 𝐿 1
411 374 410 itgcl φ n π 0 F X + s D n s ds
412 361 362 363 411 fvmptd φ n m π 0 F X + s D m s ds n = π 0 F X + s D n s ds
413 412 411 eqeltrd φ n m π 0 F X + s D m s ds n
414 eqidd φ n m 0 π F X + s D m s ds = m 0 π F X + s D m s ds
415 340 adantl φ n m = n 0 π F X + s D m s ds = 0 π F X + s D n s ds
416 1 adantr φ s 0 π F :
417 26 adantr φ s 0 π X
418 elioore s 0 π s
419 418 adantl φ s 0 π s
420 417 419 readdcld φ s 0 π X + s
421 416 420 ffvelrnd φ s 0 π F X + s
422 421 adantlr φ n s 0 π F X + s
423 418 371 sylan2 n s 0 π D n s
424 423 adantll φ n s 0 π D n s
425 422 424 remulcld φ n s 0 π F X + s D n s
426 ioossicc 0 π 0 π
427 78 79 76 ltleii π 0
428 71 leidi π π
429 iccss π π π 0 π π 0 π π π
430 78 71 427 428 429 mp4an 0 π π π
431 426 430 sstri 0 π π π
432 431 a1i φ n 0 π π π
433 ioombl 0 π dom vol
434 433 a1i φ n 0 π dom vol
435 432 434 396 409 iblss φ n s 0 π F X + s D n s 𝐿 1
436 425 435 itgcl φ n 0 π F X + s D n s ds
437 414 415 363 436 fvmptd φ n m 0 π F X + s D m s ds n = 0 π F X + s D n s ds
438 437 436 eqeltrd φ n m 0 π F X + s D m s ds n
439 eleq1w m = n m n
440 439 anbi2d m = n φ m φ n
441 fveq2 m = n Z m = Z n
442 276 340 oveq12d m = n π 0 F X + s D m s ds + 0 π F X + s D m s ds = π 0 F X + s D n s ds + 0 π F X + s D n s ds
443 441 442 eqeq12d m = n Z m = π 0 F X + s D m s ds + 0 π F X + s D m s ds Z n = π 0 F X + s D n s ds + 0 π F X + s D n s ds
444 440 443 imbi12d m = n φ m Z m = π 0 F X + s D m s ds + 0 π F X + s D m s ds φ n Z n = π 0 F X + s D n s ds + 0 π F X + s D n s ds
445 oveq1 n = m n x = m x
446 445 fveq2d n = m cos n x = cos m x
447 446 oveq2d n = m F x cos n x = F x cos m x
448 447 adantr n = m x π π F x cos n x = F x cos m x
449 448 itgeq2dv n = m π π F x cos n x dx = π π F x cos m x dx
450 449 oveq1d n = m π π F x cos n x dx π = π π F x cos m x dx π
451 450 cbvmptv n 0 π π F x cos n x dx π = m 0 π π F x cos m x dx π
452 20 451 eqtri A = m 0 π π F x cos m x dx π
453 445 fveq2d n = m sin n x = sin m x
454 453 oveq2d n = m F x sin n x = F x sin m x
455 454 adantr n = m x π π F x sin n x = F x sin m x
456 455 itgeq2dv n = m π π F x sin n x dx = π π F x sin m x dx
457 456 oveq1d n = m π π F x sin n x dx π = π π F x sin m x dx π
458 457 cbvmptv n π π F x sin n x dx π = m π π F x sin m x dx π
459 21 458 eqtri B = m π π F x sin m x dx π
460 fveq2 n = k A n = A k
461 oveq1 n = k n X = k X
462 461 fveq2d n = k cos n X = cos k X
463 460 462 oveq12d n = k A n cos n X = A k cos k X
464 fveq2 n = k B n = B k
465 461 fveq2d n = k sin n X = sin k X
466 464 465 oveq12d n = k B n sin n X = B k sin k X
467 463 466 oveq12d n = k A n cos n X + B n sin n X = A k cos k X + B k sin k X
468 467 cbvsumv n = 1 m A n cos n X + B n sin n X = k = 1 m A k cos k X + B k sin k X
469 468 oveq2i A 0 2 + n = 1 m A n cos n X + B n sin n X = A 0 2 + k = 1 m A k cos k X + B k sin k X
470 469 mpteq2i m A 0 2 + n = 1 m A n cos n X + B n sin n X = m A 0 2 + k = 1 m A k cos k X + B k sin k X
471 oveq2 m = n 1 m = 1 n
472 471 sumeq1d m = n k = 1 m A k cos k X + B k sin k X = k = 1 n A k cos k X + B k sin k X
473 472 oveq2d m = n A 0 2 + k = 1 m A k cos k X + B k sin k X = A 0 2 + k = 1 n A k cos k X + B k sin k X
474 473 cbvmptv m A 0 2 + k = 1 m A k cos k X + B k sin k X = n A 0 2 + k = 1 n A k cos k X + B k sin k X
475 fveq2 k = m A k = A m
476 oveq1 k = m k X = m X
477 476 fveq2d k = m cos k X = cos m X
478 475 477 oveq12d k = m A k cos k X = A m cos m X
479 fveq2 k = m B k = B m
480 476 fveq2d k = m sin k X = sin m X
481 479 480 oveq12d k = m B k sin k X = B m sin m X
482 478 481 oveq12d k = m A k cos k X + B k sin k X = A m cos m X + B m sin m X
483 482 cbvsumv k = 1 n A k cos k X + B k sin k X = m = 1 n A m cos m X + B m sin m X
484 483 oveq2i A 0 2 + k = 1 n A k cos k X + B k sin k X = A 0 2 + m = 1 n A m cos m X + B m sin m X
485 484 mpteq2i n A 0 2 + k = 1 n A k cos k X + B k sin k X = n A 0 2 + m = 1 n A m cos m X + B m sin m X
486 474 485 eqtri m A 0 2 + k = 1 m A k cos k X + B k sin k X = n A 0 2 + m = 1 n A m cos m X + B m sin m X
487 22 470 486 3eqtri Z = n A 0 2 + m = 1 n A m cos m X + B m sin m X
488 oveq2 y = x X + y = X + x
489 488 fveq2d y = x F X + y = F X + x
490 fveq2 y = x D m y = D m x
491 489 490 oveq12d y = x F X + y D m y = F X + x D m x
492 491 cbvmptv y F X + y D m y = x F X + x D m x
493 eqid n p 0 n | p 0 = - π - X p n = π X i 0 ..^ n p i < p i + 1 = n p 0 n | p 0 = - π - X p n = π X i 0 ..^ n p i < p i + 1
494 fveq2 j = i Q j = Q i
495 494 oveq1d j = i Q j X = Q i X
496 495 cbvmptv j 0 M Q j X = i 0 M Q i X
497 452 459 487 2 3 4 5 8 1 11 492 12 13 14 10 493 496 fourierdlem111 φ m Z m = π 0 F X + s D m s ds + 0 π F X + s D m s ds
498 444 497 chvarvv φ n Z n = π 0 F X + s D n s ds + 0 π F X + s D n s ds
499 412 437 oveq12d φ n m π 0 F X + s D m s ds n + m 0 π F X + s D m s ds n = π 0 F X + s D n s ds + 0 π F X + s D n s ds
500 498 499 eqtr4d φ n Z n = m π 0 F X + s D m s ds n + m 0 π F X + s D m s ds n
501 41 49 52 65 39 40 334 338 360 413 438 500 climaddf φ Z L 2 + R 2
502 limccl F −∞ X lim X
503 502 18 sselid φ L
504 limccl F X +∞ lim X
505 504 19 sselid φ R
506 2cnd φ 2
507 2pos 0 < 2
508 507 a1i φ 0 < 2
509 508 gt0ne0d φ 2 0
510 503 505 506 509 divdird φ L + R 2 = L 2 + R 2
511 501 510 breqtrrd φ Z L + R 2
512 0nn0 0 0
513 1 adantr φ 0 0 F :
514 eqid π π = π π
515 ioossre π π
516 515 a1i φ π π
517 1 516 feqresmpt φ F π π = x π π F x
518 ioossicc π π π π
519 518 a1i φ π π π π
520 ioombl π π dom vol
521 520 a1i φ π π dom vol
522 1 adantr φ x π π F :
523 386 sselda φ x π π x
524 522 523 ffvelrnd φ x π π F x
525 1 386 feqresmpt φ F π π = x π π F x
526 187 a1i φ
527 1 526 fssd φ F :
528 527 386 fssresd φ F π π : π π
529 ioossicc Q i Q i + 1 Q i Q i + 1
530 78 rexri π *
531 530 a1i φ i 0 ..^ M π *
532 71 rexri π *
533 532 a1i φ i 0 ..^ M π *
534 3 4 5 fourierdlem15 φ Q : 0 M π π
535 534 adantr φ i 0 ..^ M Q : 0 M π π
536 simpr φ i 0 ..^ M i 0 ..^ M
537 531 533 535 536 fourierdlem8 φ i 0 ..^ M Q i Q i + 1 π π
538 529 537 sstrid φ i 0 ..^ M Q i Q i + 1 π π
539 538 resabs1d φ i 0 ..^ M F π π Q i Q i + 1 = F Q i Q i + 1
540 539 12 eqeltrd φ i 0 ..^ M F π π Q i Q i + 1 : Q i Q i + 1 cn
541 539 eqcomd φ i 0 ..^ M F Q i Q i + 1 = F π π Q i Q i + 1
542 541 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i = F π π Q i Q i + 1 lim Q i
543 13 542 eleqtrd φ i 0 ..^ M C F π π Q i Q i + 1 lim Q i
544 541 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1 = F π π Q i Q i + 1 lim Q i + 1
545 14 544 eleqtrd φ i 0 ..^ M U F π π Q i Q i + 1 lim Q i + 1
546 3 4 5 528 540 543 545 fourierdlem69 φ F π π 𝐿 1
547 525 546 eqeltrrd φ x π π F x 𝐿 1
548 519 521 524 547 iblss φ x π π F x 𝐿 1
549 517 548 eqeltrd φ F π π 𝐿 1
550 549 adantr φ 0 0 F π π 𝐿 1
551 simpr φ 0 0 0 0
552 513 514 550 20 551 fourierdlem16 φ 0 0 A 0 x π π F x 𝐿 1 π π F x cos 0 x dx
553 552 simplld φ 0 0 A 0
554 512 553 mpan2 φ A 0
555 554 rehalfcld φ A 0 2
556 555 recnd φ A 0 2
557 335 mptex n k = 1 n A k cos k X + B k sin k X V
558 557 a1i φ n k = 1 n A k cos k X + B k sin k X V
559 simpr φ m m
560 555 adantr φ m A 0 2
561 fzfid φ m 1 m Fin
562 simpll φ m n 1 m φ
563 elfznn n 1 m n
564 563 adantl φ m n 1 m n
565 simpl φ n φ
566 363 nnnn0d φ n n 0
567 eleq1w k = n k 0 n 0
568 567 anbi2d k = n φ k 0 φ n 0
569 fveq2 k = n A k = A n
570 569 eleq1d k = n A k A n
571 568 570 imbi12d k = n φ k 0 A k φ n 0 A n
572 1 adantr φ k 0 F :
573 549 adantr φ k 0 F π π 𝐿 1
574 simpr φ k 0 k 0
575 572 514 573 20 574 fourierdlem16 φ k 0 A k x π π F x 𝐿 1 π π F x cos k x dx
576 575 simplld φ k 0 A k
577 571 576 chvarvv φ n 0 A n
578 565 566 577 syl2anc φ n A n
579 363 nnred φ n n
580 579 400 remulcld φ n n X
581 580 recoscld φ n cos n X
582 578 581 remulcld φ n A n cos n X
583 eleq1w k = n k n
584 583 anbi2d k = n φ k φ n
585 fveq2 k = n B k = B n
586 585 eleq1d k = n B k B n
587 584 586 imbi12d k = n φ k B k φ n B n
588 1 adantr φ k F :
589 549 adantr φ k F π π 𝐿 1
590 simpr φ k k
591 588 514 589 21 590 fourierdlem21 φ k B k x π π F x sin k x 𝐿 1 π π F x sin k x dx
592 591 simplld φ k B k
593 587 592 chvarvv φ n B n
594 580 resincld φ n sin n X
595 593 594 remulcld φ n B n sin n X
596 582 595 readdcld φ n A n cos n X + B n sin n X
597 562 564 596 syl2anc φ m n 1 m A n cos n X + B n sin n X
598 561 597 fsumrecl φ m n = 1 m A n cos n X + B n sin n X
599 560 598 readdcld φ m A 0 2 + n = 1 m A n cos n X + B n sin n X
600 22 fvmpt2 m A 0 2 + n = 1 m A n cos n X + B n sin n X Z m = A 0 2 + n = 1 m A n cos n X + B n sin n X
601 559 599 600 syl2anc φ m Z m = A 0 2 + n = 1 m A n cos n X + B n sin n X
602 601 599 eqeltrd φ m Z m
603 602 recnd φ m Z m
604 eqidd φ m n k = 1 n A k cos k X + B k sin k X = n k = 1 n A k cos k X + B k sin k X
605 oveq2 n = m 1 n = 1 m
606 605 sumeq1d n = m k = 1 n A k cos k X + B k sin k X = k = 1 m A k cos k X + B k sin k X
607 606 adantl φ m n = m k = 1 n A k cos k X + B k sin k X = k = 1 m A k cos k X + B k sin k X
608 sumex k = 1 m A k cos k X + B k sin k X V
609 608 a1i φ m k = 1 m A k cos k X + B k sin k X V
610 604 607 559 609 fvmptd φ m n k = 1 n A k cos k X + B k sin k X m = k = 1 m A k cos k X + B k sin k X
611 560 recnd φ m A 0 2
612 598 recnd φ m n = 1 m A n cos n X + B n sin n X
613 611 612 pncan2d φ m A 0 2 + n = 1 m A n cos n X + B n sin n X - A 0 2 = n = 1 m A n cos n X + B n sin n X
614 613 468 eqtr2di φ m k = 1 m A k cos k X + B k sin k X = A 0 2 + n = 1 m A n cos n X + B n sin n X - A 0 2
615 ovex A 0 2 + n = 1 m A n cos n X + B n sin n X V
616 22 fvmpt2 m A 0 2 + n = 1 m A n cos n X + B n sin n X V Z m = A 0 2 + n = 1 m A n cos n X + B n sin n X
617 559 615 616 sylancl φ m Z m = A 0 2 + n = 1 m A n cos n X + B n sin n X
618 617 eqcomd φ m A 0 2 + n = 1 m A n cos n X + B n sin n X = Z m
619 618 oveq1d φ m A 0 2 + n = 1 m A n cos n X + B n sin n X - A 0 2 = Z m A 0 2
620 610 614 619 3eqtrd φ m n k = 1 n A k cos k X + B k sin k X m = Z m A 0 2
621 39 40 511 556 558 603 620 climsubc1 φ n k = 1 n A k cos k X + B k sin k X L + R 2 A 0 2
622 seqex seq 1 + j A j cos j X + B j sin j X V
623 622 a1i φ seq 1 + j A j cos j X + B j sin j X V
624 eqidd φ l n k = 1 n A k cos k X + B k sin k X = n k = 1 n A k cos k X + B k sin k X
625 oveq2 n = l 1 n = 1 l
626 625 sumeq1d n = l k = 1 n A k cos k X + B k sin k X = k = 1 l A k cos k X + B k sin k X
627 626 adantl φ l n = l k = 1 n A k cos k X + B k sin k X = k = 1 l A k cos k X + B k sin k X
628 simpr φ l l
629 fzfid φ l 1 l Fin
630 elfznn k 1 l k
631 630 nnnn0d k 1 l k 0
632 631 576 sylan2 φ k 1 l A k
633 630 nnred k 1 l k
634 633 adantl φ k 1 l k
635 8 adantr φ k 1 l X
636 634 635 remulcld φ k 1 l k X
637 636 recoscld φ k 1 l cos k X
638 632 637 remulcld φ k 1 l A k cos k X
639 630 592 sylan2 φ k 1 l B k
640 636 resincld φ k 1 l sin k X
641 639 640 remulcld φ k 1 l B k sin k X
642 638 641 readdcld φ k 1 l A k cos k X + B k sin k X
643 642 adantlr φ l k 1 l A k cos k X + B k sin k X
644 629 643 fsumrecl φ l k = 1 l A k cos k X + B k sin k X
645 624 627 628 644 fvmptd φ l n k = 1 n A k cos k X + B k sin k X l = k = 1 l A k cos k X + B k sin k X
646 eleq1w n = l n l
647 646 anbi2d n = l φ n φ l
648 fveq2 n = l seq 1 + j A j cos j X + B j sin j X n = seq 1 + j A j cos j X + B j sin j X l
649 626 648 eqeq12d n = l k = 1 n A k cos k X + B k sin k X = seq 1 + j A j cos j X + B j sin j X n k = 1 l A k cos k X + B k sin k X = seq 1 + j A j cos j X + B j sin j X l
650 647 649 imbi12d n = l φ n k = 1 n A k cos k X + B k sin k X = seq 1 + j A j cos j X + B j sin j X n φ l k = 1 l A k cos k X + B k sin k X = seq 1 + j A j cos j X + B j sin j X l
651 eqidd φ n k 1 n j A j cos j X + B j sin j X = j A j cos j X + B j sin j X
652 fveq2 j = k A j = A k
653 oveq1 j = k j X = k X
654 653 fveq2d j = k cos j X = cos k X
655 652 654 oveq12d j = k A j cos j X = A k cos k X
656 fveq2 j = k B j = B k
657 653 fveq2d j = k sin j X = sin k X
658 656 657 oveq12d j = k B j sin j X = B k sin k X
659 655 658 oveq12d j = k A j cos j X + B j sin j X = A k cos k X + B k sin k X
660 659 adantl φ n k 1 n j = k A j cos j X + B j sin j X = A k cos k X + B k sin k X
661 elfznn k 1 n k
662 661 adantl φ n k 1 n k
663 simpll φ n k 1 n φ
664 nnnn0 k k 0
665 nn0re k 0 k
666 665 adantl φ k 0 k
667 8 adantr φ k 0 X
668 666 667 remulcld φ k 0 k X
669 668 recoscld φ k 0 cos k X
670 576 669 remulcld φ k 0 A k cos k X
671 664 670 sylan2 φ k A k cos k X
672 664 668 sylan2 φ k k X
673 672 resincld φ k sin k X
674 592 673 remulcld φ k B k sin k X
675 671 674 readdcld φ k A k cos k X + B k sin k X
676 663 662 675 syl2anc φ n k 1 n A k cos k X + B k sin k X
677 651 660 662 676 fvmptd φ n k 1 n j A j cos j X + B j sin j X k = A k cos k X + B k sin k X
678 363 39 eleqtrdi φ n n 1
679 676 recnd φ n k 1 n A k cos k X + B k sin k X
680 677 678 679 fsumser φ n k = 1 n A k cos k X + B k sin k X = seq 1 + j A j cos j X + B j sin j X n
681 650 680 chvarvv φ l k = 1 l A k cos k X + B k sin k X = seq 1 + j A j cos j X + B j sin j X l
682 645 681 eqtrd φ l n k = 1 n A k cos k X + B k sin k X l = seq 1 + j A j cos j X + B j sin j X l
683 39 558 623 40 682 climeq φ n k = 1 n A k cos k X + B k sin k X L + R 2 A 0 2 seq 1 + j A j cos j X + B j sin j X L + R 2 A 0 2
684 621 683 mpbid φ seq 1 + j A j cos j X + B j sin j X L + R 2 A 0 2
685 38 684 eqbrtrd φ seq 1 + S L + R 2 A 0 2
686 eqidd φ n j A j cos j X + B j sin j X = j A j cos j X + B j sin j X
687 fveq2 j = n A j = A n
688 oveq1 j = n j X = n X
689 688 fveq2d j = n cos j X = cos n X
690 687 689 oveq12d j = n A j cos j X = A n cos n X
691 fveq2 j = n B j = B n
692 688 fveq2d j = n sin j X = sin n X
693 691 692 oveq12d j = n B j sin j X = B n sin n X
694 690 693 oveq12d j = n A j cos j X + B j sin j X = A n cos n X + B n sin n X
695 694 adantl φ n j = n A j cos j X + B j sin j X = A n cos n X + B n sin n X
696 686 695 363 596 fvmptd φ n j A j cos j X + B j sin j X n = A n cos n X + B n sin n X
697 596 recnd φ n A n cos n X + B n sin n X
698 39 40 696 697 684 isumclim φ n A n cos n X + B n sin n X = L + R 2 A 0 2
699 698 oveq2d φ A 0 2 + n A n cos n X + B n sin n X = A 0 2 + L + R 2 - A 0 2
700 503 505 addcld φ L + R
701 700 halfcld φ L + R 2
702 556 701 pncan3d φ A 0 2 + L + R 2 - A 0 2 = L + R 2
703 699 702 eqtrd φ A 0 2 + n A n cos n X + B n sin n X = L + R 2
704 685 703 jca φ seq 1 + S L + R 2 A 0 2 A 0 2 + n A n cos n X + B n sin n X = L + R 2