API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Mar 28th, 2019
156
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 54.18 KB | None | 0 0
raw download clone embed print report
  1. $( <MM> <PROOF_ASST> THEOREM=areaquad LOC_AFTER=?
  2.  
  3. * The area of a quadrilateral with two sides which are parallel to the y-axis in RR X. RR
  4. is its width multiplied by the average height of it's top minus the average height of it's bottom.
  5. (Contributed by Jon Pennant, 31-Mar-2019.)
  6.  
  7. h1::areaquad.1 |- A e. RR
  8. h2::areaquad.2 |- B e. RR
  9. h3::areaquad.3 |- C e. RR
  10. h4::areaquad.4 |- D e. RR
  11. h5::areaquad.5 |- E e. RR
  12. h6::areaquad.6 |- F e. RR
  13. h7::areaquad.7 |- A < B
  14. h8::areaquad.8 |- C <_ E
  15. h9::areaquad.9 |- D <_ F
  16. h10::areaquad.10 |- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  17. h11::areaquad.11 |- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  18. h12::areaquad.12 |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
  19.  
  20. *236 is broken
  21.  
  22. *10a:1:idi |- A e. RR
  23. 10ac:1:recni |- A e. CC
  24. 10ad:1:a1i |- ( x e. RR -> A e. RR )
  25. 10ae:1:rexri |- A e. RR*
  26. *10b:2:idi |- B e. RR
  27. 10bc:2:recni |- B e. CC
  28. 10bd:2:a1i |- ( x e. RR -> B e. RR )
  29. 10be:2:rexri |- B e. RR*
  30. *10c:3:idi |- C e. RR
  31. 10cc:3:recni |- C e. CC
  32. 10ce:10cc:a1i |- ( x e. RR -> C e. CC )
  33. *10d:4:idi |- D e. RR
  34. 10dc:4:recni |- D e. CC
  35. 10de:10dc:a1i |- ( x e. RR -> D e. CC )
  36. *10e:5:idi |- E e. RR
  37. 10ec:5:recni |- E e. CC
  38. 10ee:10ec:a1i |- ( x e. RR -> E e. CC )
  39. *10f:6:idi |- F e. RR
  40. 10fc:6:recni |- F e. CC
  41. 10fe:10fc:a1i |- ( x e. RR -> F e. CC )
  42. *11a:7:idi |- A < B
  43. 11aa:1,2:leloei |- ( A <_ B <-> ( A < B \/ A = B ) )
  44. 11ab::orc |- ( A < B -> ( A < B \/ A = B ) )
  45. 11ac:7,11ab:ax-mp |- ( A < B \/ A = B )
  46. 11ad:11ac,11aa:mpbir |- A <_ B
  47. 11b:8:idi |- C <_ E
  48. 11c:9:idi |- D <_ F
  49. 206::0re |- 0 e. RR
  50. 206ccc:206:recni |- 0 e. CC
  51. 28a::1red |- ( x e. RR -> 1 e. RR )
  52. 28ab::1cnd |- ( x e. RR -> 1 e. CC )
  53. 11e::tru |- T.
  54. 11f::2cn |- 2 e. CC
  55. 11g::2ne0 |- 2 =/= 0
  56. 11h:10ac,11f:mulcli |- ( A x. 2 ) e. CC
  57. 11hc:10cc,11f:mulcli |- ( C x. 2 ) e. CC
  58. 11he:10ec,11f:mulcli |- ( E x. 2 ) e. CC
  59. 11i::2cnne0 |- ( 2 e. CC /\ 2 =/= 0 )
  60. 11j:10fc,10ec:subcli |- ( F - E ) e. CC
  61. 11k:11j:a1i |- ( x e. ( A [,] B ) -> ( F - E ) e. CC )
  62. 11fe:10fc,10ec:addcli |- ( F + E ) e. CC
  63. 11dc:10dc,10cc:addcli |- ( D + C ) e. CC
  64.  
  65. *12a:10:idi |- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  66. *12b:11:idi |- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  67.  
  68. *12c:: |- U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) )
  69. *12d:: |- V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) )
  70.  
  71. *13:12:idi |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
  72.  
  73. *things to prove
  74. dmarea::dmarea |- ( S e. dom area <-> ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  75. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 ) )
  76. areaval::areaval |- ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )
  77.  
  78. *get A,B in RR
  79.  
  80. 14::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
  81. 15:1,2,14:mp2an |- ( A [,] B ) C_ RR
  82. 15a::axresscn |- RR C_ CC
  83. 15b:15,15a:sstri |- ( A [,] B ) C_ CC
  84. 15c:15b:a1i |- ( x e. RR -> ( A [,] B ) C_ CC )
  85. 15d::dfss3 |- ( ( A [,] B ) C_ RR <-> A. x e. ( A [,] B ) x e. RR )
  86. 15e:15,15d:mpbi |- A. x e. ( A [,] B ) x e. RR
  87. 15f:15e:rspec |- ( x e. ( A [,] B ) -> x e. RR )
  88. *get U,V in RR
  89. 16:2,1:resubcli |- ( B - A ) e. RR
  90. 16a:16:recni |- ( B - A ) e. CC
  91. 16ab:10ac,16a:mulcli |- ( A x. ( B - A ) ) e. CC
  92. 16ac:10bc:sqcli |- ( B ^ 2 ) e. CC
  93. 16ad:10ac:sqcli |- ( A ^ 2 ) e. CC
  94. 16ae:16ac,16ad:subcli |- ( ( B ^ 2 ) - ( A ^ 2 ) ) e. CC
  95. 16af:16ae,11f,11g:divcli |- ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) e. CC
  96. 16c::resubcl |- ( ( x e. RR /\ A e. RR ) -> ( x - A ) e. RR )
  97. 16ca:1,16c:mpan2 |- ( x e. RR -> ( x - A ) e. RR )
  98. 16cb:15f,16ca:syl |- ( x e. ( A [,] B ) -> ( x - A ) e. RR )
  99. 17::ltne |- ( ( A e. RR /\ A < B ) -> B =/= A )
  100. 18:1,7,17:mp2an |- B =/= A
  101. d2:10bc:a1i |- ( A e. RR -> B e. CC )
  102. d3:10ac:a1i |- ( A e. RR -> A e. CC )
  103. d4:18:a1i |- ( A e. RR -> B =/= A )
  104. 23:d2,d3,d4:subne0d |- ( A e. RR -> ( B - A ) =/= 0 )
  105. 24:1,23:ax-mp |- ( B - A ) =/= 0
  106. 25::redivcl |- ( ( ( x - A ) e. RR /\ ( B - A ) e. RR /\ ( B - A ) =/= 0 ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  107. 26a:16:a1i |- ( x e. RR -> ( B - A ) e. RR )
  108. 26aa:15f,26a:syl |- ( x e. ( A [,] B ) -> ( B - A ) e. RR )
  109. 26b:24:a1i |- ( x e. RR -> ( B - A ) =/= 0 )
  110. 26c:3:a1i |- ( x e. RR -> C e. RR )
  111. 26e:5:a1i |- ( x e. RR -> E e. RR )
  112. 26d:4:a1i |- ( x e. RR -> D e. RR )
  113. 26f:6:a1i |- ( x e. RR -> F e. RR )
  114. 27:16ca,26a,26b,25:syl3anc |- ( x e. RR -> ( ( x - A ) / ( B - A ) ) e. RR )
  115. 27a:15f,27:syl |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  116. 27ab:27:recnd |- ( x e. RR -> ( ( x - A ) / ( B - A ) ) e. CC )
  117. 27b:27a:recnd |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. CC )
  118. 28::resubcl |- ( ( 1 e. RR /\ ( ( x - A ) / ( B - A ) ) e. RR ) -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
  119. 29:28a,27,28:syl2anc |- ( x e. RR -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
  120. 29c:29:recnd |- ( x e. RR -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. CC )
  121. 30c:26c,29:remulcld |- ( x e. RR -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  122. 30ca:30c:recnd |- ( x e. RR -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. CC )
  123. 30e:26e,29:remulcld |- ( x e. RR -> ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  124. 30d:26d,27:remulcld |- ( x e. RR -> ( D x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  125. 30f:26f,27:remulcld |- ( x e. RR -> ( F x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  126. *convert U and V to a form suited to inequalities
  127. 12aa::subdi |- ( ( ( ( x - A ) / ( B - A ) ) e. CC /\ D e. CC /\ C e. CC )
  128. -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  129. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  130. 12ab:27ab,10de,10ce,12aa:syl3anc |- ( x e. RR
  131. -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  132. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  133. 12ac:12ab:oveq2d |- ( x e. RR
  134. -> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  135. = ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  136. 12ad:10,12ac:syl5eq |- ( x e. RR -> U
  137. = ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  138. 12ae::addsub12 |- ( ( C e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. D ) e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. C ) e. CC )
  139. -> ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  140. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  141. 12af:27ab,10de:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. D ) e. CC )
  142. 12ag:27ab,10ce:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. C ) e. CC )
  143. 12ah:10ce,12af,12ag,12ae:syl3anc |- ( x e. RR
  144. -> ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  145. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  146. 12ai:12ad,12ah:eqtrd |- ( x e. RR -> U = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  147. 12ak:10cc:mulid2i |- ( 1 x. C ) = C
  148. 12al::oveq1 |- ( ( 1 x. C ) = C -> ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  149. 12am:12ak,12al:ax-mp |- ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) )
  150. 12an::subdir |- ( ( 1 e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC /\ C e. CC )
  151. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  152. 12ao:28ab,27ab,10ce,12an:syl3anc |- ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  153. 12ap:12ao,12am:syl6eq |- ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  154. 12aq:12ap:oveq2d |- ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) )
  155. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  156. 12ar:12ai,12aq:eqtr4d |- ( x e. RR -> U = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) ) )
  157. 12as::addcomgi |- ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) )
  158. = ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) )
  159. 12au:12ar,12as:syl6eq |- ( x e. RR -> U =
  160. ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) ) )
  161. 12av:29c,10ce:mulcomd |- ( x e. RR
  162. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  163. 12aw:27ab,10de:mulcomd |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. D ) = ( D x. ( ( x - A ) / ( B - A ) ) ) )
  164. 12ax:12av,12aw:oveq12d |- ( x e. RR -> ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) )
  165. = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
  166. 12ay:12au,12ax:eqtrd |- ( x e. RR -> U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
  167. 12az:15f,12ay:syl |- ( x e. ( A [,] B ) -> U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
  168.  
  169. 12ba::subdi |- ( ( ( ( x - A ) / ( B - A ) ) e. CC /\ F e. CC /\ E e. CC )
  170. -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  171. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  172. 12bb:27ab,10fe,10ee,12ba:syl3anc |- ( x e. RR
  173. -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  174. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  175. 12bc:12bb:oveq2d |- ( x e. RR
  176. -> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  177. = ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  178. 12bd:11,12bc:syl5eq |- ( x e. RR -> V
  179. = ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  180. 12be::addsub12 |- ( ( E e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. F ) e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. E ) e. CC )
  181. -> ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  182. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  183. 12bf:27ab,10fe:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. F ) e. CC )
  184. 12bg:27ab,10ee:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. E ) e. CC )
  185. 12bh:10ee,12bf,12bg,12be:syl3anc |- ( x e. RR
  186. -> ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  187. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  188. 12bi:12bd,12bh:eqtrd |- ( x e. RR -> V = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  189. 12bk:10ec:mulid2i |- ( 1 x. E ) = E
  190. 12bl::oveq1 |- ( ( 1 x. E ) = E -> ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) )
  191. = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  192. 12bm:12bk,12bl:ax-mp |- ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) )
  193. 12bn::subdir |- ( ( 1 e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC /\ E e. CC )
  194. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  195. 12bo:28ab,27ab,10ee,12bn:syl3anc |- ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  196. 12bp:12bo,12bm:syl6eq |- ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  197. 12bq:12bp:oveq2d |- ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) )
  198. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  199. 12br:12bi,12bq:eqtr4d |- ( x e. RR -> V = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) ) )
  200. 12bs::addcomgi |- ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) )
  201. = ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) )
  202. 12bu:12br,12bs:syl6eq |- ( x e. RR -> V =
  203. ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) ) )
  204. 12bv:29c,10ee:mulcomd |- ( x e. RR
  205. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  206. 12bw:27ab,10fe:mulcomd |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. F ) = ( F x. ( ( x - A ) / ( B - A ) ) ) )
  207. 12bx:12bv,12bw:oveq12d |- ( x e. RR -> ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) )
  208. = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  209. 12by:12bu,12bx:eqtrd |- ( x e. RR -> V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  210. 12bz:15f,12by:syl |- ( x e. ( A [,] B ) -> V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  211. *now get U,V in RR
  212. 31v:30e,30f:readdcld |- ( x e. RR -> ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  213. 31u:30c,30d:readdcld |- ( x e. RR -> ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  214. 36:12ay,31u:eqeltrd |- ( x e. RR -> U e. RR )
  215. 37:12by,31v:eqeltrd |- ( x e. RR -> V e. RR )
  216. 36b:15f,36:syl |- ( x e. ( A [,] B ) -> U e. RR )
  217. 36c:15f,37:syl |- ( x e. ( A [,] B ) -> V e. RR )
  218. 36d:36b,36c:jca |- ( x e. ( A [,] B ) -> ( U e. RR /\ V e. RR ) )
  219. 37a:36,37:jca |- ( x e. RR -> ( U e. RR /\ V e. RR ) )
  220. 37aa:37,36:jca |- ( x e. RR -> ( V e. RR /\ U e. RR ) )
  221. 37e::resubcl |- ( ( V e. RR /\ U e. RR ) -> ( V - U ) e. RR )
  222. 37f:37aa,37e:syl |- ( x e. RR -> ( V - U ) e. RR )
  223. 37fb:36c,36b:resubcld |- ( x e. ( A [,] B ) -> ( V - U ) e. RR )
  224. 37g:37f:recnd |- ( x e. RR -> ( V - U ) e. CC )
  225. 38::iccssre |- ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) C_ RR )
  226. 39:36,37,38:syl2anc |- ( x e. RR -> ( U [,] V ) C_ RR )
  227. *prove U <_V in ( A [,] B )
  228. *first get both 1 - ( ( x - A ) / ( B - A ) ) >_ 0, then 0 <_ ( ( x - A ) / ( B - A ) )
  229. 40a::iccleub |- ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> x <_ B )
  230. 40b:10ae,10be,40a:mp3an12 |- ( x e. ( A [,] B ) -> x <_ B )
  231. d11:2:a1i |- ( x e. ( A [,] B ) -> B e. RR )
  232. d12:1:a1i |- ( x e. ( A [,] B ) -> A e. RR )
  233. 40c:15f,d11,d12:lesub1d |- ( x e. ( A [,] B ) -> ( x <_ B <-> ( x - A ) <_ ( B - A ) ) )
  234. 40e:40b,40c:mpbid |- ( x e. ( A [,] B ) -> ( x - A ) <_ ( B - A ) )
  235. 40f:d12,d11,d12:ltsub1d |- ( x e. ( A [,] B ) -> ( A < B <-> ( A - A ) < ( B - A ) ) )
  236. 40g:7,40f:mpbii |- ( x e. ( A [,] B ) -> ( A - A ) < ( B - A ) )
  237. 40h::subid |- ( A e. CC -> ( A - A ) = 0 )
  238. 40i:10ac,40h:ax-mp |- ( A - A ) = 0
  239. 40j:40i,40g:syl5eqbrr |- ( x e. ( A [,] B ) -> 0 < ( B - A ) )
  240. 40k:26aa,40j:jca |- ( x e. ( A [,] B ) -> ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
  241. 40l::lediv1 |- ( ( ( x - A ) e. RR /\ ( B - A ) e. RR /\ ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
  242. -> ( ( x - A ) <_ ( B - A ) <-> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) ) )
  243. 40m:16cb,26aa,40k,40l:syl3anc |- ( x e. ( A [,] B )
  244. -> ( ( x - A ) <_ ( B - A ) <-> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) ) )
  245. 40n:40e,40m:mpbid |- ( x e. ( A [,] B )
  246. -> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) )
  247. 40o:16a,24:dividi |- ( ( B - A ) / ( B - A ) ) = 1
  248. 40p:40n,40o:syl6breq |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) <_ 1 )
  249. d13:15f,27:syl |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  250. d14:15f,28a:syl |- ( x e. ( A [,] B ) -> 1 e. RR )
  251. 40q:d13,d14,d13:lesub1d |- ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) <_ 1
  252. <-> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  253. 40r:40p,40q:mpbid |- ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) )
  254. <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) )
  255. 40s::subid |- ( ( ( x - A ) / ( B - A ) ) e. CC -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) = 0 )
  256. 40t:27b,40s:syl |- ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) = 0 )
  257. 40u:40t,40r:eqbrtrrd |- ( x e. ( A [,] B ) -> 0 <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) )
  258. *not get 0 <_ ( ( x - A ) / ( B - A ) )
  259. 41::elicc1 |- ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ x /\ x <_ B ) ) )
  260. 41a::simp2 |- ( ( x e. RR* /\ A <_ x /\ x <_ B ) -> A <_ x )
  261. 41b:41,41a:syl6bi |- ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,] B ) -> A <_ x ) )
  262. 41c:41b:3impia |- ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> A <_ x )
  263. 41d:10ae,10be,41c:mp3an12 |- ( x e. ( A [,] B ) -> A <_ x )
  264. 41e:d12,15f,d12:lesub1d |- ( x e. ( A [,] B ) -> ( A <_ x <-> ( A - A ) <_ ( x - A ) ) )
  265. 41f::subid |- ( A e. CC -> ( A - A ) = 0 )
  266. 41g:10ac,41f:ax-mp |- ( A - A ) = 0
  267. 41h:41d,41e:mpbid |- ( x e. ( A [,] B ) -> ( A - A ) <_ ( x - A ) )
  268. 41i:41g,41h:syl5eqbrr |- ( x e. ( A [,] B ) -> 0 <_ ( x - A ) )
  269. 41j::lediv1 |- ( ( 0 e. RR /\ ( x - A ) e. RR /\ ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
  270. -> ( 0 <_ ( x - A ) <-> ( 0 / ( B - A ) ) <_ ( ( x - A ) / ( B - A ) ) ) )
  271. 41k:206,16cb,40k,41j:eel011 |- ( x e. ( A [,] B ) -> ( 0 <_ ( x - A ) <-> ( 0 / ( B - A ) ) <_ ( ( x - A ) / ( B - A ) ) ) )
  272. 41l:41i,41k:mpbid |- ( x e. ( A [,] B ) -> ( 0 / ( B - A ) ) <_ ( ( x - A ) / ( B - A ) ) )
  273. 41m::diveq0 |- ( ( 0 e. CC /\ ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( ( 0 / ( B - A ) ) = 0 <-> 0 = 0 ) )
  274. 41n:206ccc,16a,24,41m:mp3an |- ( ( 0 / ( B - A ) ) = 0 <-> 0 = 0 )
  275. 41o::eqid |- 0 = 0
  276. 41p:41o,41n:mpbir |- ( 0 / ( B - A ) ) = 0
  277. 41q:41p,41l:syl5eqbrr |- ( x e. ( A [,] B ) -> 0 <_ ( ( x - A ) / ( B - A ) ) )
  278. *now establish the inequalities
  279. d5:3:a1i |- ( x e. ( A [,] B ) -> C e. RR )
  280. d6:5:a1i |- ( x e. ( A [,] B ) -> E e. RR )
  281. d7:15f,29:syl |- ( x e. ( A [,] B ) -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
  282. d9:11b:a1i |- ( x e. ( A [,] B ) -> C <_ E )
  283. 42:d5,d6,d7,40u,d9:lemul1ad
  284. |- ( x e. ( A [,] B ) -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) <_ ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  285. d15:4:a1i |- ( x e. ( A [,] B ) -> D e. RR )
  286. d16:6:a1i |- ( x e. ( A [,] B ) -> F e. RR )
  287. d19:11c:a1i |- ( x e. ( A [,] B ) -> D <_ F )
  288. 43:d15,d16,27a,41q,d19:lemul1ad
  289. |- ( x e. ( A [,] B ) -> ( D x. ( ( x - A ) / ( B - A ) ) ) <_ ( F x. ( ( x - A ) / ( B - A ) ) ) )
  290. d20:15f,30c:syl |- ( x e. ( A [,] B ) -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  291. d21:15f,30d:syl |- ( x e. ( A [,] B ) -> ( D x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  292. d22:15f,30e:syl |- ( x e. ( A [,] B ) -> ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  293. d23:15f,30f:syl |- ( x e. ( A [,] B ) -> ( F x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  294. 44:d20,d21,d22,d23,42,43:le2addd
  295. |- ( x e. ( A [,] B ) -> ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) )
  296. <_ ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  297. 45:44,12az,12bz:3brtr4d |- ( x e. ( A [,] B ) -> U <_ V )
  298. 46:36b,36c,45:3jca |- ( x e. ( A [,] B ) -> ( U e. RR /\ V e. RR /\ U <_ V ) )
  299. *you did it :) **
  300.  
  301. 50a::iftrue |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) = ( U [,] V ) )
  302. 50b::iffalse |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) = (/) )
  303. *compute the image of S
  304. 51::vex |- x e. _V
  305. 52::vex |- y e. _V
  306. 53:51,52:elimasn |- ( y e. ( S " { x } ) <-> <. x , y >. e. S )
  307. 54::nfopab2 |- F/_ y { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
  308. 55:12,54:nfcxfr |- F/_ y S
  309. 56::nfcv |- F/_ y { x }
  310. 57:55,56:nfima |- F/_ y ( S " { x } )
  311. 58::nfcv |- F/_ y ( U [,] V )
  312. 59::nfv |- F/ y x e. ( A [,] B )
  313. 60a:12:eleq2i |- ( <. x , y >. e. S <-> <. x , y >. e. { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } )
  314. 60b::opabid |- ( <. x , y >. e. { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
  315. 60ba:60a,60b:bitri |- ( <. x , y >. e. S <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
  316. 60c:53,60a,60b:3bitri |- ( y e. ( S " { x } ) <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
  317. 60d:60c:baib |- ( x e. ( A [,] B ) -> ( y e. ( S " { x } ) <-> y e. ( U [,] V ) ) )
  318. 60e:59,57,58,60d:eqrd |- ( x e. ( A [,] B ) -> ( S " { x } ) = ( U [,] V ) )
  319. 60f:59:nfn |- F/ y -. x e. ( A [,] B )
  320. 60g::nfcv |- F/_ y (/)
  321. 60h:60c:simplbi |- ( y e. ( S " { x } ) -> x e. ( A [,] B ) )
  322. 60i::noel |- -. y e. (/)
  323. 60j:60i:pm2.21i |- ( y e. (/) -> x e. ( A [,] B ) )
  324. 60k:60h,60j:pm5.21ni |- ( -. x e. ( A [,] B ) -> ( y e. ( S " { x } ) <-> y e. (/) ) )
  325. 60l:60f,57,60g,60k:eqrd |- ( -. x e. ( A [,] B ) -> ( S " { x } ) = (/) )
  326. 60m:60e,50a:eqtr4d |- ( x e. ( A [,] B ) -> ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
  327. 60n:60l,50b:eqtr4d |- ( -. x e. ( A [,] B ) -> ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
  328. *work with the image of S at x and find it's integral
  329. 60:60m,60n:pm2.61i |- ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) )
  330. 61:60:fveq2i |- ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
  331. 62:61:a1i |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) )
  332. 63:61:a1i |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) )
  333. 64:50a:fveq2d |- ( x e. ( A [,] B )
  334. -> ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) = ( vol ` ( U [,] V ) ) )
  335. 65:50b:fveq2d |- ( -. x e. ( A [,] B )
  336. -> ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) = ( vol ` (/) ) )
  337. 66:62,64:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` ( U [,] V ) ) )
  338. 67:63,65:eqtrd |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` (/) ) )
  339.  
  340.  
  341. *part 1 of the conditions of dmarea prove S subset R2
  342. 70c:15f,39:syl |- ( x e. ( A [,] B ) -> ( U [,] V ) C_ RR )
  343. 71::dfss3 |- ( ( U [,] V ) C_ RR <-> A. y e. ( U [,] V ) y e. RR )
  344. 71a:70c,71:sylib |- ( x e. ( A [,] B ) -> A. y e. ( U [,] V ) y e. RR )
  345. 71b::rsp |- ( A. y e. ( U [,] V ) y e. RR -> ( y e. ( U [,] V ) -> y e. RR ) )
  346. 71c:71a,71b:syl |- ( x e. ( A [,] B ) -> ( y e. ( U [,] V ) -> y e. RR ) )
  347. 72:15f:adantr |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> x e. RR )
  348. 72a:71c:imp |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> y e. RR )
  349. 72b:72,72a:jca |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> ( x e. RR /\ y e. RR ) )
  350. 75e::df-xp |- ( RR X. RR ) = { <. x , y >. | ( x e. RR /\ y e. RR ) }
  351. 75f:72b:ssopab2i |- { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } C_ { <. x , y >. | ( x e. RR /\ y e. RR ) }
  352. 76:75f,12,75e:3sstr4i |- S C_ ( RR X. RR )
  353.  
  354. *part 2 of the conditions of dmarea prove A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  355. 100::iccmbl |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )
  356. 101:1,2,100:mp2an |- ( A [,] B ) e. dom vol
  357. 102::iccmbl |- ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) e. dom vol )
  358. 104:36d,102:syl |- ( x e. ( A [,] B ) -> ( U [,] V ) e. dom vol )
  359. 104a:37a,102:syl |- ( x e. RR -> ( U [,] V ) e. dom vol )
  360. 105::0mbl |- (/) e. dom vol
  361. 106:105:a1i |- ( x e. RR -> (/) e. dom vol )
  362. 107:104a,106:jca |- ( x e. RR -> ( ( U [,] V ) e. dom vol /\ (/) e. dom vol ) )
  363. 108::ifcl |- ( ( ( U [,] V ) e. dom vol /\ (/) e. dom vol )
  364. -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
  365. 109:107,108:syl |- ( x e. RR -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
  366. 110:60,109:syl5eqel |- ( x e. RR -> ( S " { x } ) e. dom vol )
  367. *jump to 200 for the completion of this part
  368.  
  369. *compute vols
  370. 168::ovolicc |- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
  371. 168a::ovolicc |- ( ( U e. RR /\ V e. RR /\ U <_ V ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
  372. 169:1,2,11ad,168:mp3an |- ( vol* ` ( A [,] B ) ) = ( B - A )
  373. 169a:46,168a:syl |- ( x e. ( A [,] B ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
  374. 170::mblvol |- ( ( A [,] B ) e. dom vol -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
  375. 170a::mblvol |- ( ( U [,] V ) e. dom vol -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
  376. 171:101,170:ax-mp |- ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) )
  377. 171a:104,170a:syl |- ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
  378. 172:171,169:eqtri |- ( vol ` ( A [,] B ) ) = ( B - A )
  379. 172aa:172,16:eqeltri |- ( vol ` ( A [,] B ) ) e. RR
  380. 172a:171a,169a:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( V - U ) )
  381. 178::ssel2 |- ( ( ( A [,] B ) C_ RR /\ x e. ( A [,] B ) ) -> x e. RR )
  382. 181::ovol0 |- ( vol* ` (/) ) = 0
  383. 182::mblvol |- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
  384. 183:105,182:ax-mp |- ( vol ` (/) ) = ( vol* ` (/) )
  385. 184:183,181:eqtri |- ( vol ` (/) ) = 0
  386. 185:184:a1i |- ( -. x e. ( A [,] B ) -> ( vol ` (/) ) = 0 )
  387. *apply these to S
  388. 186:66,172a:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( V - U ) )
  389. 188:186,37fb:eqeltrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) e. RR )
  390. 189:67,184:syl6eq |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = 0 )
  391. 190::iftrue |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( V - U ) )
  392. 191::iffalse |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = 0 )
  393. 192:190,186:eqtr4d |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
  394. 192a:191,189:eqtr4d |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
  395. 193:192,192a:pm2.61i |- if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) )
  396. 194:193:eqcomi |- ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  397. 195:194:a1i |- ( x e. RR -> ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 ) )
  398. 196:195:rgen |- A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  399. 197::itgeq2 |- ( A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  400. -> S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
  401. 198:196,197:ax-mp |- S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  402.  
  403. *continue with part 2 of conditions of dmarea
  404. 200::fvimacnv |- ( ( Fun vol /\ ( S " { x } ) e. dom vol ) -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  405. 201::volf |- vol : dom vol --> ( 0 [,] +oo )
  406. 202::ffun |- ( vol : dom vol --> ( 0 [,] +oo ) -> Fun vol )
  407. 203:201,202:ax-mp |- Fun vol
  408. 203a:110,203:jctil |- ( x e. RR -> ( Fun vol /\ ( S " { x } ) e. dom vol ) )
  409. 204:203a,200:syl |- ( x e. RR -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  410. 205::ifcl |- ( ( ( V - U ) e. RR /\ 0 e. RR ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
  411. 206a:37f,206:jctir |- ( x e. RR -> ( ( V - U ) e. RR /\ 0 e. RR ) )
  412. 207:206a,205:syl |- ( x e. RR -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
  413. 208:195,207:eqeltrd |- ( x e. RR -> ( vol ` ( S " { x } ) ) e. RR )
  414. 209:208,204:mpbid |- ( x e. RR -> ( S " { x } ) e. ( `' vol " RR ) )
  415. 210:209:rgen |- A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  416.  
  417. *part 3 of the conditions of dmarea, prove L1
  418. 220:15:a1i |- ( 0 e. RR -> ( A [,] B ) C_ RR )
  419. 221::rembl |- RR e. dom vol
  420. 222:221:a1i |- ( 0 e. RR -> RR e. dom vol )
  421. 223:188:adantl |- ( ( 0 e. RR /\ x e. ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) e. RR )
  422. 224::eldifn |- ( x e. ( RR \ ( A [,] B ) ) -> -. x e. ( A [,] B ) )
  423. 225:224,189:syl |- ( x e. ( RR \ ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  424. 226:225:adantl |- ( ( 0 e. RR /\ x e. ( RR \ ( A [,] B ) ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  425.  
  426. 227::cncfmptc |- ( ( ( V - U ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  427. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  428. 228::ssid |- CC C_ CC
  429. 228a:228:a1i |- ( x e. RR -> CC C_ CC )
  430. 228b:37g,15c,228a:3jca |- ( x e. RR -> ( ( V - U ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) )
  431. 229:228b,227:syl |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  432. 230::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  433. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  434. 231:10ad,10bd,229:3jca |- ( x e. RR -> ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
  435. 232:231,230:syl |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  436. 233:186:mpteq2ia |- ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) = ( x e. ( A [,] B ) |-> ( V - U ) )
  437. 234:233,232:syl5eqel |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  438. 234a:15f,234:syl |- ( x e. ( A [,] B ) -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  439. 234ab:234:rgen |- A. x e. RR ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
  440. 234b:234ab: |- ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
  441. 235:234b:a1i |- ( 0 e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  442. 236:220,222,223,226,235:iblss2
  443. |- ( 0 e. RR -> ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  444. 237:206,236:ax-mp |- ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1
  445.  
  446. *value of the integral of x
  447. 250:: |- S. ( A [,] B ) x _d x = ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 )
  448.  
  449. *evaluate the integral
  450. d24:186:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) = ( V - U ) )
  451. 300:d24:itgeq2dv |- ( T. -> S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x = S. ( A [,] B ) ( V - U ) _d x )
  452. 300a:11e,300:ax-mp |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x = S. ( A [,] B ) ( V - U ) _d x
  453. d25:36c:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> V e. RR )
  454. !d26:: |- ( T. -> ( x e. ( A [,] B ) |-> V ) e. L^1 )
  455. d27:36b:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> U e. RR )
  456. !d28:: |- ( T. -> ( x e. ( A [,] B ) |-> U ) e. L^1 )
  457. *break up int S = int V - int U
  458. 301:d25,d26,d27,d28:itgsub |- ( T. -> S. ( A [,] B ) ( V - U ) _d x = ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x ) )
  459. 301a:11e,301:ax-mp |- S. ( A [,] B ) ( V - U ) _d x = ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x )
  460. 302:10:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) )
  461. 303:302:itgeq2dv |- ( T. -> S. ( A [,] B ) U _d x
  462. = S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x )
  463. 303a:11e,303:ax-mp |- S. ( A [,] B ) U _d x
  464. = S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  465. d29:3:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> C e. RR )
  466. d29a::cncfmptc |- ( ( C e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  467. -> ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
  468. d29b:10cc,15b,228,d29a:mp3an |- ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC )
  469. d29c::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
  470. -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
  471. d29d:1,2,d29b,d29c:mp3an |- ( x e. ( A [,] B ) |-> C ) e. L^1
  472. d30:d29d:a1i |- ( T. -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
  473. d50:27a:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  474. d51:4:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> D e. RR )
  475. d52:d51,d29:resubcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( D - C ) e. RR )
  476. d31:d50,d52:remulcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) e. RR )
  477. !d32:: |- ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1 )
  478. *int U = int C + int I (D - C)
  479. 304:d29,d30,d31,d32:itgadd |- ( T. -> S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  480. = ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x ) )
  481. 304a:11e,304:ax-mp |- S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  482. = ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
  483. 305::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ C e. CC )
  484. -> S. ( A [,] B ) C _d x = ( C x. ( vol ` ( A [,] B ) ) ) )
  485. 305a:101,172aa,10cc,305:mp3an |- S. ( A [,] B ) C _d x = ( C x. ( vol ` ( A [,] B ) ) )
  486. 305b:172:oveq2i |- ( C x. ( vol ` ( A [,] B ) ) ) = ( C x. ( B - A ) )
  487. 305c:305a,305b:eqtri |- S. ( A [,] B ) C _d x = ( C x. ( B - A ) )
  488. d43:10dc:a1i |- ( T. -> D e. CC )
  489. d44:10cc:a1i |- ( T. -> C e. CC )
  490. d33:d43,d44:subcld |- ( T. -> ( D - C ) e. CC )
  491. !d35:: |- ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1 )
  492. *int I ( D - C ) = ( D - C ) int I
  493. 306:d33,d50,d35:itgmulc2 |- ( T. -> ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  494. = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x )
  495. 306a:11e,306:ax-mp |- ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  496. = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  497. d36:15a,16cb:sseldi |- ( x e. ( A [,] B ) -> ( x - A ) e. CC )
  498. d37:16a:a1i |- ( x e. ( A [,] B ) -> ( B - A ) e. CC )
  499. d38:24:a1i |- ( x e. ( A [,] B ) -> ( B - A ) =/= 0 )
  500. 307:d36,d37,d38:divrecd |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( x - A ) x. ( 1 / ( B - A ) ) ) )
  501. d39:d37,d38:reccld |- ( x e. ( A [,] B ) -> ( 1 / ( B - A ) ) e. CC )
  502. 308:d36,d39:mulcomd |- ( x e. ( A [,] B ) -> ( ( x - A ) x. ( 1 / ( B - A ) ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) ) )
  503. 309:307,308:eqtrd |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) ) )
  504. 309a:309:rgen |- A. x e. ( A [,] B ) ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) )
  505. 309c::itgeq2 |- ( A. x e. ( A [,] B ) ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) )
  506. -> S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x )
  507. 309d:309a,309c:ax-mp |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
  508. d45:10bc:a1i |- ( T. -> B e. CC )
  509. d46:10ac:a1i |- ( T. -> A e. CC )
  510. d47:d45,d46:subcld |- ( T. -> ( B - A ) e. CC )
  511. d48:18:a1i |- ( T. -> B =/= A )
  512. d49:d45,d46,d48:subne0d |- ( T. -> ( B - A ) =/= 0 )
  513. d40:d47,d49:reccld |- ( T. -> ( 1 / ( B - A ) ) e. CC )
  514. d40a:11e,d40:ax-mp |- ( 1 / ( B - A ) ) e. CC
  515. d41:16cb:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x - A ) e. RR )
  516. !d42:: |- ( T. -> ( x e. ( A [,] B ) |-> ( x - A ) ) e. L^1 )
  517. *int I = int ( x - A ) / B - A = 1 / B - A int ( x - A )
  518. 310:d40,d41,d42:itgmulc2 |- ( T. -> ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  519. = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x )
  520. 310a:11e,310:ax-mp |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  521. = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
  522.  
  523. d53:15f:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> x e. RR )
  524. !d54:: |- ( T. -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
  525. d55:1:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> A e. RR )
  526. d56a::cncfmptc |- ( ( A e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  527. -> ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
  528. d56b:10ac,15b,228,d56a:mp3an |- ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC )
  529. d56c::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
  530. -> ( x e. ( A [,] B ) |-> A ) e. L^1 )
  531. d56:1,2,d56b,d56c:eel000cT |- ( T. -> ( x e. ( A [,] B ) |-> A ) e. L^1 )
  532. * int x - A = int X - int A
  533. 315:d53,d54,d55,d56:itgsub
  534. |- ( T. -> S. ( A [,] B ) ( x - A ) _d x = ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x ) )
  535. 315a:11e,315:ax-mp |- S. ( A [,] B ) ( x - A ) _d x = ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x )
  536. 316::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ A e. CC )
  537. -> S. ( A [,] B ) A _d x = ( A x. ( vol ` ( A [,] B ) ) ) )
  538. 317:101,172aa,10ac,316:mp3an |- S. ( A [,] B ) A _d x = ( A x. ( vol ` ( A [,] B ) ) )
  539. 318:172:oveq2i |- ( A x. ( vol ` ( A [,] B ) ) ) = ( A x. ( B - A ) )
  540. 319:317,318:eqtri |- S. ( A [,] B ) A _d x = ( A x. ( B - A ) )
  541. *now rebuild :)
  542. 320:250,319:oveq12i |- ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x ) = ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) )
  543. 321:315a,320:eqtri |- S. ( A [,] B ) ( x - A ) _d x = ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) )
  544. 322:321:oveq2i |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  545. = ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
  546. 323::subdi |- ( ( ( 1 / ( B - A ) ) e. CC /\ ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) e. CC /\ ( A x. ( B - A ) ) e. CC )
  547. -> ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
  548. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) ) )
  549. 324:d40a,16af,16ab,323:mp3an |- ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
  550. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
  551. 345:d40a,16ab:mulcomi |- ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = ( ( A x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  552. 346:16ab,16a,24:divreci |- ( ( A x. ( B - A ) ) / ( B - A ) ) = ( ( A x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  553. 347:345,346:eqtr4i |- ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = ( ( A x. ( B - A ) ) / ( B - A ) )
  554. 348:10ac,16a,24:divcan4i |- ( ( A x. ( B - A ) ) / ( B - A ) ) = A
  555. 349:347,348:eqtri |- ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = A
  556. 350:322,324:eqtri |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  557. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
  558. 351:349:oveq2i |- ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
  559. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  560. 352:350,351:eqtri |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  561. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  562. 353:310a,352:eqtr3i |- S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
  563. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  564. *this is to be simplified
  565. 354:309d,353:eqtri |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x
  566. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  567. 355:10bc,10ac:subsqi |- ( ( B ^ 2 ) - ( A ^ 2 ) ) = ( ( B + A ) x. ( B - A ) )
  568. 355a:355:oveq1i |- ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) = ( ( ( B + A ) x. ( B - A ) ) / 2 )
  569. 355b:355a:oveq2i |- ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) )
  570. = ( ( 1 / ( B - A ) ) x. ( ( ( B + A ) x. ( B - A ) ) / 2 ) )
  571. d58:355,16ae:eqeltrri |- ( ( B + A ) x. ( B - A ) ) e. CC
  572. 356:d40a,d58,11f,11g:divassi
  573. |- ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 ) = ( ( 1 / ( B - A ) ) x. ( ( ( B + A ) x. ( B - A ) ) / 2 ) )
  574. 357:355b,356:eqtr4i |- ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) )
  575. = ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 )
  576. 358:d40a,d58:mulcomi
  577. |- ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) = ( ( ( B + A ) x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  578. 359:d58,16a,24:divreci
  579. |- ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) ) = ( ( ( B + A ) x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  580. 360:358,359:eqtr4i |- ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) )
  581. = ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) )
  582. d59:10bc,10ac:addcli |- ( B + A ) e. CC
  583. 361:d59,16a,24:divcan4i |- ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) ) = ( B + A )
  584. 362:360,361:eqtri |- ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) = ( B + A )
  585. 363:362:oveq1i |- ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 ) = ( ( B + A ) / 2 )
  586. 364:357,363:eqtri |- ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) = ( ( B + A ) / 2 )
  587. 365:364:oveq1i |- ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A ) = ( ( ( B + A ) / 2 ) - A )
  588. *this is to be simplified further
  589. 366:354,365:eqtri |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = ( ( ( B + A ) / 2 ) - A )
  590. 367:10ac,11f,11g:divcan4i |- ( ( A x. 2 ) / 2 ) = A
  591. 368:367:oveq2i |- ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) = ( ( ( B + A ) / 2 ) - A )
  592. 369::divsubdir |- ( ( ( B + A ) e. CC /\ ( A x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) )
  593. -> ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) )
  594. 370:d59,11h,11i,369:mp3an |- ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) )
  595. 371:370,368:eqtri |- ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - A )
  596. 372:10bc,10ac,11h:addsubassi |- ( ( B + A ) - ( A x. 2 ) ) = ( B + ( A - ( A x. 2 ) ) )
  597. 373::subsub2 |- ( ( B e. CC /\ ( A x. 2 ) e. CC /\ A e. CC )
  598. -> ( B - ( ( A x. 2 ) - A ) ) = ( B + ( A - ( A x. 2 ) ) ) )
  599. 374:10bc,11h,10ac,373:mp3an |- ( B - ( ( A x. 2 ) - A ) ) = ( B + ( A - ( A x. 2 ) ) )
  600. *375::pncan |- ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) - A ) = A )
  601. 376:10ac,10ac:pncan3oi |- ( ( A + A ) - A ) = A
  602. 377:10ac:times2i |- ( A x. 2 ) = ( A + A )
  603. 378:377:oveq1i |- ( ( A x. 2 ) - A ) = ( ( A + A ) - A )
  604. 379:378,376:eqtri |- ( ( A x. 2 ) - A ) = A
  605. 380:379:oveq2i |- ( B - ( ( A x. 2 ) - A ) ) = ( B - A )
  606. 381:374,380:eqtr3i |- ( B + ( A - ( A x. 2 ) ) ) = ( B - A )
  607. 382:372,381:eqtri |- ( ( B + A ) - ( A x. 2 ) ) = ( B - A )
  608. 383:382:oveq1i |- ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( B - A ) / 2 )
  609. 384:370,383:eqtr3i |- ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) = ( ( B - A ) / 2 )
  610. 385:368,384:eqtr3i |- ( ( ( B + A ) / 2 ) - A ) = ( ( B - A ) / 2 )
  611.  
  612. *this is the integral of I :) :)
  613. 386:366,385:eqtri |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = ( ( B - A ) / 2 )
  614.  
  615. *build up to the integral of U
  616. 387:386:oveq2i |- ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  617. = ( ( D - C ) x. ( ( B - A ) / 2 ) )
  618. 388:387,306a:eqtr3i |- ( ( D - C ) x. ( ( B - A ) / 2 ) )
  619. = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  620. d60:11e,d33:ax-mp |- ( D - C ) e. CC
  621. d60a:d60:a1i |- ( x e. ( A [,] B ) -> ( D - C ) e. CC )
  622. 389::mulcom |- ( ( ( D - C ) e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC )
  623. -> ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  624. 390:d60a,27b,389:syl2anc |- ( x e. ( A [,] B )
  625. -> ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  626. 391:390:rgen |- A. x e. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  627. 392::itgeq2 |- ( A. x e. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) )
  628. = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  629. -> S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  630. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
  631. 393:391,392:ax-mp |- S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  632. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x
  633. 394:388,393:eqtr2i |- S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x
  634. = ( ( D - C ) x. ( ( B - A ) / 2 ) )
  635. 395:305c,394:oveq12i |- ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
  636. = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  637. 396:304a,395:eqtri |- S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  638. = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  639. *now simplify this
  640. 397:303a,396:eqtri |- S. ( A [,] B ) U _d x = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  641. 398:10cc,11f,11g:divcan4i |- ( ( C x. 2 ) / 2 ) = C
  642. 399:398:oveq1i |- ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( C x. ( B - A ) )
  643. 400::div32 |- ( ( ( C x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  644. -> ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) )
  645. 401:11hc,11i,16a,400:mp3an |- ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) )
  646. 402:399,401:eqtr3i |- ( C x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) )
  647. 403:402:oveq1i |- ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  648. = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  649. 404:397,403:eqtri |- S. ( A [,] B ) U _d x
  650. = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  651. d63:16a,11f,11g:divcli |- ( ( B - A ) / 2 ) e. CC
  652. 405:11hc,d60,d63:adddiri |- ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) )
  653. = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  654. 406:404,405:eqtr4i |- S. ( A [,] B ) U _d x
  655. = ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) )
  656. 407::addsub12 |- ( ( D e. CC /\ ( C x. 2 ) e. CC /\ C e. CC )
  657. -> ( D + ( ( C x. 2 ) - C ) ) = ( ( C x. 2 ) + ( D - C ) ) )
  658. 408:10dc,11hc,10cc,407:mp3an |- ( D + ( ( C x. 2 ) - C ) ) = ( ( C x. 2 ) + ( D - C ) )
  659. 409:10cc,10cc:pncan3oi |- ( ( C + C ) - C ) = C
  660. 410:10cc:times2i |- ( C x. 2 ) = ( C + C )
  661. 411:410:oveq1i |- ( ( C x. 2 ) - C ) = ( ( C + C ) - C )
  662. 412:411,409:eqtri |- ( ( C x. 2 ) - C ) = C
  663. 413:412:oveq2i |- ( D + ( ( C x. 2 ) - C ) ) = ( D + C )
  664. 414:408,413:eqtr3i |- ( ( C x. 2 ) + ( D - C ) ) = ( D + C )
  665. 415:414:oveq1i |- ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) )
  666. *we have the integral for U :) :) :)
  667. 416:406,415:eqtri |- S. ( A [,] B ) U _d x = ( ( D + C ) x. ( ( B - A ) / 2 ) )
  668.  
  669. 417::itgeq2 |- ( A. x e. ( A [,] B ) V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  670. -> S. ( A [,] B ) V _d x = S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x )
  671. 418:11:a1i |- ( x e. ( A [,] B ) -> V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) )
  672. 419:418:rgen |- A. x e. ( A [,] B ) V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  673. *this is the integral for V to be proven
  674. 420:419,417:ax-mp |- S. ( A [,] B ) V _d x = S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  675. d64:5:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> E e. RR )
  676. d65a:5:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> E e. RR )
  677. d66a::cncfmptc |- ( ( E e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  678. -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
  679. d66b:10ec,15b,228,d66a:mp3an |- ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC )
  680. d66c::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
  681. -> ( x e. ( A [,] B ) |-> E ) e. L^1 )
  682. d66ca:1,2,d66b,d66c:mp3an |- ( x e. ( A [,] B ) |-> E ) e. L^1
  683. d66d:d66ca:a1i |- ( T. -> ( x e. ( A [,] B ) |-> E ) e. L^1 )
  684. d68:6:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> F e. RR )
  685. d69:d68,d64:resubcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( F - E ) e. RR )
  686. d66:d50,d69:remulcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) e. RR )
  687. !d67:: |- ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1 )
  688. 421:d64,d66d,d66,d67:itgadd |- ( T. -> S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  689. = ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x ) )
  690. 421a:11e,421:ax-mp |- S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  691. = ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
  692. 422::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ E e. CC )
  693. -> S. ( A [,] B ) E _d x = ( E x. ( vol ` ( A [,] B ) ) ) )
  694. 422a:101,172aa,10ec,422:mp3an |- S. ( A [,] B ) E _d x = ( E x. ( vol ` ( A [,] B ) ) )
  695. 422b:172:oveq2i |- ( E x. ( vol ` ( A [,] B ) ) ) = ( E x. ( B - A ) )
  696. 422c:422a,422b:eqtri |- S. ( A [,] B ) E _d x = ( E x. ( B - A ) )
  697. *get int I ( F - E )
  698. d73:10fc:a1i |- ( T. -> F e. CC )
  699. d74:10ec:a1i |- ( T. -> E e. CC )
  700. d70:d73,d74:subcld |- ( T. -> ( F - E ) e. CC )
  701. 423:d70,d50,d35:itgmulc2 |- ( T. -> ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  702. = S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x )
  703. 423a:11e,423:ax-mp |- ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  704. = S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  705. 424:386:oveq2i |- ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  706. = ( ( F - E ) x. ( ( B - A ) / 2 ) )
  707. 425:423a,424:eqtr3i |- S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x = ( ( F - E ) x. ( ( B - A ) / 2 ) )
  708. 426::itgeq2 |- ( A. x e. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) )
  709. = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  710. -> S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  711. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
  712. 427::mulcom |- ( ( ( F - E ) e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC )
  713. -> ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  714. 428:11k,27b,427:syl2anc |- ( x e. ( A [,] B )
  715. -> ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  716. 429:428:rgen |- A. x e. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) )
  717. = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  718. 430:429,426:ax-mp |- S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  719. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x
  720. 431:430,425:eqtr3i |- S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x
  721. = ( ( F - E ) x. ( ( B - A ) / 2 ) )
  722. 432:422c,431:oveq12i |- ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
  723. = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  724. 433:421a,432:eqtri |- S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  725. = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  726. 434:420,433:eqtri |- S. ( A [,] B ) V _d x = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  727. *now simplify this
  728. 498:10ec,11f,11g:divcan4i |- ( ( E x. 2 ) / 2 ) = E
  729. 499:498:oveq1i |- ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( E x. ( B - A ) )
  730. 500::div32 |- ( ( ( E x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  731. -> ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) )
  732. 501:11he,11i,16a,500:mp3an |- ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) )
  733. 502:499,501:eqtr3i |- ( E x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) )
  734. 503:502:oveq1i |- ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  735. = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  736. 504:434,503:eqtri |- S. ( A [,] B ) V _d x
  737. = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  738. 505:11he,11j,d63:adddiri |- ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) )
  739. = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  740. 506:504,505:eqtr4i |- S. ( A [,] B ) V _d x
  741. = ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) )
  742. 507::addsub12 |- ( ( F e. CC /\ ( E x. 2 ) e. CC /\ E e. CC )
  743. -> ( F + ( ( E x. 2 ) - E ) ) = ( ( E x. 2 ) + ( F - E ) ) )
  744. 508:10fc,11he,10ec,507:mp3an |- ( F + ( ( E x. 2 ) - E ) ) = ( ( E x. 2 ) + ( F - E ) )
  745. 509:10ec,10ec:pncan3oi |- ( ( E + E ) - E ) = E
  746. 510:10ec:times2i |- ( E x. 2 ) = ( E + E )
  747. 511:510:oveq1i |- ( ( E x. 2 ) - E ) = ( ( E + E ) - E )
  748. 512:511,509:eqtri |- ( ( E x. 2 ) - E ) = E
  749. 513:512:oveq2i |- ( F + ( ( E x. 2 ) - E ) ) = ( F + E )
  750. 514:508,513:eqtr3i |- ( ( E x. 2 ) + ( F - E ) ) = ( F + E )
  751. 515:514:oveq1i |- ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) )
  752. *we have the integral for V :) :) :)
  753. 516:506,515:eqtri |- S. ( A [,] B ) V _d x = ( ( F + E ) x. ( ( B - A ) / 2 ) )
  754. 517:516,416:oveq12i |- ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x )
  755. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  756. 518:301a,517:eqtri |- S. ( A [,] B ) ( V - U ) _d x
  757. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  758. 519:300a,518:eqtri |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x
  759. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  760. *simplify
  761. 520::div32 |- ( ( ( F + E ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  762. -> ( ( ( F + E ) / 2 ) x. ( B - A ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) ) )
  763. 521:11fe,11i,16a,520:mp3an |- ( ( ( F + E ) / 2 ) x. ( B - A ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) )
  764. 522::div32 |- ( ( ( D + C ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  765. -> ( ( ( D + C ) / 2 ) x. ( B - A ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  766. 523:11dc,11i,16a,522:mp3an |- ( ( ( D + C ) / 2 ) x. ( B - A ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) )
  767. 524:521,523:oveq12i |- ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
  768. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  769. 525:519,524:eqtr4i |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x
  770. = ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
  771. d75:11fe,11f,11g:divcli |- ( ( F + E ) / 2 ) e. CC
  772. d76:11dc,11f,11g:divcli |- ( ( D + C ) / 2 ) e. CC
  773. 526:d75,d76,16a:subdiri |- ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  774. = ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
  775. *this is the integral on A,B !! :)
  776. 527:525,526:eqtr4i |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x
  777. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  778. 528:300a,527:eqtr3i |- S. ( A [,] B ) ( V - U ) _d x
  779. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  780.  
  781. *now get the integral on RR
  782. 600::itgss2 |- ( ( A [,] B ) C_ RR -> S. ( A [,] B ) ( V - U ) _d x
  783. = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
  784. 600a:15,600:ax-mp |- S. ( A [,] B ) ( V - U ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  785. *41::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ ( D - C ) e. CC ) -> S. ( A [,] B ) ( D - C ) _d x = ( ( D - C ) x. ( vol ` ( A [,] B ) ) ) )
  786. *42:16a,25d,25ac,41:mp3an |- S. ( A [,] B ) ( D - C ) _d x = ( ( D - C ) x. ( vol ` ( A [,] B ) ) )
  787. 601:600a,528:eqtr3i |- S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  788. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  789. *44:43,25aaa:eqtri |- S. RR if ( x e. ( A [,] B ) , ( D - C ) , 0 ) _d x = ( ( D - C ) x. ( B - A ) )
  790. 602:198,601:eqtri |- S. RR ( vol ` ( S " { x } ) ) _d x
  791. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  792. *46:45,25acb:eqtri |- S. RR ( vol ` ( S " { x } ) ) _d x = ( ( B - A ) x. ( D - C ) )
  793.  
  794. *combine facts to get the result
  795. 997:76,210,237:3pm3.2i |- ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  796. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  797. 998:997,dmarea:mpbir |- S e. dom area
  798. 999:998,areaval:ax-mp |- ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x
  799. qed:999,602:eqtri |- ( area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  800.  
  801. $)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!