API tools faq
paste
Advertisement
FrequentPaster

intxndraft2

FrequentPaster
Apr 4th, 2019
104
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 11.07 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. 116x:9f,115x:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  61. 116a:9g,115a:mpan2 |- ( t e. CC -> ( t ^ ( N + 1 ) ) e. CC )
  62. 118:114:sseli |- ( t e. ( A [,] B ) -> t e. CC )
  63. 118xa:114:sseli |- ( x e. ( A [,] B ) -> x e. CC )
  64. 118xb:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  65. 119:118,116:syl |- ( t e. ( A [,] B ) -> ( t ^ N ) e. CC )
  66. 119xa:118xa,116x:syl |- ( x e. ( A [,] B ) -> ( x ^ N ) e. CC )
  67. 119xb:118xb,116x:syl |- ( x e. ( A (,) B ) -> ( x ^ N ) e. CC )
  68. 119a:118,116a:syl |- ( t e. ( A [,] B ) -> ( t ^ ( N + 1 ) ) e. CC )
  69. 120:116a: |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC
  70. 120a:: |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC
  71. 120b:108:feq1i |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  72. <-> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC )
  73. 121:120a,120b:mpbir |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  74. 130::ssid |- CC C_ CC
  75. 155c::fdm |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  76. -> dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC )
  77. 156:121,155c:ax-mp |- dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC
  78. 157:113,156:sseqtr4i |- RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  79. 158:130,157:pm3.2i |- ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) )
  80. 158a:110,120:pm3.2i |- ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  81. *restrict this function to the reals
  82. 170::dvres3 |- ( ( ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  83. /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) ) )
  84. -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  85. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) )
  86. 171:158a,158,170:mp2an |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  87. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR )
  88. 172:171,108a:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  89. = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  90. 173a::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  91. = ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  92. 173b:113,173a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  93. = ( t e. RR |-> ( t ^ ( N + 1 ) ) )
  94. 173c::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  95. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  96. 173d:113,173c:ax-mp |- ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  97. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  98. 174:172,173d:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  99. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  100. 175:173b:oveq2i |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  101. 176:175,174:eqtr3i |- ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  102. *we have the real derivative of x^( N + 1 ) :), almost
  103.  
  104.  
  105. *ftc
  106. d18:1:a1i |- ( T. -> A e. RR )
  107. d19:2:a1i |- ( T. -> B e. RR )
  108. d20:3:a1i |- ( T. -> A <_ B )
  109. !d21:: |- ( T. -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  110. !d22:: |- ( T. -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  111. !d23:: |- ( T. -> ( t e. RR |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  112. 250:d18,d19,d20,d21,d22,d23:ftc2
  113. |- ( T. -> S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  114. = ( ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
  115. 250a:15,250:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  116. = ( ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  117. *substitute into result
  118. d24::oveq1 |- ( t = B -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
  119. d25::eqid |- ( t e. RR |-> ( t ^ ( N + 1 ) ) ) = ( t e. RR |-> ( t ^ ( N + 1 ) ) )
  120. 251:d24,d25:fvmptg |- ( ( B e. RR /\ ( B ^ ( N + 1 ) ) e. CC )
  121. -> ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
  122. 251a:2,12c,251:mp2an |- ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) )
  123. d26::oveq1 |- ( t = A -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
  124. 252:d26,d25:fvmptg |- ( ( A e. RR /\ ( A ^ ( N + 1 ) ) e. CC )
  125. -> ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
  126. 252a:1,11c,252:mp2an |- ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) )
  127. 253:251a,252a:oveq12i |- ( ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  128. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  129. 254:250a,253:eqtri |- S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  130. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  131. *sub in for RR _D x^( N + 1 )
  132. 255:176:fveq1i |- ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  133. = ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  134. 255a:255:rgenw |- A. x e. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  135. = ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  136. 256::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  137. = ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  138. -> S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  139. = S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x )
  140. 257:255a,256:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  141. = S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  142. 258:257,254:eqtr3i |- S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  143. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  144. *get rid of evaluated at
  145.  
  146.  
  147. d32::oveq1 |- ( t = x -> ( t ^ N ) = ( x ^ N ) )
  148. d30:d32:oveq2d |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  149. d31::eqid |- ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  150. 259:d30,d31:fvmptg |- ( ( x e. RR /\ ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  151. -> ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  152.  
  153. 260a::expcl |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
  154. 260b:9f,260a:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  155. 260c::mulcl |- ( ( ( N + 1 ) e. CC /\ ( x ^ N ) e. CC ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  156. 260d:9h,260b,260c:sylancr |- ( x e. CC -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  157. 260e:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  158. 260ea:111a:sseli |- ( x e. ( A (,) B ) -> x e. RR )
  159. 260f:260e,260d:syl |- ( x e. ( A (,) B ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  160. 261:260ea,260f,259:syl2anc |- ( x e. ( A (,) B ) -> ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  161. = ( ( N + 1 ) x. ( x ^ N ) ) )
  162. 262:261:rgen |- A. x e. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  163. = ( ( N + 1 ) x. ( x ^ N ) )
  164.  
  165.  
  166. 270::itgeq2 |- ( A. x e. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  167. = ( ( N + 1 ) x. ( x ^ N ) )
  168. -> S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  169. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  170. 271:262,270:ax-mp |- S. ( A (,) B ) ( ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  171. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  172. 272:271,258:eqtr3i |- S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  173. *get result
  174.  
  175.  
  176.  
  177. d33:9h:a1i |- ( T. -> ( N + 1 ) e. CC )
  178. d34:119xb:adantl |- ( ( T. /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. CC )
  179. !d35:: |- ( T. -> ( x e. ( A (,) B ) |-> ( x ^ N ) ) e. L^1 )
  180. 300:d33,d34,d35:itgmulc2
  181. |- ( T. -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x )
  182. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  183. 300a:15,300:ax-mp |- ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x )
  184. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  185.  
  186. 301:300a,272:eqtri |- ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  187. !d41:: |- S. ( A (,) B ) ( x ^ N ) _d x e. CC
  188. **RESULT ***~~~###~~~***
  189. 302:9h,d41,9ca,301:mvllmuli
  190. |- S. ( A (,) B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  191. d40:119xa:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
  192. 303:d18,d19,d40:itgioo
  193. |- ( T. -> S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x )
  194. 303a:15,303:ax-mp |- S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x
  195. qed:303a,302:eqtr3i |- S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  196.  
  197. $)
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!