API tools faq
paste
Advertisement
FrequentPaster

intx^ndraft4

FrequentPaster
Apr 9th, 2019
111
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 18.36 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. 7a:1:rexri |- A e. RR*
  13. 7b:2:rexri |- B e. RR*
  14. 8a::lbicc2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
  15. 8aa:7a,7b,3,8a:mp3an |- A e. ( A [,] B )
  16. 8b::ubicc2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
  17. 8ba:7a,7b,3,8b:mp3an |- B e. ( A [,] B )
  18. 8c::ioossicc |- ( A (,) B ) C_ ( A [,] B )
  19. 8ca:8c:sseli |- ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
  20. *9:: |- N e. NN
  21. 9a::nnaddcl |- ( ( N e. NN /\ 1 e. NN ) -> ( N + 1 ) e. NN )
  22. 9b::1nn |- 1 e. NN
  23. 9ba::ax1cn |- 1 e. CC
  24. 9c:4,9b,9a:mp2an |- ( N + 1 ) e. NN
  25. 9ca:9c:nnne0i |- ( N + 1 ) =/= 0
  26. 9d:4:nnrei |- N e. RR
  27. 9e:9d:recni |- N e. CC
  28. 9f:4:nnnn0i |- N e. NN0
  29. 9g:9c:nnnn0i |- ( N + 1 ) e. NN0
  30. 9h:9g:nn0cni |- ( N + 1 ) e. CC
  31. *11:: |- A e. RR
  32. 11a:1:recni |- A e. CC
  33. 11b::expcl |- ( ( A e. CC /\ ( N + 1 ) e. NN0 ) -> ( A ^ ( N + 1 ) ) e. CC )
  34. 11c:11a,9g,11b:mp2an |- ( A ^ ( N + 1 ) ) e. CC
  35. *12:: |- B e. RR
  36. 12a:2:recni |- B e. CC
  37. 12b::expcl |- ( ( B e. CC /\ ( N + 1 ) e. NN0 ) -> ( B ^ ( N + 1 ) ) e. CC )
  38. 12c:12a,9g,12b:mp2an |- ( B ^ ( N + 1 ) ) e. CC
  39. *13:: |- A <_ B
  40. *14:: |- ph
  41. 15::tru |- T.
  42.  
  43. *get the derivative of x^N+1
  44. 100::dvexp |- ( ( N + 1 ) e. NN -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  45. = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
  46. 101:9c,100:ax-mp |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  47. = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) )
  48. 103:9e,9ba:pncan3oi |- ( ( N + 1 ) - 1 ) = N
  49. 104:103:oveq2i |- ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N )
  50. *105:104,10:eqtr4i |- ( t ^ ( ( N + 1 ) - 1 ) ) = F
  51. 106:104:oveq2i |- ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) )
  52. 107:106:mpteq2i |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  53. 108:101,107:eqtri |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  54. 108a:108:reseq1i |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  55.  
  56. *conditions for restriction
  57. 110::reelprrecn |- RR e. { RR , CC }
  58. 111::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
  59. 111a::ioossre |- ( A (,) B ) C_ RR
  60. 112:1,2,111:mp2an |- ( A [,] B ) C_ RR
  61. 113::axresscn |- RR C_ CC
  62. 114:112,113:sstri |- ( A [,] B ) C_ CC
  63. 114a:111a,113:sstri |- ( A (,) B ) C_ CC
  64. 115::expcl |- ( ( t e. CC /\ N e. NN0 ) -> ( t ^ N ) e. CC )
  65. 115x::expcl |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
  66. 115a::expcl |- ( ( t e. CC /\ ( N + 1 ) e. NN0 ) -> ( t ^ ( N + 1 ) ) e. CC )
  67. 116:9f,115:mpan2 |- ( t e. CC -> ( t ^ N ) e. CC )
  68. 116aa:113:sseli |- ( t e. RR -> t e. CC )
  69. 116ab:116aa,116:syl |- ( t e. RR -> ( t ^ N ) e. CC )
  70. 116n::mulcl |- ( ( ( N + 1 ) e. CC /\ ( t ^ N ) e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  71. 116na:9h,116,116n:sylancr |- ( t e. CC -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  72. 116x:9f,115x:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  73. 116a:9g,115a:mpan2 |- ( t e. CC -> ( t ^ ( N + 1 ) ) e. CC )
  74. 116aab:116aa,116a:syl |- ( t e. RR -> ( t ^ ( N + 1 ) ) e. CC )
  75. 118:114:sseli |- ( t e. ( A [,] B ) -> t e. CC )
  76. 118xa:114:sseli |- ( x e. ( A [,] B ) -> x e. CC )
  77. 118xb:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  78. 119:118,116:syl |- ( t e. ( A [,] B ) -> ( t ^ N ) e. CC )
  79. 119xa:118xa,116x:syl |- ( x e. ( A [,] B ) -> ( x ^ N ) e. CC )
  80. 119xb:118xb,116x:syl |- ( x e. ( A (,) B ) -> ( x ^ N ) e. CC )
  81. 119a:118,116a:syl |- ( t e. ( A [,] B ) -> ( t ^ ( N + 1 ) ) e. CC )
  82. d42::eqid |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) = ( t e. CC |-> ( t ^ ( N + 1 ) ) )
  83. 120:d42,116a:fmpti |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC
  84. d43::eqid |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  85. 120a:d43,116na:fmpti |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC
  86. 120b:108:feq1i |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  87. <-> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC )
  88. 121:120a,120b:mpbir |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  89. 130::ssid |- CC C_ CC
  90. 155c::fdm |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  91. -> dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC )
  92. 156:121,155c:ax-mp |- dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC
  93. 157:113,156:sseqtr4i |- RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  94. 158:130,157:pm3.2i |- ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) )
  95. 158a:110,120:pm3.2i |- ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  96. *restrict this function to the reals
  97. 170::dvres3 |- ( ( ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  98. /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) ) )
  99. -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  100. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) )
  101. 171:158a,158,170:mp2an |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  102. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR )
  103. 172:171,108a:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  104. = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  105. 173a::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  106. = ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  107. 173b:113,173a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  108. = ( t e. RR |-> ( t ^ ( N + 1 ) ) )
  109. 173c::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  110. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  111. 173d:113,173c:ax-mp |- ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  112. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  113. 174:172,173d:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  114. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  115. 175:173b:oveq2i |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  116. 176:175,174:eqtr3i |- ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  117. d48:110:a1i |- ( T. -> RR e. { RR , CC } )
  118. d49:116aab:adantl |- ( ( T. /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
  119. d56:9e:a1i |- ( ( T. /\ t e. RR ) -> N e. CC )
  120. d57::1cnd |- ( ( T. /\ t e. RR ) -> 1 e. CC )
  121. d58:d56,d57:addcld
  122. |- ( ( T. /\ t e. RR ) -> ( N + 1 ) e. CC )
  123. d59:116ab:adantl |- ( ( T. /\ t e. RR ) -> ( t ^ N ) e. CC )
  124. d50:d58,d59:mulcld |- ( ( T. /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  125. d51:176:a1i |- ( T. -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  126. d52:112:a1i |- ( T. -> ( A [,] B ) C_ RR )
  127. !d64:: |- &C4 = ( &C5 |`t RR )
  128. !d65:: |- &C5 = ( TopOpen ` CCfld )
  129. !d66:: |- ( T. -> ( A [,] B ) e. &C4 )
  130. 177:d48,d49,d50,d51,d52,d64,d65,d66:dvmptres
  131. |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  132. = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  133. 180:15,177:ax-mp |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  134. = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  135. *we have the real derivative of x^( N + 1 ) :), almost
  136.  
  137. *prove some continuity resutls
  138. *get t^N cts
  139. 200::expcncf |- ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
  140. 201::rescncf |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  141. -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
  142. 202::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) )
  143. = ( t e. ( A [,] B ) |-> ( t ^ N ) ) )
  144. 210:9f,200:ax-mp |- ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  145. 211:114,201:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  146. -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
  147. 212:114,202:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ N ) )
  148. 220:210,211:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
  149. 230:212,220:eqeltrri |- ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC )
  150. *get x^N cts
  151. 200b::expcncf |- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
  152. 201b::rescncf |- ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC )
  153. -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
  154. 202b::resmpt |- ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) )
  155. = ( x e. ( A [,] B ) |-> ( x ^ N ) ) )
  156. 210b:9f,200b:ax-mp |- ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC )
  157. 211b:114,201b:ax-mp |- ( ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC )
  158. -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
  159. 212b:114,202b:ax-mp |- ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x ^ N ) )
  160. 220b:210b,211b:ax-mp |- ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
  161. 230bb:212b,220b:eqeltrri |- ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. ( ( A [,] B ) -cn-> CC )
  162. *get t^N+1 cts
  163. 200a::expcncf |- ( ( N + 1 ) e. NN0 -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
  164. 201a::rescncf |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC )
  165. -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
  166. 202a::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) )
  167. = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  168. 210a:9g,200a:ax-mp |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC )
  169. 211a:114,201a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC )
  170. -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
  171. 212a:114,202a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
  172. 220a:210a,211a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
  173. 230aa:212a,220a:eqeltrri |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC )
  174. *get N+1 x. t^N
  175. d44::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
  176. 230a:d44:mulcn |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
  177. d45:230a:a1i |- ( T. -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
  178. 230b::cncfmptc |- ( ( ( N + 1 ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC )
  179. -> ( t e. ( A [,] B ) |-> ( N + 1 ) ) e. ( ( A [,] B ) -cn-> CC ) )
  180. 230c:9h,114,130,230b:mp3an |- ( t e. ( A [,] B ) |-> ( N + 1 ) ) e. ( ( A [,] B ) -cn-> CC )
  181. d46:230c:a1i |- ( T. -> ( t e. ( A [,] B ) |-> ( N + 1 ) ) e. ( ( A [,] B ) -cn-> CC ) )
  182. d47:230:a1i |- ( T. -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
  183. 231:d44,d45,d46,d47:cncfmpt2f
  184. |- ( T. -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  185. 231a:15,231:ax-mp |- ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC )
  186.  
  187. *conditions for ftc
  188. 240:180,231a:eqeltri |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A [,] B ) -cn-> CC )
  189. 241::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( RR _D ( t e. ( A [,] B )
  190. |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  191. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  192. 241a:1,2,240,241:mp3an |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1
  193. *ftc
  194. d18:1:a1i |- ( T. -> A e. RR )
  195. d19:2:a1i |- ( T. -> B e. RR )
  196. d20:3:a1i |- ( T. -> A <_ B )
  197. !d21:: |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  198. d22:241a:a1i |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  199. d23:230aa:a1i |- ( T. -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  200. 250:d18,d19,d20,d21,d22,d23:ftc2
  201. |- ( T. -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  202. = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
  203. 250a:15,250:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  204. = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  205. *substitute into result
  206. d24::oveq1 |- ( t = B -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
  207. d25::eqid |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
  208. 251:d24,d25:fvmptg |- ( ( B e. ( A [,] B ) /\ ( B ^ ( N + 1 ) ) e. CC )
  209. -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
  210. 251a:8ba,12c,251:mp2an |- ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) )
  211. d26::oveq1 |- ( t = A -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
  212. 252:d26,d25:fvmptg |- ( ( A e. ( A [,] B ) /\ ( A ^ ( N + 1 ) ) e. CC )
  213. -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
  214. 252a:8aa,11c,252:mp2an |- ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) )
  215. 253:251a,252a:oveq12i |- ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  216. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  217. 254:250a,253:eqtri |- S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  218. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  219. *sub in for RR _D x^( N + 1 )
  220. 255:180:fveq1i |- ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  221. = ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  222. 255a:255:rgenw |- A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  223. = ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  224. 256::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  225. = ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  226. -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  227. = S. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x )
  228. 257:255a,256:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  229. = S. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  230. 258:257,254:eqtr3i |- S. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  231. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  232. *get rid of evaluated at
  233.  
  234.  
  235. d32::oveq1 |- ( t = x -> ( t ^ N ) = ( x ^ N ) )
  236. d30:d32:oveq2d |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  237. d31::eqid |- ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  238. = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  239. 259:d30,d31:fvmptg |- ( ( x e. ( A [,] B ) /\ ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  240. -> ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  241.  
  242. 260a::expcl |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
  243. 260b:9f,260a:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  244. 260c::mulcl |- ( ( ( N + 1 ) e. CC /\ ( x ^ N ) e. CC ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  245. 260d:9h,260b,260c:sylancr |- ( x e. CC -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  246. 260e:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  247. 260ea:111a:sseli |- ( x e. ( A (,) B ) -> x e. RR )
  248. 260f:260e,260d:syl |- ( x e. ( A (,) B ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  249. 261:8ca,260f,259:syl2anc |- ( x e. ( A (,) B ) -> ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  250. = ( ( N + 1 ) x. ( x ^ N ) ) )
  251. 262:261:rgen |- A. x e. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  252. = ( ( N + 1 ) x. ( x ^ N ) )
  253.  
  254.  
  255. 270::itgeq2 |- ( A. x e. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  256. = ( ( N + 1 ) x. ( x ^ N ) )
  257. -> S. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  258. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  259. 271:262,270:ax-mp |- S. ( A (,) B ) ( ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  260. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  261. 272:271,258:eqtr3i |- S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  262. *get result
  263.  
  264.  
  265. 281::
  266.  
  267.  
  268. d33:9h:a1i |- ( T. -> ( N + 1 ) e. CC )
  269. d33a::axmulcl |- ( ( ( N + 1 ) e. CC /\ ( x ^ N ) e. CC ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  270. d40:d33,119xa,d33a:syl2an |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  271. 280:d18,d19,d40:itgioo |- ( T. -> S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  272. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  273. 280a:15,280:ax-mp |- S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  274. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  275. 280b:280a,272:eqtr3i |- S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  276.  
  277. d61:119xa:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
  278. 290::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
  279. -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1 )
  280. 290a:1,2,230bb,290:mp3an |- ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1
  281. d62:290a:a1i |- ( T. -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1 )
  282. 300:d33,d61,d62:itgmulc2
  283. |- ( T. -> ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x )
  284. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  285. 300a:15,300:ax-mp |- ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x )
  286. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  287.  
  288. 301:300a,280b:eqtri |- ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  289. d63:119xa:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
  290. d41a:d63,d62:itgcl |- ( T. -> S. ( A [,] B ) ( x ^ N ) _d x e. CC )
  291. d41:15,d41a:ax-mp |- S. ( A [,] B ) ( x ^ N ) _d x e. CC
  292. **RESULT ***~~~###~~~***
  293. 302:9h,d41,9ca,301:mvllmuli
  294. |- S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  295.  
  296.  
  297. qed:302:idi |- S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  298.  
  299. $)
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!