Metamath Proof Explorer

Theorem itgpowd

Description: The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019) (Revised by Thierry Arnoux, 14-Jun-2019)

Ref Expression
Hypotheses itgpowd.1 
|- ( ph -> A e. RR )
itgpowd.2 
|- ( ph -> B e. RR )
itgpowd.3 
|- ( ph -> A <_ B )
itgpowd.4 
|- ( ph -> N e. NN0 )
Assertion itgpowd 
|- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 itgpowd.1 
 |-  ( ph -> A e. RR )
2 itgpowd.2 
 |-  ( ph -> B e. RR )
3 itgpowd.3 
 |-  ( ph -> A <_ B )
4 itgpowd.4 
 |-  ( ph -> N e. NN0 )
5 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
6 4 5 syl 
 |-  ( ph -> ( N + 1 ) e. NN )
7 6 nncnd 
 |-  ( ph -> ( N + 1 ) e. CC )
8 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
9 1 2 8 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
10 ax-resscn 
 |-  RR C_ CC
11 9 10 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
12 11 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
13 4 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> N e. NN0 )
14 12 13 expcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
15 11 resmptd 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x ^ N ) ) )
16 expcncf 
 |-  ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
17 4 16 syl 
 |-  ( ph -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
18 rescncf 
 |-  ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
19 11 17 18 sylc 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
20 15 19 eqeltrrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
21 cnicciblnc 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1 )
22 1 2 20 21 syl3anc 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( x ^ N ) ) e. L^1 )
23 14 22 itgcl 
 |-  ( ph -> S. ( A [,] B ) ( x ^ N ) _d x e. CC )
24 6 nnne0d 
 |-  ( ph -> ( N + 1 ) =/= 0 )
25 7 14 22 itgmulc2 
 |-  ( ph -> ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x ) = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
26 eqidd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
27 oveq1 
 |-  ( t = x -> ( t ^ N ) = ( x ^ N ) )
28 27 oveq2d 
 |-  ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
29 28 adantl 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ t = x ) -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
30 simpr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
31 7 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( N + 1 ) e. CC )
32 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
33 32 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
34 33 sselda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
35 34 14 syldan 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. CC )
36 31 35 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
37 26 29 30 36 fvmptd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
38 37 itgeq2dv 
 |-  ( ph -> S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
39 reelprrecn 
 |-  RR e. { RR , CC }
40 39 a1i 
 |-  ( ph -> RR e. { RR , CC } )
41 10 a1i 
 |-  ( ph -> RR C_ CC )
42 41 sselda 
 |-  ( ( ph /\ t e. RR ) -> t e. CC )
43 1nn0 
 |-  1 e. NN0
44 43 a1i 
 |-  ( ph -> 1 e. NN0 )
45 4 44 nn0addcld 
 |-  ( ph -> ( N + 1 ) e. NN0 )
46 45 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
47 42 46 expcld 
 |-  ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
48 4 nn0cnd 
 |-  ( ph -> N e. CC )
49 48 adantr 
 |-  ( ( ph /\ t e. RR ) -> N e. CC )
50 1cnd 
 |-  ( ( ph /\ t e. RR ) -> 1 e. CC )
51 49 50 addcld 
 |-  ( ( ph /\ t e. RR ) -> ( N + 1 ) e. CC )
52 4 adantr 
 |-  ( ( ph /\ t e. RR ) -> N e. NN0 )
53 42 52 expcld 
 |-  ( ( ph /\ t e. RR ) -> ( t ^ N ) e. CC )
54 51 53 mulcld 
 |-  ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
55 simpr 
 |-  ( ( ph /\ t e. CC ) -> t e. CC )
56 45 adantr 
 |-  ( ( ph /\ t e. CC ) -> ( N + 1 ) e. NN0 )
57 55 56 expcld 
 |-  ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
58 57 fmpttd 
 |-  ( ph -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC )
59 ssidd 
 |-  ( ph -> CC C_ CC )
60 7 adantr 
 |-  ( ( ph /\ t e. CC ) -> ( N + 1 ) e. CC )
61 4 adantr 
 |-  ( ( ph /\ t e. CC ) -> N e. NN0 )
62 55 61 expcld 
 |-  ( ( ph /\ t e. CC ) -> ( t ^ N ) e. CC )
63 60 62 mulcld 
 |-  ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
64 63 fmpttd 
 |-  ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC )
65 dvexp 
 |-  ( ( N + 1 ) e. NN -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
66 6 65 syl 
 |-  ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
67 1cnd 
 |-  ( ph -> 1 e. CC )
68 48 67 pncand 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
69 68 oveq2d 
 |-  ( ph -> ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N ) )
70 69 oveq2d 
 |-  ( ph -> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) ) )
71 70 mpteq2dv 
 |-  ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
72 66 71 eqtrd 
 |-  ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
73 72 feq1d 
 |-  ( ph -> ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC <-> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) : CC --> CC ) )
74 64 73 mpbird 
 |-  ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) : CC --> CC )
75 74 fdmd 
 |-  ( ph -> dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = CC )
76 10 75 sseqtrrid 
 |-  ( ph -> RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) )
