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 syl5eq 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