API tools faq
paste
Advertisement
FrequentPaster

intx^ndraft4

FrequentPaster
Apr 11th, 2019
105
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 21.05 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. 118a:111a:sseli |- ( t e. ( A (,) B ) -> t e. RR )
  77. 118xa:114:sseli |- ( x e. ( A [,] B ) -> x e. CC )
  78. 118xb:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  79. 119:118,116:syl |- ( t e. ( A [,] B ) -> ( t ^ N ) e. CC )
  80. 119xa:118xa,116x:syl |- ( x e. ( A [,] B ) -> ( x ^ N ) e. CC )
  81. 119xb:118xb,116x:syl |- ( x e. ( A (,) B ) -> ( x ^ N ) e. CC )
  82. 119a:118,116a:syl |- ( t e. ( A [,] B ) -> ( t ^ ( N + 1 ) ) e. CC )
  83. d42::eqid |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) = ( t e. CC |-> ( t ^ ( N + 1 ) ) )
  84. 120:d42,116a:fmpti |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC
  85. d43::eqid |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  86. 120a:d43,116na:fmpti |- ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC
  87. 120b:108:feq1i |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  88. <-> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC )
  89. 121:120a,120b:mpbir |- ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  90. 130::ssid |- CC C_ CC
  91. 155c::fdm |- ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC
  92. -> dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC )
  93. 156:121,155c:ax-mp |- dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC
  94. 157:113,156:sseqtr4i |- RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) )
  95. 158:130,157:pm3.2i |- ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) )
  96. 158a:110,120:pm3.2i |- ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  97. *restrict this function to the reals
  98. 170::dvres3 |- ( ( ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
  99. /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) ) )
  100. -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  101. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) )
  102. 171:158a,158,170:mp2an |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  103. = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR )
  104. 172:171,108a:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  105. = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  106. 173a::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  107. = ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  108. 173b:113,173a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR )
  109. = ( t e. RR |-> ( t ^ ( N + 1 ) ) )
  110. 173c::resmpt |- ( RR C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  111. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  112. 173d:113,173c:ax-mp |- ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR )
  113. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  114. 174:172,173d:eqtri |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  115. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  116. 175:173b:oveq2i |- ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) )
  117. = ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  118. 176:175,174:eqtr3i |- ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  119. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  120. d48:110:a1i |- ( T. -> RR e. { RR , CC } )
  121. d49:116aab:adantl |- ( ( T. /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
  122. d56:9e:a1i |- ( ( T. /\ t e. RR ) -> N e. CC )
  123. d57::1cnd |- ( ( T. /\ t e. RR ) -> 1 e. CC )
  124. d58:d56,d57:addcld
  125. |- ( ( T. /\ t e. RR ) -> ( N + 1 ) e. CC )
  126. d59:116ab:adantl |- ( ( T. /\ t e. RR ) -> ( t ^ N ) e. CC )
  127. d50:d58,d59:mulcld |- ( ( T. /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  128. d50a:15,d50:mpan |- ( t e. RR -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  129. d51:176:a1i |- ( T. -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
  130. = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  131. d52:112:a1i |- ( T. -> ( A [,] B ) C_ RR )
  132. *we have the real derivative of x^( N + 1 ) :), almost
  133.  
  134. d75::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
  135. d72:d75:tgioo2 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
  136. d73::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
  137. d74a::iccntr |- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
  138. d74b:1,2,d74a:mp2an |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B )
  139. d74:d74b:a1i |- ( T. -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
  140. 181:d48,d49,d50,d51,d52,d72,d73,d74:dvmptres2
  141. |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  142. = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
  143. 181a:15,181:ax-mp |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  144. = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  145. *prove some continuity resutls
  146. *get t^N cts
  147. 200::expcncf |- ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
  148. 201::rescncf |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  149. -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
  150. 202::resmpt |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) )
  151. = ( t e. ( A (,) B ) |-> ( t ^ N ) ) )
  152. 210:9f,200:ax-mp |- ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  153. 211:114a,201:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC )
  154. -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
  155. 212:114a,202:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( t ^ N ) )
  156. 220:210,211:ax-mp |- ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC )
  157. 230:212,220:eqeltrri |- ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. ( ( A (,) B ) -cn-> CC )
  158. *get x^N cts
  159. 200b::expcncf |- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
  160. 201b::rescncf |- ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC )
  161. -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
  162. 202b::resmpt |- ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) )
  163. = ( x e. ( A [,] B ) |-> ( x ^ N ) ) )
  164. 210b:9f,200b:ax-mp |- ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC )
  165. 211b:114,201b:ax-mp |- ( ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC )
  166. -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
  167. 212b:114,202b:ax-mp |- ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x ^ N ) )
  168. 220b:210b,211b:ax-mp |- ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
  169. 230bb:212b,220b:eqeltrri |- ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. ( ( A [,] B ) -cn-> CC )
  170. *get t^N+1 cts
  171. 200a::expcncf |- ( ( N + 1 ) e. NN0 -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
  172. 201a::rescncf |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC )
  173. -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
  174. 202a::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) )
  175. = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  176. 210a:9g,200a:ax-mp |- ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC )
  177. 211a:114,201a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC )
  178. -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
  179. 212a:114,202a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
  180. 220a:210a,211a:ax-mp |- ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
  181. 230aa:212a,220a:eqeltrri |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC )
  182. *get N+1 x. t^N
  183. d44::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
  184. 230a:d44:mulcn |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
  185. d45:230a:a1i |- ( T. -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
  186. 230b::cncfmptc |- ( ( ( N + 1 ) e. CC /\ ( A (,) B ) C_ CC /\ CC C_ CC )
  187. -> ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC ) )
  188. 230c:9h,114a,130,230b:mp3an |- ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC )
  189. d46:230c:a1i |- ( T. -> ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC ) )
  190. d47:230:a1i |- ( T. -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. ( ( A (,) B ) -cn-> CC ) )
  191. 231:d44,d45,d46,d47:cncfmpt2f
  192. |- ( T. -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  193. 231a:15,231:ax-mp |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC )
  194.  
  195. *conditions for ftc
  196. 240:181a,231a:eqeltri |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC )
  197. *241::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( RR _D ( t e. ( A [,] B )
  198. |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  199. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  200. *241a:1,2,240,241:mp3an |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1
  201. *use cool new theorem :)
  202. d76:1:a1i |- ( T. -> A e. RR )
  203. d77:2:a1i |- ( T. -> B e. RR )
  204. d78:240:a1i |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  205. *prove boundedness of t^(N+1)
  206. *get dom of the RR term
  207. d80::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  208. = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  209. d81:118a,d50a:syl |- ( t e. ( A (,) B ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
  210. 241a:d80,d81:fmpti |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : ( A (,) B ) --> CC
  211. 241b::fdm |- ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : ( A (,) B ) --> CC
  212. -> dom ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( A (,) B ) )
  213. 241c:241a,241b:ax-mp |- dom ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( A (,) B )
  214. d83::eqcom |- ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  215. = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  216. <-> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  217. = ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) )
  218. d82:181a,d83:mpbi |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  219. = ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  220. 241d:d82:dmeqi |- dom ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  221. = dom ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  222. 241e:241d,241c:eqtr3i |- dom ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( A (,) B )
  223. *show the function is bounded
  224. 241f::cniccbdd |- ( ( A e. RR /\ B e. RR
  225. /\ ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  226. -> E. z e. RR A. y e. ( A [,] B )
  227. ( abs ` ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` y ) ) <_ z )
  228. !241g:: |- E. z e. RR A. y e. ( A [,] B )
  229. ( abs ` ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` y ) ) <_ z
  230. !d79:: |- ( T. -> E. z e. RR A. y e. dom ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
  231. ( abs ` ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` y ) ) <_ z )
  232. 242:d76,d77,d78,d79:cnioobibld
  233. |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  234. 242a:15,242:ax-mp |- ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1
  235. *ftc
  236. d18:1:a1i |- ( T. -> A e. RR )
  237. d19:2:a1i |- ( T. -> B e. RR )
  238. d20:3:a1i |- ( T. -> A <_ B )
  239. d21:240:a1i |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
  240. d22:242a:a1i |- ( T. -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
  241. d23:230aa:a1i |- ( T. -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
  242. 250:d18,d19,d20,d21,d22,d23:ftc2
  243. |- ( T. -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  244. = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
  245. 250a:15,250:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  246. = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  247. *substitute into result
  248. d24::oveq1 |- ( t = B -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
  249. d25::eqid |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
  250. 251:d24,d25:fvmptg |- ( ( B e. ( A [,] B ) /\ ( B ^ ( N + 1 ) ) e. CC )
  251. -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
  252. 251a:8ba,12c,251:mp2an |- ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) )
  253. d26::oveq1 |- ( t = A -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
  254. 252:d26,d25:fvmptg |- ( ( A e. ( A [,] B ) /\ ( A ^ ( N + 1 ) ) e. CC )
  255. -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
  256. 252a:8aa,11c,252:mp2an |- ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) )
  257. 253:251a,252a:oveq12i |- ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) )
  258. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  259. 254:250a,253:eqtri |- S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  260. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  261. *sub in for RR _D x^( N + 1 )
  262. 255:181a:fveq1i |- ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  263. = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  264. 255a:255:rgenw |- A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  265. = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  266. 256::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x )
  267. = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  268. -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  269. = S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x )
  270. 257:255a,256:ax-mp |- S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x
  271. = S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  272. 258:257,254:eqtr3i |- S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  273. = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  274. *get rid of evaluated at
  275.  
  276.  
  277. d32::oveq1 |- ( t = x -> ( t ^ N ) = ( x ^ N ) )
  278. d30:d32:oveq2d |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  279. d31::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  280. = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
  281. 259:d30,d31:fvmptg |- ( ( x e. ( A (,) B ) /\ ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  282. -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
  283.  
  284. 260a::expcl |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
  285. 260b:9f,260a:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
  286. 260c::mulcl |- ( ( ( N + 1 ) e. CC /\ ( x ^ N ) e. CC ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  287. 260d:9h,260b,260c:sylancr |- ( x e. CC -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  288. 260e:114a:sseli |- ( x e. ( A (,) B ) -> x e. CC )
  289. 260ea:111a:sseli |- ( x e. ( A (,) B ) -> x e. RR )
  290. 260f:260e,260d:syl |- ( x e. ( A (,) B ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  291. 261:260f,259:mpdan |- ( x e. ( A (,) B ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  292. = ( ( N + 1 ) x. ( x ^ N ) ) )
  293. 262:261:rgen |- A. x e. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  294. = ( ( N + 1 ) x. ( x ^ N ) )
  295.  
  296.  
  297. 270::itgeq2 |- ( A. x e. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x )
  298. = ( ( N + 1 ) x. ( x ^ N ) )
  299. -> S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  300. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  301. 271:262,270:ax-mp |- S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x
  302. = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  303. 272:271,258:eqtr3i |- S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  304. *get result
  305.  
  306. d33:9h:a1i |- ( T. -> ( N + 1 ) e. CC )
  307. d33a::axmulcl |- ( ( ( N + 1 ) e. CC /\ ( x ^ N ) e. CC ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  308. d40:d33,119xa,d33a:syl2an |- ( ( T. /\ x e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
  309. 280:d18,d19,d40:itgioo |- ( T. -> S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  310. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  311. 280a:15,280:ax-mp |- S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  312. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  313. 280b:280a,272:eqtr3i |- S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  314.  
  315. d61:119xa:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
  316. 290::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
  317. -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1 )
  318. 290a:1,2,230bb,290:mp3an |- ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1
  319. d62:290a:a1i |- ( T. -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1 )
  320. 300:d33,d61,d62:itgmulc2
  321. |- ( T. -> ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x )
  322. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
  323. 300a:15,300:ax-mp |- ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x )
  324. = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x
  325.  
  326. 301:300a,280b:eqtri |- ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) )
  327. d63:119xa:adantl |- ( ( T. /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
  328. d41a:d63,d62:itgcl |- ( T. -> S. ( A [,] B ) ( x ^ N ) _d x e. CC )
  329. d41:15,d41a:ax-mp |- S. ( A [,] B ) ( x ^ N ) _d x e. CC
  330. **RESULT ***~~~###~~~***
  331. 302:9h,d41,9ca,301:mvllmuli
  332. |- S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  333.  
  334.  
  335. qed:302:idi |- S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) )
  336.  
  337. $)
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!