API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Apr 2nd, 2019
125
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 62.30 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. *73::opelxpi |- ( ( x e. RR /\ y e. RR ) -> <. x , y >. e. ( RR X. RR ) )
  351. *73b:72b,73:syl |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> <. x , y >. e. ( RR X. RR ) )
  352. *73c:60ba,73b:sylbi |- ( <. x , y >. e. S -> <. x , y >. e. ( RR X. RR ) )
  353. *73cb:73c:rgenw |- A. t e. S ( <. x , y >. e. S -> <. x , y >. e. ( RR X. RR ) )
  354. *73e::dfss2 |- ( S C_ ( RR X. RR ) <-> A. &S1 ( &S1 e. S -> &S1 e. ( RR X. RR ) ) )
  355. *74:73e,73cb: |- S C_ ( RR X. RR )
  356. 75e::df-xp |- ( RR X. RR ) = { <. x , y >. | ( x e. RR /\ y e. RR ) }
  357. 75f:72b:ssopab2i |- { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } C_ { <. x , y >. | ( x e. RR /\ y e. RR ) }
  358. 76:75f,12,75e:3sstr4i |- S C_ ( RR X. RR )
  359.  
  360. *part 2 of the conditions of dmarea prove A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  361. 100::iccmbl |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )
  362. 101:1,2,100:mp2an |- ( A [,] B ) e. dom vol
  363. 102::iccmbl |- ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) e. dom vol )
  364. 104:36d,102:syl |- ( x e. ( A [,] B ) -> ( U [,] V ) e. dom vol )
  365. 104a:37a,102:syl |- ( x e. RR -> ( U [,] V ) e. dom vol )
  366. 105::0mbl |- (/) e. dom vol
  367. 106:105:a1i |- ( x e. RR -> (/) e. dom vol )
  368. 107:104a,106:jca |- ( x e. RR -> ( ( U [,] V ) e. dom vol /\ (/) e. dom vol ) )
  369. 108::ifcl |- ( ( ( U [,] V ) e. dom vol /\ (/) e. dom vol )
  370. -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
  371. 109:107,108:syl |- ( x e. RR -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
  372. 110:60,109:syl5eqel |- ( x e. RR -> ( S " { x } ) e. dom vol )
  373. *jump to 200 for the completion of this part
  374.  
  375. *compute vols
  376. 168::ovolicc |- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
  377. 168a::ovolicc |- ( ( U e. RR /\ V e. RR /\ U <_ V ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
  378. 169:1,2,11ad,168:mp3an |- ( vol* ` ( A [,] B ) ) = ( B - A )
  379. 169a:46,168a:syl |- ( x e. ( A [,] B ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
  380. 170::mblvol |- ( ( A [,] B ) e. dom vol -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
  381. 170a::mblvol |- ( ( U [,] V ) e. dom vol -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
  382. 171:101,170:ax-mp |- ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) )
  383. 171a:104,170a:syl |- ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
  384. 172:171,169:eqtri |- ( vol ` ( A [,] B ) ) = ( B - A )
  385. 172aa:172,16:eqeltri |- ( vol ` ( A [,] B ) ) e. RR
  386. 172a:171a,169a:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( V - U ) )
  387. 178::ssel2 |- ( ( ( A [,] B ) C_ RR /\ x e. ( A [,] B ) ) -> x e. RR )
  388. 181::ovol0 |- ( vol* ` (/) ) = 0
  389. 182::mblvol |- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
  390. 183:105,182:ax-mp |- ( vol ` (/) ) = ( vol* ` (/) )
  391. 184:183,181:eqtri |- ( vol ` (/) ) = 0
  392. 185:184:a1i |- ( -. x e. ( A [,] B ) -> ( vol ` (/) ) = 0 )
  393. *apply these to S
  394. 186:66,172a:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( V - U ) )
  395. 188:186,37fb:eqeltrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) e. RR )
  396. 189:67,184:syl6eq |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = 0 )
  397. 190::iftrue |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( V - U ) )
  398. 191::iffalse |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = 0 )
  399. 192:190,186:eqtr4d |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
  400. 192a:191,189:eqtr4d |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
  401. 193:192,192a:pm2.61i |- if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) )
  402. 194:193:eqcomi |- ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  403. 195:194:a1i |- ( x e. RR -> ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 ) )
  404. 196:195:rgen |- A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  405. 197::itgeq2 |- ( A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  406. -> S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
  407. 198:196,197:ax-mp |- S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  408.  
  409. *continue with part 2 of conditions of dmarea
  410. 200::fvimacnv |- ( ( Fun vol /\ ( S " { x } ) e. dom vol ) -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  411. 201::volf |- vol : dom vol --> ( 0 [,] +oo )
  412. 202::ffun |- ( vol : dom vol --> ( 0 [,] +oo ) -> Fun vol )
  413. 203:201,202:ax-mp |- Fun vol
  414. 203a:110,203:jctil |- ( x e. RR -> ( Fun vol /\ ( S " { x } ) e. dom vol ) )
  415. 204:203a,200:syl |- ( x e. RR -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  416. 205::ifcl |- ( ( ( V - U ) e. RR /\ 0 e. RR ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
  417. 206a:37f,206:jctir |- ( x e. RR -> ( ( V - U ) e. RR /\ 0 e. RR ) )
  418. 207:206a,205:syl |- ( x e. RR -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
  419. 208:195,207:eqeltrd |- ( x e. RR -> ( vol ` ( S " { x } ) ) e. RR )
  420. 209:208,204:mpbid |- ( x e. RR -> ( S " { x } ) e. ( `' vol " RR ) )
  421. 210:209:rgen |- A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  422.  
  423. *prove a lot of functions are continuous
  424. 211::ssid |- CC C_ CC
  425. d77::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
  426. 238:d77:subcn |- - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
  427. d87:d77:addcn |- + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
  428. d98::eqid |- ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) )
  429. d87a:d77,d98:divcn |- / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) )
  430. d78:238:a1i |- ( T. -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
  431. d82:d87:a1i |- ( T. -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
  432. d82a:d87a:a1i |- ( T. -> / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) ) )
  433. 239:10:mpteq2i |- ( x e. ( A [,] B ) |-> U )
  434. = ( x e. ( A [,] B ) |-> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) )
  435. 239a:11:mpteq2i |- ( x e. ( A [,] B ) |-> V )
  436. = ( x e. ( A [,] B ) |-> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) )
  437. *get the constants as cts
  438. 240a::cncfmptc |- ( ( A e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  439. -> ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
  440. 240b::cncfmptc |- ( ( B e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  441. -> ( x e. ( A [,] B ) |-> B ) e. ( ( A [,] B ) -cn-> CC ) )
  442. 240::cncfmptc |- ( ( C e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  443. -> ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
  444. d96::cncfmptc |- ( ( D e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  445. -> ( x e. ( A [,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC ) )
  446. 211a::cncfmptc |- ( ( E e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  447. -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
  448. 211b::cncfmptc |- ( ( F e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  449. -> ( x e. ( A [,] B ) |-> F ) e. ( ( A [,] B ) -cn-> CC ) )
  450. 240c:10ac,15b,211,240a:mp3an |- ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC )
  451. 240d:10bc,15b,211,240b:mp3an |- ( x e. ( A [,] B ) |-> B ) e. ( ( A [,] B ) -cn-> CC )
  452. d88:10cc,15b,211,240:mp3an |- ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC )
  453. d92:10dc,15b,211,d96:mp3an |- ( x e. ( A [,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC )
  454. 211c:10ec,15b,211,211a:mp3an |- ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC )
  455. 211d:10fc,15b,211,211b:mp3an |- ( x e. ( A [,] B ) |-> F ) e. ( ( A [,] B ) -cn-> CC )
  456. 211g:240c:a1i |- ( T. -> ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
  457. 211h:240d:a1i |- ( T. -> ( x e. ( A [,] B ) |-> B ) e. ( ( A [,] B ) -cn-> CC ) )
  458. d83:d88:a1i |- ( T. -> ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
  459. d91:d92:a1i |- ( T. -> ( x e. ( A [,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC ) )
  460. 211e:211c:a1i |- ( T. -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
  461. 211f:211d:a1i |- ( T. -> ( x e. ( A [,] B ) |-> F ) e. ( ( A [,] B ) -cn-> CC ) )
  462. *prove I is cts
  463. 212aa::cncfmptid |- ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
  464. 212ab:15b,211,212aa:mp2an |- ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC )
  465. *212:: |- ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC )
  466. 212a:212ab:a1i |- ( T. -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
  467. 212b:d77,d78,212a,211g:cncfmpt2f
  468. |- ( T. -> ( x e. ( A [,] B ) |-> ( x - A ) ) e. ( ( A [,] B ) -cn-> CC ) )
  469. 212c:d77,d78,211h,211g:cncfmpt2f
  470. |- ( T. -> ( x e. ( A [,] B ) |-> ( B - A ) ) e. ( ( A [,] B ) -cn-> CC ) )
  471. *##################################
  472. *this is the only problem remaining :)
  473. 212e::
  474. |- ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  475. d86:d77,d78,d91,d83:cncfmpt2f |- ( T. -> ( x e. ( A [,] B ) |-> ( D - C ) ) e. ( ( A [,] B ) -cn-> CC ) )
  476. d84:212e,d86:mulcncf |- ( T. -> ( x e. ( A [,] B )
  477. |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  478. 247:d77,d82,d83,d84:cncfmpt2f |- ( T. -> ( x e. ( A [,] B )
  479. |-> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  480. d79:239,247:syl5eqel |- ( T. -> ( x e. ( A [,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC ) )
  481. d80a:d77,d78,211f,211e:cncfmpt2f |- ( T. -> ( x e. ( A [,] B ) |-> ( F - E ) ) e. ( ( A [,] B ) -cn-> CC ) )
  482. d80b:212e,d80a:mulcncf |- ( T. -> ( x e. ( A [,] B )
  483. |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  484. d80c:d77,d82,211e,d80b:cncfmpt2f |- ( T. -> ( x e. ( A [,] B )
  485. |-> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  486. d80:239a,d80c:syl5eqel |- ( T. -> ( x e. ( A [,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC ) )
  487. 249:d77,d78,d80,d79:cncfmpt2f |- ( T. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  488. 249a:11e,249:ax-mp |- ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC )
  489.  
  490. *get things in L^1
  491. d29c::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
  492. -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
  493. d29d:1,2,d88,d29c:mp3an |- ( x e. ( A [,] B ) |-> C ) e. L^1
  494. d30:d29d:a1i |- ( T. -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
  495. d66c::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
  496. -> ( x e. ( A [,] B ) |-> E ) e. L^1 )
  497. d66ca:1,2,211c,d66c:mp3an |- ( x e. ( A [,] B ) |-> E ) e. L^1
  498. d66d:d66ca:a1i |- ( T. -> ( x e. ( A [,] B ) |-> E ) e. L^1 )
  499. 249b::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  500. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  501. 249c:1,2,249a,249b:mp3an |- ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1
  502. 249d:249c:a1i |- ( T. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  503. 249e:11e,249d:ax-mp |- ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1
  504.  
  505. d29:3:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> C e. RR )
  506. *d29a::cncfmptc |- ( ( C e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  507. -> ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
  508. *d29b:10cc,15b,211,d29a:mp3an |- ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC )
  509. d50:27a:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  510. d51:4:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> D e. RR )
  511. d52:d51,d29:resubcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( D - C ) e. RR )
  512. d31:d50,d52:remulcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) e. RR )
  513. d31a::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  514. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1 )
  515. d101:11e,d84:ax-mp |- ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. ( ( A [,] B ) -cn-> CC )
  516. d31b:1,2,d101,d31a:mp3an |- ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1
  517. d31c:d31b:a1i |- ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1 )
  518. d53:15f:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> x e. RR )
  519. d53a::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
  520. -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
  521. d53b:1,2,212ab,d53a:mp3an |- ( x e. ( A [,] B ) |-> x ) e. L^1
  522. d53c:d53b:a1i |- ( T. -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
  523. d55:1:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> A e. RR )
  524. d56a::cncfmptc |- ( ( A e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  525. -> ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
  526. d56b:10ac,15b,211,d56a:mp3an |- ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC )
  527. d56c::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
  528. -> ( x e. ( A [,] B ) |-> A ) e. L^1 )
  529. d56d:1,2,d56b,d56c:mp3an |- ( x e. ( A [,] B ) |-> A ) e. L^1
  530. d56:d56d:a1i |- ( T. -> ( x e. ( A [,] B ) |-> A ) e. L^1 )
  531. d64:5:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> E e. RR )
  532. *d65a:5:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> E e. RR )
  533. *d66a::cncfmptc |- ( ( E e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  534. -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
  535. *d66b:10ec,15b,211,d66a:mp3an |- ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC )
  536. d68:6:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> F e. RR )
  537. d69:d68,d64:resubcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( F - E ) e. RR )
  538. d66:d50,d69:remulcld |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) e. RR )
  539. d66aaa::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  540. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1 )
  541. d104:11e,d80b:ax-mp |- ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. ( ( A [,] B ) -cn-> CC )
  542. d66baa:1,2,d104,d66aaa:mp3an |- ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1
  543. d66caa:d66baa:a1i |- ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1 )
  544. d25:36c:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> V e. RR )
  545. d25a::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC ) )
  546. -> ( x e. ( A [,] B ) |-> V ) e. L^1 )
  547. d107:11e,d80:ax-mp |- ( x e. ( A [,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC )
  548. d25b:1,2,d107,d25a:mp3an |- ( x e. ( A [,] B ) |-> V ) e. L^1
  549. d25c:d25b:a1i |- ( T. -> ( x e. ( A [,] B ) |-> V ) e. L^1 )
  550. d27:36b:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> U e. RR )
  551. d27a::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC ) )
  552. -> ( x e. ( A [,] B ) |-> U ) e. L^1 )
  553. d110:11e,d79:ax-mp |- ( x e. ( A [,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC )
  554. d27b:1,2,d110,d27a:mp3an |- ( x e. ( A [,] B ) |-> U ) e. L^1
  555. d27c:d27b:a1i |- ( T. -> ( x e. ( A [,] B ) |-> U ) e. L^1 )
  556. d41:16cb:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x - A ) e. RR )
  557. d42:d53,d53c,d55,d56:iblsub |- ( T. -> ( x e. ( A [,] B ) |-> ( x - A ) ) e. L^1 )
  558. d43:10dc:a1i |- ( T. -> D e. CC )
  559. d44:10cc:a1i |- ( T. -> C e. CC )
  560. d33:d43,d44:subcld |- ( T. -> ( D - C ) e. CC )
  561. d53aaa::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  562. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1 )
  563. d113:11e,212e:ax-mp |- ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC )
  564. d53baa:1,2,d113,d53aaa:mp3an |- ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1
  565. d53caa:d53baa:a1i |- ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1 )
  566.  
  567. *part 3 of the conditions of dmarea, prove L1
  568. 220:15:a1i |- ( 0 e. RR -> ( A [,] B ) C_ RR )
  569. 221::rembl |- RR e. dom vol
  570. 222:221:a1i |- ( 0 e. RR -> RR e. dom vol )
  571. 223:188:adantl |- ( ( 0 e. RR /\ x e. ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) e. RR )
  572. 224::eldifn |- ( x e. ( RR \ ( A [,] B ) ) -> -. x e. ( A [,] B ) )
  573. 225:224,189:syl |- ( x e. ( RR \ ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  574. 226:225:adantl |- ( ( 0 e. RR /\ x e. ( RR \ ( A [,] B ) ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  575.  
  576. *227::cncfmptc |- ( ( ( V - U ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  577. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  578. *228::ssid |- CC C_ CC
  579. *228a:228:a1i |- ( x e. RR -> CC C_ CC )
  580. *228b:37g,15c,228a:3jca |- ( x e. RR -> ( ( V - U ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) )
  581. *229:228b,227:syl |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  582. *230::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  583. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  584. *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 ) ) )
  585. *232:231,230:syl |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  586.  
  587. 233:186:mpteq2ia |- ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) = ( x e. ( A [,] B ) |-> ( V - U ) )
  588. *234:233: |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  589. *234a:15f,234:syl |- ( x e. ( A [,] B ) -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  590. *234ab:234:rgen |- A. x e. RR ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
  591. 234b:233,249e:eqeltri |- ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
  592. 235:234b:a1i |- ( 0 e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  593. 236:220,222,223,226,235:iblss2
  594. |- ( 0 e. RR -> ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  595. 237:206,236:ax-mp |- ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1
  596.  
  597. *value of the integral of x
  598. 250:: |- S. ( A [,] B ) x _d x = ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 )
  599.  
  600. *evaluate the integral
  601. d24:186:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) = ( V - U ) )
  602. 300:d24:itgeq2dv |- ( T. -> S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x = S. ( A [,] B ) ( V - U ) _d x )
  603. 300a:11e,300:ax-mp |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x = S. ( A [,] B ) ( V - U ) _d x
  604. *break up int S = int V - int U
  605. 301:d25,d25c,d27,d27c:itgsub |- ( T. -> S. ( A [,] B ) ( V - U ) _d x = ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x ) )
  606. 301a:11e,301:ax-mp |- S. ( A [,] B ) ( V - U ) _d x = ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x )
  607. 302:10:a1i |- ( ( T. /\ x e. ( A [,] B ) ) -> U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) )
  608. 303:302:itgeq2dv |- ( T. -> S. ( A [,] B ) U _d x
  609. = S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x )
  610. 303a:11e,303:ax-mp |- S. ( A [,] B ) U _d x
  611. = S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  612. *int U = int C + int I (D - C)
  613. 304:d29,d30,d31,d31c:itgadd |- ( T. -> S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  614. = ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x ) )
  615. 304a:11e,304:ax-mp |- S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  616. = ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
  617. 305::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ C e. CC )
  618. -> S. ( A [,] B ) C _d x = ( C x. ( vol ` ( A [,] B ) ) ) )
  619. 305a:101,172aa,10cc,305:mp3an |- S. ( A [,] B ) C _d x = ( C x. ( vol ` ( A [,] B ) ) )
  620. 305b:172:oveq2i |- ( C x. ( vol ` ( A [,] B ) ) ) = ( C x. ( B - A ) )
  621. 305c:305a,305b:eqtri |- S. ( A [,] B ) C _d x = ( C x. ( B - A ) )
  622. *int I ( D - C ) = ( D - C ) int I
  623. 306:d33,d50,d53caa:itgmulc2 |- ( T. -> ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  624. = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x )
  625. 306a:11e,306:ax-mp |- ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  626. = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  627. d36:15a,16cb:sseldi |- ( x e. ( A [,] B ) -> ( x - A ) e. CC )
  628. d37:16a:a1i |- ( x e. ( A [,] B ) -> ( B - A ) e. CC )
  629. d38:24:a1i |- ( x e. ( A [,] B ) -> ( B - A ) =/= 0 )
  630. 307:d36,d37,d38:divrecd |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( x - A ) x. ( 1 / ( B - A ) ) ) )
  631. d39:d37,d38:reccld |- ( x e. ( A [,] B ) -> ( 1 / ( B - A ) ) e. CC )
  632. 308:d36,d39:mulcomd |- ( x e. ( A [,] B ) -> ( ( x - A ) x. ( 1 / ( B - A ) ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) ) )
  633. 309:307,308:eqtrd |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) ) )
  634. 309a:309:rgen |- A. x e. ( A [,] B ) ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) )
  635. 309c::itgeq2 |- ( A. x e. ( A [,] B ) ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) )
  636. -> S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x )
  637. 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
  638. d45:10bc:a1i |- ( T. -> B e. CC )
  639. d46:10ac:a1i |- ( T. -> A e. CC )
  640. d47:d45,d46:subcld |- ( T. -> ( B - A ) e. CC )
  641. d48:18:a1i |- ( T. -> B =/= A )
  642. d49:d45,d46,d48:subne0d |- ( T. -> ( B - A ) =/= 0 )
  643. d40:d47,d49:reccld |- ( T. -> ( 1 / ( B - A ) ) e. CC )
  644. d40a:11e,d40:ax-mp |- ( 1 / ( B - A ) ) e. CC
  645. *int I = int ( x - A ) / B - A = 1 / B - A int ( x - A )
  646. 310:d40,d41,d42:itgmulc2 |- ( T. -> ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  647. = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x )
  648. 310a:11e,310:ax-mp |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  649. = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
  650. * int x - A = int X - int A
  651. 315:d53,d53c,d55,d56:itgsub
  652. |- ( T. -> S. ( A [,] B ) ( x - A ) _d x = ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x ) )
  653. 315a:11e,315:ax-mp |- S. ( A [,] B ) ( x - A ) _d x = ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x )
  654. 316::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ A e. CC )
  655. -> S. ( A [,] B ) A _d x = ( A x. ( vol ` ( A [,] B ) ) ) )
  656. 317:101,172aa,10ac,316:mp3an |- S. ( A [,] B ) A _d x = ( A x. ( vol ` ( A [,] B ) ) )
  657. 318:172:oveq2i |- ( A x. ( vol ` ( A [,] B ) ) ) = ( A x. ( B - A ) )
  658. 319:317,318:eqtri |- S. ( A [,] B ) A _d x = ( A x. ( B - A ) )
  659. *now rebuild :)
  660. 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 ) ) )
  661. 321:315a,320:eqtri |- S. ( A [,] B ) ( x - A ) _d x = ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) )
  662. 322:321:oveq2i |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  663. = ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
  664. 323::subdi |- ( ( ( 1 / ( B - A ) ) e. CC /\ ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) e. CC /\ ( A x. ( B - A ) ) e. CC )
  665. -> ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
  666. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) ) )
  667. 324:d40a,16af,16ab,323:mp3an |- ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
  668. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
  669. 345:d40a,16ab:mulcomi |- ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = ( ( A x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  670. 346:16ab,16a,24:divreci |- ( ( A x. ( B - A ) ) / ( B - A ) ) = ( ( A x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  671. 347:345,346:eqtr4i |- ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = ( ( A x. ( B - A ) ) / ( B - A ) )
  672. 348:10ac,16a,24:divcan4i |- ( ( A x. ( B - A ) ) / ( B - A ) ) = A
  673. 349:347,348:eqtri |- ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = A
  674. 350:322,324:eqtri |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  675. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
  676. 351:349:oveq2i |- ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
  677. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  678. 352:350,351:eqtri |- ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x )
  679. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  680. 353:310a,352:eqtr3i |- S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
  681. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  682. *this is to be simplified
  683. 354:309d,353:eqtri |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x
  684. = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
  685. 355:10bc,10ac:subsqi |- ( ( B ^ 2 ) - ( A ^ 2 ) ) = ( ( B + A ) x. ( B - A ) )
  686. 355a:355:oveq1i |- ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) = ( ( ( B + A ) x. ( B - A ) ) / 2 )
  687. 355b:355a:oveq2i |- ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) )
  688. = ( ( 1 / ( B - A ) ) x. ( ( ( B + A ) x. ( B - A ) ) / 2 ) )
  689. d58:355,16ae:eqeltrri |- ( ( B + A ) x. ( B - A ) ) e. CC
  690. 356:d40a,d58,11f,11g:divassi
  691. |- ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 ) = ( ( 1 / ( B - A ) ) x. ( ( ( B + A ) x. ( B - A ) ) / 2 ) )
  692. 357:355b,356:eqtr4i |- ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) )
  693. = ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 )
  694. 358:d40a,d58:mulcomi
  695. |- ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) = ( ( ( B + A ) x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  696. 359:d58,16a,24:divreci
  697. |- ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) ) = ( ( ( B + A ) x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
  698. 360:358,359:eqtr4i |- ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) )
  699. = ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) )
  700. d59:10bc,10ac:addcli |- ( B + A ) e. CC
  701. 361:d59,16a,24:divcan4i |- ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) ) = ( B + A )
  702. 362:360,361:eqtri |- ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) = ( B + A )
  703. 363:362:oveq1i |- ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 ) = ( ( B + A ) / 2 )
  704. 364:357,363:eqtri |- ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) = ( ( B + A ) / 2 )
  705. 365:364:oveq1i |- ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A ) = ( ( ( B + A ) / 2 ) - A )
  706. *this is to be simplified further
  707. 366:354,365:eqtri |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = ( ( ( B + A ) / 2 ) - A )
  708. 367:10ac,11f,11g:divcan4i |- ( ( A x. 2 ) / 2 ) = A
  709. 368:367:oveq2i |- ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) = ( ( ( B + A ) / 2 ) - A )
  710. 369::divsubdir |- ( ( ( B + A ) e. CC /\ ( A x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) )
  711. -> ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) )
  712. 370:d59,11h,11i,369:mp3an |- ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) )
  713. 371:370,368:eqtri |- ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - A )
  714. 372:10bc,10ac,11h:addsubassi |- ( ( B + A ) - ( A x. 2 ) ) = ( B + ( A - ( A x. 2 ) ) )
  715. 373::subsub2 |- ( ( B e. CC /\ ( A x. 2 ) e. CC /\ A e. CC )
  716. -> ( B - ( ( A x. 2 ) - A ) ) = ( B + ( A - ( A x. 2 ) ) ) )
  717. 374:10bc,11h,10ac,373:mp3an |- ( B - ( ( A x. 2 ) - A ) ) = ( B + ( A - ( A x. 2 ) ) )
  718. *375::pncan |- ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) - A ) = A )
  719. 376:10ac,10ac:pncan3oi |- ( ( A + A ) - A ) = A
  720. 377:10ac:times2i |- ( A x. 2 ) = ( A + A )
  721. 378:377:oveq1i |- ( ( A x. 2 ) - A ) = ( ( A + A ) - A )
  722. 379:378,376:eqtri |- ( ( A x. 2 ) - A ) = A
  723. 380:379:oveq2i |- ( B - ( ( A x. 2 ) - A ) ) = ( B - A )
  724. 381:374,380:eqtr3i |- ( B + ( A - ( A x. 2 ) ) ) = ( B - A )
  725. 382:372,381:eqtri |- ( ( B + A ) - ( A x. 2 ) ) = ( B - A )
  726. 383:382:oveq1i |- ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( B - A ) / 2 )
  727. 384:370,383:eqtr3i |- ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) = ( ( B - A ) / 2 )
  728. 385:368,384:eqtr3i |- ( ( ( B + A ) / 2 ) - A ) = ( ( B - A ) / 2 )
  729.  
  730. *this is the integral of I :) :)
  731. 386:366,385:eqtri |- S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = ( ( B - A ) / 2 )
  732.  
  733. *build up to the integral of U
  734. 387:386:oveq2i |- ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  735. = ( ( D - C ) x. ( ( B - A ) / 2 ) )
  736. 388:387,306a:eqtr3i |- ( ( D - C ) x. ( ( B - A ) / 2 ) )
  737. = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  738. d60:11e,d33:ax-mp |- ( D - C ) e. CC
  739. d60a:d60:a1i |- ( x e. ( A [,] B ) -> ( D - C ) e. CC )
  740. 389::mulcom |- ( ( ( D - C ) e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC )
  741. -> ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  742. 390:d60a,27b,389:syl2anc |- ( x e. ( A [,] B )
  743. -> ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  744. 391:390:rgen |- A. x e. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  745. 392::itgeq2 |- ( A. x e. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) )
  746. = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  747. -> S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  748. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
  749. 393:391,392:ax-mp |- S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  750. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x
  751. 394:388,393:eqtr2i |- S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x
  752. = ( ( D - C ) x. ( ( B - A ) / 2 ) )
  753. 395:305c,394:oveq12i |- ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
  754. = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  755. 396:304a,395:eqtri |- S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
  756. = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  757. *now simplify this
  758. 397:303a,396:eqtri |- S. ( A [,] B ) U _d x = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  759. 398:10cc,11f,11g:divcan4i |- ( ( C x. 2 ) / 2 ) = C
  760. 399:398:oveq1i |- ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( C x. ( B - A ) )
  761. 400::div32 |- ( ( ( C x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  762. -> ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) )
  763. 401:11hc,11i,16a,400:mp3an |- ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) )
  764. 402:399,401:eqtr3i |- ( C x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) )
  765. 403:402:oveq1i |- ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  766. = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  767. 404:397,403:eqtri |- S. ( A [,] B ) U _d x
  768. = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  769. d63:16a,11f,11g:divcli |- ( ( B - A ) / 2 ) e. CC
  770. 405:11hc,d60,d63:adddiri |- ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) )
  771. = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
  772. 406:404,405:eqtr4i |- S. ( A [,] B ) U _d x
  773. = ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) )
  774. 407::addsub12 |- ( ( D e. CC /\ ( C x. 2 ) e. CC /\ C e. CC )
  775. -> ( D + ( ( C x. 2 ) - C ) ) = ( ( C x. 2 ) + ( D - C ) ) )
  776. 408:10dc,11hc,10cc,407:mp3an |- ( D + ( ( C x. 2 ) - C ) ) = ( ( C x. 2 ) + ( D - C ) )
  777. 409:10cc,10cc:pncan3oi |- ( ( C + C ) - C ) = C
  778. 410:10cc:times2i |- ( C x. 2 ) = ( C + C )
  779. 411:410:oveq1i |- ( ( C x. 2 ) - C ) = ( ( C + C ) - C )
  780. 412:411,409:eqtri |- ( ( C x. 2 ) - C ) = C
  781. 413:412:oveq2i |- ( D + ( ( C x. 2 ) - C ) ) = ( D + C )
  782. 414:408,413:eqtr3i |- ( ( C x. 2 ) + ( D - C ) ) = ( D + C )
  783. 415:414:oveq1i |- ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) )
  784. *we have the integral for U :) :) :)
  785. 416:406,415:eqtri |- S. ( A [,] B ) U _d x = ( ( D + C ) x. ( ( B - A ) / 2 ) )
  786.  
  787. 417::itgeq2 |- ( A. x e. ( A [,] B ) V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  788. -> S. ( A [,] B ) V _d x = S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x )
  789. 418:11:a1i |- ( x e. ( A [,] B ) -> V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) )
  790. 419:418:rgen |- A. x e. ( A [,] B ) V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  791. *this is the integral for V to be proven
  792. 420:419,417:ax-mp |- S. ( A [,] B ) V _d x = S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  793.  
  794. 421:d64,d66d,d66,d66caa:itgadd |- ( T. -> S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  795. = ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x ) )
  796. 421a:11e,421:ax-mp |- S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  797. = ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
  798. 422::itgconst |- ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ E e. CC )
  799. -> S. ( A [,] B ) E _d x = ( E x. ( vol ` ( A [,] B ) ) ) )
  800. 422a:101,172aa,10ec,422:mp3an |- S. ( A [,] B ) E _d x = ( E x. ( vol ` ( A [,] B ) ) )
  801. 422b:172:oveq2i |- ( E x. ( vol ` ( A [,] B ) ) ) = ( E x. ( B - A ) )
  802. 422c:422a,422b:eqtri |- S. ( A [,] B ) E _d x = ( E x. ( B - A ) )
  803. *get int I ( F - E )
  804. d73:10fc:a1i |- ( T. -> F e. CC )
  805. d74:10ec:a1i |- ( T. -> E e. CC )
  806. d70:d73,d74:subcld |- ( T. -> ( F - E ) e. CC )
  807. 423:d70,d50,d53caa:itgmulc2 |- ( T. -> ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  808. = S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x )
  809. 423a:11e,423:ax-mp |- ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  810. = S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  811. 424:386:oveq2i |- ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x )
  812. = ( ( F - E ) x. ( ( B - A ) / 2 ) )
  813. 425:423a,424:eqtr3i |- S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x = ( ( F - E ) x. ( ( B - A ) / 2 ) )
  814. 426::itgeq2 |- ( A. x e. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) )
  815. = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  816. -> S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  817. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
  818. 427::mulcom |- ( ( ( F - E ) e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC )
  819. -> ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  820. 428:11k,27b,427:syl2anc |- ( x e. ( A [,] B )
  821. -> ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  822. 429:428:rgen |- A. x e. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) )
  823. = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  824. 430:429,426:ax-mp |- S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
  825. = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x
  826. 431:430,425:eqtr3i |- S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x
  827. = ( ( F - E ) x. ( ( B - A ) / 2 ) )
  828. 432:422c,431:oveq12i |- ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
  829. = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  830. 433:421a,432:eqtri |- S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
  831. = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  832. 434:420,433:eqtri |- S. ( A [,] B ) V _d x = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  833. *now simplify this
  834. 498:10ec,11f,11g:divcan4i |- ( ( E x. 2 ) / 2 ) = E
  835. 499:498:oveq1i |- ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( E x. ( B - A ) )
  836. 500::div32 |- ( ( ( E x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  837. -> ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) )
  838. 501:11he,11i,16a,500:mp3an |- ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) )
  839. 502:499,501:eqtr3i |- ( E x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) )
  840. 503:502:oveq1i |- ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  841. = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  842. 504:434,503:eqtri |- S. ( A [,] B ) V _d x
  843. = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  844. 505:11he,11j,d63:adddiri |- ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) )
  845. = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
  846. 506:504,505:eqtr4i |- S. ( A [,] B ) V _d x
  847. = ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) )
  848. 507::addsub12 |- ( ( F e. CC /\ ( E x. 2 ) e. CC /\ E e. CC )
  849. -> ( F + ( ( E x. 2 ) - E ) ) = ( ( E x. 2 ) + ( F - E ) ) )
  850. 508:10fc,11he,10ec,507:mp3an |- ( F + ( ( E x. 2 ) - E ) ) = ( ( E x. 2 ) + ( F - E ) )
  851. 509:10ec,10ec:pncan3oi |- ( ( E + E ) - E ) = E
  852. 510:10ec:times2i |- ( E x. 2 ) = ( E + E )
  853. 511:510:oveq1i |- ( ( E x. 2 ) - E ) = ( ( E + E ) - E )
  854. 512:511,509:eqtri |- ( ( E x. 2 ) - E ) = E
  855. 513:512:oveq2i |- ( F + ( ( E x. 2 ) - E ) ) = ( F + E )
  856. 514:508,513:eqtr3i |- ( ( E x. 2 ) + ( F - E ) ) = ( F + E )
  857. 515:514:oveq1i |- ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) )
  858. *we have the integral for V :) :) :)
  859. 516:506,515:eqtri |- S. ( A [,] B ) V _d x = ( ( F + E ) x. ( ( B - A ) / 2 ) )
  860. 517:516,416:oveq12i |- ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x )
  861. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  862. 518:301a,517:eqtri |- S. ( A [,] B ) ( V - U ) _d x
  863. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  864. 519:300a,518:eqtri |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x
  865. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  866. *simplify
  867. 520::div32 |- ( ( ( F + E ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  868. -> ( ( ( F + E ) / 2 ) x. ( B - A ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) ) )
  869. 521:11fe,11i,16a,520:mp3an |- ( ( ( F + E ) / 2 ) x. ( B - A ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) )
  870. 522::div32 |- ( ( ( D + C ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC )
  871. -> ( ( ( D + C ) / 2 ) x. ( B - A ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  872. 523:11dc,11i,16a,522:mp3an |- ( ( ( D + C ) / 2 ) x. ( B - A ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) )
  873. 524:521,523:oveq12i |- ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
  874. = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
  875. 525:519,524:eqtr4i |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x
  876. = ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
  877. d75:11fe,11f,11g:divcli |- ( ( F + E ) / 2 ) e. CC
  878. d76:11dc,11f,11g:divcli |- ( ( D + C ) / 2 ) e. CC
  879. 526:d75,d76,16a:subdiri |- ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  880. = ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
  881. *this is the integral on A,B !! :)
  882. 527:525,526:eqtr4i |- S. ( A [,] B ) ( vol ` ( S " { x } ) ) _d x
  883. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  884. 528:300a,527:eqtr3i |- S. ( A [,] B ) ( V - U ) _d x
  885. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  886.  
  887. *now get the integral on RR
  888. 600::itgss2 |- ( ( A [,] B ) C_ RR -> S. ( A [,] B ) ( V - U ) _d x
  889. = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
  890. 600a:15,600:ax-mp |- S. ( A [,] B ) ( V - U ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  891. *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 ) ) ) )
  892. *42:16a,25d,25ac,41:mp3an |- S. ( A [,] B ) ( D - C ) _d x = ( ( D - C ) x. ( vol ` ( A [,] B ) ) )
  893. 601:600a,528:eqtr3i |- S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  894. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  895. *44:43,25aaa:eqtri |- S. RR if ( x e. ( A [,] B ) , ( D - C ) , 0 ) _d x = ( ( D - C ) x. ( B - A ) )
  896. 602:198,601:eqtri |- S. RR ( vol ` ( S " { x } ) ) _d x
  897. = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  898. *46:45,25acb:eqtri |- S. RR ( vol ` ( S " { x } ) ) _d x = ( ( B - A ) x. ( D - C ) )
  899.  
  900. *combine facts to get the result
  901. 997:76,210,237:3pm3.2i |- ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  902. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  903. 998:997,dmarea:mpbir |- S e. dom area
  904. 999:998,areaval:ax-mp |- ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x
  905. qed:999,602:eqtri |- ( area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
  906.  
  907. $)
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!