Metamath Proof Explorer


Theorem fourierdlem95

Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem95.f φ F :
fourierdlem95.xre φ X
fourierdlem95.p P = m p 0 m | p 0 = - π + X p m = π + X i 0 ..^ m p i < p i + 1
fourierdlem95.m φ M
fourierdlem95.v φ V P M
fourierdlem95.x φ X ran V
fourierdlem95.fcn φ i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
fourierdlem95.r φ i 0 ..^ M R F V i V i + 1 lim V i
fourierdlem95.l φ i 0 ..^ M L F V i V i + 1 lim V i + 1
fourierdlem95.h H = s π π if s = 0 0 F X + s if 0 < s Y W s
fourierdlem95.k K = s π π if s = 0 1 s 2 sin s 2
fourierdlem95.u U = s π π H s K s
fourierdlem95.s S = s π π sin n + 1 2 s
fourierdlem95.g G = s π π U s S s
fourierdlem95.i I = D F
fourierdlem95.ifn φ i 0 ..^ M I V i V i + 1 : V i V i + 1
fourierdlem95.b φ B I −∞ X lim X
fourierdlem95.c φ C I X +∞ lim X
fourierdlem95.y φ Y F X +∞ lim X
fourierdlem95.w φ W F −∞ X lim X
fourierdlem95.admvol φ A dom vol
fourierdlem95.ass φ A π π 0
fourierlemenplusacver2eqitgdirker.e E = n A G s ds π
fourierdlem95.d D = n s if s mod 2 π = 0 2 n + 1 2 π sin n + 1 2 s 2 π sin s 2
fourierdlem95.o φ O
fourierdlem95.ifeqo φ s A if 0 < s Y W = O
fourierdlem95.itgdirker φ n A D n s ds = 1 2
Assertion fourierdlem95 φ n E n + O 2 = A F X + s D n s ds

Proof

Step Hyp Ref Expression
1 fourierdlem95.f φ F :
2 fourierdlem95.xre φ X
3 fourierdlem95.p P = m p 0 m | p 0 = - π + X p m = π + X i 0 ..^ m p i < p i + 1
4 fourierdlem95.m φ M
5 fourierdlem95.v φ V P M
6 fourierdlem95.x φ X ran V
7 fourierdlem95.fcn φ i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
8 fourierdlem95.r φ i 0 ..^ M R F V i V i + 1 lim V i
9 fourierdlem95.l φ i 0 ..^ M L F V i V i + 1 lim V i + 1
10 fourierdlem95.h H = s π π if s = 0 0 F X + s if 0 < s Y W s
11 fourierdlem95.k K = s π π if s = 0 1 s 2 sin s 2
12 fourierdlem95.u U = s π π H s K s
13 fourierdlem95.s S = s π π sin n + 1 2 s
14 fourierdlem95.g G = s π π U s S s
15 fourierdlem95.i I = D F
16 fourierdlem95.ifn φ i 0 ..^ M I V i V i + 1 : V i V i + 1
17 fourierdlem95.b φ B I −∞ X lim X
18 fourierdlem95.c φ C I X +∞ lim X
19 fourierdlem95.y φ Y F X +∞ lim X
20 fourierdlem95.w φ W F −∞ X lim X
21 fourierdlem95.admvol φ A dom vol
22 fourierdlem95.ass φ A π π 0
23 fourierlemenplusacver2eqitgdirker.e E = n A G s ds π
24 fourierdlem95.d D = n s if s mod 2 π = 0 2 n + 1 2 π sin n + 1 2 s 2 π sin s 2
25 fourierdlem95.o φ O
26 fourierdlem95.ifeqo φ s A if 0 < s Y W = O
27 fourierdlem95.itgdirker φ n A D n s ds = 1 2
28 simpr φ n n
29 22 difss2d φ A π π
30 29 adantr φ n A π π
31 30 sselda φ n s A s π π
32 1 adantr φ n F :
33 2 adantr φ n X
34 ioossre X +∞
35 34 a1i φ X +∞
36 1 35 fssresd φ F X +∞ : X +∞
37 ioosscn X +∞
38 37 a1i φ X +∞
39 eqid TopOpen fld = TopOpen fld
40 pnfxr +∞ *
41 40 a1i φ +∞ *
42 2 ltpnfd φ X < +∞
43 39 41 2 42 lptioo1cn φ X limPt TopOpen fld X +∞
44 36 38 43 19 limcrecl φ Y
45 44 adantr φ n Y
46 ioossre −∞ X
47 46 a1i φ −∞ X
48 1 47 fssresd φ F −∞ X : −∞ X
49 ioosscn −∞ X
50 49 a1i φ −∞ X
51 mnfxr −∞ *
52 51 a1i φ −∞ *
53 2 mnfltd φ −∞ < X
54 39 52 2 53 lptioo2cn φ X limPt TopOpen fld −∞ X
55 48 50 54 20 limcrecl φ W
56 55 adantr φ n W
57 28 nnred φ n n
58 32 33 45 56 10 11 12 57 13 14 fourierdlem67 φ n G : π π
59 58 ffvelrnda φ n s π π G s
60 31 59 syldan φ n s A G s
61 21 adantr φ n A dom vol
62 58 feqmptd φ n G = s π π G s
63 6 adantr φ n X ran V
64 19 adantr φ n Y F X +∞ lim X
65 20 adantr φ n W F −∞ X lim X
66 4 adantr φ n M
67 5 adantr φ n V P M
68 7 adantlr φ n i 0 ..^ M F V i V i + 1 : V i V i + 1 cn
69 8 adantlr φ n i 0 ..^ M R F V i V i + 1 lim V i
70 9 adantlr φ n i 0 ..^ M L F V i V i + 1 lim V i + 1
71 fveq2 j = i V j = V i
72 71 oveq1d j = i V j X = V i X
73 72 cbvmptv j 0 M V j X = i 0 M V i X
74 eqid m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = π p m = π i 0 ..^ m p i < p i + 1
75 16 adantlr φ n i 0 ..^ M I V i V i + 1 : V i V i + 1
76 17 adantr φ n B I −∞ X lim X
77 18 adantr φ n C I X +∞ lim X
78 3 32 63 64 65 10 11 12 57 13 14 66 67 68 69 70 73 74 15 75 76 77 fourierdlem88 φ n G 𝐿 1
79 62 78 eqeltrrd φ n s π π G s 𝐿 1
80 30 61 59 79 iblss φ n s A G s 𝐿 1
81 60 80 itgrecl φ n A G s ds
82 pire π
83 82 a1i φ n π
84 pipos 0 < π
85 82 84 gt0ne0ii π 0
86 85 a1i φ n π 0
87 81 83 86 redivcld φ n A G s ds π
88 23 fvmpt2 n A G s ds π E n = A G s ds π
89 28 87 88 syl2anc φ n E n = A G s ds π
90 25 recnd φ O
91 2cnd φ 2
92 2ne0 2 0
93 92 a1i φ 2 0
94 90 91 93 divrecd φ O 2 = O 1 2
95 94 adantr φ n O 2 = O 1 2
96 27 eqcomd φ n 1 2 = A D n s ds
97 96 oveq2d φ n O 1 2 = O A D n s ds
98 95 97 eqtrd φ n O 2 = O A D n s ds
99 89 98 oveq12d φ n E n + O 2 = A G s ds π + O A D n s ds
100 22 sselda φ s A s π π 0
101 100 adantlr φ n s A s π π 0
102 eqid π π 0 = π π 0
103 1 2 44 55 24 10 11 12 13 14 102 fourierdlem66 φ n s π π 0 G s = π F X + s if 0 < s Y W D n s
104 101 103 syldan φ n s A G s = π F X + s if 0 < s Y W D n s
105 104 itgeq2dv φ n A G s ds = A π F X + s if 0 < s Y W D n s ds
106 105 oveq1d φ n A G s ds π = A π F X + s if 0 < s Y W D n s ds π
107 83 recnd φ n π
108 1 adantr φ s A F :
109 2 adantr φ s A X
110 difss π π 0 π π
111 82 renegcli π
112 iccssre π π π π
113 111 82 112 mp2an π π
114 110 113 sstri π π 0
115 114 100 sseldi φ s A s
116 109 115 readdcld φ s A X + s
117 108 116 ffvelrnd φ s A F X + s
118 44 55 ifcld φ if 0 < s Y W
119 118 adantr φ s A if 0 < s Y W
120 117 119 resubcld φ s A F X + s if 0 < s Y W
121 120 adantlr φ n s A F X + s if 0 < s Y W
122 28 adantr φ n s A n
123 115 adantlr φ n s A s
124 24 dirkerre n s D n s
125 122 123 124 syl2anc φ n s A D n s
126 121 125 remulcld φ n s A F X + s if 0 < s Y W D n s
127 104 eqcomd φ n s A π F X + s if 0 < s Y W D n s = G s
128 127 oveq1d φ n s A π F X + s if 0 < s Y W D n s π = G s π
129 picn π
130 129 a1i φ n s A π
131 126 recnd φ n s A F X + s if 0 < s Y W D n s
132 85 a1i φ n s A π 0
133 130 131 130 132 div23d φ n s A π F X + s if 0 < s Y W D n s π = π π F X + s if 0 < s Y W D n s
134 60 recnd φ n s A G s
135 134 130 132 divrec2d φ n s A G s π = 1 π G s
136 128 133 135 3eqtr3rd φ n s A 1 π G s = π π F X + s if 0 < s Y W D n s
137 129 85 dividi π π = 1
138 137 a1i φ n s A π π = 1
139 138 oveq1d φ n s A π π F X + s if 0 < s Y W D n s = 1 F X + s if 0 < s Y W D n s
140 131 mulid2d φ n s A 1 F X + s if 0 < s Y W D n s = F X + s if 0 < s Y W D n s
141 136 139 140 3eqtrrd φ n s A F X + s if 0 < s Y W D n s = 1 π G s
142 141 mpteq2dva φ n s A F X + s if 0 < s Y W D n s = s A 1 π G s
143 107 86 reccld φ n 1 π
144 143 60 80 iblmulc2 φ n s A 1 π G s 𝐿 1
145 142 144 eqeltrd φ n s A F X + s if 0 < s Y W D n s 𝐿 1
146 107 126 145 itgmulc2 φ n π A F X + s if 0 < s Y W D n s ds = A π F X + s if 0 < s Y W D n s ds
147 146 eqcomd φ n A π F X + s if 0 < s Y W D n s ds = π A F X + s if 0 < s Y W D n s ds
148 147 oveq1d φ n A π F X + s if 0 < s Y W D n s ds π = π A F X + s if 0 < s Y W D n s ds π
149 126 145 itgcl φ n A F X + s if 0 < s Y W D n s ds
150 149 107 86 divcan3d φ n π A F X + s if 0 < s Y W D n s ds π = A F X + s if 0 < s Y W D n s ds
151 106 148 150 3eqtrd φ n A G s ds π = A F X + s if 0 < s Y W D n s ds
152 90 adantr φ n O
153 113 sseli s π π s
154 153 124 sylan2 n s π π D n s
155 154 adantll φ n s π π D n s
156 111 a1i φ n π
157 ax-resscn
158 157 a1i n
159 ssid
160 cncfss π π cn π π cn
161 158 159 160 sylancl n π π cn π π cn
162 eqid s D n s = s D n s
163 24 dirkerf n D n :
164 163 feqmptd n D n = s D n s
165 24 dirkercncf n D n : cn
166 164 165 eqeltrrd n s D n s : cn
167 113 a1i n π π
168 ssid
169 168 a1i n
170 162 166 167 169 154 cncfmptssg n s π π D n s : π π cn
171 161 170 sseldd n s π π D n s : π π cn
172 171 adantl φ n s π π D n s : π π cn
173 cniccibl π π s π π D n s : π π cn s π π D n s 𝐿 1
174 156 83 172 173 syl3anc φ n s π π D n s 𝐿 1
175 30 61 155 174 iblss φ n s A D n s 𝐿 1
176 152 125 175 itgmulc2 φ n O A D n s ds = A O D n s ds
177 151 176 oveq12d φ n A G s ds π + O A D n s ds = A F X + s if 0 < s Y W D n s ds + A O D n s ds
178 25 ad2antrr φ n s A O
179 178 125 remulcld φ n s A O D n s
180 152 125 175 iblmulc2 φ n s A O D n s 𝐿 1
181 126 145 179 180 itgadd φ n A F X + s if 0 < s Y W D n s + O D n s ds = A F X + s if 0 < s Y W D n s ds + A O D n s ds
182 26 eqcomd φ s A O = if 0 < s Y W
183 182 adantlr φ n s A O = if 0 < s Y W
184 183 oveq1d φ n s A O D n s = if 0 < s Y W D n s
185 184 oveq2d φ n s A F X + s if 0 < s Y W D n s + O D n s = F X + s if 0 < s Y W D n s + if 0 < s Y W D n s
186 117 recnd φ s A F X + s
187 186 adantlr φ n s A F X + s
188 119 recnd φ s A if 0 < s Y W
189 188 adantlr φ n s A if 0 < s Y W
190 125 recnd φ n s A D n s
191 187 189 190 subdird φ n s A F X + s if 0 < s Y W D n s = F X + s D n s if 0 < s Y W D n s
192 191 oveq1d φ n s A F X + s if 0 < s Y W D n s + if 0 < s Y W D n s = F X + s D n s - if 0 < s Y W D n s + if 0 < s Y W D n s
193 187 190 mulcld φ n s A F X + s D n s
194 189 190 mulcld φ n s A if 0 < s Y W D n s
195 193 194 npcand φ n s A F X + s D n s - if 0 < s Y W D n s + if 0 < s Y W D n s = F X + s D n s
196 185 192 195 3eqtrd φ n s A F X + s if 0 < s Y W D n s + O D n s = F X + s D n s
197 196 itgeq2dv φ n A F X + s if 0 < s Y W D n s + O D n s ds = A F X + s D n s ds
198 181 197 eqtr3d φ n A F X + s if 0 < s Y W D n s ds + A O D n s ds = A F X + s D n s ds
199 99 177 198 3eqtrd φ n E n + O 2 = A F X + s D n s ds