*proving that integral of X^N = X^N+1/N+1

9:: |- N e. NN
9a::nnaddcl |- ( ( N e. NN /\ 1 e. NN ) -> ( N + 1 ) e. NN )
9b::1nn |- 1 e. NN
9ba::ax1cn |- 1 e. CC
9c:9,9b,9a:mp2an |- ( N + 1 ) e. NN
9ca:9c:nnne0i |- ( N + 1 ) =/= 0
9d:9:nnrei |- N e. RR
9e:9d:recni |- N e. CC
9f:9:nnnn0i |- N e. NN0
9g:9c:nnnn0i |- ( N + 1 ) e. NN0
11:: |- A e. RR
12:: |- B e. RR
13:: |- A <_ B
14:: |- ph

*get the derivative of x^N+1
100::dvexp         |- ( ( N + 1 ) e. NN -> ( CC _D ( x e. CC |-> ( x ^ ( N + 1 ) ) ) )
	= ( x e. CC |-> ( ( N + 1 ) x. ( x ^ ( ( N + 1 ) - 1 ) ) ) ) )
101:9c,100:ax-mp |- ( CC _D ( x e. CC |-> ( x ^ ( N + 1 ) ) ) )
	= ( x e. CC |-> ( ( N + 1 ) x. ( x ^ ( ( N + 1 ) - 1 ) ) ) )
103:9e,9ba:pncan3oi |- ( ( N + 1 ) - 1 ) = N
104:103:oveq2i |- ( x ^ ( ( N + 1 ) - 1 ) ) = ( x ^ N )
*105:104,10:eqtr4i |- ( x ^ ( ( N + 1 ) - 1 ) ) = F
106:104:oveq2i |- ( ( N + 1 ) x. ( x ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( x ^ N ) )
107:106:mpteq2i |- ( x e. CC |-> ( ( N + 1 ) x. ( x ^ ( ( N + 1 ) - 1 ) ) ) ) = ( x e. CC |-> ( ( N + 1 ) x. ( x ^ N ) ) )
108:101,107:eqtri |- ( CC _D ( x e. CC |-> ( x ^ ( N + 1 ) ) ) )  = ( x e. CC |-> ( ( N + 1 ) x. ( x ^ N ) ) )

*conditions for restriction
110::reelprrecn |- RR e. { RR , CC }
111::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
112:11,12,111:mp2an |- ( A [,] B ) C_ RR
113::axresscn |- RR C_ CC
114:112,113:sstri |- ( A [,] B ) C_ CC
115::expcl         |- ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
115a::expcl |- ( ( x e. CC /\ ( N + 1 ) e. NN0 ) -> ( x ^ ( N + 1 ) ) e. CC )
116:9f,115:mpan2 |- ( x e. CC -> ( x ^ N ) e. CC )
116a:9g,115a:mpan2 |- ( x e. CC -> ( x ^ ( N + 1 ) ) e. CC )
118:114:sseli |- ( x e. ( A [,] B )  -> x e. CC )
119:118,116:syl |- ( x e. ( A [,] B ) -> ( x ^ N ) e. CC )
119a:118,116a:syl |- ( x e. ( A [,] B ) -> ( x ^ ( N + 1 ) ) e. CC )
120:: |- ( A. x e. ( A [,] B ) ( x ^ N ) e. CC ->  ( x ^ N ) : ( A [,] B ) --> CC )
155::fdm           |- ( &C3 : &C1 --> &C2 -> dom &C3 = &C1 )
155a::fdm          |- ( ( CC _D ( x ^ ( N + 1 ) ) ) : CC --> CC -> dom ( CC _D ( x ^ ( N + 1 ) ) ) = CC )
*restrict this function to the reals
150a::dvres3       |- ( ( ( RR e. { RR , CC } /\ ( x ^ ( N + 1 ) ) : ( A [,] B ) --> CC ) /\ ( ( A [,] B ) C_ CC
	/\ RR C_ dom ( CC _D ( x ^ ( N + 1 ) ) ) ) ) -> ( RR _D ( ( x ^ ( N + 1 ) ) |` RR ) )
	= ( ( CC _D ( x ^ ( N + 1 ) ) ) |` RR ) )
150b:: |- ( RR _D ( ( x ^ ( N + 1 ) ) |` RR ) ) = ( ( CC _D ( x ^ ( N + 1 ) ) ) |` RR )
160:: |- ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) = ( ( ( N + 1 ) x. ( x ^ N ) ) ` t )
161:160:rgenw |- A. t e. ( A [,] B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) = ( ( ( N + 1 ) x. ( x ^ N ) ) ` t )

*use the fundamental theorem of calculus
d1:11:a1i          |- ( ph -> A e. RR )
d2:12:a1i          |- ( ph -> B e. RR )
d3:13:a1i          |- ( ph -> A <_ B )
!d4::              |- ( ph -> ( RR _D ( x ^ ( N + 1 ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
!d5::              |- ( ph -> ( RR _D ( x ^ ( N + 1 ) ) ) e. L^1 )
!d6::              |- ( ph -> ( x ^ ( N + 1 ) ) e. ( ( A [,] B ) -cn-> CC ) )
200:d1,d2,d3,d4,d5,d6:ftc2
                   |- ( ph -> S. ( A (,) B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) _d t
	= ( ( ( x ^ ( N + 1 ) ) ` B ) - ( ( x ^ ( N + 1 ) ) ` A ) ) )
200a:14,200:ax-mp |- S. ( A (,) B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) _d t
	= ( ( ( x ^ ( N + 1 ) ) ` B ) - ( ( x ^ ( N + 1 ) ) ` A ) )
201::itgeq2        |- ( A. t e. ( A [,] B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) = ( ( ( N + 1 ) x. ( x ^ N ) ) ` t )
	-> S. ( A [,] B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) _d t = S. ( A [,] B ) ( ( ( N + 1 ) x. ( x ^ N ) ) ` t ) _d t )
202:161,201:ax-mp |- S. ( A [,] B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t )  _d t
	= S. ( A [,] B ) ( ( ( N + 1 ) x. ( x ^ N ) ) ` t ) _d t

d10:9e:a1i         |- ( ph -> N e. CC )
d11::1cnd          |- ( ph -> 1 e. CC )
d7:d10,d11:addcld  |- ( ph -> ( N + 1 ) e. CC )
!d14::             |- ( ph -> ( x ^ N ) : ( A [,] B ) --> CC )
d8:d14:ffvelrnda   |- ( ( ph /\ t e. ( A [,] B ) ) -> ( ( x ^ N ) ` t ) e. CC )
!d9::              |- ( ph -> ( t e. ( A [,] B ) |-> ( ( x ^ N ) ` t ) ) e. L^1 )
210:d7,d8,d9:itgmulc2
                   |- ( ph -> ( ( N + 1 ) x. S. ( A [,] B ) ( ( x ^ N ) ` t ) _d t )
	= S. ( A [,] B ) ( ( N + 1 ) x. ( ( x ^ N ) ` t ) ) _d t )
211:14,210:ax-mp |- ( ( N + 1 ) x. S. ( A [,] B ) ( ( x ^ N ) ` t ) _d t )
	= S. ( A [,] B ) ( ( N + 1 ) x. ( ( x ^ N ) ` t ) ) _d t
212:202,211: |-  S. ( A [,] B ) ( ( RR _D ( x ^ ( N + 1 ) ) ) ` t ) _d t
	= ( ( N + 1 ) x. S. ( A [,] B ) ( ( x ^ N ) ` t ) _d t )
213:212,200a:  |- ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d t )
	= ( ( ( x ^ ( N + 1 ) ) ` B ) - ( ( x ^ ( N + 1 ) ) ` A ) )
d12:14,d7:ax-mp    |- ( N + 1 ) e. CC
!d13::             |- S. ( A [,] B ) ( x ^ N ) _d t e. CC
214:d12,d13,9ca,213:mvllmuli
	|- S. ( A [,] B ) ( x ^ N ) _d t = ( ( ( ( x ^ ( N + 1 ) ) ` B ) - ( ( x ^ ( N + 1 ) ) ` A ) ) / ( N + 1 ) )
215:: |- ( ( x ^ ( N + 1 ) ) ` B ) = ( B ^ ( N + 1 ) )