API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Mar 26th, 2019
110
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 27.81 KB | None | 0 0
raw download clone embed print report
  1. *74 is broken
  2. *236 is broken
  3.  
  4. 10a:: |- A e. RR
  5. 10ac:10a:recni |- A e. CC
  6. 10ad:10a:a1i |- ( x e. RR -> A e. RR )
  7. 10ae:10a:rexri |- A e. RR*
  8. 10b:: |- B e. RR
  9. 10bc:10b:recni |- B e. CC
  10. 10bd:10b:a1i |- ( x e. RR -> B e. RR )
  11. 10be:10b:rexri |- B e. RR*
  12. 10c:: |- C e. RR
  13. 10cc:10c:recni |- C e. CC
  14. 10ce:10cc:a1i |- ( x e. RR -> C e. CC )
  15. 10d:: |- D e. RR
  16. 10dc:10d:recni |- D e. CC
  17. 10de:10dc:a1i |- ( x e. RR -> D e. CC )
  18. 10e:: |- E e. RR
  19. 10ec:10e:recni |- E e. CC
  20. 10ee:10ec:a1i |- ( x e. RR -> E e. CC )
  21. 10f:: |- F e. RR
  22. 10fc:10f:recni |- F e. CC
  23. 10fe:10fc:a1i |- ( x e. RR -> F e. CC )
  24. 11a:: |- A < B
  25. 11aa:10a,10b:leloei |- ( A <_ B <-> ( A < B \/ A = B ) )
  26. 11ab::orc |- ( A < B -> ( A < B \/ A = B ) )
  27. 11ac:11a,11ab:ax-mp |- ( A < B \/ A = B )
  28. 11ad:11ac,11aa:mpbir |- A <_ B
  29. 11b:: |- C <_ E
  30. 11c:: |- D <_ F
  31. 206::0re |- 0 e. RR
  32. 206ccc:206:recni |- 0 e. CC
  33. 28a::1red |- ( x e. RR -> 1 e. RR )
  34. 28ab::1cnd |- ( x e. RR -> 1 e. CC )
  35.  
  36. 12a:: |- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  37. 12b:: |- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  38.  
  39. *12c:: |- U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) )
  40. *12d:: |- V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) )
  41.  
  42. 13:: |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
  43.  
  44. *things to prove
  45. dmarea::dmarea |- ( S e. dom area <-> ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  46. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 ) )
  47. areaval::areaval |- ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )
  48.  
  49. *get A,B in RR
  50.  
  51. 14::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
  52. 15:10a,10b,14:mp2an |- ( A [,] B ) C_ RR
  53. 15a::axresscn |- RR C_ CC
  54. 15b:15,15a:sstri |- ( A [,] B ) C_ CC
  55. 15c:15b:a1i |- ( x e. RR -> ( A [,] B ) C_ CC )
  56. 15d::dfss3 |- ( ( A [,] B ) C_ RR <-> A. x e. ( A [,] B ) x e. RR )
  57. 15e:15,15d:mpbi |- A. x e. ( A [,] B ) x e. RR
  58. 15f:15e:rspec |- ( x e. ( A [,] B ) -> x e. RR )
  59. *get U,V in RR
  60. 16:10b,10a:resubcli |- ( B - A ) e. RR
  61. 16a:16:recni |- ( B - A ) e. CC
  62. 16c::resubcl |- ( ( x e. RR /\ A e. RR ) -> ( x - A ) e. RR )
  63. 16ca:10a,16c:mpan2 |- ( x e. RR -> ( x - A ) e. RR )
  64. 16cb:15f,16ca:syl |- ( x e. ( A [,] B ) -> ( x - A ) e. RR )
  65. 17::ltne |- ( ( A e. RR /\ A < B ) -> B =/= A )
  66. 18:10a,11a,17:mp2an |- B =/= A
  67. d2:10bc:a1i |- ( A e. RR -> B e. CC )
  68. d3:10ac:a1i |- ( A e. RR -> A e. CC )
  69. d4:18:a1i |- ( A e. RR -> B =/= A )
  70. 23:d2,d3,d4:subne0d |- ( A e. RR -> ( B - A ) =/= 0 )
  71. 24:10a,23:ax-mp |- ( B - A ) =/= 0
  72. 25::redivcl |- ( ( ( x - A ) e. RR /\ ( B - A ) e. RR /\ ( B - A ) =/= 0 ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  73. 26a:16:a1i |- ( x e. RR -> ( B - A ) e. RR )
  74. 26aa:15f,26a:syl |- ( x e. ( A [,] B ) -> ( B - A ) e. RR )
  75. 26b:24:a1i |- ( x e. RR -> ( B - A ) =/= 0 )
  76. 26c:10c:a1i |- ( x e. RR -> C e. RR )
  77. 26e:10e:a1i |- ( x e. RR -> E e. RR )
  78. 26d:10d:a1i |- ( x e. RR -> D e. RR )
  79. 26f:10f:a1i |- ( x e. RR -> F e. RR )
  80. 27:16ca,26a,26b,25:syl3anc |- ( x e. RR -> ( ( x - A ) / ( B - A ) ) e. RR )
  81. 27a:15f,27:syl |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  82. 27ab:27:recnd |- ( x e. RR -> ( ( x - A ) / ( B - A ) ) e. CC )
  83. 27b:27a:recnd |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. CC )
  84. 28::resubcl |- ( ( 1 e. RR /\ ( ( x - A ) / ( B - A ) ) e. RR ) -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
  85. 29:28a,27,28:syl2anc |- ( x e. RR -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
  86. 29c:29:recnd |- ( x e. RR -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. CC )
  87. 30c:26c,29:remulcld |- ( x e. RR -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  88. 30ca:30c:recnd |- ( x e. RR -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. CC )
  89. 30e:26e,29:remulcld |- ( x e. RR -> ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  90. 30d:26d,27:remulcld |- ( x e. RR -> ( D x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  91. 30f:26f,27:remulcld |- ( x e. RR -> ( F x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  92. *convert U and V to a form suited to inequalities
  93. 12aa::subdi |- ( ( ( ( x - A ) / ( B - A ) ) e. CC /\ D e. CC /\ C e. CC )
  94. -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  95. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  96. 12ab:27ab,10de,10ce,12aa:syl3anc |- ( x e. RR
  97. -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) )
  98. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  99. 12ac:12ab:oveq2d |- ( x e. RR
  100. -> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
  101. = ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  102. 12ad:12a,12ac:syl5eq |- ( x e. RR -> U
  103. = ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  104. 12ae::addsub12 |- ( ( C e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. D ) e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. C ) e. CC )
  105. -> ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  106. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  107. 12af:27ab,10de:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. D ) e. CC )
  108. 12ag:27ab,10ce:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. C ) e. CC )
  109. 12ah:10ce,12af,12ag,12ae:syl3anc |- ( x e. RR
  110. -> ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  111. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  112. 12ai:12ad,12ah:eqtrd |- ( x e. RR -> U = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  113. 12ak:10cc:mulid2i |- ( 1 x. C ) = C
  114. 12al::oveq1 |- ( ( 1 x. C ) = C -> ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  115. 12am:12ak,12al:ax-mp |- ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) )
  116. 12an::subdir |- ( ( 1 e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC /\ C e. CC )
  117. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  118. 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 ) ) )
  119. 12ap:12ao,12am:syl6eq |- ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
  120. 12aq:12ap:oveq2d |- ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) )
  121. = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
  122. 12ar:12ai,12aq:eqtr4d |- ( x e. RR -> U = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) ) )
  123. 12as::addcomgi |- ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) )
  124. = ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) )
  125. 12au:12ar,12as:syl6eq |- ( x e. RR -> U =
  126. ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) ) )
  127. 12av:29c,10ce:mulcomd |- ( x e. RR
  128. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  129. 12aw:27ab,10de:mulcomd |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. D ) = ( D x. ( ( x - A ) / ( B - A ) ) ) )
  130. 12ax:12av,12aw:oveq12d |- ( x e. RR -> ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) )
  131. = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
  132. 12ay:12au,12ax:eqtrd |- ( x e. RR -> U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
  133. 12az:15f,12ay:syl |- ( x e. ( A [,] B ) -> U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
  134.  
  135. 12ba::subdi |- ( ( ( ( x - A ) / ( B - A ) ) e. CC /\ F e. CC /\ E e. CC )
  136. -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  137. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  138. 12bb:27ab,10fe,10ee,12ba:syl3anc |- ( x e. RR
  139. -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) )
  140. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  141. 12bc:12bb:oveq2d |- ( x e. RR
  142. -> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
  143. = ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  144. 12bd:12b,12bc:syl5eq |- ( x e. RR -> V
  145. = ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  146. 12be::addsub12 |- ( ( E e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. F ) e. CC /\ ( ( ( x - A ) / ( B - A ) ) x. E ) e. CC )
  147. -> ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  148. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  149. 12bf:27ab,10fe:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. F ) e. CC )
  150. 12bg:27ab,10ee:mulcld |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. E ) e. CC )
  151. 12bh:10ee,12bf,12bg,12be:syl3anc |- ( x e. RR
  152. -> ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  153. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  154. 12bi:12bd,12bh:eqtrd |- ( x e. RR -> V = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  155. 12bk:10ec:mulid2i |- ( 1 x. E ) = E
  156. 12bl::oveq1 |- ( ( 1 x. E ) = E -> ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) )
  157. = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  158. 12bm:12bk,12bl:ax-mp |- ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) )
  159. 12bn::subdir |- ( ( 1 e. CC /\ ( ( x - A ) / ( B - A ) ) e. CC /\ E e. CC )
  160. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  161. 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 ) ) )
  162. 12bp:12bo,12bm:syl6eq |- ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
  163. 12bq:12bp:oveq2d |- ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) )
  164. = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
  165. 12br:12bi,12bq:eqtr4d |- ( x e. RR -> V = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) ) )
  166. 12bs::addcomgi |- ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) )
  167. = ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) )
  168. 12bu:12br,12bs:syl6eq |- ( x e. RR -> V =
  169. ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) ) )
  170. 12bv:29c,10ee:mulcomd |- ( x e. RR
  171. -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  172. 12bw:27ab,10fe:mulcomd |- ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. F ) = ( F x. ( ( x - A ) / ( B - A ) ) ) )
  173. 12bx:12bv,12bw:oveq12d |- ( x e. RR -> ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) )
  174. = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  175. 12by:12bu,12bx:eqtrd |- ( x e. RR -> V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  176. 12bz:15f,12by:syl |- ( x e. ( A [,] B ) -> V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  177. *now get U,V in RR
  178. 31v:30e,30f:readdcld |- ( x e. RR -> ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  179. 31u:30c,30d:readdcld |- ( x e. RR -> ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  180. 36:12ay,31u:eqeltrd |- ( x e. RR -> U e. RR )
  181. 37:12by,31v:eqeltrd |- ( x e. RR -> V e. RR )
  182. 36b:15f,36:syl |- ( x e. ( A [,] B ) -> U e. RR )
  183. 36c:15f,37:syl |- ( x e. ( A [,] B ) -> V e. RR )
  184. 36d:36b,36c:jca |- ( x e. ( A [,] B ) -> ( U e. RR /\ V e. RR ) )
  185. 37a:36,37:jca |- ( x e. RR -> ( U e. RR /\ V e. RR ) )
  186. 37aa:37,36:jca |- ( x e. RR -> ( V e. RR /\ U e. RR ) )
  187. 37e::resubcl |- ( ( V e. RR /\ U e. RR ) -> ( V - U ) e. RR )
  188. 37f:37aa,37e:syl |- ( x e. RR -> ( V - U ) e. RR )
  189. 37fb:36c,36b:resubcld |- ( x e. ( A [,] B ) -> ( V - U ) e. RR )
  190. 37g:37f:recnd |- ( x e. RR -> ( V - U ) e. CC )
  191. 38::iccssre |- ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) C_ RR )
  192. 39:36,37,38:syl2anc |- ( x e. RR -> ( U [,] V ) C_ RR )
  193. *prove U <_V in ( A [,] B )
  194. *first get both 1 - ( ( x - A ) / ( B - A ) ) >_ 0, then 0 <_ ( ( x - A ) / ( B - A ) )
  195. 40a::iccleub |- ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> x <_ B )
  196. 40b:10ae,10be,40a:mp3an12 |- ( x e. ( A [,] B ) -> x <_ B )
  197. d11:10b:a1i |- ( x e. ( A [,] B ) -> B e. RR )
  198. d12:10a:a1i |- ( x e. ( A [,] B ) -> A e. RR )
  199. 40c:15f,d11,d12:lesub1d |- ( x e. ( A [,] B ) -> ( x <_ B <-> ( x - A ) <_ ( B - A ) ) )
  200. 40e:40b,40c:mpbid |- ( x e. ( A [,] B ) -> ( x - A ) <_ ( B - A ) )
  201. 40f:d12,d11,d12:ltsub1d |- ( x e. ( A [,] B ) -> ( A < B <-> ( A - A ) < ( B - A ) ) )
  202. 40g:11a,40f:mpbii |- ( x e. ( A [,] B ) -> ( A - A ) < ( B - A ) )
  203. 40h::subid |- ( A e. CC -> ( A - A ) = 0 )
  204. 40i:10ac,40h:ax-mp |- ( A - A ) = 0
  205. 40j:40i,40g:syl5eqbrr |- ( x e. ( A [,] B ) -> 0 < ( B - A ) )
  206. 40k:26aa,40j:jca |- ( x e. ( A [,] B ) -> ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
  207. 40l::lediv1 |- ( ( ( x - A ) e. RR /\ ( B - A ) e. RR /\ ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
  208. -> ( ( x - A ) <_ ( B - A ) <-> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) ) )
  209. 40m:16cb,26aa,40k,40l:syl3anc |- ( x e. ( A [,] B )
  210. -> ( ( x - A ) <_ ( B - A ) <-> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) ) )
  211. 40n:40e,40m:mpbid |- ( x e. ( A [,] B )
  212. -> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) )
  213. 40o:16a,24:dividi |- ( ( B - A ) / ( B - A ) ) = 1
  214. 40p:40n,40o:syl6breq |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) <_ 1 )
  215. d13:15f,27:syl |- ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. RR )
  216. d14:15f,28a:syl |- ( x e. ( A [,] B ) -> 1 e. RR )
  217. 40q:d13,d14,d13:lesub1d |- ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) <_ 1
  218. <-> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  219. 40r:40p,40q:mpbid |- ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) )
  220. <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) )
  221. 40s::subid |- ( ( ( x - A ) / ( B - A ) ) e. CC -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) = 0 )
  222. 40t:27b,40s:syl |- ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) = 0 )
  223. 40u:40t,40r:eqbrtrrd |- ( x e. ( A [,] B ) -> 0 <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) )
  224. *not get 0 <_ ( ( x - A ) / ( B - A ) )
  225. 41::elicc1 |- ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ x /\ x <_ B ) ) )
  226. 41a::simp2 |- ( ( x e. RR* /\ A <_ x /\ x <_ B ) -> A <_ x )
  227. 41b:41,41a:syl6bi |- ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,] B ) -> A <_ x ) )
  228. 41c:41b:3impia |- ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> A <_ x )
  229. 41d:10ae,10be,41c:mp3an12 |- ( x e. ( A [,] B ) -> A <_ x )
  230. 41e:d12,15f,d12:lesub1d |- ( x e. ( A [,] B ) -> ( A <_ x <-> ( A - A ) <_ ( x - A ) ) )
  231. 41f::subid |- ( A e. CC -> ( A - A ) = 0 )
  232. 41g:10ac,41f:ax-mp |- ( A - A ) = 0
  233. 41h:41d,41e:mpbid |- ( x e. ( A [,] B ) -> ( A - A ) <_ ( x - A ) )
  234. 41i:41g,41h:syl5eqbrr |- ( x e. ( A [,] B ) -> 0 <_ ( x - A ) )
  235. 41j::lediv1 |- ( ( 0 e. RR /\ ( x - A ) e. RR /\ ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
  236. -> ( 0 <_ ( x - A ) <-> ( 0 / ( B - A ) ) <_ ( ( x - A ) / ( B - A ) ) ) )
  237. 41k:206,16cb,40k,41j:eel011 |- ( x e. ( A [,] B ) -> ( 0 <_ ( x - A ) <-> ( 0 / ( B - A ) ) <_ ( ( x - A ) / ( B - A ) ) ) )
  238. 41l:41i,41k:mpbid |- ( x e. ( A [,] B ) -> ( 0 / ( B - A ) ) <_ ( ( x - A ) / ( B - A ) ) )
  239. 41m::diveq0 |- ( ( 0 e. CC /\ ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( ( 0 / ( B - A ) ) = 0 <-> 0 = 0 ) )
  240. 41n:206ccc,16a,24,41m:mp3an |- ( ( 0 / ( B - A ) ) = 0 <-> 0 = 0 )
  241. 41o::eqid |- 0 = 0
  242. 41p:41o,41n:mpbir |- ( 0 / ( B - A ) ) = 0
  243. 41q:41p,41l:syl5eqbrr |- ( x e. ( A [,] B ) -> 0 <_ ( ( x - A ) / ( B - A ) ) )
  244. *now establish the inequalities
  245. d5:10c:a1i |- ( x e. ( A [,] B ) -> C e. RR )
  246. d6:10e:a1i |- ( x e. ( A [,] B ) -> E e. RR )
  247. d7:15f,29:syl |- ( x e. ( A [,] B ) -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
  248. d9:11b:a1i |- ( x e. ( A [,] B ) -> C <_ E )
  249. 42:d5,d6,d7,40u,d9:lemul1ad
  250. |- ( x e. ( A [,] B ) -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) <_ ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
  251. d15:10d:a1i |- ( x e. ( A [,] B ) -> D e. RR )
  252. d16:10f:a1i |- ( x e. ( A [,] B ) -> F e. RR )
  253. d19:11c:a1i |- ( x e. ( A [,] B ) -> D <_ F )
  254. 43:d15,d16,27a,41q,d19:lemul1ad
  255. |- ( x e. ( A [,] B ) -> ( D x. ( ( x - A ) / ( B - A ) ) ) <_ ( F x. ( ( x - A ) / ( B - A ) ) ) )
  256. d20:15f,30c:syl |- ( x e. ( A [,] B ) -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  257. d21:15f,30d:syl |- ( x e. ( A [,] B ) -> ( D x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  258. d22:15f,30e:syl |- ( x e. ( A [,] B ) -> ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
  259. d23:15f,30f:syl |- ( x e. ( A [,] B ) -> ( F x. ( ( x - A ) / ( B - A ) ) ) e. RR )
  260. 44:d20,d21,d22,d23,42,43:le2addd
  261. |- ( x e. ( A [,] B ) -> ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) )
  262. <_ ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
  263. 45:44,12az,12bz:3brtr4d |- ( x e. ( A [,] B ) -> U <_ V )
  264. 46:36b,36c,45:3jca |- ( x e. ( A [,] B ) -> ( U e. RR /\ V e. RR /\ U <_ V ) )
  265. *you did it :) **
  266.  
  267. 50a::iftrue |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) = ( U [,] V ) )
  268. 50b::iffalse |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) = (/) )
  269. *compute the image of S
  270. 51::vex |- x e. _V
  271. 52::vex |- y e. _V
  272. 53:51,52:elimasn |- ( y e. ( S " { x } ) <-> <. x , y >. e. S )
  273. 54::nfopab2 |- F/_ y { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
  274. 55:13,54:nfcxfr |- F/_ y S
  275. 56::nfcv |- F/_ y { x }
  276. 57:55,56:nfima |- F/_ y ( S " { x } )
  277. 58::nfcv |- F/_ y ( U [,] V )
  278. 59::nfv |- F/ y x e. ( A [,] B )
  279. 60a:13:eleq2i |- ( <. x , y >. e. S <-> <. x , y >. e. { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } )
  280. 60b::opabid |- ( <. x , y >. e. { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
  281. 60ba:60a,60b:bitri |- ( <. x , y >. e. S <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
  282. 60c:53,60a,60b:3bitri |- ( y e. ( S " { x } ) <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
  283. 60d:60c:baib |- ( x e. ( A [,] B ) -> ( y e. ( S " { x } ) <-> y e. ( U [,] V ) ) )
  284. 60e:59,57,58,60d:eqrd |- ( x e. ( A [,] B ) -> ( S " { x } ) = ( U [,] V ) )
  285. 60f:59:nfn |- F/ y -. x e. ( A [,] B )
  286. 60g::nfcv |- F/_ y (/)
  287. 60h:60c:simplbi |- ( y e. ( S " { x } ) -> x e. ( A [,] B ) )
  288. 60i::noel |- -. y e. (/)
  289. 60j:60i:pm2.21i |- ( y e. (/) -> x e. ( A [,] B ) )
  290. 60k:60h,60j:pm5.21ni |- ( -. x e. ( A [,] B ) -> ( y e. ( S " { x } ) <-> y e. (/) ) )
  291. 60l:60f,57,60g,60k:eqrd |- ( -. x e. ( A [,] B ) -> ( S " { x } ) = (/) )
  292. 60m:60e,50a:eqtr4d |- ( x e. ( A [,] B ) -> ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
  293. 60n:60l,50b:eqtr4d |- ( -. x e. ( A [,] B ) -> ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
  294. *work with the image of S at x and find it's integral
  295. 60:60m,60n:pm2.61i |- ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) )
  296. 61:60:fveq2i |- ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
  297. 62:61:a1i |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) )
  298. 63:61:a1i |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) )
  299. 64:50a:fveq2d |- ( x e. ( A [,] B )
  300. -> ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) = ( vol ` ( U [,] V ) ) )
  301. 65:50b:fveq2d |- ( -. x e. ( A [,] B )
  302. -> ( vol ` if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) ) = ( vol ` (/) ) )
  303. 66:62,64:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` ( U [,] V ) ) )
  304. 67:63,65:eqtrd |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` (/) ) )
  305.  
  306.  
  307. *part 1 of the conditions of dmarea prove S subset R2
  308. 70c:15f,39:syl |- ( x e. ( A [,] B ) -> ( U [,] V ) C_ RR )
  309. 71::dfss3 |- ( ( U [,] V ) C_ RR <-> A. y e. ( U [,] V ) y e. RR )
  310. 71a:70c,71:sylib |- ( x e. ( A [,] B ) -> A. y e. ( U [,] V ) y e. RR )
  311. 71b::rsp |- ( A. y e. ( U [,] V ) y e. RR -> ( y e. ( U [,] V ) -> y e. RR ) )
  312. 71c:71a,71b:syl |- ( x e. ( A [,] B ) -> ( y e. ( U [,] V ) -> y e. RR ) )
  313. 72:15f:adantr |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> x e. RR )
  314. 72a:71c:imp |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> y e. RR )
  315. 72b:72,72a:jca |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> ( x e. RR /\ y e. RR ) )
  316. 73::opelxpi |- ( ( x e. RR /\ y e. RR ) -> <. x , y >. e. ( RR X. RR ) )
  317. 73b:72b,73:syl |- ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> <. x , y >. e. ( RR X. RR ) )
  318. 73c:60ba,73b:sylbi |- ( <. x , y >. e. S -> <. x , y >. e. ( RR X. RR ) )
  319. 73cb:73c:rgenw |- A. t e. S ( <. x , y >. e. S -> <. x , y >. e. ( RR X. RR ) )
  320. 73e::dfss2 |- ( S C_ ( RR X. RR ) <-> A. &S1 ( &S1 e. S -> &S1 e. ( RR X. RR ) ) )
  321. 74:73e,73cb: |- S C_ ( RR X. RR )
  322.  
  323. *part 2 of the conditions of dmarea prove A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  324. 100::iccmbl |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )
  325. 101:10a,10b,100:mp2an |- ( A [,] B ) e. dom vol
  326. 102::iccmbl |- ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) e. dom vol )
  327. 104:36d,102:syl |- ( x e. ( A [,] B ) -> ( U [,] V ) e. dom vol )
  328. 104a:37a,102:syl |- ( x e. RR -> ( U [,] V ) e. dom vol )
  329. 105::0mbl |- (/) e. dom vol
  330. 106:105:a1i |- ( x e. RR -> (/) e. dom vol )
  331. 107:104a,106:jca |- ( x e. RR -> ( ( U [,] V ) e. dom vol /\ (/) e. dom vol ) )
  332. 108::ifcl |- ( ( ( U [,] V ) e. dom vol /\ (/) e. dom vol )
  333. -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
  334. 109:107,108:syl |- ( x e. RR -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
  335. 110:60,109:syl5eqel |- ( x e. RR -> ( S " { x } ) e. dom vol )
  336. *jump to 200 for the completion of this part
  337.  
  338. *compute vols
  339. 168::ovolicc |- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
  340. 168a::ovolicc |- ( ( U e. RR /\ V e. RR /\ U <_ V ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
  341. 169:10a,10b,11ad,168:mp3an |- ( vol* ` ( A [,] B ) ) = ( B - A )
  342. 169a:46,168a:syl |- ( x e. ( A [,] B ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
  343. 170::mblvol |- ( ( A [,] B ) e. dom vol -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
  344. 170a::mblvol |- ( ( U [,] V ) e. dom vol -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
  345. 171:101,170:ax-mp |- ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) )
  346. 171a:104,170a:syl |- ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
  347. 172:171,169:eqtri |- ( vol ` ( A [,] B ) ) = ( B - A )
  348. 172a:171a,169a:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( V - U ) )
  349. 178::ssel2 |- ( ( ( A [,] B ) C_ RR /\ x e. ( A [,] B ) ) -> x e. RR )
  350. 181::ovol0 |- ( vol* ` (/) ) = 0
  351. 182::mblvol |- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
  352. 183:105,182:ax-mp |- ( vol ` (/) ) = ( vol* ` (/) )
  353. 184:183,181:eqtri |- ( vol ` (/) ) = 0
  354. 185:184:a1i |- ( -. x e. ( A [,] B ) -> ( vol ` (/) ) = 0 )
  355. *apply these to S
  356. 186:66,172a:eqtrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( V - U ) )
  357. 188:186,37fb:eqeltrd |- ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) e. RR )
  358. 189:67,184:syl6eq |- ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = 0 )
  359. 190::iftrue |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( V - U ) )
  360. 191::iffalse |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = 0 )
  361. 192:190,186:eqtr4d |- ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
  362. 192a:191,189:eqtr4d |- ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
  363. 193:192,192a:pm2.61i |- if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) )
  364. 194:193:eqcomi |- ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  365. 195:194:a1i |- ( x e. RR -> ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 ) )
  366. 196:195:rgen |- A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  367. 197::itgeq2 |- ( A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
  368. -> S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
  369. 198:196,197:ax-mp |- S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
  370.  
  371. *continue with part 2 of conditions of dmarea
  372. 200::fvimacnv |- ( ( Fun vol /\ ( S " { x } ) e. dom vol ) -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  373. 201::volf |- vol : dom vol --> ( 0 [,] +oo )
  374. 202::ffun |- ( vol : dom vol --> ( 0 [,] +oo ) -> Fun vol )
  375. 203:201,202:ax-mp |- Fun vol
  376. 203a:110,203:jctil |- ( x e. RR -> ( Fun vol /\ ( S " { x } ) e. dom vol ) )
  377. 204:203a,200:syl |- ( x e. RR -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  378. 205::ifcl |- ( ( ( V - U ) e. RR /\ 0 e. RR ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
  379. 206a:37f,206:jctir |- ( x e. RR -> ( ( V - U ) e. RR /\ 0 e. RR ) )
  380. 207:206a,205:syl |- ( x e. RR -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
  381. 208:195,207:eqeltrd |- ( x e. RR -> ( vol ` ( S " { x } ) ) e. RR )
  382. 209:208,204:mpbid |- ( x e. RR -> ( S " { x } ) e. ( `' vol " RR ) )
  383. 210:209:rgen |- A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  384.  
  385. *part 3 of the conditions of dmarea, prove L1
  386. 220:15:a1i |- ( 0 e. RR -> ( A [,] B ) C_ RR )
  387. 221::rembl |- RR e. dom vol
  388. 222:221:a1i |- ( 0 e. RR -> RR e. dom vol )
  389. 223:188:adantl |- ( ( 0 e. RR /\ x e. ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) e. RR )
  390. 224::eldifn |- ( x e. ( RR \ ( A [,] B ) ) -> -. x e. ( A [,] B ) )
  391. 225:224,189:syl |- ( x e. ( RR \ ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  392. 226:225:adantl |- ( ( 0 e. RR /\ x e. ( RR \ ( A [,] B ) ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  393.  
  394. 227::cncfmptc |- ( ( ( V - U ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  395. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  396. 228::ssid |- CC C_ CC
  397. 228a:228:a1i |- ( x e. RR -> CC C_ CC )
  398. 228b:37g,15c,228a:3jca |- ( x e. RR -> ( ( V - U ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) )
  399. 229:228b,227:syl |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  400. 230::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
  401. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  402. 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 ) ) )
  403. 232:231,230:syl |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
  404. 233:186:mpteq2ia |- ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) = ( x e. ( A [,] B ) |-> ( V - U ) )
  405. 234:233,232:syl5eqel |- ( x e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  406. 234a:15f,234:syl |- ( x e. ( A [,] B ) -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  407. 234b:234a: |- ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
  408. 235:234: |- ( 0 e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  409. 236:220,222,223,226,235:iblss2
  410. |- ( 0 e. RR -> ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  411. 237:206,236:ax-mp |- ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1
  412.  
  413. *combine facts to get the result
  414. 997:74,210,237:3pm3.2i |- ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  415. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  416. 998:997,dmarea:mpbir |- S e. dom area
  417. 999:998,areaval:ax-mp |- ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x
  418. 1000:999: |- ( area ` S ) = A
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!