Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgperiod Structured version   Unicode version

Theorem itgperiod 31622
Description: The integral of a periodic function, with period  T stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
itgperiod.a  |-  ( ph  ->  A  e.  RR )
itgperiod.b  |-  ( ph  ->  B  e.  RR )
itgperiod.aleb  |-  ( ph  ->  A  <_  B )
itgperiod.t  |-  ( ph  ->  T  e.  RR+ )
itgperiod.f  |-  ( ph  ->  F : RR --> CC )
itgperiod.fper  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
itgperiod.fcn  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> CC ) )
Assertion
Ref Expression
itgperiod  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
Distinct variable groups:    x, A    x, B    x, F    x, T    ph, x

Proof of Theorem itgperiod
Dummy variables  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itgperiod.a . . . . 5  |-  ( ph  ->  A  e.  RR )
2 itgperiod.b . . . . 5  |-  ( ph  ->  B  e.  RR )
3 itgperiod.t . . . . . 6  |-  ( ph  ->  T  e.  RR+ )
43rpred 11268 . . . . 5  |-  ( ph  ->  T  e.  RR )
5 itgperiod.aleb . . . . 5  |-  ( ph  ->  A  <_  B )
61, 2, 4, 5leadd1dd 10178 . . . 4  |-  ( ph  ->  ( A  +  T
)  <_  ( B  +  T ) )
76ditgpos 22128 . . 3  |-  ( ph  ->  S__ [ ( A  +  T )  -> 
( B  +  T
) ] ( F `
 x )  _d x  =  S. ( ( A  +  T
) (,) ( B  +  T ) ) ( F `  x
)  _d x )
81, 4readdcld 9635 . . . 4  |-  ( ph  ->  ( A  +  T
)  e.  RR )
92, 4readdcld 9635 . . . 4  |-  ( ph  ->  ( B  +  T
)  e.  RR )
10 itgperiod.f . . . . . 6  |-  ( ph  ->  F : RR --> CC )
1110adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  F : RR --> CC )
128adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR )
139adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR )
14 simpr 461 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
15 eliccre 31427 . . . . . 6  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  ->  x  e.  RR )
1612, 13, 14, 15syl3anc 1228 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  RR )
17 ffvelrn 6030 . . . . 5  |-  ( ( F : RR --> CC  /\  x  e.  RR )  ->  ( F `  x
)  e.  CC )
1811, 16, 17syl2anc 661 . . . 4  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  x )  e.  CC )
198, 9, 18itgioo 22090 . . 3  |-  ( ph  ->  S. ( ( A  +  T ) (,) ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( ( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x )
20 eqidd 2468 . . 3  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( ( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x )
217, 19, 203eqtrrd 2513 . 2  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S__ [
( A  +  T
)  ->  ( B  +  T ) ] ( F `  x )  _d x )
22 eqid 2467 . . . 4  |-  ( y  e.  CC  |->  ( y  +  T ) )  =  ( y  e.  CC  |->  ( y  +  T ) )
23 ax-resscn 9561 . . . . . 6  |-  RR  C_  CC
2423, 4sseldi 3507 . . . . 5  |-  ( ph  ->  T  e.  CC )
2522addccncf 21288 . . . . 5  |-  ( T  e.  CC  ->  (
y  e.  CC  |->  ( y  +  T ) )  e.  ( CC
-cn-> CC ) )
2624, 25syl 16 . . . 4  |-  ( ph  ->  ( y  e.  CC  |->  ( y  +  T
) )  e.  ( CC -cn-> CC ) )
27 iccssre 11618 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
281, 2, 27syl2anc 661 . . . . 5  |-  ( ph  ->  ( A [,] B
)  C_  RR )
2928, 23syl6ss 3521 . . . 4  |-  ( ph  ->  ( A [,] B
)  C_  CC )
30 iccssre 11618 . . . . . 6  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR )  ->  ( ( A  +  T ) [,] ( B  +  T
) )  C_  RR )
318, 9, 30syl2anc 661 . . . . 5  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  C_  RR )
3223a1i 11 . . . . 5  |-  ( ph  ->  RR  C_  CC )
3331, 32sstrd 3519 . . . 4  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  C_  CC )
3428sselda 3509 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  RR )
354adantr 465 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  T  e.  RR )
3634, 35readdcld 9635 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  +  T )  e.  RR )
371adantr 465 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  A  e.  RR )
38 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  ( A [,] B ) )
392adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  B  e.  RR )
40 elicc2 11601 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( y  e.  ( A [,] B )  <-> 
( y  e.  RR  /\  A  <_  y  /\  y  <_  B ) ) )
4137, 39, 40syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  e.  ( A [,] B
)  <->  ( y  e.  RR  /\  A  <_ 
y  /\  y  <_  B ) ) )
4238, 41mpbid 210 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  e.  RR  /\  A  <_ 
y  /\  y  <_  B ) )
4342simp2d 1009 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  A  <_  y )
4437, 34, 35, 43leadd1dd 10178 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( A  +  T )  <_  (
y  +  T ) )
4542simp3d 1010 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  <_  B )
4634, 39, 35, 45leadd1dd 10178 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  +  T )  <_  ( B  +  T )
)
4736, 44, 463jca 1176 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( (
y  +  T )  e.  RR  /\  ( A  +  T )  <_  ( y  +  T
)  /\  ( y  +  T )  <_  ( B  +  T )
) )
488adantr 465 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( A  +  T )  e.  RR )
499adantr 465 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( B  +  T )  e.  RR )
50 elicc2 11601 . . . . . 6  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR )  ->  ( ( y  +  T )  e.  ( ( A  +  T ) [,] ( B  +  T )
)  <->  ( ( y  +  T )  e.  RR  /\  ( A  +  T )  <_ 
( y  +  T
)  /\  ( y  +  T )  <_  ( B  +  T )
) ) )
5148, 49, 50syl2anc 661 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( (
y  +  T )  e.  ( ( A  +  T ) [,] ( B  +  T
) )  <->  ( (
y  +  T )  e.  RR  /\  ( A  +  T )  <_  ( y  +  T
)  /\  ( y  +  T )  <_  ( B  +  T )
) ) )
5247, 51mpbird 232 . . . 4  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  +  T )  e.  ( ( A  +  T
) [,] ( B  +  T ) ) )
5322, 26, 29, 33, 52cncfmptssg 31531 . . 3  |-  ( ph  ->  ( y  e.  ( A [,] B ) 
|->  ( y  +  T
) )  e.  ( ( A [,] B
) -cn-> ( ( A  +  T ) [,] ( B  +  T
) ) ) )
54 eqeq1 2471 . . . . . . . 8  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
5554rexbidv 2978 . . . . . . 7  |-  ( w  =  x  ->  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  <->  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )
56 oveq1 6302 . . . . . . . . . 10  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
5756eqeq2d 2481 . . . . . . . . 9  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
5857cbvrexv 3094 . . . . . . . 8  |-  ( E. z  e.  ( A [,] B ) x  =  ( z  +  T )  <->  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) )
5958a1i 11 . . . . . . 7  |-  ( w  =  x  ->  ( E. z  e.  ( A [,] B ) x  =  ( z  +  T )  <->  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) ) )
6055, 59bitrd 253 . . . . . 6  |-  ( w  =  x  ->  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  <->  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) ) )
6160cbvrabv 3117 . . . . 5  |-  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  =  { x  e.  CC  |  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) }
62 ffdm 5751 . . . . . . 7  |-  ( F : RR --> CC  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
6310, 62syl 16 . . . . . 6  |-  ( ph  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
6463simpld 459 . . . . 5  |-  ( ph  ->  F : dom  F --> CC )
65 simp3 998 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  w  =  ( z  +  T ) )  ->  w  =  ( z  +  T
) )
6628sselda 3509 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  z  e.  RR )
674adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  T  e.  RR )
6866, 67readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  +  T )  e.  RR )
69683adant3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  w  =  ( z  +  T ) )  ->  ( z  +  T )  e.  RR )
7065, 69eqeltrd 2555 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  w  =  ( z  +  T ) )  ->  w  e.  RR )
71703exp 1195 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( z  e.  ( A [,] B )  ->  ( w  =  ( z  +  T
)  ->  w  e.  RR ) ) )
7271rexlimdv 2957 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E. z  e.  ( A [,] B
) w  =  ( z  +  T )  ->  w  e.  RR ) )
7372adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  CC )  ->  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  ->  w  e.  RR ) )
7473ralrimiva 2881 . . . . . . . . . . 11  |-  ( ph  ->  A. w  e.  CC  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  ->  w  e.  RR )
)
75 rabss 3582 . . . . . . . . . . 11  |-  ( { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  C_  RR 
<-> 
A. w  e.  CC  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  ->  w  e.  RR )
)
7674, 75sylibr 212 . . . . . . . . . 10  |-  ( ph  ->  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } 
C_  RR )
7776adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  C_  RR )
78 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )
7977, 78sseldd 3510 . . . . . . . 8  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  x  e.  RR )
80 fdm 5741 . . . . . . . . . . 11  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
8110, 80syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  F  =  RR )
8281eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  RR  =  dom  F
)
8382adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  RR  =  dom  F )
8479, 83eleqtrd 2557 . . . . . . 7  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  x  e.  dom  F )
8584ralrimiva 2881 . . . . . 6  |-  ( ph  ->  A. x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } x  e.  dom  F )
86 dfss3 3499 . . . . . 6  |-  ( { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  C_  dom  F  <->  A. x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } x  e.  dom  F )
8785, 86sylibr 212 . . . . 5  |-  ( ph  ->  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } 
C_  dom  F )
88 itgperiod.fper . . . . 5  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
89 itgperiod.fcn . . . . 5  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> CC ) )
9029, 4, 61, 64, 87, 88, 89cncfperiod 31540 . . . 4  |-  ( ph  ->  ( F  |`  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } )  e.  ( { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }
-cn-> CC ) )
91 nfv 1683 . . . . . . . . 9  |-  F/ x ph
9255elrab 3266 . . . . . . . . . . . . 13  |-  ( x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  <->  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )
9378, 92sylib 196 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )
94 simprr 756 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )  ->  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) )
95 nfv 1683 . . . . . . . . . . . . . . . . 17  |-  F/ z
ph
96 nfv 1683 . . . . . . . . . . . . . . . . . 18  |-  F/ z  x  e.  CC
97 nfre1 2928 . . . . . . . . . . . . . . . . . 18  |-  F/ z E. z  e.  ( A [,] B ) x  =  ( z  +  T )
9896, 97nfan 1875 . . . . . . . . . . . . . . . . 17  |-  F/ z ( x  e.  CC  /\ 
E. z  e.  ( A [,] B ) x  =  ( z  +  T ) )
9995, 98nfan 1875 . . . . . . . . . . . . . . . 16  |-  F/ z ( ph  /\  (
x  e.  CC  /\  E. z  e.  ( A [,] B ) x  =  ( z  +  T ) ) )
100 nfv 1683 . . . . . . . . . . . . . . . 16  |-  F/ z  x  e.  ( ( A  +  T ) [,] ( B  +  T ) )
101 simp3 998 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  x  =  ( z  +  T
) )
102 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( A [,] B ) )
1031adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  A  e.  RR )
1042adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  B  e.  RR )
105 elicc2 11601 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( z  e.  ( A [,] B )  <-> 
( z  e.  RR  /\  A  <_  z  /\  z  <_  B ) ) )
106103, 104, 105syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  e.  ( A [,] B
)  <->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) ) )
107102, 106mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) )
108107simp2d 1009 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  A  <_  z )
109103, 66, 67leadd1d 10158 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( A  <_  z  <->  ( A  +  T )  <_  (
z  +  T ) ) )
110108, 109mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( A  +  T )  <_  (
z  +  T ) )
111107simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  z  <_  B )
11266, 104, 67leadd1d 10158 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  <_  B  <->  ( z  +  T )  <_  ( B  +  T )
) )
113111, 112mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  +  T )  <_  ( B  +  T )
)
11468, 110, 1133jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( (
z  +  T )  e.  RR  /\  ( A  +  T )  <_  ( z  +  T
)  /\  ( z  +  T )  <_  ( B  +  T )
) )
1151143adant3 1016 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( (
z  +  T )  e.  RR  /\  ( A  +  T )  <_  ( z  +  T
)  /\  ( z  +  T )  <_  ( B  +  T )
) )
11683ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( A  +  T )  e.  RR )
11793ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( B  +  T )  e.  RR )
118 elicc2 11601 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR )  ->  ( ( z  +  T )  e.  ( ( A  +  T ) [,] ( B  +  T )
)  <->  ( ( z  +  T )  e.  RR  /\  ( A  +  T )  <_ 
( z  +  T
)  /\  ( z  +  T )  <_  ( B  +  T )
) ) )
119116, 117, 118syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( (
z  +  T )  e.  ( ( A  +  T ) [,] ( B  +  T
) )  <->  ( (
z  +  T )  e.  RR  /\  ( A  +  T )  <_  ( z  +  T
)  /\  ( z  +  T )  <_  ( B  +  T )
) ) )
120115, 119mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( z  +  T )  e.  ( ( A  +  T
) [,] ( B  +  T ) ) )
121101, 120eqeltrd 2555 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
1221213exp 1195 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( z  e.  ( A [,] B )  ->  ( x  =  ( z  +  T
)  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) ) )
123122adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )  ->  (
z  e.  ( A [,] B )  -> 
( x  =  ( z  +  T )  ->  x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) ) ) )
12499, 100, 123rexlimd 2951 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )  ->  ( E. z  e.  ( A [,] B ) x  =  ( z  +  T )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) )
12594, 124mpd 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
126125ex 434 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) )
127126adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  ( ( x  e.  CC  /\  E. z  e.  ( A [,] B ) x  =  ( z  +  T
) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) )
12893, 127mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) )
129128ex 434 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) ) )
13023, 16sseldi 3507 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  CC )
1314adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  RR )
13216, 131resubcld 9999 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  e.  RR )
13323, 1sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  CC )
134133, 24pncand 9943 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
135134eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  =  ( ( A  +  T )  -  T ) )
136135adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  =  ( ( A  +  T )  -  T ) )
137 elicc2 11601 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR )  ->  ( x  e.  ( ( A  +  T ) [,] ( B  +  T )
)  <->  ( x  e.  RR  /\  ( A  +  T )  <_  x  /\  x  <_  ( B  +  T )
) ) )
13812, 13, 137syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  e.  ( ( A  +  T ) [,] ( B  +  T ) )  <->  ( x  e.  RR  /\  ( A  +  T )  <_  x  /\  x  <_  ( B  +  T )
) ) )
13914, 138mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  e.  RR  /\  ( A  +  T
)  <_  x  /\  x  <_  ( B  +  T ) ) )
140139simp2d 1009 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
14112, 16, 131lesub1d 10171 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  <_  x  <->  ( ( A  +  T )  -  T )  <_  (
x  -  T ) ) )
142140, 141mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  -  T )  <_  ( x  -  T ) )
143136, 142eqbrtrd 4473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  <_  ( x  -  T
) )
144139simp3d 1010 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
14516, 13, 131lesub1d 10171 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  <_  ( B  +  T )  <->  ( x  -  T )  <_  (
( B  +  T
)  -  T ) ) )
146144, 145mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  <_  ( ( B  +  T )  -  T ) )
14723, 2sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  CC )
148147, 24pncand 9943 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  +  T )  -  T
)  =  B )
149148adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  -  T )  =  B )
150146, 149breqtrd 4477 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  <_  B )
151132, 143, 1503jca 1176 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  e.  RR  /\  A  <_  ( x  -  T )  /\  (
x  -  T )  <_  B ) )
1521adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  e.  RR )
1532adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  B  e.  RR )
154 elicc2 11601 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( x  -  T )  e.  ( A [,] B )  <-> 
( ( x  -  T )  e.  RR  /\  A  <_  ( x  -  T )  /\  (
x  -  T )  <_  B ) ) )
155152, 153, 154syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  e.  ( A [,] B )  <->  ( (
x  -  T )  e.  RR  /\  A  <_  ( x  -  T
)  /\  ( x  -  T )  <_  B
) ) )
156151, 155mpbird 232 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  e.  ( A [,] B ) )
15724adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  CC )
158130, 157npcand 9946 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  +  T )  =  x )
159158eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  =  ( ( x  -  T )  +  T ) )
160 oveq1 6302 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( x  -  T )  ->  (
z  +  T )  =  ( ( x  -  T )  +  T ) )
161160eqeq2d 2481 . . . . . . . . . . . . . . 15  |-  ( z  =  ( x  -  T )  ->  (
x  =  ( z  +  T )  <->  x  =  ( ( x  -  T )  +  T
) ) )
162161rspcev 3219 . . . . . . . . . . . . . 14  |-  ( ( ( x  -  T
)  e.  ( A [,] B )  /\  x  =  ( (
x  -  T )  +  T ) )  ->  E. z  e.  ( A [,] B ) x  =  ( z  +  T ) )
163156, 159, 162syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) )
164130, 163jca 532 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  e.  CC  /\  E. z  e.  ( A [,] B ) x  =  ( z  +  T ) ) )
165164, 92sylibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )
166165ex 434 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( ( A  +  T
) [,] ( B  +  T ) )  ->  x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } ) )
167129, 166impbid 191 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  <->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) )
16891, 167alrimi 1825 . . . . . . . 8  |-  ( ph  ->  A. x ( x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  <->  x  e.  (
( A  +  T
) [,] ( B  +  T ) ) ) )
169 dfcleq 2460 . . . . . . . 8  |-  ( { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  =  ( ( A  +  T ) [,] ( B  +  T )
)  <->  A. x ( x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  <->  x  e.  (
( A  +  T
) [,] ( B  +  T ) ) ) )
170168, 169sylibr 212 . . . . . . 7  |-  ( ph  ->  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  =  ( ( A  +  T ) [,] ( B  +  T
) ) )
171170reseq2d 5279 . . . . . 6  |-  ( ph  ->  ( F  |`  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } )  =  ( F  |`  ( ( A  +  T ) [,] ( B  +  T
) ) ) )
172170, 87eqsstr3d 3544 . . . . . . 7  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  C_  dom  F )
17364, 172feqresmpt 5928 . . . . . 6  |-  ( ph  ->  ( F  |`  (
( A  +  T
) [,] ( B  +  T ) ) )  =  ( x  e.  ( ( A  +  T ) [,] ( B  +  T
) )  |->  ( F `
 x ) ) )
174171, 173eqtr2d 2509 . . . . 5  |-  ( ph  ->  ( x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) 
|->  ( F `  x
) )  =  ( F  |`  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } ) )
1751, 2, 4iccshift 31445 . . . . . 6  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  =  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } )
176175oveq1d 6310 . . . . 5  |-  ( ph  ->  ( ( ( A  +  T ) [,] ( B  +  T
) ) -cn-> CC )  =  ( { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } -cn-> CC ) )
177174, 176eleq12d 2549 . . . 4  |-  ( ph  ->  ( ( x  e.  ( ( A  +  T ) [,] ( B  +  T )
)  |->  ( F `  x ) )  e.  ( ( ( A  +  T ) [,] ( B  +  T
) ) -cn-> CC )  <-> 
( F  |`  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } )  e.  ( { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }
-cn-> CC ) ) )
17890, 177mpbird 232 . . 3  |-  ( ph  ->  ( x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) 
|->  ( F `  x
) )  e.  ( ( ( A  +  T ) [,] ( B  +  T )
) -cn-> CC ) )
179 ax-1cn 9562 . . . . . . 7  |-  1  e.  CC
180179a1i 11 . . . . . 6  |-  ( ph  ->  1  e.  CC )
181 ioosscn 31414 . . . . . . 7  |-  ( A (,) B )  C_  CC
182181a1i 11 . . . . . 6  |-  ( ph  ->  ( A (,) B
)  C_  CC )
183 ssid 3528 . . . . . . 7  |-  CC  C_  CC
184183a1i 11 . . . . . 6  |-  ( ph  ->  CC  C_  CC )
185 cncfmptc 21283 . . . . . 6  |-  ( ( 1  e.  CC  /\  ( A (,) B ) 
C_  CC  /\  CC  C_  CC )  ->  ( y  e.  ( A (,) B )  |->  1 )  e.  ( ( A (,) B ) -cn-> CC ) )
186180, 182, 184, 185syl3anc 1228 . . . . 5  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  e.  ( ( A (,) B
) -cn-> CC ) )
187 fconstmpt 5049 . . . . . . . 8  |-  ( ( A (,) B )  X.  { 1 } )  =  ( y  e.  ( A (,) B )  |->  1 )
188187eqcomi 2480 . . . . . . 7  |-  ( y  e.  ( A (,) B )  |->  1 )  =  ( ( A (,) B )  X. 
{ 1 } )
189188a1i 11 . . . . . 6  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  =  ( ( A (,) B
)  X.  { 1 } ) )
190 ioombl 21843 . . . . . . . 8  |-  ( A (,) B )  e. 
dom  vol
191190a1i 11 . . . . . . 7  |-  ( ph  ->  ( A (,) B
)  e.  dom  vol )
192 ioovolcl 21847 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A (,) B ) )  e.  RR )
1931, 2, 192syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( vol `  ( A (,) B ) )  e.  RR )
194 iblconst 22092 . . . . . . 7  |-  ( ( ( A (,) B
)  e.  dom  vol  /\  ( vol `  ( A (,) B ) )  e.  RR  /\  1  e.  CC )  ->  (
( A (,) B
)  X.  { 1 } )  e.  L^1 )
195191, 193, 180, 194syl3anc 1228 . . . . . 6  |-  ( ph  ->  ( ( A (,) B )  X.  {
1 } )  e.  L^1 )
196189, 195eqeltrd 2555 . . . . 5  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  e.  L^1 )
197186, 196jca 532 . . . 4  |-  ( ph  ->  ( ( y  e.  ( A (,) B
)  |->  1 )  e.  ( ( A (,) B ) -cn-> CC )  /\  ( y  e.  ( A (,) B
)  |->  1 )  e.  L^1 ) )
198 elin 3692 . . . 4  |-  ( ( y  e.  ( A (,) B )  |->  1 )  e.  ( ( ( A (,) B
) -cn-> CC )  i^i  L^1 )  <->  ( ( y  e.  ( A (,) B )  |->  1 )  e.  ( ( A (,) B ) -cn-> CC )  /\  ( y  e.  ( A (,) B )  |->  1 )  e.  L^1 ) )
199197, 198sylibr 212 . . 3  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  e.  ( ( ( A (,) B ) -cn-> CC )  i^i  L^1 ) )
200 resmpt 5329 . . . . . . . 8  |-  ( ( A [,] B ) 
C_  RR  ->  ( ( y  e.  RR  |->  ( y  +  T ) )  |`  ( A [,] B ) )  =  ( y  e.  ( A [,] B ) 
|->  ( y  +  T
) ) )
20128, 200syl 16 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  RR  |->  ( y  +  T ) )  |`  ( A [,] B ) )  =  ( y  e.  ( A [,] B )  |->  ( y  +  T ) ) )
202201eqcomd 2475 . . . . . 6  |-  ( ph  ->  ( y  e.  ( A [,] B ) 
|->  ( y  +  T
) )  =  ( ( y  e.  RR  |->  ( y  +  T
) )  |`  ( A [,] B ) ) )
203202oveq2d 6311 . . . . 5  |-  ( ph  ->  ( RR  _D  (
y  e.  ( A [,] B )  |->  ( y  +  T ) ) )  =  ( RR  _D  ( ( y  e.  RR  |->  ( y  +  T ) )  |`  ( A [,] B ) ) ) )
20432sselda 3509 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
20524adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR )  ->  T  e.  CC )
206204, 205addcld 9627 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  T )  e.  CC )
207 eqid 2467 . . . . . . . 8  |-  ( y  e.  RR  |->  ( y  +  T ) )  =  ( y  e.  RR  |->  ( y  +  T ) )
208206, 207fmptd 6056 . . . . . . 7  |-  ( ph  ->  ( y  e.  RR  |->  ( y  +  T
) ) : RR --> CC )
20932, 208jca 532 . . . . . 6  |-  ( ph  ->  ( RR  C_  CC  /\  ( y  e.  RR  |->  ( y  +  T
) ) : RR --> CC ) )
210 ssid 3528 . . . . . . . 8  |-  RR  C_  RR
211210a1i 11 . . . . . . 7  |-  ( ph  ->  RR  C_  RR )
212211, 28jca 532 . . . . . 6  |-  ( ph  ->  ( RR  C_  RR  /\  ( A [,] B
)  C_  RR )
)
213 eqid 2467 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
214213tgioo2 21176 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
215213, 214dvres 22183 . . . . . 6  |-  ( ( ( RR  C_  CC  /\  ( y  e.  RR  |->  ( y  +  T
) ) : RR --> CC )  /\  ( RR  C_  RR  /\  ( A [,] B )  C_  RR ) )  ->  ( RR  _D  ( ( y  e.  RR  |->  ( y  +  T ) )  |`  ( A [,] B
) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
216209, 212, 215syl2anc 661 . . . . 5  |-  ( ph  ->  ( RR  _D  (
( y  e.  RR  |->  ( y  +  T
) )  |`  ( A [,] B ) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T ) ) )  |`  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) ) ) )
217203, 216eqtrd 2508 . . . 4  |-  ( ph  ->  ( RR  _D  (
y  e.  ( A [,] B )  |->  ( y  +  T ) ) )  =  ( ( RR  _D  (
y  e.  RR  |->  ( y  +  T ) ) )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
218 iccntr 21194 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
2191, 2, 218syl2anc 661 . . . . 5  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
220219reseq2d 5279 . . . 4  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  =  ( ( RR 
_D  ( y  e.  RR  |->  ( y  +  T ) ) )  |`  ( A (,) B
) ) )
221 reex 9595 . . . . . . . . 9  |-  RR  e.  _V
222221prid1 4141 . . . . . . . 8  |-  RR  e.  { RR ,  CC }
223222a1i 11 . . . . . . 7  |-  ( ph  ->  RR  e.  { RR ,  CC } )
224179a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  1  e.  CC )
225223dvmptid 22228 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  y ) )  =  ( y  e.  RR  |->  1 ) )
226 0cn 9600 . . . . . . . 8  |-  0  e.  CC
227226a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  0  e.  CC )
228223, 24dvmptc 22229 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  T ) )  =  ( y  e.  RR  |->  0 ) )
229223, 204, 224, 225, 205, 227, 228dvmptadd 22231 . . . . . 6  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( y  +  T ) ) )  =  ( y  e.  RR  |->  ( 1  +  0 ) ) )
230229reseq1d 5278 . . . . 5  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( A (,) B ) )  =  ( ( y  e.  RR  |->  ( 1  +  0 ) )  |`  ( A (,) B ) ) )
231 ioossre 11598 . . . . . . 7  |-  ( A (,) B )  C_  RR
232231a1i 11 . . . . . 6  |-  ( ph  ->  ( A (,) B
)  C_  RR )
233 resmpt 5329 . . . . . 6  |-  ( ( A (,) B ) 
C_  RR  ->  ( ( y  e.  RR  |->  ( 1  +  0 ) )  |`  ( A (,) B ) )  =  ( y  e.  ( A (,) B ) 
|->  ( 1  +  0 ) ) )
234232, 233syl 16 . . . . 5  |-  ( ph  ->  ( ( y  e.  RR  |->  ( 1  +  0 ) )  |`  ( A (,) B ) )  =  ( y  e.  ( A (,) B )  |->  ( 1  +  0 ) ) )
235179addid1i 9778 . . . . . . 7  |-  ( 1  +  0 )  =  1
236235mpteq2i 4536 . . . . . 6  |-  ( y  e.  ( A (,) B )  |->  ( 1  +  0 ) )  =  ( y  e.  ( A (,) B
)  |->  1 )
237236a1i 11 . . . . 5  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  ( 1  +  0 ) )  =  ( y  e.  ( A (,) B )  |->  1 ) )
238230, 234, 2373eqtrd 2512 . . . 4  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( A (,) B ) )  =  ( y  e.  ( A (,) B )  |->  1 ) )
239217, 220, 2383eqtrd 2512 . . 3  |-  ( ph  ->  ( RR  _D  (
y  e.  ( A [,] B )  |->  ( y  +  T ) ) )  =  ( y  e.  ( A (,) B )  |->  1 ) )
240 fveq2 5872 . . 3  |-  ( x  =  ( y  +  T )  ->  ( F `  x )  =  ( F `  ( y  +  T
) ) )
241 oveq1 6302 . . 3  |-  ( y  =  A  ->  (
y  +  T )  =  ( A  +  T ) )
242 oveq1 6302 . . 3  |-  ( y  =  B  ->  (
y  +  T )  =  ( B  +  T ) )
2431, 2, 5, 53, 178, 199, 239, 240, 241, 242, 8, 9itgsubsticc 31617 . 2  |-  ( ph  ->  S__ [ ( A  +  T )  -> 
( B  +  T
) ] ( F `
 x )  _d x  =  S__ [ A  ->  B ] ( ( F `  (
y  +  T ) )  x.  1 )  _d y )
2445ditgpos 22128 . . 3  |-  ( ph  ->  S__ [ A  ->  B ] ( ( F `
 ( y  +  T ) )  x.  1 )  _d y  =  S. ( A (,) B ) ( ( F `  (
y  +  T ) )  x.  1 )  _d y )
24510adantr 465 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  F : RR
--> CC )
246 ffvelrn 6030 . . . . . 6  |-  ( ( F : RR --> CC  /\  ( y  +  T
)  e.  RR )  ->  ( F `  ( y  +  T
) )  e.  CC )
247245, 36, 246syl2anc 661 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  ( y  +  T
) )  e.  CC )
248179a1i 11 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  1  e.  CC )
249247, 248mulcld 9628 . . . 4  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( ( F `  ( y  +  T ) )  x.  1 )  e.  CC )
2501, 2, 249itgioo 22090 . . 3  |-  ( ph  ->  S. ( A (,) B ) ( ( F `  ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( ( F `  ( y  +  T
) )  x.  1 )  _d y )
251 oveq1 6302 . . . . . . . 8  |-  ( y  =  x  ->  (
y  +  T )  =  ( x  +  T ) )
252251fveq2d 5876 . . . . . . 7  |-  ( y  =  x  ->  ( F `  ( y  +  T ) )  =  ( F `  (
x  +  T ) ) )
253252oveq1d 6310 . . . . . 6  |-  ( y  =  x  ->  (
( F `  (
y  +  T ) )  x.  1 )  =  ( ( F `
 ( x  +  T ) )  x.  1 ) )
254 nfcv 2629 . . . . . 6  |-  F/_ x
( ( F `  ( y  +  T
) )  x.  1 )
255 nfcv 2629 . . . . . 6  |-  F/_ y
( ( F `  ( x  +  T
) )  x.  1 )
256253, 254, 255cbvitg 22050 . . . . 5  |-  S. ( A [,] B ) ( ( F `  ( y  +  T
) )  x.  1 )  _d y  =  S. ( A [,] B ) ( ( F `  ( x  +  T ) )  x.  1 )  _d x
257256a1i 11 . . . 4  |-  ( ph  ->  S. ( A [,] B ) ( ( F `  ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( ( F `  ( x  +  T
) )  x.  1 )  _d x )
25810adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  F : RR
--> CC )
25928sselda 3509 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  x  e.  RR )
2604adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  T  e.  RR )
261259, 260readdcld 9635 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( x  +  T )  e.  RR )
262258, 261ffvelrnd 6033 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  e.  CC )
263262mulid1d 9625 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( ( F `  ( x  +  T ) )  x.  1 )  =  ( F `  ( x  +  T ) ) )
264263, 88eqtrd 2508 . . . . 5  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( ( F `  ( x  +  T ) )  x.  1 )  =  ( F `  x ) )
265264itgeq2dv 22056 . . . 4  |-  ( ph  ->  S. ( A [,] B ) ( ( F `  ( x  +  T ) )  x.  1 )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
266257, 265eqtrd 2508 . . 3  |-  ( ph  ->  S. ( A [,] B ) ( ( F `  ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( F `  x
)  _d x )
267244, 250, 2663eqtrd 2512 . 2  |-  ( ph  ->  S__ [ A  ->  B ] ( ( F `
 ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( F `  x )  _d x )
26821, 243, 2673eqtrd 2512 1  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973   A.wal 1377    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818   {crab 2821    i^i cin 3480    C_ wss 3481   {csn 4033   {cpr 4035   class class class wbr 4453    |-> cmpt 4511    X. cxp 5003   dom cdm 5005   ran crn 5006    |` cres 5007   -->wf 5590   ` cfv 5594  (class class class)co 6295   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505    + caddc 9507    x. cmul 9509    <_ cle 9641    - cmin 9817   RR+crp 11232   (,)cioo 11541   [,]cicc 11544   TopOpenctopn 14694   topGenctg 14710  ℂfldccnfld 18290   intcnt 19386   -cn->ccncf 21248   volcvol 21743   L^1cibl 21894   S.citg 21895   S__cdit 22118    _D cdv 22135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cc 8827  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-disj 4424  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-ofr 6536  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-omul 7147  df-er 7323  df-map 7434  df-pm 7435  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-acn 8335  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-mod 11977  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-limsup 13274  df-clim 13291  df-rlim 13292  df-sum 13489  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-fbas 18286  df-fg 18287  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-perf 19506  df-cn 19596  df-cnp 19597  df-haus 19684  df-cmp 19755  df-tx 19931  df-hmeo 20124  df-fil 20215  df-fm 20307  df-flim 20308  df-flf 20309  df-xms 20691  df-ms 20692  df-tms 20693  df-cncf 21250  df-ovol 21744  df-vol 21745  df-mbf 21896  df-itg1 21897  df-itg2 21898  df-ibl 21899  df-itg 21900  df-0p 21945  df-ditg 22119  df-limc 22138  df-dv 22139
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator