API tools faq
paste
Advertisement
FrequentPaster

intx^ndraft2

FrequentPaster
Apr 6th, 2019
115
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 13.50 KB | None | 0 0
raw download clone embed print report
  1. $( <MM> <PROOF_ASST> THEOREM=itexp LOC_AFTER=?
  2.  
  3. *
  4. The integral of an exponent on the real line.
  5.  
  6.  
  7. h1::itexp.1 |- A e. RR
  8. h2::itexp.2 |- B e. RR
  9. h3::itexp.3 |- A <_ B
  10. h4::itexp.4 |- N e. NN
  11.  
  12. *9:: |- N e. NN
  13. 9a::nnaddcl |- ( ( N e. NN /\ 1 e. NN ) -> ( N + 1 ) e. NN )
  14. 9b::1nn |- 1 e. NN
  15. 9ba::ax1cn |- 1 e. CC
  16. 9c:4,9b,9a:mp2an |- ( N + 1 ) e. NN
  17. 9ca:9c:nnne0i |- ( N + 1 ) =/= 0
  18. 9d:4:nnrei |- N e. RR
  19. 9e:9d:recni |- N e. CC
  20. 9f:4:nnnn0i |- N e. NN0
  21. 9g:9c:nnnn0i |- ( N + 1 ) e. NN0
  22. 9h:9g:nn0cni |- ( N + 1 ) e. CC
  23. *11:: |- A e. RR
  24. 11a:1:recni |- A e. CC
  25. 11b::expcl |- ( ( A e. CC /\ ( N + 1 ) e. NN0 ) -> ( A ^ ( N + 1 ) ) e. CC )
  26. 11c:11a,9g,11b:mp2an |- ( A ^ ( N + 1 ) ) e. CC
  27. *12:: |- B e. RR
  28. 12a:2:recni |- B e. CC
  29. 12b::expcl |- ( ( B e. CC /\ ( N + 1 ) e. NN0 ) -> ( B ^ ( N + 1 ) ) e. CC )
  30. 12c:12a,9g,12b:mp2an |- ( B ^ ( N + 1 ) ) e. CC
  31. *13:: |- A <_ B
  32. *14:: |- ph
  33. 15::tru |- T.
  34.  
  35. *get the derivative of x^N+1
  36. 100::dvexp |- ( ( N + 1 ) e. NN -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  37. = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
  38. 101:9c,100:ax-mp |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  39. = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) )
  40. 103:9e,9ba:pncan3oi |- ( ( N + 1 ) - 1 ) = N
  41. 104:103:oveq2i |- ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N )
  42. *105:104,10:eqtr4i |- ( t ^ ( ( N + 1 ) - 1 ) ) = F
  43. 106:104:oveq2i |- ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) )
  44. 107:106:mpteq2i |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  45. 108:101,107:eqtri |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  46. 108a:108:reseq1i |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  47.  
  48. *conditions for restriction
  49. 110::reelprrecn |- RR e. { RR , CC }
  50. 111::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
  51. 111a::ioossre |- ( A (,) B ) C_ RR
  52. 112:1,2,111:mp2an |- ( A [,] B ) C_ RR
  53. 113::axresscn |- RR C_ CC
  54. 114:112,113:sstri |- ( A [,] B ) C_ CC
  55. 114a:111a,113:sstri |- ( A (,) B ) C_ CC
  56. 115::expcl |- ( ( t e. CC /\ N e. NN0 ) -> ( t ^ N ) e. CC )
  57. 115x::expcl |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
  58. 115a::expcl |- ( ( t e. CC /\ ( N + 1 ) e. NN0 ) -> ( t ^ ( N + 1 ) ) e. CC )
  59. 116:9f,115:mpan2 |- ( t e. CC -> ( t ^ N ) e. CC )
  60. 116n::mulcl |- ( ( ( N + 1 ) e. CC /\ ( t ^ N ) e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  61. 116na:9h,116,116n:sylancr |- ( t e. CC -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  62. 116x:9f,115x:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  63. 116a:9g,115a:mpan2 |- ( t e. CC -> ( t ^ ( N + 1 ) ) e. CC )
  64. 118:114:sseli |- ( t e. ( A [,] B ) -> t e. CC )
  65. 118xa:114:sseli |- ( x e. ( A [,] B ) -> x e. CC )
  66. 118xb:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  67. 119:118,116:syl |- ( t e. ( A [,] B ) -> ( t ^ N ) e. CC )
  68. 119xa:118xa,116x:syl |- ( x e. ( A [,] B ) -> ( x ^ N ) e. CC )
  69. 119xb:118xb,116x:syl |- ( x e. ( A (,) B ) -> ( x ^ N ) e. CC )
  70. 119a:118,116a:syl |- ( t e. ( A [,] B ) -> ( t ^ ( N + 1 ) ) e. CC )
  71. d42::eqid |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) = ( t e. CC |-> ( t ^ ( N + 1 ) ) )
  72. 120:d42,116a:fmpti |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC
  73. d43::eqid |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  74. 120a:d43,116na:fmpti |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC
  75. 120b:108:feq1i |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  76. <-> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC )
  77. 121:120a,120b:mpbir |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  78. 130::ssid |- CC C_ CC
  79. 155c::fdm |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  80. -> dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC )
  81. 156:121,155c:ax-mp |- dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC
  82. 157:113,156:sseqtr4i |- RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  83. 158:130,157:pm3.2i |- ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) )
  84. 158a:110,120:pm3.2i |- ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  85. *restrict this function to the reals
  86. 170::dvres3 |- ( ( ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  87. /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) ) )
  88. -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  89. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) )
  90. 171:158a,158,170:mp2an |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  91. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR )
  92. 172:171,108a:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  93. = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  94. 173a::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  95. = ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  96. 173b:113,173a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  97. = ( t e. RR |-> ( t ^ ( N + 1 ) ) )
  98. 173c::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  99. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  100. 173d:113,173c:ax-mp |- ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  101. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  102. 174:172,173d:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  103. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  104. 175:173b:oveq2i |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  105. 176:175,174:eqtr3i |- ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  106. *we have the real derivative of x^( N + 1 ) :), almost
  107.  
  108. *prove some continuity resutls
  109. 200::expcncf |- ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
  110. 201::rescncf |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  111. -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
  112. 202::resmpt |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) )
  113. = ( t e. ( A (,) B ) |-> ( t ^ N ) ) )
  114. 210:9f,200:ax-mp |- ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  115. 211:114a,201:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  116. -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
  117. 212:114a,202:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( t ^ N ) )
  118. 220:210,211:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC )
  119. 230:212,220:eqeltrri |- ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. ( ( A (,) B ) -cn-> CC )
  120. d44::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
  121. 230a:d44:mulcn |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
  122. d45:230a:a1i |- ( T. -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
  123. 230b::cncfmptc |- ( ( ( N + 1 ) e. CC /\ ( A (,) B ) C_ CC /\ CC C_ CC )
  124. -> ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC ) )
  125. 230c:9h,114a,130,230b:mp3an |- ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC )
  126. d46:230c:a1i |- ( T. -> ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC ) )
  127. d47:230:a1i |- ( T. -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. ( ( A (,) B ) -cn-> CC ) )
  128. 231:d44,d45,d46,d47:cncfmpt2f
  129. |- ( T. -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  130. 231a:15,231:ax-mp |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC )
  131. *ftc
  132. d18:1:a1i |- ( T. -> A e. RR )
  133. d19:2:a1i |- ( T. -> B e. RR )
  134. d20:3:a1i |- ( T. -> A <_ B )
  135. !d21:: |- ( T. -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  136. !d22:: |- ( T. -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  137. !d23:: |- ( T. -> ( t e. RR |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  138. 250:d18,d19,d20,d21,d22,d23:ftc2
  139. |- ( T. -> S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  140. = ( ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
  141. 250a:15,250:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  142. = ( ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  143. *substitute into result
  144. d24::oveq1 |- ( t = B -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
  145. d25::eqid |- ( t e. RR |-> ( t ^ ( N + 1 ) ) ) = ( t e. RR |-> ( t ^ ( N + 1 ) ) )
  146. 251:d24,d25:fvmptg |- ( ( B e. RR /\ ( B ^ ( N + 1 ) ) e. CC )
  147. -> ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
  148. 251a:2,12c,251:mp2an |- ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) )
  149. d26::oveq1 |- ( t = A -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
  150. 252:d26,d25:fvmptg |- ( ( A e. RR /\ ( A ^ ( N + 1 ) ) e. CC )
  151. -> ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
  152. 252a:1,11c,252:mp2an |- ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) )
  153. 253:251a,252a:oveq12i |- ( ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  154. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  155. 254:250a,253:eqtri |- S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  156. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  157. *sub in for RR _D x^( N + 1 )
  158. 255:176:fveq1i |- ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  159. = ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  160. 255a:255:rgenw |- A. x e. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  161. = ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  162. 256::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  163. = ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  164. -> S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  165. = S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x )
  166. 257:255a,256:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  167. = S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  168. 258:257,254:eqtr3i |- S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  169. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  170. *get rid of evaluated at
  171.  
  172.  
  173. d32::oveq1 |- ( t = x -> ( t ^ N ) = ( x ^ N ) )
  174. d30:d32:oveq2d |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  175. d31::eqid |- ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  176. 259:d30,d31:fvmptg |- ( ( x e. RR /\ ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  177. -> ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  178.  
  179. 260a::expcl |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
  180. 260b:9f,260a:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  181. 260c::mulcl |- ( ( ( N + 1 ) e. CC /\ ( x ^ N ) e. CC ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  182. 260d:9h,260b,260c:sylancr |- ( x e. CC -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  183. 260e:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  184. 260ea:111a:sseli |- ( x e. ( A (,) B ) -> x e. RR )
  185. 260f:260e,260d:syl |- ( x e. ( A (,) B ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  186. 261:260ea,260f,259:syl2anc |- ( x e. ( A (,) B ) -> ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  187. = ( ( N + 1 ) x. ( x ^ N ) ) )
  188. 262:261:rgen |- A. x e. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  189. = ( ( N + 1 ) x. ( x ^ N ) )
  190.  
  191.  
  192. 270::itgeq2 |- ( A. x e. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  193. = ( ( N + 1 ) x. ( x ^ N ) )
  194. -> S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  195. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  196. 271:262,270:ax-mp |- S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  197. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  198. 272:271,258:eqtr3i |- S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  199. *get result
  200.  
  201.  
  202. 290::cniccibl |- ( ( &C1 e. RR /\ &C2 e. RR /\ &C3 e. ( ( &C1 [,] &C2 ) -cn-> CC ) ) -> &C3 e. L^1 )
  203. d33:9h:a1i |- ( T. -> ( N + 1 ) e. CC )
  204. d34:119xb:adantl |- ( ( T. /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. CC )
  205. !d35:: |- ( T. -> ( x e. ( A (,) B ) |-> ( x ^ N ) ) e. L^1 )
  206. 300:d33,d34,d35:itgmulc2
  207. |- ( T. -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x )
  208. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  209. 300a:15,300:ax-mp |- ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x )
  210. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  211.  
  212. 301:300a,272:eqtri |- ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  213. d41a:d34,d35:itgcl |- ( T. -> S. ( A (,) B ) ( x ^ N ) _d x e. CC )
  214. d41:15,d41a:ax-mp |- S. ( A (,) B ) ( x ^ N ) _d x e. CC
  215. **RESULT ***~~~###~~~***
  216. 302:9h,d41,9ca,301:mvllmuli
  217. |- S. ( A (,) B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  218. d40:119xa:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
  219. 303:d18,d19,d40:itgioo
  220. |- ( T. -> S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x )
  221. 303a:15,303:ax-mp |- S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x
  222. qed:303a,302:eqtr3i |- S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  223.  
  224. $)
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!