Metamath Proof Explorer


Theorem areaquad

Description: The area of a quadrilateral with two sides which are parallel to the y-axis in ( RR X. RR ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019)

Ref Expression
Hypotheses areaquad.1 A
areaquad.2 B
areaquad.3 C
areaquad.4 D
areaquad.5 E
areaquad.6 F
areaquad.7 A<B
areaquad.8 CE
areaquad.9 DF
areaquad.10 U=C+xABADC
areaquad.11 V=E+xABAFE
areaquad.12 S=xy|xAByUV
Assertion areaquad areaS=F+E2D+C2BA

Proof

Step Hyp Ref Expression
1 areaquad.1 A
2 areaquad.2 B
3 areaquad.3 C
4 areaquad.4 D
5 areaquad.5 E
6 areaquad.6 F
7 areaquad.7 A<B
8 areaquad.8 CE
9 areaquad.9 DF
10 areaquad.10 U=C+xABADC
11 areaquad.11 V=E+xABAFE
12 areaquad.12 S=xy|xAByUV
13 iccssre ABAB
14 1 2 13 mp2an AB
15 14 sseli xABx
16 15 adantr xAByUVx
17 3 recni C
18 17 a1i xC
19 resubcl xAxA
20 1 19 mpan2 xxA
21 2 1 resubcli BA
22 21 a1i xBA
23 2 recni B
24 23 a1i AB
25 recn AA
26 1 7 gtneii BA
27 26 a1i ABA
28 24 25 27 subne0d ABA0
29 1 28 ax-mp BA0
30 29 a1i xBA0
31 20 22 30 redivcld xxABA
32 31 recnd xxABA
33 4 recni D
34 33 a1i xD
35 32 34 mulcld xxABAD
36 32 18 mulcld xxABAC
37 18 35 36 addsub12d xC+xABAD-xABAC=xABAD+C-xABAC
38 32 34 18 subdid xxABADC=xABADxABAC
39 38 oveq2d xC+xABADC=C+xABAD-xABAC
40 10 39 eqtrid xU=C+xABAD-xABAC
41 1cnd x1
42 41 32 18 subdird x1xABAC=1CxABAC
43 17 mulid2i 1C=C
44 43 oveq1i 1CxABAC=CxABAC
45 42 44 eqtrdi x1xABAC=CxABAC
46 45 oveq2d xxABAD+1xABAC=xABAD+C-xABAC
47 37 40 46 3eqtr4d xU=xABAD+1xABAC
48 1red x1
49 48 31 resubcld x1xABA
50 49 recnd x1xABA
51 50 18 mulcld x1xABAC
52 35 51 addcomd xxABAD+1xABAC=1xABAC+xABAD
53 50 18 mulcomd x1xABAC=C1xABA
54 32 34 mulcomd xxABAD=DxABA
55 53 54 oveq12d x1xABAC+xABAD=C1xABA+DxABA
56 47 52 55 3eqtrd xU=C1xABA+DxABA
57 3 a1i xC
58 57 49 remulcld xC1xABA
59 4 a1i xD
60 59 31 remulcld xDxABA
61 58 60 readdcld xC1xABA+DxABA
62 56 61 eqeltrd xU
63 5 recni E
64 63 a1i xE
65 6 recni F
66 65 a1i xF
67 32 66 mulcld xxABAF
68 32 64 mulcld xxABAE
69 64 67 68 addsub12d xE+xABAF-xABAE=xABAF+E-xABAE
70 32 66 64 subdid xxABAFE=xABAFxABAE
71 70 oveq2d xE+xABAFE=E+xABAF-xABAE
72 11 71 eqtrid xV=E+xABAF-xABAE
73 41 32 64 subdird x1xABAE=1ExABAE
74 63 mulid2i 1E=E
75 74 oveq1i 1ExABAE=ExABAE
76 73 75 eqtrdi x1xABAE=ExABAE
77 76 oveq2d xxABAF+1xABAE=xABAF+E-xABAE
78 69 72 77 3eqtr4d xV=xABAF+1xABAE
79 50 64 mulcld x1xABAE
80 67 79 addcomd xxABAF+1xABAE=1xABAE+xABAF
81 50 64 mulcomd x1xABAE=E1xABA
82 32 66 mulcomd xxABAF=FxABA
83 81 82 oveq12d x1xABAE+xABAF=E1xABA+FxABA
84 78 80 83 3eqtrd xV=E1xABA+FxABA
85 5 a1i xE
86 85 49 remulcld xE1xABA
87 6 a1i xF
88 87 31 remulcld xFxABA
89 86 88 readdcld xE1xABA+FxABA
90 84 89 eqeltrd xV
91 iccssre UVUV
92 62 90 91 syl2anc xUV
93 15 92 syl xABUV
94 93 sselda xAByUVy
95 16 94 jca xAByUVxy
96 95 ssopab2i xy|xAByUVxy|xy
97 df-xp 2=xy|xy
98 96 12 97 3sstr4i S2
99 iftrue xABifxABVU0=VU
100 nfv yxAB
101 nfopab2 _yxy|xAByUV
102 12 101 nfcxfr _yS
103 nfcv _yx
104 102 103 nfima _ySx
105 nfcv _yUV
106 vex xV
107 vex yV
108 106 107 elimasn ySxxyS
109 12 eleq2i xySxyxy|xAByUV
110 opabidw xyxy|xAByUVxAByUV
111 108 109 110 3bitri ySxxAByUV
112 111 baib xABySxyUV
113 100 104 105 112 eqrd xABSx=UV
114 113 fveq2d xABvolSx=volUV
115 15 62 syl xABU
116 15 90 syl xABV
117 iccmbl UVUVdomvol
118 115 116 117 syl2anc xABUVdomvol
119 mblvol UVdomvolvolUV=vol*UV
120 118 119 syl xABvolUV=vol*UV
121 15 58 syl xABC1xABA
122 15 60 syl xABDxABA
123 15 86 syl xABE1xABA
124 15 88 syl xABFxABA
125 3 a1i xABC
126 5 a1i xABE
127 15 49 syl xAB1xABA
128 15 31 syl xABxABA
129 128 recnd xABxABA
130 129 subidd xABxABAxABA=0
131 1red xAB1
132 2 a1i xABB
133 1 a1i xABA
134 1 rexri A*
135 2 rexri B*
136 iccleub A*B*xABxB
137 134 135 136 mp3an12 xABxB
138 15 132 133 137 lesub1dd xABxABA
139 15 1 19 sylancl xABxA
140 21 a1i xABBA
141 1 recni A
142 141 subidi AA=0
143 133 132 133 ltsub1d xABA<BAA<BA
144 7 143 mpbii xABAA<BA
145 142 144 eqbrtrrid xAB0<BA
146 lediv1 xABABA0<BAxABAxABABABA
147 139 140 140 145 146 syl112anc xABxABAxABABABA
148 138 147 mpbid xABxABABABA
149 21 recni BA
150 149 29 dividi BABA=1
151 148 150 breqtrdi xABxABA1
152 128 131 128 151 lesub1dd xABxABAxABA1xABA
153 130 152 eqbrtrrd xAB01xABA
154 8 a1i xABCE
155 125 126 127 153 154 lemul1ad xABC1xABAE1xABA
156 4 a1i xABD
157 6 a1i xABF
158 140 145 elrpd xABBA+
159 iccgelb A*B*xABAx
160 134 135 159 mp3an12 xABAx
161 133 15 133 160 lesub1dd xABAAxA
162 142 161 eqbrtrrid xAB0xA
163 139 158 162 divge0d xAB0xABA
164 9 a1i xABDF
165 156 157 128 163 164 lemul1ad xABDxABAFxABA
166 121 122 123 124 155 165 le2addd xABC1xABA+DxABAE1xABA+FxABA
167 15 56 syl xABU=C1xABA+DxABA
168 15 84 syl xABV=E1xABA+FxABA
169 166 167 168 3brtr4d xABUV
170 ovolicc UVUVvol*UV=VU
171 115 116 169 170 syl3anc xABvol*UV=VU
172 114 120 171 3eqtrd xABvolSx=VU
173 99 172 eqtr4d xABifxABVU0=volSx
174 iffalse ¬xABifxABVU0=0
175 nfv y¬xAB
176 nfcv _y
177 111 simplbi ySxxAB
178 noel ¬y
179 178 pm2.21i yxAB
180 177 179 pm5.21ni ¬xABySxy
181 175 104 176 180 eqrd ¬xABSx=
182 181 fveq2d ¬xABvolSx=vol
183 0mbl domvol
184 mblvol domvolvol=vol*
185 183 184 ax-mp vol=vol*
186 ovol0 vol*=0
187 185 186 eqtri vol=0
188 182 187 eqtrdi ¬xABvolSx=0
189 174 188 eqtr4d ¬xABifxABVU0=volSx
190 173 189 pm2.61i ifxABVU0=volSx
191 190 eqcomi volSx=ifxABVU0
192 90 62 resubcld xVU
193 0re 0
194 ifcl VU0ifxABVU0
195 192 193 194 sylancl xifxABVU0
196 191 195 eqeltrid xvolSx
197 volf vol:domvol0+∞
198 ffun vol:domvol0+∞Funvol
199 197 198 ax-mp Funvol
200 iftrue xABifxABUV=UV
201 113 200 eqtr4d xABSx=ifxABUV
202 iffalse ¬xABifxABUV=
203 181 202 eqtr4d ¬xABSx=ifxABUV
204 201 203 pm2.61i Sx=ifxABUV
205 62 90 117 syl2anc xUVdomvol
206 183 a1i xdomvol
207 205 206 ifcld xifxABUVdomvol
208 204 207 eqeltrid xSxdomvol
209 fvimacnv FunvolSxdomvolvolSxSxvol-1
210 199 208 209 sylancr xvolSxSxvol-1
211 196 210 mpbid xSxvol-1
212 211 rgen xSxvol-1
213 14 a1i 0AB
214 rembl domvol
215 214 a1i 0domvol
216 116 115 resubcld xABVU
217 172 216 eqeltrd xABvolSx
218 217 adantl 0xABvolSx
219 eldifn xAB¬xAB
220 219 188 syl xABvolSx=0
221 220 adantl 0xABvolSx=0
222 172 mpteq2ia xABvolSx=xABVU
223 eqid TopOpenfld=TopOpenfld
224 223 subcn TopOpenfld×tTopOpenfldCnTopOpenfld
225 224 a1i TopOpenfld×tTopOpenfldCnTopOpenfld
226 11 mpteq2i xABV=xABE+xABAFE
227 223 addcn +TopOpenfld×tTopOpenfldCnTopOpenfld
228 227 a1i +TopOpenfld×tTopOpenfldCnTopOpenfld
229 ax-resscn
230 14 229 sstri AB
231 ssid
232 cncfmptc EABxABE:ABcn
233 63 230 231 232 mp3an xABE:ABcn
234 233 a1i xABE:ABcn
235 230 sseli xABx
236 141 a1i xABA
237 149 a1i xABBA
238 29 a1i xABBA0
239 235 236 237 238 divsubdird xABxABA=xBAABA
240 239 adantl xABxABA=xBAABA
241 240 mpteq2dva xABxABA=xABxBAABA
242 resmpt ABxxBAAB=xABxBA
243 230 242 ax-mp xxBAAB=xABxBA
244 eqid xxBA=xxBA
245 244 divccncf BABA0xxBA:cn
246 149 29 245 mp2an xxBA:cn
247 rescncf ABxxBA:cnxxBAAB:ABcn
248 230 246 247 mp2 xxBAAB:ABcn
249 243 248 eqeltrri xABxBA:ABcn
250 249 a1i xABxBA:ABcn
251 141 149 29 divcli ABA
252 cncfmptc ABAABxABABA:ABcn
253 251 230 231 252 mp3an xABABA:ABcn
254 253 a1i xABABA:ABcn
255 223 225 250 254 cncfmpt2f xABxBAABA:ABcn
256 241 255 eqeltrd xABxABA:ABcn
257 cncfmptc FABxABF:ABcn
258 65 230 231 257 mp3an xABF:ABcn
259 258 a1i xABF:ABcn
260 223 225 259 234 cncfmpt2f xABFE:ABcn
261 256 260 mulcncf xABxABAFE:ABcn
262 223 228 234 261 cncfmpt2f xABE+xABAFE:ABcn
263 226 262 eqeltrid xABV:ABcn
264 10 mpteq2i xABU=xABC+xABADC
265 cncfmptc CABxABC:ABcn
266 17 230 231 265 mp3an xABC:ABcn
267 266 a1i xABC:ABcn
268 cncfmptc DABxABD:ABcn
269 33 230 231 268 mp3an xABD:ABcn
270 269 a1i xABD:ABcn
271 223 225 270 267 cncfmpt2f xABDC:ABcn
272 256 271 mulcncf xABxABADC:ABcn
273 223 228 267 272 cncfmpt2f xABC+xABADC:ABcn
274 264 273 eqeltrid xABU:ABcn
275 223 225 263 274 cncfmpt2f xABVU:ABcn
276 275 mptru xABVU:ABcn
277 cniccibl ABxABVU:ABcnxABVU𝐿1
278 1 2 276 277 mp3an xABVU𝐿1
279 222 278 eqeltri xABvolSx𝐿1
280 279 a1i 0xABvolSx𝐿1
281 213 215 218 221 280 iblss2 0xvolSx𝐿1
282 193 281 ax-mp xvolSx𝐿1
283 dmarea SdomareaS2xSxvol-1xvolSx𝐿1
284 98 212 282 283 mpbir3an Sdomarea
285 areaval SdomareaareaS=volSxdx
286 284 285 ax-mp areaS=volSxdx
287 itgeq2 xvolSx=ifxABVU0volSxdx=ifxABVU0dx
288 191 a1i xvolSx=ifxABVU0
289 287 288 mprg volSxdx=ifxABVU0dx
290 itgss2 ABABVUdx=ifxABVU0dx
291 14 290 ax-mp ABVUdx=ifxABVU0dx
292 65 63 addcli F+E
293 2cnne0 220
294 div32 F+E220BAF+E2BA=F+EBA2
295 292 293 149 294 mp3an F+E2BA=F+EBA2
296 33 17 addcli D+C
297 div32 D+C220BAD+C2BA=D+CBA2
298 296 293 149 297 mp3an D+C2BA=D+CBA2
299 295 298 oveq12i F+E2BAD+C2BA=F+EBA2D+CBA2
300 2cn 2
301 2ne0 20
302 292 300 301 divcli F+E2
303 296 300 301 divcli D+C2
304 302 303 149 subdiri F+E2D+C2BA=F+E2BAD+C2BA
305 116 adantl xABV
306 263 mptru xABV:ABcn
307 cniccibl ABxABV:ABcnxABV𝐿1
308 1 2 306 307 mp3an xABV𝐿1
309 308 a1i xABV𝐿1
310 115 adantl xABU
311 274 mptru xABU:ABcn
312 cniccibl ABxABU:ABcnxABU𝐿1
313 1 2 311 312 mp3an xABU𝐿1
314 313 a1i xABU𝐿1
315 305 309 310 314 itgsub ABVUdx=ABVdxABUdx
316 315 mptru ABVUdx=ABVdxABUdx
317 63 300 301 divcan4i E22=E
318 317 oveq1i E22BA=EBA
319 63 300 mulcli E2
320 div32 E2220BAE22BA=E2BA2
321 319 293 149 320 mp3an E22BA=E2BA2
322 318 321 eqtr3i EBA=E2BA2
323 322 oveq1i EBA+FEBA2=E2BA2+FEBA2
324 itgeq2 xABV=E+xABAFEABVdx=ABE+xABAFEdx
325 11 a1i xABV=E+xABAFE
326 324 325 mprg ABVdx=ABE+xABAFEdx
327 5 a1i xABE
328 cniccibl ABxABE:ABcnxABE𝐿1
329 1 2 233 328 mp3an xABE𝐿1
330 329 a1i xABE𝐿1
331 128 adantl xABxABA
332 6 a1i xABF
333 332 327 resubcld xABFE
334 331 333 remulcld xABxABAFE
335 261 mptru xABxABAFE:ABcn
336 cniccibl ABxABxABAFE:ABcnxABxABAFE𝐿1
337 1 2 335 336 mp3an xABxABAFE𝐿1
338 337 a1i xABxABAFE𝐿1
339 327 330 334 338 itgadd ABE+xABAFEdx=ABEdx+ABxABAFEdx
340 339 mptru ABE+xABAFEdx=ABEdx+ABxABAFEdx
341 iccmbl ABABdomvol
342 1 2 341 mp2an ABdomvol
343 mblvol ABdomvolvolAB=vol*AB
344 342 343 ax-mp volAB=vol*AB
345 1 2 7 ltleii AB
346 ovolicc ABABvol*AB=BA
347 1 2 345 346 mp3an vol*AB=BA
348 344 347 eqtri volAB=BA
349 348 21 eqeltri volAB
350 itgconst ABdomvolvolABEABEdx=EvolAB
351 342 349 63 350 mp3an ABEdx=EvolAB
352 348 oveq2i EvolAB=EBA
353 351 352 eqtri ABEdx=EBA
354 65 a1i F
355 63 a1i E
356 354 355 subcld FE
357 256 mptru xABxABA:ABcn
358 cniccibl ABxABxABA:ABcnxABxABA𝐿1
359 1 2 357 358 mp3an xABxABA𝐿1
360 359 a1i xABxABA𝐿1
361 356 331 360 itgmulc2 FEABxABAdx=ABFExABAdx
362 361 mptru FEABxABAdx=ABFExABAdx
363 itgeq2 xABxABA=1BAxAABxABAdx=AB1BAxAdx
364 139 recnd xABxA
365 364 237 238 divrec2d xABxABA=1BAxA
366 363 365 mprg ABxABAdx=AB1BAxAdx
367 15 adantl xABx
368 cncfmptid ABxABx:ABcn
369 230 231 368 mp2an xABx:ABcn
370 cniccibl ABxABx:ABcnxABx𝐿1
371 1 2 369 370 mp3an xABx𝐿1
372 371 a1i xABx𝐿1
373 1 a1i xABA
374 cncfmptc AABxABA:ABcn
375 141 230 231 374 mp3an xABA:ABcn
376 cniccibl ABxABA:ABcnxABA𝐿1
377 1 2 375 376 mp3an xABA𝐿1
378 377 a1i xABA𝐿1
379 367 372 373 378 itgsub ABxAdx=ABxdxABAdx
380 379 mptru ABxAdx=ABxdxABAdx
381 1 a1i A
382 2 a1i B
383 345 a1i AB
384 1nn0 10
385 384 a1i 10
386 381 382 383 385 itgpowd ABx1dx=B1+1A1+11+1
387 386 mptru ABx1dx=B1+1A1+11+1
388 1p1e2 1+1=2
389 388 oveq2i B1+1A1+11+1=B1+1A1+12
390 387 389 eqtri ABx1dx=B1+1A1+12
391 itgeq2 xABx1=xABx1dx=ABxdx
392 235 exp1d xABx1=x
393 391 392 mprg ABx1dx=ABxdx
394 388 oveq2i B1+1=B2
395 388 oveq2i A1+1=A2
396 394 395 oveq12i B1+1A1+1=B2A2
397 396 oveq1i B1+1A1+12=B2A22
398 390 393 397 3eqtr3i ABxdx=B2A22
399 itgconst ABdomvolvolABAABAdx=AvolAB
400 342 349 141 399 mp3an ABAdx=AvolAB
401 348 oveq2i AvolAB=ABA
402 400 401 eqtri ABAdx=ABA
403 398 402 oveq12i ABxdxABAdx=B2A22ABA
404 380 403 eqtri ABxAdx=B2A22ABA
405 404 oveq2i 1BAABxAdx=1BAB2A22ABA
406 23 a1i B
407 141 a1i A
408 406 407 subcld BA
409 26 a1i BA
410 406 407 409 subne0d BA0
411 408 410 reccld 1BA
412 411 mptru 1BA
413 23 sqcli B2
414 141 sqcli A2
415 413 414 subcli B2A2
416 415 300 301 divcli B2A22
417 141 149 mulcli ABA
418 412 416 417 subdii 1BAB2A22ABA=1BAB2A221BAABA
419 405 418 eqtri 1BAABxAdx=1BAB2A221BAABA
420 139 adantl xABxA
421 367 372 373 378 iblsub xABxA𝐿1
422 411 420 421 itgmulc2 1BAABxAdx=AB1BAxAdx
423 422 mptru 1BAABxAdx=AB1BAxAdx
424 412 417 mulcomi 1BAABA=ABA1BA
425 417 149 29 divreci ABABA=ABA1BA
426 141 149 29 divcan4i ABABA=A
427 424 425 426 3eqtr2i 1BAABA=A
428 427 oveq2i 1BAB2A221BAABA=1BAB2A22A
429 419 423 428 3eqtr3i AB1BAxAdx=1BAB2A22A
430 366 429 eqtri ABxABAdx=1BAB2A22A
431 23 141 subsqi B2A2=B+ABA
432 431 oveq1i B2A22=B+ABA2
433 432 oveq2i 1BAB2A22=1BAB+ABA2
434 431 415 eqeltrri B+ABA
435 412 434 300 301 divassi 1BAB+ABA2=1BAB+ABA2
436 412 434 mulcomi 1BAB+ABA=B+ABA1BA
437 434 149 29 divreci B+ABABA=B+ABA1BA
438 23 141 addcli B+A
439 438 149 29 divcan4i B+ABABA=B+A
440 436 437 439 3eqtr2i 1BAB+ABA=B+A
441 440 oveq1i 1BAB+ABA2=B+A2
442 433 435 441 3eqtr2i 1BAB2A22=B+A2
443 442 oveq1i 1BAB2A22A=B+A2A
444 141 300 mulcli A2
445 divsubdir B+AA2220B+A-A22=B+A2A22
446 438 444 293 445 mp3an B+A-A22=B+A2A22
447 23 141 444 addsubassi B+A-A2=B+A-A2
448 subsub2 BA2ABA2A=B+A-A2
449 23 444 141 448 mp3an BA2A=B+A-A2
450 141 times2i A2=A+A
451 450 oveq1i A2A=A+A-A
452 141 141 pncan3oi A+A-A=A
453 451 452 eqtri A2A=A
454 453 oveq2i BA2A=BA
455 447 449 454 3eqtr2i B+A-A2=BA
456 455 oveq1i B+A-A22=BA2
457 141 300 301 divcan4i A22=A
458 457 oveq2i B+A2A22=B+A2A
459 446 456 458 3eqtr3ri B+A2A=BA2
460 430 443 459 3eqtri ABxABAdx=BA2
461 460 oveq2i FEABxABAdx=FEBA2
462 itgeq2 xABFExABA=xABAFEABFExABAdx=ABxABAFEdx
463 65 63 subcli FE
464 463 a1i xABFE
465 464 129 mulcomd xABFExABA=xABAFE
466 462 465 mprg ABFExABAdx=ABxABAFEdx
467 362 461 466 3eqtr3ri ABxABAFEdx=FEBA2
468 353 467 oveq12i ABEdx+ABxABAFEdx=EBA+FEBA2
469 326 340 468 3eqtri ABVdx=EBA+FEBA2
470 149 300 301 divcli BA2
471 319 463 470 adddiri E2+F-EBA2=E2BA2+FEBA2
472 323 469 471 3eqtr4i ABVdx=E2+F-EBA2
473 addsub12 FE2EF+E2-E=E2+F-E
474 65 319 63 473 mp3an F+E2-E=E2+F-E
475 63 times2i E2=E+E
476 475 oveq1i E2E=E+E-E
477 63 63 pncan3oi E+E-E=E
478 476 477 eqtri E2E=E
479 478 oveq2i F+E2-E=F+E
480 474 479 eqtr3i E2+F-E=F+E
481 480 oveq1i E2+F-EBA2=F+EBA2
482 472 481 eqtri ABVdx=F+EBA2
483 17 300 301 divcan4i C22=C
484 483 oveq1i C22BA=CBA
485 17 300 mulcli C2
486 div32 C2220BAC22BA=C2BA2
487 485 293 149 486 mp3an C22BA=C2BA2
488 484 487 eqtr3i CBA=C2BA2
489 488 oveq1i CBA+DCBA2=C2BA2+DCBA2
490 10 a1i xABU=C+xABADC
491 490 itgeq2dv ABUdx=ABC+xABADCdx
492 491 mptru ABUdx=ABC+xABADCdx
493 3 a1i xABC
494 cniccibl ABxABC:ABcnxABC𝐿1
495 1 2 266 494 mp3an xABC𝐿1
496 495 a1i xABC𝐿1
497 4 a1i xABD
498 497 493 resubcld xABDC
499 331 498 remulcld xABxABADC
500 272 mptru xABxABADC:ABcn
501 cniccibl ABxABxABADC:ABcnxABxABADC𝐿1
502 1 2 500 501 mp3an xABxABADC𝐿1
503 502 a1i xABxABADC𝐿1
504 493 496 499 503 itgadd ABC+xABADCdx=ABCdx+ABxABADCdx
505 504 mptru ABC+xABADCdx=ABCdx+ABxABADCdx
506 itgconst ABdomvolvolABCABCdx=CvolAB
507 342 349 17 506 mp3an ABCdx=CvolAB
508 348 oveq2i CvolAB=CBA
509 507 508 eqtri ABCdx=CBA
510 33 a1i D
511 17 a1i C
512 510 511 subcld DC
513 512 331 360 itgmulc2 DCABxABAdx=ABDCxABAdx
514 513 mptru DCABxABAdx=ABDCxABAdx
515 460 oveq2i DCABxABAdx=DCBA2
516 itgeq2 xABDCxABA=xABADCABDCxABAdx=ABxABADCdx
517 33 17 subcli DC
518 517 a1i xABDC
519 518 129 mulcomd xABDCxABA=xABADC
520 516 519 mprg ABDCxABAdx=ABxABADCdx
521 514 515 520 3eqtr3ri ABxABADCdx=DCBA2
522 509 521 oveq12i ABCdx+ABxABADCdx=CBA+DCBA2
523 492 505 522 3eqtri ABUdx=CBA+DCBA2
524 485 517 470 adddiri C2+D-CBA2=C2BA2+DCBA2
525 489 523 524 3eqtr4i ABUdx=C2+D-CBA2
526 addsub12 DC2CD+C2-C=C2+D-C
527 33 485 17 526 mp3an D+C2-C=C2+D-C
528 17 times2i C2=C+C
529 528 oveq1i C2C=C+C-C
530 17 17 pncan3oi C+C-C=C
531 529 530 eqtri C2C=C
532 531 oveq2i D+C2-C=D+C
533 527 532 eqtr3i C2+D-C=D+C
534 533 oveq1i C2+D-CBA2=D+CBA2
535 525 534 eqtri ABUdx=D+CBA2
536 482 535 oveq12i ABVdxABUdx=F+EBA2D+CBA2
537 316 536 eqtri ABVUdx=F+EBA2D+CBA2
538 299 304 537 3eqtr4ri ABVUdx=F+E2D+C2BA
539 289 291 538 3eqtr2i volSxdx=F+E2D+C2BA
540 286 539 eqtri areaS=F+E2D+C2BA