77 dvres3 
 |-  ( ( ( RR e. { RR , CC } /\ ( t e. CC |-> ( t ^ ( N + 1 ) ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) ) ) -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) )
78 40 58 59 76 77 syl22anc 
 |-  ( ph -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) )
79 72 reseq1d 
 |-  ( ph -> ( ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) |` RR ) = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR ) )
80 78 79 eqtrd 
 |-  ( ph -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR ) )
81 resmpt 
 |-  ( RR C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) = ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
82 10 81 mp1i 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) = ( t e. RR |-> ( t ^ ( N + 1 ) ) ) )
83 82 oveq2d 
 |-  ( ph -> ( RR _D ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` RR ) ) = ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) )
84 resmpt 
 |-  ( RR C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
85 10 84 mp1i 
 |-  ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` RR ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
86 80 83 85 3eqtr3d 
 |-  ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
87 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
88 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
89 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
90 1 2 89 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
91 40 47 54 86 9 87 88 90 dvmptres2 
 |-  ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
92 ioossre 
 |-  ( A (,) B ) C_ RR
93 92 10 sstri 
 |-  ( A (,) B ) C_ CC
94 93 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
95 cncfmptc 
 |-  ( ( ( N + 1 ) e. CC /\ ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC ) )
96 7 94 59 95 syl3anc 
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( N + 1 ) ) e. ( ( A (,) B ) -cn-> CC ) )
97 resmpt 
 |-  ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( t ^ N ) ) )
98 93 97 mp1i 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( t ^ N ) ) )
99 expcncf 
 |-  ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
100 4 99 syl 
 |-  ( ph -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
101 rescncf 
 |-  ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
102 94 100 101 sylc 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
103 98 102 eqeltrrd 
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. ( ( A (,) B ) -cn-> CC ) )
104 96 103 mulcncf 
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
105 91 104 eqeltrd 
 |-  ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
106 ioombl 
 |-  ( A (,) B ) e. dom vol
107 106 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
108 48 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> N e. CC )
109 1cnd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> 1 e. CC )
110 108 109 addcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( N + 1 ) e. CC )
111 11 sselda 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. CC )
112 4 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> N e. NN0 )
113 111 112 expcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t ^ N ) e. CC )
114 110 113 mulcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
115 cncfmptc 
 |-  ( ( ( N + 1 ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( t e. ( A [,] B ) |-> ( N + 1 ) ) e. ( ( A [,] B ) -cn-> CC ) )
116 7 11 59 115 syl3anc 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( N + 1 ) ) e. ( ( A [,] B ) -cn-> CC ) )
117 11 resmptd 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ N ) ) )
118 rescncf 
 |-  ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
119 11 100 118 sylc 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
120 117 119 eqeltrrd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
121 116 120 mulcncf 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
122 cnicciblnc 
 |-  ( ( A e. RR /\ B e. RR /\ ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
123 1 2 121 122 syl3anc 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
124 33 107 114 123 iblss 
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
125 91 124 eqeltrd 
 |-  ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
126 11 resmptd 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
127 expcncf 
 |-  ( ( N + 1 ) e. NN0 -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
128 45 127 syl 
 |-  ( ph -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
129 rescncf 
 |-  ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
130 11 128 129 sylc 
 |-  ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
131 126 130 eqeltrrd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
132 1 2 3 105 125 131 ftc2 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
133 91 fveq1d 
 |-  ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) )
134 133 ralrimivw 
 |-  ( ph -> A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) )
135 itgeq2 
 |-  ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x )
136 134 135 syl 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x )
137 eqidd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
138 simpr 
 |-  ( ( ph /\ t = B ) -> t = B )
139 138 oveq1d 
 |-  ( ( ph /\ t = B ) -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
140 1 rexrd 
 |-  ( ph -> A e. RR* )
141 2 rexrd 
 |-  ( ph -> B e. RR* )
142 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
143 140 141 3 142 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
144 2 recnd 
 |-  ( ph -> B e. CC )
145 144 45 expcld 
 |-  ( ph -> ( B ^ ( N + 1 ) ) e. CC )
146 137 139 143 145 fvmptd 
 |-  ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
147 simpr 
 |-  ( ( ph /\ t = A ) -> t = A )
148 147 oveq1d 
 |-  ( ( ph /\ t = A ) -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
149 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
150 140 141 3 149 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
151 1 recnd 
 |-  ( ph -> A e. CC )
152 151 45 expcld 
 |-  ( ph -> ( A ^ ( N + 1 ) ) e. CC )
153 137 148 150 152 fvmptd 
 |-  ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
154 146 153 oveq12d 
 |-  ( ph -> ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
155 132 136 154 3eqtr3d 
 |-  ( ph -> S. ( A (,) B ) ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
156 7 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( N + 1 ) e. CC )
157 156 14 mulcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( x ^ N ) ) e. CC )
158 1 2 157 itgioo 
 |-  ( ph -> S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
159 38 155 158 3eqtr3rd 
 |-  ( ph -> S. ( A [,] B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
160 25 159 eqtrd 
 |-  ( ph -> ( ( N + 1 ) x. S. ( A [,] B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
161 7 23 24 160 mvllmuld 
 |-  ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )