Created
April 12, 2019 10:07
-
-
Save digama0/d547ff03f3616a5df0beea6224de558a to your computer and use it in GitHub Desktop.
Metamath proof tutorial
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
*** 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