Skip to content

Instantly share code, notes, and snippets.

@digama0

digama0/itexp.txt

Created April 12, 2019 10:07
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save digama0/d547ff03f3616a5df0beea6224de558a to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save digama0/d547ff03f3616a5df0beea6224de558a to your computer and use it in GitHub Desktop.
Download ZIP
Metamath proof tutorial
Raw
itexp.txt
*** The goal today is to prove the following theorem:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** Jon thinks it would be easier to do this without the "ph ->", but I think he may regret that decision later.
*** Anyway it is epsilon harder to have a context so let's just go with it.
*** Let's try ftc2 with the right substitution:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
!54:: |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
!55:: |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
!56:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
57:50,51,52,54,55,56: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 ) ) )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** We prove the derivative is equal to something, which we use for 54 and 55:
!d1:: |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = &C1 )
!d2:: |- ( ph -> &C1 e. ( ( A (,) B ) -cn-> CC ) )
54:d1,d2:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
*** and apply dvmptres2 and substitute:
!d3:: |- ( ph -> RR e. { RR , CC } )
!d4:: |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
!d5:: |- ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. &C5 )
!d6:: |- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
!d7:: |- ( ph -> ( A [,] B ) C_ RR )
!d8:: |- &C3 = ( &C4 |`t RR )
!d9:: |- &C4 = ( TopOpen ` CCfld )
!d10:: |- ( ph -> ( ( int ` &C3 ) ` ( A [,] B ) ) = ( A (,) B ) )
d1:d3,d4,d5,d6,d7,d8,d9,d10:dvmptres2
|- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
*** let's clean up some side conditions:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
54::reelprrecn |- RR e. { RR , CC }
55:54:a1i |- ( ph -> RR e. { RR , CC } )
56::simpr |- ( ( ph /\ t e. RR ) -> t e. RR )
!57:: |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
58:56,57:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. RR )
59:58:recnd |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
!60:: |- ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. &C5 )
!61:: |- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
62::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
63:50,51,62:syl2anc |- ( ph -> ( A [,] B ) C_ RR )
!64:: |- &C3 = ( &C4 |`t RR )
!65:: |- &C4 = ( TopOpen ` CCfld )
!66:: |- ( ph -> ( ( int ` &C3 ) ` ( A [,] B ) ) = ( A (,) B ) )
67:55,59,60,61,63,64,65,66:dvmptres2
|- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
!68:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
69:67,68:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
!70:: |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
!71:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
72:50,51,52,69,70,71: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 ) ) )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** Oops, I forgot the name of this one:
! |- ( ( ph /\ t e. RR ) -> N e. NN0 )
!57:: |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
*** thanks mmj2!
!d1:: |- ( ( ph /\ t e. RR ) -> N e. NN0 )
d2::peano2nn0 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
57:d1,d2:syl |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
*** Okay, cleaned up:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
54::reelprrecn |- RR e. { RR , CC }
55:54:a1i |- ( ph -> RR e. { RR , CC } )
56::simpr |- ( ( ph /\ t e. RR ) -> t e. RR )
57:53:nnnn0d |- ( ph -> N e. NN0 )
58:57:adantr |- ( ( ph /\ t e. RR ) -> N e. NN0 )
59::peano2nn0 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
60:58,59:syl |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
61:56,60:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. RR )
62:61:recnd |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
63:60:nn0red |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. RR )
64:56,58:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ N ) e. RR )
65:63,64:remulcld |- ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. RR )
!66:: |- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
67::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
68:50,51,67:syl2anc |- ( ph -> ( A [,] B ) C_ RR )
69::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
70:69:tgioo2 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
!71:: |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
72:55,62,65,66,68,70,69,71:dvmptres2
|- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
!73:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
74:72,73:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
!75:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
76:72,75:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
!77:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
78:50,51,52,74,76,77: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 ) ) )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** Now line 66 is provable without too much trouble.
*** let's ask mmj2 for dvexp:
!dvexp
d1::dvexp |- ( &C1 e. NN -> ( CC _D ( &S1 e. CC |-> ( &S1 ^ &C1 ) ) ) = ( &S1 e. CC |-> ( &C1 x. ( &S1 ^ ( &C1 - 1 ) ) ) ) )
*** so we need to further relax the domain to CC, that's dvmptres3:
!d2:: |- &C2 = ( TopOpen ` CCfld )
!d3:: |- ( ph -> CC e. &C2 )
!d4:: |- ( ph -> ( RR i^i CC ) = RR )
!d5:: |- ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
!d6:: |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. &C3 )
!d7:: |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
66:d2,55,d3,d4,d5,d6,d7:dvmptres3 |- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
*** Here d3 says CC is open, toponmax is useful for that, and d4 is just set theory:
!d2::eqid |- &C2 = ( TopOpen ` CCfld )
!d8:: |- &C2 e. ( TopOn ` CC )
d9::toponmax |- ( &C2 e. ( TopOn ` CC ) -> CC e. &C2 )
d3:d8,d9:mp1i |- ( ph -> CC e. &C2 )
*** thanks mmj2:
d2::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
d8:d2:cnfldtopon |- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
d9::toponmax |- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
d3:d8,d9:mp1i |- ( ph -> CC e. ( TopOpen ` CCfld ) )
*** for the other, apply sylib:
!d10:: |- ( ph -> &W1 )
!d11:: |- ( &W1 <-> ( RR i^i CC ) = RR )
d4:d10,d11:sylib |- ( ph -> ( RR i^i CC ) = RR )
*** and double click on d11, because I know there is a theorem about this one but I forget the name:
!d10:: |- ( ph -> RR C_ CC )
d11::df-ss |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
d4:d10,d11:sylib |- ( ph -> ( RR i^i CC ) = RR )
*** Turns out it's the definition. Moving on...
d12::ax-resscn |- RR C_ CC
d10:d12:a1i |- ( ph -> RR C_ CC )
*** Now we have these closure lemmas; unfortunately the previous closure lemmas don't apply because we are on CC now:
!d5:: |- ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
!d6:: |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. &C3 )
*** (I typed expcld and then adantr to get the following:)
d13::simpr |- ( ( ph /\ t e. CC ) -> t e. CC )
d15:57,59:syl |- ( ph -> ( N + 1 ) e. NN0 )
d14:d15:adantr |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. NN0 )
d5:d13,d14:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
*** (and expcld and adantr again:)
d18:57:adantr |- ( ( ph /\ t e. CC ) -> N e. NN0 )
d17:d13,d18:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ N ) e. CC )
d6:d16,d17:mulcld |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
*** Finally, we have the real goal:
!d7:: |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
*** which unfortunately doesn't quite match dvexp because it uses -1 instead of +1. So we will use transitivity:
d21:53:peano2nnd |- ( ph -> ( N + 1 ) e. NN )
d19:d21,d1:syl |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
!d20:: |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
d7:d19,d20:eqtrd |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
*** use mpteq2dva, oveq2 twice then pncan, and we're done.
d26:53:nncnd |- ( ph -> N e. CC )
d27::1cnd |- ( ph -> 1 e. CC )
d25:d26,d27:pncand |- ( ph -> ( ( N + 1 ) - 1 ) = N )
d24:d25:adantr |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) - 1 ) = N )
d23:d24:oveq2d |- ( ( ph /\ t e. CC ) -> ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N ) )
d22:d23:oveq2d |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) ) )
d20:d22:mpteq2dva |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
*** Let's clean up and take stock, which means use Ctrl-Shift-U to unify/renumber and Ctrl-R to reformat:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
54::reelprrecn |- RR e. { RR , CC }
55:54:a1i |- ( ph -> RR e. { RR , CC } )
56::simpr |- ( ( ph /\ t e. RR ) -> t e. RR )
57:53:nnnn0d |- ( ph -> N e. NN0 )
58:57:adantr |- ( ( ph /\ t e. RR ) -> N e. NN0 )
59::peano2nn0 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
60:58,59:syl |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
61:56,60:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. RR )
62:61:recnd |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
63:60:nn0red |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. RR )
64:56,58:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ N ) e. RR )
65:63,64:remulcld |- ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. RR )
66::dvexp |- ( ( N + 1 ) e. NN -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
67::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
68:67:cnfldtopon |- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
69::toponmax |- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
70:68,69:mp1i |- ( ph -> CC e. ( TopOpen ` CCfld ) )
71::ax-resscn |- RR C_ CC
72:71:a1i |- ( ph -> RR C_ CC )
73::df-ss |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
74:72,73:sylib |- ( ph -> ( RR i^i CC ) = RR )
75::simpr |- ( ( ph /\ t e. CC ) -> t e. CC )
76:57,59:syl |- ( ph -> ( N + 1 ) e. NN0 )
77:76:adantr |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. NN0 )
78:75,77:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
79:77:nn0cnd |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. CC )
80:57:adantr |- ( ( ph /\ t e. CC ) -> N e. NN0 )
81:75,80:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ N ) e. CC )
82:79,81:mulcld |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
83:53:peano2nnd |- ( ph -> ( N + 1 ) e. NN )
84:83,66:syl |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
85:53:nncnd |- ( ph -> N e. CC )
86::1cnd |- ( ph -> 1 e. CC )
87:85,86:pncand |- ( ph -> ( ( N + 1 ) - 1 ) = N )
88:87:adantr |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) - 1 ) = N )
89:88:oveq2d |- ( ( ph /\ t e. CC ) -> ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N ) )
90:89:oveq2d |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) ) )
91:90:mpteq2dva |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
92:84,91:eqtrd |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
93:67,55,70,74,78,82,92:dvmptres3
|- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
94::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
95:50,51,94:syl2anc |- ( ph -> ( A [,] B ) C_ RR )
96::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
97:96:tgioo2 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
!98:: |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
99:55,62,65,93,95,97,96,98:dvmptres2
|- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
!100:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
101:99,100:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
!102:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
103:99,102:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
!104:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
105:50,51,52,101,103,104: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 ) ) )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** The next goal is:
!98:: |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
*** I know there is some theorem about this, I'll use syl2anc because I know it takes the assumptions A e. RR and B e. RR
!d1:: |- ( ph -> &W1 )
!d2:: |- ( ph -> &W2 )
!d3:: |- ( ( &W1 /\ &W2 ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
98:d1,d2,d3:syl2anc |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
*** and double click so mmj2 finds it for me:
d3::iccntr |- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
98:50,51,d3:syl2anc |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
*** Okay, so we are getting to the hard goals:
!100:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
!102:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
!104:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
*** well the first one isn't that hard. That's a thing about restrictions of continuous functions:
rescncf
d4::rescncf |- ( &C3 C_ &C1 -> ( &C4 e. ( &C1 -cn-> &C2 ) -> ( &C4 |` &C3 ) e. ( &C3 -cn-> &C2 ) ) )
*** Oh, it uses explicit restrictions so we need to use the theorem on restrictions of a mapping.
d4::rescncf |- ( ( A (,) B ) C_ &C1 ->
( ( t e. &C5 |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( &C1 -cn-> CC ) -> ( ( t e. &C5 |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
)
!d9:: |- ( ph -> ( A (,) B ) C_ &C5 )
d10::resmpt |- ( ( A (,) B ) C_ &C5 -> ( ( t e. &C5 |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
d5:d9,d10:syl |- ( ph -> ( ( t e. &C5 |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
!d7:: |- ( ph -> ( A (,) B ) C_ &C1 )
!d8:: |- ( ph -> ( t e. &C5 |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( &C1 -cn-> CC ) )
d6:d7,d8,d4:sylc |- ( ph -> ( ( t e. &C5 |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
100:d5,d6:eqeltrrd |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
*** A bit of duplication here, I want &C5 and &C1 to be CC:
!d9:: |- ( ph -> ( A (,) B ) C_ CC )
d10::resmpt |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
d5:d9,d10:syl |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
!d8:: |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) )
d6:d9,d8,d4:sylc |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
*** We've already proved most of this subsetting so it's easy:
d12::ioossicc |- ( A (,) B ) C_ ( A [,] B )
d11:d12,95:syl5ss |- ( ph -> ( A (,) B ) C_ RR )
d9:d11,71:syl6ss |- ( ph -> ( A (,) B ) C_ CC )
*** To prove d8, we use the mapping functions for proving continuity:
!d13:: |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
!d14::a1i |- ( ph -> x. e. ( ( &C1 tX &C1 ) Cn &C1 ) )
!d15:: |- ( ph -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
!d16:: |- ( ph -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
d8:d13,d14,d15,d16:cncfmpt2f |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) )
d17:67:mulcn |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
d14:d17:a1i |- ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
!d15:: |- ( ph -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
!d16:: |- ( ph -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
d8:67,d14,d15,d16:cncfmpt2f |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) )
d18:85,86:addcld |- ( ph -> ( N + 1 ) e. CC )
!d19:: |- ( ph -> CC C_ CC )
d21::cncfmptc |- ( ( ( N + 1 ) e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
d15:d18,d19,d19,d21:syl3anc |- ( ph -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
d22::ssid |- CC C_ CC
d19:d22:a1i |- ( ph -> CC C_ CC )
d23::expcncf |- ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
d16:57,d23:syl |- ( ph -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
*** Okay, that finishes continuity on ( A (,) B ). Luckily we can overlap the work for continuity on ( A [,] B ):
!d29:: |- ( ph -> ( A [,] B ) C_ &C4 )
d30::resmpt |- ( ( A [,] B ) C_ &C4 -> ( ( t e. &C4 |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
d24:d29,d30:syl |- ( ph -> ( ( t e. &C4 |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
!d26:: |- ( ph -> ( A [,] B ) C_ &C2 )
!d27:: |- ( ph -> ( t e. &C4 |-> ( t ^ ( N + 1 ) ) ) e. ( &C2 -cn-> CC ) )
d28::rescncf |- ( ( A [,] B ) C_ &C2 ->
( ( t e. &C4 |-> ( t ^ ( N + 1 ) ) ) e. ( &C2 -cn-> CC ) -> ( ( t e. &C4 |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
d25:d26,d27,d28:sylc |- ( ph -> ( ( t e. &C4 |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
104:d24,d25:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
d29:95,72:sstrd |- ( ph -> ( A [,] B ) C_ CC )
d30::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
d24:d29,d30:syl |- ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
!d27:: |- ( ph -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
d28::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 ) ) )
d25:d29,d27,d28:sylc |- ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
104:d24,d25:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
d32::expcncf |- ( ( N + 1 ) e. NN0 -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
d27:76,d32:syl |- ( ph -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
*** Yay, almost done. We have left the best for last:
!102:: |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** and also we haven't started on connecting this whole proof to the qed step.
105:50,51,52,101,103,104: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 ) ) )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** I looked around the library and found iblss, which helps:
d33:d12:a1i |- ( ph -> ( A (,) B ) C_ ( A [,] B ) )
d37::ioombl |- ( A (,) B ) e. dom vol
d34:d37:a1i |- ( ph -> ( A (,) B ) e. dom vol )
!d35:: |- ( ( ph /\ t e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. &C2 )
!d36:: |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
102:d33,d34,d35,d36:iblss |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** We can do d35 by reference to a previous proof of it in a different context:
d38:d29:sselda |- ( ( ph /\ t e. ( A [,] B ) ) -> t e. CC )
d35:d38,82:syldan |- ( ( ph /\ t e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
*** (I had to move d38 up from below to avoid duplicate steps, although it's not a big deal as it would
*** get deduplicated anyway in the final proof.)
*** For d36 we use cniccibl:
!d39:: |- ( ph -> &C1 e. RR )
!d40:: |- ( ph -> &C2 e. RR )
!d41:: |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( &C1 [,] &C2 ) -cn-> CC ) )
d42::cniccibl |- ( ( &C1 e. RR /\ &C2 e. RR /\ ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( &C1 [,] &C2 ) -cn-> CC ) ) ->
( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
d36:d39,d40,d41,d42:syl3anc |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
!d41:: |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
d42::cniccibl |- ( ( 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 )
d36:50,51,d41,d42:syl3anc |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** I guess we still haven't proven this variation yet. Once again, let's take it to CC so we can use the previous result.
d46::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
d43:d29,d46:syl |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
d49::rescncf |- ( ( A [,] B ) C_ CC ->
( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
)
d44:d29,d8,d49:sylc |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
d41:d43,d44:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
*** Wow, we're done! Let's clean up and renumber again:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
54::reelprrecn |- RR e. { RR , CC }
55:54:a1i |- ( ph -> RR e. { RR , CC } )
56::simpr |- ( ( ph /\ t e. RR ) -> t e. RR )
57:53:nnnn0d |- ( ph -> N e. NN0 )
58:57:adantr |- ( ( ph /\ t e. RR ) -> N e. NN0 )
59::peano2nn0 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
60:58,59:syl |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
61:56,60:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. RR )
62:61:recnd |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
63:60:nn0red |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. RR )
64:56,58:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ N ) e. RR )
65:63,64:remulcld |- ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. RR )
66::dvexp |- ( ( N + 1 ) e. NN -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
67::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
68:67:cnfldtopon |- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
69::toponmax |- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
70:68,69:mp1i |- ( ph -> CC e. ( TopOpen ` CCfld ) )
71::ax-resscn |- RR C_ CC
72:71:a1i |- ( ph -> RR C_ CC )
73::df-ss |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
74:72,73:sylib |- ( ph -> ( RR i^i CC ) = RR )
75::simpr |- ( ( ph /\ t e. CC ) -> t e. CC )
76:57,59:syl |- ( ph -> ( N + 1 ) e. NN0 )
77:76:adantr |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. NN0 )
78:75,77:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
79:77:nn0cnd |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. CC )
80:57:adantr |- ( ( ph /\ t e. CC ) -> N e. NN0 )
81:75,80:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ N ) e. CC )
82:79,81:mulcld |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
83:53:peano2nnd |- ( ph -> ( N + 1 ) e. NN )
84:83,66:syl |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
85:53:nncnd |- ( ph -> N e. CC )
86::1cnd |- ( ph -> 1 e. CC )
87:85,86:pncand |- ( ph -> ( ( N + 1 ) - 1 ) = N )
88:87:adantr |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) - 1 ) = N )
89:88:oveq2d |- ( ( ph /\ t e. CC ) -> ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N ) )
90:89:oveq2d |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) ) )
91:90:mpteq2dva |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
92:84,91:eqtrd |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
93:67,55,70,74,78,82,92:dvmptres3
|- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
94::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
95:50,51,94:syl2anc |- ( ph -> ( A [,] B ) C_ RR )
96::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
97:96:tgioo2 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
98::iccntr |- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
99:50,51,98:syl2anc |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
100:55,62,65,93,95,97,96,99:dvmptres2
|- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
101::rescncf |- ( ( A (,) B ) C_ CC ->
( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
102::ioossicc |- ( A (,) B ) C_ ( A [,] B )
103:102,95:syl5ss |- ( ph -> ( A (,) B ) C_ RR )
104:103,71:syl6ss |- ( ph -> ( A (,) B ) C_ CC )
105::resmpt |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
106:104,105:syl |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
107:67:mulcn |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
108:107:a1i |- ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
109:85,86:addcld |- ( ph -> ( N + 1 ) e. CC )
110::ssid |- CC C_ CC
111:110:a1i |- ( ph -> CC C_ CC )
112::cncfmptc |- ( ( ( N + 1 ) e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
113:109,111,111,112:syl3anc
|- ( ph -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
114::expcncf |- ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
115:57,114:syl |- ( ph -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
116:67,108,113,115:cncfmpt2f
|- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) )
117:104,116,101:sylc |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
118:106,117:eqeltrrd |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
119:100,118:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
120:102:a1i |- ( ph -> ( A (,) B ) C_ ( A [,] B ) )
121::ioombl |- ( A (,) B ) e. dom vol
122:121:a1i |- ( ph -> ( A (,) B ) e. dom vol )
123:95,72:sstrd |- ( ph -> ( A [,] B ) C_ CC )
124:123:sselda |- ( ( ph /\ t e. ( A [,] B ) ) -> t e. CC )
125:124,82:syldan |- ( ( ph /\ t e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
126::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
127:123,126:syl |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
128::rescncf |- ( ( A [,] B ) C_ CC ->
( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
)
129:123,116,128:sylc |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
130:127,129:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
131::cniccibl |- ( ( 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 )
132:50,51,130,131:syl3anc
|- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
133:120,122,125,132:iblss
|- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
134:100,133:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
135::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
136:123,135:syl |- ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
137::expcncf |- ( ( N + 1 ) e. NN0 -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
138:76,137:syl |- ( ph -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
139::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 ) ) )
140:123,138,139:sylc |- ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
141:136,140:eqeltrrd
|- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
142:50,51,52,119,134,141: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 ) ) )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** One step left, which is to connect this all to the goal.
!d1:: |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A [,] B ) ( x ^ N ) _d x )
!d2:: |- ( ph ->
( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) =
( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
qed:142,d1,d2:3eqtr3d |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** Oh, that first one is inconvenient, it uses the wrong interval. That's a measure zero difference,
*** surely there's a theorem about that. (Later:) Aha, it's itgioo.
!d3:: |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( x ^ N ) _d x )
d6:123:sselda |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
d7:57:adantr |- ( ( ph /\ x e. ( A [,] B ) ) -> N e. NN0 )
d5:d6,d7:expcld |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
d4:50,51,d5:itgioo |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x )
*** Thank goodness for mmj2 coming up with that closure proof so I don't have to.
*** (I had to give expcld and it figured out the rest)
*** Now back to equality lemmas:
!d3::itgeq2dva |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( x ^ N ) _d x )
*** Oops, invalid ref. What's it called again? (Later:) It's just itgeq2, no one bothered to make the deduction version.
!d10:: |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) )
d8:d10:ralrimiva |- ( ph -> A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) )
d9::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) ->
S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( x ^ N ) _d x )
d3:d8,d9:syl |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( x ^ N ) _d x )
*** Okay, let's be clever here, and prove that the left bit is the derivative mapping and the right bit is the substitution:
!d13:: |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = &C2 )
d11:d13:fveq1d |- ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( &C2 ` x ) )
!d12:: |- ( x e. ( A (,) B ) -> ( &C2 ` x ) = ( x ^ N ) )
d10:d11,d12:sylan9eq |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) )
*** I'm sure d13 is above somewhere: (Later: it's 100)
!d13::#100 |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = &C2 )
d11:100:fveq1d |- ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) )
!d12:: |- ( x e. ( A (,) B ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( x ^ N ) )
d10:d11,d12:sylan9eq |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) )
!d13:: |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( x ^ N ) )
d14::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
d15::ovex |- ( x ^ N ) e. _V
d12:d13,d14,d15:fvmpt |- ( x e. ( A (,) B ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( x ^ N ) )
*** Oh no! I wasn't paying enough attention to the goal, and I've got some nonsense in the proof.
*** The integrands aren't actually equal, they differ by a constant. Okay, let's delete all the
*** garbage steps and double check our place, starting at the ftc proof:
142:50,51,52,119,134,141: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 ) ) )
143:100:fveq1d |- ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) )
144::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
145::ovex |- ( x ^ N ) e. _V
146::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) ->
S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( x ^ N ) _d x )
147:123:sselda |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
148:57:adantr |- ( ( ph /\ x e. ( A [,] B ) ) -> N e. NN0 )
149:147,148:expcld |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
150:50,51,149:itgioo
|- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x )
qed:: |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** What we should actually be doing here is move the ( N + 1 ) to the other side
!d2:: |- ( ph -> ( &C2 / ( N + 1 ) ) = S. ( A (,) B ) ( x ^ N ) _d x )
!d4:: |- ( ph -> &C2 = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
d3:d4:oveq1d |- ( ph -> ( &C2 / ( N + 1 ) ) = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
d1:d2,d3:eqtr3d |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
qed:150,d1:eqtr3d |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
*** We will prove d4 by transitivity to the ftc.
!d5:: |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x e. CC )
d6:83:nnne0d |- ( ph -> ( N + 1 ) =/= 0 )
d2:d5,109,d6:divcan3d
|- ( ph -> ( ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) / ( N + 1 ) ) = S. ( A (,) B ) ( x ^ N ) _d x )
!d7:: |- ( ( ph /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. &C1 )
!d8:: |- ( ph -> ( x e. ( A (,) B ) |-> ( x ^ N ) ) e. L^1 )
d5:d7,d8:itgcl |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x e. CC )
*** Just in case you haven't seen enough of integrability proofs.
*** I don't like using x as a bound variable though, all our earlier results used t, so let's back up and change it:
d9::oveq1 |- ( x = t -> ( x ^ N ) = ( t ^ N ) )
d7:d9:cbvitgv |- S. ( A (,) B ) ( x ^ N ) _d x = S. ( A (,) B ) ( t ^ N ) _d t
!d8:: |- ( ph -> S. ( A (,) B ) ( t ^ N ) _d t e. CC )
d5:d7,d8:syl5eqel |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x e. CC )
*** Look at all those previous results that match. So nice.
d13:124,81:syldan |- ( ( ph /\ t e. ( A [,] B ) ) -> ( t ^ N ) e. CC )
d15:102:sseli |- ( t e. ( A (,) B ) -> t e. ( A [,] B ) )
d10:d15,d13:sylan2 |- ( ( ph /\ t e. ( A (,) B ) ) -> ( t ^ N ) e. CC )
!d14:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. L^1 )
d11:120,122,d13,d14:iblss |- ( ph -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. L^1 )
d8:d10,d11:itgcl |- ( ph -> S. ( A (,) B ) ( t ^ N ) _d t e. CC )
!d18:: |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
d19::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. L^1 )
d14:50,51,d18,d19:syl3anc |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. L^1 )
*** You know the drill.
d23::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ N ) ) )
d20:123,d23:syl |- ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ N ) ) )
d26::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 ) ) )
d21:123,115,d26:sylc |- ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
d18:d20,d21:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
*** In hindsight, I might not have bothered to prove that
*** |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** if I had known we would do it for this function too. Let's move that proof (step 133) right here:
d11:120,122,d13,d14:iblss |- ( ph -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. L^1 )
133:120,122,125,132:iblss
|- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** and now mmj2 reorders the steps, moving ftc down to restore the dag order:
d11:120,122,d13,d14:iblss |- ( ph -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. L^1 )
133:120,122,125,132:iblss
|- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
134:100,133:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
142:50,51,52,119,134,141: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 ) ) )
*** Instead of iblss, let's use iblmulc2:
!d27:: |- ( ( ph /\ t e. ( A (,) B ) ) -> ( t ^ N ) e. &C1 )
133:109,d27,d11:iblmulc2
|- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** Nice! No side conditions except the easy one...
133:109,d10,d11:iblmulc2
|- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
*** and we've already done it.
*** One last step, and then we're done. Luckily it's an easy one.
142:50,51,52,119,134,141: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 ) ) )
!d4:: |- ( ph -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
!d30:: |- ( ( ph /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. CC )
!d31:: |- ( ph -> ( x e. ( A (,) B ) |-> ( x ^ N ) ) e. L^1 )
d27:109,d30,d31:itgmulc2
|- ( ph -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
!d28:: |- ( ph -> S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = &C2 )
!d29:: |- ( ph -> &C2 = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
d4:d27,d28,d29:3eqtrd |- ( ph -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
*** Eh, we're back to x again. I won't rename it this time since it's going to interact with t in ftc2.
*** Still, we proved d30 already, on a different domain:
d32:102:sseli |- ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
d30:d32,149:sylan2 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. CC )
*** Definitely not proving integrability again
d33:d9:cbvmptv |- ( x e. ( A (,) B ) |-> ( x ^ N ) ) = ( t e. ( A (,) B ) |-> ( t ^ N ) )
d31:d33,d11:syl5eqel |- ( ph -> ( x e. ( A (,) B ) |-> ( x ^ N ) ) e. L^1 )
*** Okay, for these we want to use ftc2
!d28:: |- ( ph -> S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = &C2 )
!d29:: |- ( ph -> &C2 = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
*** so we need another transitivity
!d28:,142:eqtr3d |- ( ph -> S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = &C2 )
!d29:: |- ( ph -> &C2 = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
!d34:: |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
d28:d34,142:eqtr3d |- ( ph ->
S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
!d29:: |- ( ph -> ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
*** As we saw, there is no itgeq2dva, so we make do
!d37:: |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
d35:d37:ralrimiva |- ( ph -> A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
d36::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) ->
S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
d34:d35,d36:syl |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
*** and I'm bound and determined to use my trick
!d40::#100 |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = &C2 )
d38:d40:fveq1d |- ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( &C2 ` x ) )
!d39:: |- ( x e. ( A (,) B ) -> ( &C2 ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
d37:d38,d39:sylan9eq |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
!d40:: |- ( &S1 = x -> &C1 = ( ( N + 1 ) x. ( x ^ N ) ) )
!d41::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( &S1 e. ( A (,) B ) |-> &C1 )
d42::ovex |- ( ( N + 1 ) x. ( x ^ N ) ) e. _V
d39:d40,d41,d42:fvmpt |- ( x e. ( A (,) B ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
*** Hey look it works this time
d43::oveq1 |- ( t = x -> ( t ^ N ) = ( x ^ N ) )
d40:d43:oveq2d |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
d41::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
d42::ovex |- ( ( N + 1 ) x. ( x ^ N ) ) e. _V
d39:d40,d41,d42:fvmpt |- ( x e. ( A (,) B ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
*** One last proof:
!d29:: |- ( ph -> ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
!d46:: |- ( ph -> B e. ( A [,] B ) )
d48::oveq1 |- ( t = B -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
d49::eqid |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
d50::ovex |- ( B ^ ( N + 1 ) ) e. _V
d47:d48,d49,d50:fvmpt |- ( B e. ( A [,] B ) -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
d44:d46,d47:syl |- ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
!d45:: |- ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
d29:d44,d45:oveq12d |- ( ph -> ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
*** d46 has a name, let's use syl3anc and double click to look it up (scroll to the bottom past the boring lemmas):
*** It's ubicc2 and the rest gets filled in.
d51:50:rexrd |- ( ph -> A e. RR* )
d52:51:rexrd |- ( ph -> B e. RR* )
d54::ubicc2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
d46:d51,d52,52,d54:syl3anc |- ( ph -> B e. ( A [,] B ) )
*** Do it again for the other goal:
d63::lbicc2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
d55:d51,d52,52,d63:syl3anc |- ( ph -> A e. ( A [,] B ) )
d57::oveq1 |- ( t = A -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
d58::eqid |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
d59::ovex |- ( A ^ ( N + 1 ) ) e. _V
d56:d57,d58,d59:fvmpt |- ( A e. ( A [,] B ) -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
d45:d55,d56:syl |- ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
*** And we're done! Cleanup and renumber again, and here's the final result:
h50::itexp.1 |- ( ph -> A e. RR )
h51::itexp.2 |- ( ph -> B e. RR )
h52::itexp.3 |- ( ph -> A <_ B )
h53::itexp.4 |- ( ph -> N e. NN )
54::reelprrecn |- RR e. { RR , CC }
55:54:a1i |- ( ph -> RR e. { RR , CC } )
56::simpr |- ( ( ph /\ t e. RR ) -> t e. RR )
57:53:nnnn0d |- ( ph -> N e. NN0 )
58:57:adantr |- ( ( ph /\ t e. RR ) -> N e. NN0 )
59::peano2nn0 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
60:58,59:syl |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. NN0 )
61:56,60:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. RR )
62:61:recnd |- ( ( ph /\ t e. RR ) -> ( t ^ ( N + 1 ) ) e. CC )
63:60:nn0red |- ( ( ph /\ t e. RR ) -> ( N + 1 ) e. RR )
64:56,58:reexpcld |- ( ( ph /\ t e. RR ) -> ( t ^ N ) e. RR )
65:63,64:remulcld |- ( ( ph /\ t e. RR ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. RR )
66::dvexp |- ( ( N + 1 ) e. NN -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
67::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
68:67:cnfldtopon |- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
69::toponmax |- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
70:68,69:mp1i |- ( ph -> CC e. ( TopOpen ` CCfld ) )
71::ax-resscn |- RR C_ CC
72:71:a1i |- ( ph -> RR C_ CC )
73::df-ss |- ( RR C_ CC <-> ( RR i^i CC ) = RR )
74:72,73:sylib |- ( ph -> ( RR i^i CC ) = RR )
75::simpr |- ( ( ph /\ t e. CC ) -> t e. CC )
76:57,59:syl |- ( ph -> ( N + 1 ) e. NN0 )
77:76:adantr |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. NN0 )
78:75,77:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ ( N + 1 ) ) e. CC )
79:77:nn0cnd |- ( ( ph /\ t e. CC ) -> ( N + 1 ) e. CC )
80:57:adantr |- ( ( ph /\ t e. CC ) -> N e. NN0 )
81:75,80:expcld |- ( ( ph /\ t e. CC ) -> ( t ^ N ) e. CC )
82:79,81:mulcld |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
83:53:peano2nnd |- ( ph -> ( N + 1 ) e. NN )
84:83,66:syl |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) )
85:53:nncnd |- ( ph -> N e. CC )
86::1cnd |- ( ph -> 1 e. CC )
87:85,86:pncand |- ( ph -> ( ( N + 1 ) - 1 ) = N )
88:87:adantr |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) - 1 ) = N )
89:88:oveq2d |- ( ( ph /\ t e. CC ) -> ( t ^ ( ( N + 1 ) - 1 ) ) = ( t ^ N ) )
90:89:oveq2d |- ( ( ph /\ t e. CC ) -> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) = ( ( N + 1 ) x. ( t ^ N ) ) )
91:90:mpteq2dva |- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ ( ( N + 1 ) - 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
92:84,91:eqtrd |- ( ph -> ( CC _D ( t e. CC |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
93:67,55,70,74,78,82,92:dvmptres3
|- ( ph -> ( RR _D ( t e. RR |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. RR |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
94::iccssre |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
95:50,51,94:syl2anc |- ( ph -> ( A [,] B ) C_ RR )
96::eqid |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
97:96:tgioo2 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
98::iccntr |- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
99:50,51,98:syl2anc |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
100:55,62,65,93,95,97,96,99:dvmptres2
|- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
101::rescncf |- ( ( A (,) B ) C_ CC ->
( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) ->
( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) ) )
102::ioossicc |- ( A (,) B ) C_ ( A [,] B )
103:102,95:syl5ss |- ( ph -> ( A (,) B ) C_ RR )
104:103,71:syl6ss |- ( ph -> ( A (,) B ) C_ CC )
105::resmpt |- ( ( A (,) B ) C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
106:104,105:syl |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
107:67:mulcn |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
108:107:a1i |- ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
109:85,86:addcld |- ( ph -> ( N + 1 ) e. CC )
110::ssid |- CC C_ CC
111:110:a1i |- ( ph -> CC C_ CC )
112::cncfmptc |- ( ( ( N + 1 ) e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
113:109,111,111,112:syl3anc
|- ( ph -> ( t e. CC |-> ( N + 1 ) ) e. ( CC -cn-> CC ) )
114::expcncf |- ( N e. NN0 -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
115:57,114:syl |- ( ph -> ( t e. CC |-> ( t ^ N ) ) e. ( CC -cn-> CC ) )
116:67,108,113,115:cncfmpt2f
|- ( ph -> ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) )
117:104,116,101:sylc |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
118:106,117:eqeltrrd |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
119:100,118:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
120:102:a1i |- ( ph -> ( A (,) B ) C_ ( A [,] B ) )
121::ioombl |- ( A (,) B ) e. dom vol
122:121:a1i |- ( ph -> ( A (,) B ) e. dom vol )
123:95,72:sstrd |- ( ph -> ( A [,] B ) C_ CC )
124:123:sselda |- ( ( ph /\ t e. ( A [,] B ) ) -> t e. CC )
125:124,82:syldan |- ( ( ph /\ t e. ( A [,] B ) ) -> ( ( N + 1 ) x. ( t ^ N ) ) e. CC )
126::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
127:123,126:syl |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) )
128::rescncf |- ( ( A [,] B ) C_ CC ->
( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
129:123,116,128:sylc |- ( ph -> ( ( t e. CC |-> ( ( N + 1 ) x. ( t ^ N ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
130:127,129:eqeltrrd
|- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
131::cniccibl |- ( ( 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 )
132:50,51,130,131:syl3anc
|- ( ph -> ( t e. ( A [,] B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
133::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
134:123,133:syl |- ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) )
135::expcncf |- ( ( N + 1 ) e. NN0 -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
136:76,135:syl |- ( ph -> ( t e. CC |-> ( t ^ ( N + 1 ) ) ) e. ( CC -cn-> CC ) )
137::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 ) ) )
138:123,136,137:sylc |- ( ph -> ( ( t e. CC |-> ( t ^ ( N + 1 ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
139:134,138:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
140:100:fveq1d |- ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) )
141::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
142::ovex |- ( x ^ N ) e. _V
143::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( x ^ N ) ->
S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( x ^ N ) _d x )
144:123:sselda |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
145:57:adantr |- ( ( ph /\ x e. ( A [,] B ) ) -> N e. NN0 )
146:144,145:expcld |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x ^ N ) e. CC )
147:50,51,146:itgioo
|- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x = S. ( A [,] B ) ( x ^ N ) _d x )
148::oveq1 |- ( x = t -> ( x ^ N ) = ( t ^ N ) )
149:148:cbvitgv |- S. ( A (,) B ) ( x ^ N ) _d x = S. ( A (,) B ) ( t ^ N ) _d t
150:124,81:syldan |- ( ( ph /\ t e. ( A [,] B ) ) -> ( t ^ N ) e. CC )
151:102:sseli |- ( t e. ( A (,) B ) -> t e. ( A [,] B ) )
152:151,150:sylan2 |- ( ( ph /\ t e. ( A (,) B ) ) -> ( t ^ N ) e. CC )
153::resmpt |- ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ N ) ) )
154:123,153:syl |- ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t ^ N ) ) )
155::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 ) ) )
156:123,115,155:sylc |- ( ph -> ( ( t e. CC |-> ( t ^ N ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
157:154,156:eqeltrrd |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
158::cniccibl |- ( ( A e. RR /\ B e. RR /\ ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. L^1 )
159:50,51,157,158:syl3anc |- ( ph -> ( t e. ( A [,] B ) |-> ( t ^ N ) ) e. L^1 )
160:120,122,150,159:iblss
|- ( ph -> ( t e. ( A (,) B ) |-> ( t ^ N ) ) e. L^1 )
161:109,152,160:iblmulc2 |- ( ph -> ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) e. L^1 )
162:100,161:eqeltrd |- ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) e. L^1 )
163:50,51,52,119,162,139: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 ) ) )
164:152,160:itgcl |- ( ph -> S. ( A (,) B ) ( t ^ N ) _d t e. CC )
165:149,164:syl5eqel |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x e. CC )
166:83:nnne0d |- ( ph -> ( N + 1 ) =/= 0 )
167:165,109,166:divcan3d
|- ( ph -> ( ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) / ( N + 1 ) ) = S. ( A (,) B ) ( x ^ N ) _d x )
168:102:sseli |- ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
169:168,146:sylan2 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( x ^ N ) e. CC )
170:148:cbvmptv |- ( x e. ( A (,) B ) |-> ( x ^ N ) ) = ( t e. ( A (,) B ) |-> ( t ^ N ) )
171:170,160:syl5eqel |- ( ph -> ( x e. ( A (,) B ) |-> ( x ^ N ) ) e. L^1 )
172:109,169,171:itgmulc2
|- ( ph -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
173:100:fveq1d |- ( ph -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) )
174::oveq1 |- ( t = x -> ( t ^ N ) = ( x ^ N ) )
175:174:oveq2d |- ( t = x -> ( ( N + 1 ) x. ( t ^ N ) ) = ( ( N + 1 ) x. ( x ^ N ) ) )
176::eqid |- ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) = ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) )
177::ovex |- ( ( N + 1 ) x. ( x ^ N ) ) e. _V
178:175,176,177:fvmpt |- ( x e. ( A (,) B ) -> ( ( t e. ( A (,) B ) |-> ( ( N + 1 ) x. ( t ^ N ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
179:173,178:sylan9eq |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
180:179:ralrimiva |- ( ph -> A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) )
181::itgeq2 |- ( A. x e. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) = ( ( N + 1 ) x. ( x ^ N ) ) ->
S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
182:180,181:syl |- ( ph -> S. ( A (,) B ) ( ( RR _D ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ) ` x ) _d x = S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x )
183:182,163:eqtr3d |- ( ph ->
S. ( A (,) B ) ( ( N + 1 ) x. ( x ^ N ) ) _d x = ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) )
184:50:rexrd |- ( ph -> A e. RR* )
185:51:rexrd |- ( ph -> B e. RR* )
186::ubicc2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
187:184,185,52,186:syl3anc
|- ( ph -> B e. ( A [,] B ) )
188::oveq1 |- ( t = B -> ( t ^ ( N + 1 ) ) = ( B ^ ( N + 1 ) ) )
189::eqid |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
190::ovex |- ( B ^ ( N + 1 ) ) e. _V
191:188,189,190:fvmpt |- ( B e. ( A [,] B ) -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
192:187,191:syl |- ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) = ( B ^ ( N + 1 ) ) )
193::lbicc2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
194:184,185,52,193:syl3anc
|- ( ph -> A e. ( A [,] B ) )
195::oveq1 |- ( t = A -> ( t ^ ( N + 1 ) ) = ( A ^ ( N + 1 ) ) )
196::eqid |- ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) = ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) )
197::ovex |- ( A ^ ( N + 1 ) ) e. _V
198:195,196,197:fvmpt |- ( A e. ( A [,] B ) -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
199:194,198:syl |- ( ph -> ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) = ( A ^ ( N + 1 ) ) )
200:192,199:oveq12d |- ( ph -> ( ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` B ) - ( ( t e. ( A [,] B ) |-> ( t ^ ( N + 1 ) ) ) ` A ) ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
201:172,183,200:3eqtrd
|- ( ph -> ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) = ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) )
202:201:oveq1d |- ( ph -> ( ( ( N + 1 ) x. S. ( A (,) B ) ( x ^ N ) _d x ) / ( N + 1 ) ) = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
203:167,202:eqtr3d |- ( ph -> S. ( A (,) B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
qed:147,203:eqtr3d |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
$d t x
$d A t
$d A x
$d B t
$d B x
$d N t
$d N x
$d ph t
$d ph x
$= ( itexp.1 itexp.2 vt co cexp wcel cc cr wss a1i cmul cmpt wceq syl cfv cioo
itexp.4 itexp.3 cv citg cicc c1 caddc cmin cdiv wa iccssre ax-resscn sselda
syl2anc sstrd cn0 nnnn0d adantr expcld itgioo oveq1 cbvitgv ioossicc syldan
sseli simpr sylan2 cvol cdm ioombl ccncf cibl cres expcncf rescncf eqeltrrd
resmpt sylc cniccibl syl3anc iblss itgcl nncnd 1cnd addcld peano2nnd nnne0d
syl5eqel divcan3d cbvmptv itgmulc2 cdv wral crn ctg ccnfld ctopn reelprrecn
cpr peano2nn0 reexpcld nn0red remulcld eqid ctopon cnfldtopon toponmax mp1i
recnd cin df-ss sylib nn0cnd mulcld dvexp pncand oveq2d mpteq2dva dvmptres3
cn eqtrd tgioo2 cnt iccntr dvmptres2 fveq1d fvmpt sylan9eq ralrimiva itgeq2
ovex syl5ss syl6ss ctx ccn eqeltrd eqtr3d cxr rexrd ssid cncfmptc cncfmpt2f
mulcn iblmulc2 ftc2 cle wbr ubicc2 lbicc2 oveq12d 3eqtrd oveq1d ) ABCDUAIZB
UDZEJIZUEZBCDUFIZUUPUEDEUGUHIZJIZCUUSJIZUIIZUUSUJIZABCDUUPFGAUUOUURKZUKUUOE
AUURLUUOAUURMLACMKZDMKZUURMNFGCDULUOZMLNZAUMOZUPZUNAEUQKZUVDAEUBURZUSUTZVAA
UUSUUQPIZUUSUJIUUQUVCAUUQUUSAUUQHUUNHUDZEJIZUELBHUUNUUPUVPUUOUVOEJVBZVCAHUU
NUVPLUVOUUNKAUVOUURKZUVPLKZUUNUURUVOCDVDZVFAUVRUVOLKZUVSAUURLUVOUVJUNAUWAUK
ZUVOEAUWAVGZAUVKUWAUVLUSUTZVEZVHZAHUUNUURUVPLUUNUURNAUVTOUUNVIVJKACDVKOUWEA
UVEUVFHUURUVPQZUURLVLIZKUWGVMKFGAHLUVPQZUURVNZUWGUWHAUURLNZUWJUWGRUVJHLUURU
VPVRSAUWKUWILLVLIZKZUWJUWHKUVJAUVKUWMUVLHEVOSZLLUURUWIVPVSVQCDUWGVTWAWBZWCW
IAEUGAEUBWDZAWEZWFZAUUSAEUBWGZWHWJAUVNUVBUUSUJAUVNBUUNUUSUUPPIZUEZDHUURUVOU
USJIZQZTZCUXCTZUIIZUVBABUUNUUPUUSLUWRUUOUUNKZAUVDUUPLKUUNUURUUOUVTVFUVMVHAB
UUNUUPQHUUNUVPQVMBHUUNUUPUVPUVQWKUWOWIWLABUUNUUOMUXCWMIZTZUEZUXAUXFAUXIUWTR
ZBUUNWNUXJUXARAUXKBUUNAUXGUXIUUOHUUNUUSUVPPIZQZTUWTAUUOUXHUXMAHUXBUXLMUAWOW
PTZWQWRTZMMUUNUURMMLWTKAWSOZAUVOMKZUKZUXBUXRUVOUUSAUXQVGZUXRUVKUUSUQKZAUVKU
XQUVLUSZEXAZSZXBXJUXRUUSUVPUXRUUSUYCXCUXRUVOEUXSUYAXBXDAHUXBUXLMUXOLLMUXOXE
ZUXPUXOLXFTKLUXOKAUXOUYDXGLUXOXHXIAUVHMLXKMRUVIMLXLXMUWBUVOUUSUWCAUXTUWAAUV
KUXTUVLUYBSZUSZUTUWBUUSUVPUWBUUSUYFXNUWDXOALHLUXBQZWMIZHLUUSUVOUUSUGUIIZJIZ
PIZQZHLUXLQZAUUSYAKUYHUYLRUWSHUUSXPSAHLUYKUXLUWBUYJUVPUUSPUWBUYIEUVOJAUYIER
UWAAEUGUWPUWQXQUSXRXRXSYBXTUVGUXOUYDYCUYDAUVEUVFUURUXNYDTTUUNRFGCDYEUOYFZYG
HUUOUXLUWTUUNUXMUVOUUORUVPUUPUUSPUVOUUOEJVBXRUXMXEUUSUUPPYLYHYIYJBUUNUXIUWT
YKSABCDUXCFGUCAUXHUXMUUNLVLIZUYNAUYMUUNVNZUXMUYOAUUNLNZUYPUXMRAUUNMLAUUNUUR
MUVTUVGYMUMYNZHLUUNUXLVRSAUYQUYMUWLKUYPUYOKUYRAHUUSUVPPUXOLUYDPUXOUXOYOIUXO
YPIKAUXOUYDUUDOAUUSLKLLNZUYSHLUUSQUWLKUWRUYSALUUAOZUYTHUUSLLUUBWAUWNUUCLLUU
NUYMVPVSVQYQAUXHUXMVMUYNAHUUNUVPUUSLUWRUWFUWOUUEYQAUYGUURVNZUXCUWHAUWKVUAUX
CRUVJHLUURUXBVRSAUWKUYGUWLKZVUAUWHKUVJAUXTVUBUYEHUUSVOSLLUURUYGVPVSVQUUFYRA
UXDUUTUXEUVAUIADUURKZUXDUUTRACYSKZDYSKZCDUUGUUHZVUCACFYTZADGYTZUCCDUUIWAHDU
XBUUTUURUXCUVODUUSJVBUXCXEZDUUSJYLYHSACUURKZUXEUVARAVUDVUEVUFVUJVUGVUHUCCDU
UJWAHCUXBUVAUURUXCUVOCUUSJVBVUICUUSJYLYHSUUKUULUUMYRYR $.
*** I've never been so happy to see a perfectly rectangular encrypted mess. :)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment