Metamath Proof Explorer


Theorem fourierdlem107

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any positive value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem107.a φ A
fourierdlem107.b φ B
fourierdlem107.t T = B A
fourierdlem107.x φ X +
fourierdlem107.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem107.m φ M
fourierdlem107.q φ Q P M
fourierdlem107.f φ F :
fourierdlem107.fper φ x F x + T = F x
fourierdlem107.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem107.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
fourierdlem107.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
fourierdlem107.o O = m p 0 m | p 0 = A X p m = A i 0 ..^ m p i < p i + 1
fourierdlem107.h H = A X A y A X A | k y + k T ran Q
fourierdlem107.n N = H 1
fourierdlem107.s S = ι f | f Isom < , < 0 N H
fourierdlem107.e E = x x + B x T T
fourierdlem107.z Z = y A B if y = B A y
fourierdlem107.i I = x sup i 0 ..^ M | Q i Z E x <
Assertion fourierdlem107 φ A X B X F x dx = A B F x dx

Proof

Step Hyp Ref Expression
1 fourierdlem107.a φ A
2 fourierdlem107.b φ B
3 fourierdlem107.t T = B A
4 fourierdlem107.x φ X +
5 fourierdlem107.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
6 fourierdlem107.m φ M
7 fourierdlem107.q φ Q P M
8 fourierdlem107.f φ F :
9 fourierdlem107.fper φ x F x + T = F x
10 fourierdlem107.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
11 fourierdlem107.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
12 fourierdlem107.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
13 fourierdlem107.o O = m p 0 m | p 0 = A X p m = A i 0 ..^ m p i < p i + 1
14 fourierdlem107.h H = A X A y A X A | k y + k T ran Q
15 fourierdlem107.n N = H 1
16 fourierdlem107.s S = ι f | f Isom < , < 0 N H
17 fourierdlem107.e E = x x + B x T T
18 fourierdlem107.z Z = y A B if y = B A y
19 fourierdlem107.i I = x sup i 0 ..^ M | Q i Z E x <
20 3 oveq2i A - X + T = A X + B - A
21 1 recnd φ A
22 4 rpred φ X
23 22 recnd φ X
24 2 recnd φ B
25 21 23 24 21 subadd4b φ A X + B - A = A A + B - X
26 20 25 syl5eq φ A - X + T = A A + B - X
27 21 subidd φ A A = 0
28 27 oveq1d φ A A + B - X = 0 + B - X
29 2 22 resubcld φ B X
30 29 recnd φ B X
31 30 addid2d φ 0 + B - X = B X
32 26 28 31 3eqtrd φ A - X + T = B X
33 3 oveq2i A + T = A + B - A
34 21 24 pncan3d φ A + B - A = B
35 33 34 syl5eq φ A + T = B
36 32 35 oveq12d φ A - X + T A + T = B X B
37 36 eqcomd φ B X B = A - X + T A + T
38 37 itgeq1d φ B X B F x dx = A - X + T A + T F x dx
39 1 22 resubcld φ A X
40 fveq2 i = j p i = p j
41 oveq1 i = j i + 1 = j + 1
42 41 fveq2d i = j p i + 1 = p j + 1
43 40 42 breq12d i = j p i < p i + 1 p j < p j + 1
44 43 cbvralvw i 0 ..^ m p i < p i + 1 j 0 ..^ m p j < p j + 1
45 44 a1i m i 0 ..^ m p i < p i + 1 j 0 ..^ m p j < p j + 1
46 45 anbi2d m p 0 = A X p m = A i 0 ..^ m p i < p i + 1 p 0 = A X p m = A j 0 ..^ m p j < p j + 1
47 46 rabbidv m p 0 m | p 0 = A X p m = A i 0 ..^ m p i < p i + 1 = p 0 m | p 0 = A X p m = A j 0 ..^ m p j < p j + 1
48 47 mpteq2ia m p 0 m | p 0 = A X p m = A i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = A X p m = A j 0 ..^ m p j < p j + 1
49 13 48 eqtri O = m p 0 m | p 0 = A X p m = A j 0 ..^ m p j < p j + 1
50 1 4 ltsubrpd φ A X < A
51 3 5 6 7 39 1 50 13 14 15 16 fourierdlem54 φ N S O N S Isom < , < 0 N H
52 51 simpld φ N S O N
53 52 simpld φ N
54 2 1 resubcld φ B A
55 3 54 eqeltrid φ T
56 52 simprd φ S O N
57 39 adantr φ x A X A A X
58 1 adantr φ x A X A A
59 simpr φ x A X A x A X A
60 eliccre A X A x A X A x
61 57 58 59 60 syl3anc φ x A X A x
62 61 9 syldan φ x A X A F x + T = F x
63 fveq2 i = j S i = S j
64 63 oveq1d i = j S i + T = S j + T
65 64 cbvmptv i 0 N S i + T = j 0 N S j + T
66 eqid m p 0 m | p 0 = A - X + T p m = A + T j 0 ..^ m p j < p j + 1 = m p 0 m | p 0 = A - X + T p m = A + T j 0 ..^ m p j < p j + 1
67 6 adantr φ j 0 ..^ N M
68 7 adantr φ j 0 ..^ N Q P M
69 8 adantr φ j 0 ..^ N F :
70 9 adantlr φ j 0 ..^ N x F x + T = F x
71 10 adantlr φ j 0 ..^ N i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
72 39 adantr φ j 0 ..^ N A X
73 72 rexrd φ j 0 ..^ N A X *
74 pnfxr +∞ *
75 74 a1i φ j 0 ..^ N +∞ *
76 1 adantr φ j 0 ..^ N A
77 50 adantr φ j 0 ..^ N A X < A
78 1 ltpnfd φ A < +∞
79 78 adantr φ j 0 ..^ N A < +∞
80 73 75 76 77 79 eliood φ j 0 ..^ N A A X +∞
81 simpr φ j 0 ..^ N j 0 ..^ N
82 eqid S j + 1 E S j + 1 = S j + 1 E S j + 1
83 eqid F Z E S j E S j + 1 = F Z E S j E S j + 1
84 eqid y Z E S j + S j + 1 - E S j + 1 E S j + 1 + S j + 1 - E S j + 1 F Z E S j E S j + 1 y S j + 1 E S j + 1 = y Z E S j + S j + 1 - E S j + 1 E S j + 1 + S j + 1 - E S j + 1 F Z E S j E S j + 1 y S j + 1 E S j + 1
85 5 3 67 68 69 70 71 72 80 13 14 15 16 17 18 81 82 83 84 19 fourierdlem90 φ j 0 ..^ N F S j S j + 1 : S j S j + 1 cn
86 11 adantlr φ j 0 ..^ N i 0 ..^ M R F Q i Q i + 1 lim Q i
87 eqid i 0 ..^ M R = i 0 ..^ M R
88 5 3 67 68 69 70 71 86 72 80 13 14 15 16 17 18 81 82 19 87 fourierdlem89 φ j 0 ..^ N if Z E S j = Q I S j i 0 ..^ M R I S j F Z E S j F S j S j + 1 lim S j
89 12 adantlr φ j 0 ..^ N i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
90 eqid i 0 ..^ M L = i 0 ..^ M L
91 5 3 67 68 69 70 71 89 72 80 13 14 15 16 17 18 81 82 19 90 fourierdlem91 φ j 0 ..^ N if E S j + 1 = Q I S j + 1 i 0 ..^ M L I S j F E S j + 1 F S j S j + 1 lim S j + 1
92 39 1 49 53 55 56 62 65 66 8 85 88 91 fourierdlem92 φ A - X + T A + T F x dx = A X A F x dx
93 38 92 eqtrd φ B X B F x dx = A X A F x dx
94 8 adantr φ x B X B F :
95 29 adantr φ x B X B B X
96 2 adantr φ x B X B B
97 simpr φ x B X B x B X B
98 eliccre B X B x B X B x
99 95 96 97 98 syl3anc φ x B X B x
100 94 99 ffvelrnd φ x B X B F x
101 29 rexrd φ B X *
102 74 a1i φ +∞ *
103 2 4 ltsubrpd φ B X < B
104 2 ltpnfd φ B < +∞
105 101 102 2 103 104 eliood φ B B X +∞
106 5 3 6 7 8 9 10 11 12 29 105 fourierdlem105 φ x B X B F x 𝐿 1
107 100 106 itgcl φ B X B F x dx
108 93 107 eqeltrrd φ A X A F x dx
109 108 subidd φ A X A F x dx A X A F x dx = 0
110 109 eqcomd φ 0 = A X A F x dx A X A F x dx
111 110 adantr φ T < X 0 = A X A F x dx A X A F x dx
112 39 adantr φ T < X A X
113 1 adantr φ T < X A
114 29 adantr φ T < X B X
115 5 6 7 fourierdlem11 φ A B A < B
116 115 simp3d φ A < B
117 1 2 116 ltled φ A B
118 117 adantr φ T < X A B
119 1 2 22 lesub1d φ A B A X B X
120 119 adantr φ T < X A B A X B X
121 118 120 mpbid φ T < X A X B X
122 2 adantr φ T < X B
123 22 adantr φ T < X X
124 simpr φ T < X T < X
125 3 124 eqbrtrrid φ T < X B A < X
126 122 113 123 125 ltsub23d φ T < X B X < A
127 114 113 126 ltled φ T < X B X A
128 112 113 114 121 127 eliccd φ T < X B X A X A
129 8 adantr φ x A X A F :
130 129 61 ffvelrnd φ x A X A F x
131 130 adantlr φ T < X x A X A F x
132 39 rexrd φ A X *
133 1 2 22 116 ltsub1dd φ A X < B X
134 29 ltpnfd φ B X < +∞
135 132 102 29 133 134 eliood φ B X A X +∞
136 5 3 6 7 8 9 10 11 12 39 135 fourierdlem105 φ x A X B X F x 𝐿 1
137 136 adantr φ T < X x A X B X F x 𝐿 1
138 6 adantr φ T < X M
139 7 adantr φ T < X Q P M
140 8 adantr φ T < X F :
141 9 adantlr φ T < X x F x + T = F x
142 10 adantlr φ T < X i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
143 11 adantlr φ T < X i 0 ..^ M R F Q i Q i + 1 lim Q i
144 12 adantlr φ T < X i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
145 101 adantr φ T < X B X *
146 74 a1i φ T < X +∞ *
147 113 ltpnfd φ T < X A < +∞
148 145 146 113 126 147 eliood φ T < X A B X +∞
149 5 3 138 139 140 141 142 143 144 114 148 fourierdlem105 φ T < X x B X A F x 𝐿 1
150 112 113 128 131 137 149 itgspliticc φ T < X A X A F x dx = A X B X F x dx + B X A F x dx
151 150 oveq1d φ T < X A X A F x dx A X A F x dx = A X B X F x dx + B X A F x dx - A X A F x dx
152 8 adantr φ x A X B X F :
153 39 adantr φ x A X B X A X
154 29 adantr φ x A X B X B X
155 simpr φ x A X B X x A X B X
156 eliccre A X B X x A X B X x
157 153 154 155 156 syl3anc φ x A X B X x
158 152 157 ffvelrnd φ x A X B X F x
159 158 136 itgcl φ A X B X F x dx
160 159 adantr φ T < X A X B X F x dx
161 8 adantr φ x B X A F :
162 29 adantr φ x B X A B X
163 1 adantr φ x B X A A
164 simpr φ x B X A x B X A
165 eliccre B X A x B X A x
166 162 163 164 165 syl3anc φ x B X A x
167 161 166 ffvelrnd φ x B X A F x
168 167 adantlr φ T < X x B X A F x
169 168 149 itgcl φ T < X B X A F x dx
170 108 adantr φ T < X A X A F x dx
171 160 169 170 addsubassd φ T < X A X B X F x dx + B X A F x dx - A X A F x dx = A X B X F x dx + B X A F x dx - A X A F x dx
172 111 151 171 3eqtrd φ T < X 0 = A X B X F x dx + B X A F x dx - A X A F x dx
173 172 oveq2d φ T < X A X B X F x dx 0 = A X B X F x dx A X B X F x dx + B X A F x dx - A X A F x dx
174 160 subid1d φ T < X A X B X F x dx 0 = A X B X F x dx
175 159 subidd φ A X B X F x dx A X B X F x dx = 0
176 175 oveq1d φ A X B X F x dx - A X B X F x dx - B X A F x dx A X A F x dx = 0 B X A F x dx A X A F x dx
177 176 adantr φ T < X A X B X F x dx - A X B X F x dx - B X A F x dx A X A F x dx = 0 B X A F x dx A X A F x dx
178 169 170 subcld φ T < X B X A F x dx A X A F x dx
179 160 160 178 subsub4d φ T < X A X B X F x dx - A X B X F x dx - B X A F x dx A X A F x dx = A X B X F x dx A X B X F x dx + B X A F x dx - A X A F x dx
180 df-neg B X A F x dx A X A F x dx = 0 B X A F x dx A X A F x dx
181 169 170 negsubdi2d φ T < X B X A F x dx A X A F x dx = A X A F x dx B X A F x dx
182 180 181 eqtr3id φ T < X 0 B X A F x dx A X A F x dx = A X A F x dx B X A F x dx
183 177 179 182 3eqtr3d φ T < X A X B X F x dx A X B X F x dx + B X A F x dx - A X A F x dx = A X A F x dx B X A F x dx
184 173 174 183 3eqtr3d φ T < X A X B X F x dx = A X A F x dx B X A F x dx
185 107 subidd φ B X B F x dx B X B F x dx = 0
186 185 eqcomd φ 0 = B X B F x dx B X B F x dx
187 186 oveq2d φ B X A F x dx + 0 = B X A F x dx + B X B F x dx - B X B F x dx
188 187 adantr φ T < X B X A F x dx + 0 = B X A F x dx + B X B F x dx - B X B F x dx
189 169 addid1d φ T < X B X A F x dx + 0 = B X A F x dx
190 114 122 113 127 118 eliccd φ T < X A B X B
191 100 adantlr φ T < X x B X B F x
192 1 2 iccssred φ A B
193 8 192 feqresmpt φ F A B = x A B F x
194 8 192 fssresd φ F A B : A B
195 ioossicc Q i Q i + 1 Q i Q i + 1
196 1 rexrd φ A *
197 196 adantr φ i 0 ..^ M A *
198 2 rexrd φ B *
199 198 adantr φ i 0 ..^ M B *
200 5 6 7 fourierdlem15 φ Q : 0 M A B
201 200 adantr φ i 0 ..^ M Q : 0 M A B
202 simpr φ i 0 ..^ M i 0 ..^ M
203 197 199 201 202 fourierdlem8 φ i 0 ..^ M Q i Q i + 1 A B
204 195 203 sstrid φ i 0 ..^ M Q i Q i + 1 A B
205 204 resabs1d φ i 0 ..^ M F A B Q i Q i + 1 = F Q i Q i + 1
206 205 10 eqeltrd φ i 0 ..^ M F A B Q i Q i + 1 : Q i Q i + 1 cn
207 205 eqcomd φ i 0 ..^ M F Q i Q i + 1 = F A B Q i Q i + 1
208 207 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i = F A B Q i Q i + 1 lim Q i
209 11 208 eleqtrd φ i 0 ..^ M R F A B Q i Q i + 1 lim Q i
210 207 oveq1d φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1 = F A B Q i Q i + 1 lim Q i + 1
211 12 210 eleqtrd φ i 0 ..^ M L F A B Q i Q i + 1 lim Q i + 1
212 5 6 7 194 206 209 211 fourierdlem69 φ F A B 𝐿 1
213 193 212 eqeltrrd φ x A B F x 𝐿 1
214 213 adantr φ T < X x A B F x 𝐿 1
215 114 122 190 191 149 214 itgspliticc φ T < X B X B F x dx = B X A F x dx + A B F x dx
216 215 oveq2d φ T < X B X B F x dx B X B F x dx = B X B F x dx B X A F x dx + A B F x dx
217 216 oveq2d φ T < X B X A F x dx + B X B F x dx - B X B F x dx = B X A F x dx + B X B F x dx - B X A F x dx + A B F x dx
218 107 adantr φ T < X B X B F x dx
219 215 218 eqeltrrd φ T < X B X A F x dx + A B F x dx
220 169 218 219 addsub12d φ T < X B X A F x dx + B X B F x dx - B X A F x dx + A B F x dx = B X B F x dx + B X A F x dx - B X A F x dx + A B F x dx
221 8 adantr φ x A B F :
222 1 adantr φ x A B A
223 2 adantr φ x A B B
224 simpr φ x A B x A B
225 eliccre A B x A B x
226 222 223 224 225 syl3anc φ x A B x
227 221 226 ffvelrnd φ x A B F x
228 227 213 itgcl φ A B F x dx
229 228 adantr φ T < X A B F x dx
230 169 169 229 subsub4d φ T < X B X A F x dx - B X A F x dx - A B F x dx = B X A F x dx B X A F x dx + A B F x dx
231 230 eqcomd φ T < X B X A F x dx B X A F x dx + A B F x dx = B X A F x dx - B X A F x dx - A B F x dx
232 231 oveq2d φ T < X B X B F x dx + B X A F x dx - B X A F x dx + A B F x dx = B X B F x dx + B X A F x dx B X A F x dx - A B F x dx
233 169 subidd φ T < X B X A F x dx B X A F x dx = 0
234 233 oveq1d φ T < X B X A F x dx - B X A F x dx - A B F x dx = 0 A B F x dx
235 df-neg A B F x dx = 0 A B F x dx
236 234 235 eqtr4di φ T < X B X A F x dx - B X A F x dx - A B F x dx = A B F x dx
237 236 oveq2d φ T < X B X B F x dx + B X A F x dx B X A F x dx - A B F x dx = B X B F x dx + A B F x dx
238 218 229 negsubd φ T < X B X B F x dx + A B F x dx = B X B F x dx A B F x dx
239 232 237 238 3eqtrd φ T < X B X B F x dx + B X A F x dx - B X A F x dx + A B F x dx = B X B F x dx A B F x dx
240 217 220 239 3eqtrd φ T < X B X A F x dx + B X B F x dx - B X B F x dx = B X B F x dx A B F x dx
241 188 189 240 3eqtr3d φ T < X B X A F x dx = B X B F x dx A B F x dx
242 241 oveq2d φ T < X A X A F x dx B X A F x dx = A X A F x dx B X B F x dx A B F x dx
243 108 107 228 subsubd φ A X A F x dx B X B F x dx A B F x dx = A X A F x dx - B X B F x dx + A B F x dx
244 93 oveq2d φ A X A F x dx B X B F x dx = A X A F x dx A X A F x dx
245 244 109 eqtrd φ A X A F x dx B X B F x dx = 0
246 245 oveq1d φ A X A F x dx - B X B F x dx + A B F x dx = 0 + A B F x dx
247 228 addid2d φ 0 + A B F x dx = A B F x dx
248 243 246 247 3eqtrd φ A X A F x dx B X B F x dx A B F x dx = A B F x dx
249 248 adantr φ T < X A X A F x dx B X B F x dx A B F x dx = A B F x dx
250 184 242 249 3eqtrd φ T < X A X B X F x dx = A B F x dx
251 39 adantr φ X T A X
252 29 adantr φ X T B X
253 1 adantr φ X T A
254 39 1 50 ltled φ A X A
255 254 adantr φ X T A X A
256 22 adantr φ X T X
257 2 adantr φ X T B
258 id X T X T
259 258 3 breqtrdi X T X B A
260 259 adantl φ X T X B A
261 256 257 253 260 lesubd φ X T A B X
262 251 252 253 255 261 eliccd φ X T A A X B X
263 158 adantlr φ X T x A X B X F x
264 132 102 1 50 78 eliood φ A A X +∞
265 5 3 6 7 8 9 10 11 12 39 264 fourierdlem105 φ x A X A F x 𝐿 1
266 265 adantr φ X T x A X A F x 𝐿 1
267 1 leidd φ A A
268 4 rpge0d φ 0 X
269 2 22 subge02d φ 0 X B X B
270 268 269 mpbid φ B X B
271 iccss A B A A B X B A B X A B
272 1 2 267 270 271 syl22anc φ A B X A B
273 iccmbl A B X A B X dom vol
274 1 29 273 syl2anc φ A B X dom vol
275 272 274 227 213 iblss φ x A B X F x 𝐿 1
276 275 adantr φ X T x A B X F x 𝐿 1
277 251 252 262 263 266 276 itgspliticc φ X T A X B X F x dx = A X A F x dx + A B X F x dx
278 268 adantr φ X T 0 X
279 269 adantr φ X T 0 X B X B
280 278 279 mpbid φ X T B X B
281 253 257 252 261 280 eliccd φ X T B X A B
282 227 adantlr φ X T x A B F x
283 2 leidd φ B B
284 283 adantr φ X T B B
285 iccss A B A B X B B B X B A B
286 253 257 261 284 285 syl22anc φ X T B X B A B
287 iccmbl B X B B X B dom vol
288 29 2 287 syl2anc φ B X B dom vol
289 288 adantr φ X T B X B dom vol
290 213 adantr φ X T x A B F x 𝐿 1
291 286 289 282 290 iblss φ X T x B X B F x 𝐿 1
292 253 257 281 282 276 291 itgspliticc φ X T A B F x dx = A B X F x dx + B X B F x dx
293 292 oveq1d φ X T A B F x dx B X B F x dx = A B X F x dx + B X B F x dx - B X B F x dx
294 8 adantr φ x A B X F :
295 1 adantr φ x A B X A
296 29 adantr φ x A B X B X
297 simpr φ x A B X x A B X
298 eliccre A B X x A B X x
299 295 296 297 298 syl3anc φ x A B X x
300 294 299 ffvelrnd φ x A B X F x
301 300 275 itgcl φ A B X F x dx
302 301 107 107 addsubassd φ A B X F x dx + B X B F x dx - B X B F x dx = A B X F x dx + B X B F x dx - B X B F x dx
303 302 adantr φ X T A B X F x dx + B X B F x dx - B X B F x dx = A B X F x dx + B X B F x dx - B X B F x dx
304 185 oveq2d φ A B X F x dx + B X B F x dx - B X B F x dx = A B X F x dx + 0
305 301 addid1d φ A B X F x dx + 0 = A B X F x dx
306 304 305 eqtrd φ A B X F x dx + B X B F x dx - B X B F x dx = A B X F x dx
307 306 adantr φ X T A B X F x dx + B X B F x dx - B X B F x dx = A B X F x dx
308 293 303 307 3eqtrrd φ X T A B X F x dx = A B F x dx B X B F x dx
309 308 oveq2d φ X T A X A F x dx + A B X F x dx = A X A F x dx + A B F x dx - B X B F x dx
310 93 adantr φ X T B X B F x dx = A X A F x dx
311 107 adantr φ X T B X B F x dx
312 310 311 eqeltrrd φ X T A X A F x dx
313 282 290 itgcl φ X T A B F x dx
314 312 313 311 addsub12d φ X T A X A F x dx + A B F x dx - B X B F x dx = A B F x dx + A X A F x dx - B X B F x dx
315 313 312 311 addsubassd φ X T A B F x dx + A X A F x dx - B X B F x dx = A B F x dx + A X A F x dx - B X B F x dx
316 314 315 eqtr4d φ X T A X A F x dx + A B F x dx - B X B F x dx = A B F x dx + A X A F x dx - B X B F x dx
317 277 309 316 3eqtrd φ X T A X B X F x dx = A B F x dx + A X A F x dx - B X B F x dx
318 310 oveq2d φ X T A B F x dx + A X A F x dx - B X B F x dx = A B F x dx + A X A F x dx - A X A F x dx
319 313 312 pncand φ X T A B F x dx + A X A F x dx - A X A F x dx = A B F x dx
320 317 318 319 3eqtrd φ X T A X B X F x dx = A B F x dx
321 250 320 55 22 ltlecasei φ A X B X F x dx = A B F x dx