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

Theorem itgperiod 37798
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 11348 . . . . 5  |-  ( ph  ->  T  e.  RR )
5 itgperiod.aleb . . . . 5  |-  ( ph  ->  A  <_  B )
61, 2, 4, 5leadd1dd 10234 . . . 4  |-  ( ph  ->  ( A  +  T
)  <_  ( B  +  T ) )
76ditgpos 22809 . . 3  |-  ( ph  ->  S__ [ ( A  +  T )  -> 
( B  +  T
) ] ( F `
 x )  _d x  =  S. ( ( A  +  T
) (,) ( B  +  T ) ) ( F `  x
)  _d x )
81, 4readdcld 9677 . . . 4  |-  ( ph  ->  ( A  +  T
)  e.  RR )
92, 4readdcld 9677 . . . 4  |-  ( ph  ->  ( B  +  T
)  e.  RR )
10 itgperiod.f . . . . . 6  |-  ( ph  ->  F : RR --> CC )
1110adantr 466 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  F : RR --> CC )
128adantr 466 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  e.  RR )
139adantr 466 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( B  +  T )  e.  RR )
14 simpr 462 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
15 eliccre 37552 . . . . . 6  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T
) ) )  ->  x  e.  RR )
1612, 13, 14, 15syl3anc 1264 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  RR )
1711, 16ffvelrnd 6038 . . . 4  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( F `  x )  e.  CC )
188, 9, 17itgioo 22771 . . 3  |-  ( ph  ->  S. ( ( A  +  T ) (,) ( B  +  T
) ) ( F `
 x )  _d x  =  S. ( ( A  +  T
) [,] ( B  +  T ) ) ( F `  x
)  _d x )
197, 18eqtr2d 2464 . 2  |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T
) ) ( F `
 x )  _d x  =  S__ [
( A  +  T
)  ->  ( B  +  T ) ] ( F `  x )  _d x )
20 eqid 2422 . . . 4  |-  ( y  e.  CC  |->  ( y  +  T ) )  =  ( y  e.  CC  |->  ( y  +  T ) )
214recnd 9676 . . . . 5  |-  ( ph  ->  T  e.  CC )
2220addccncf 21946 . . . . 5  |-  ( T  e.  CC  ->  (
y  e.  CC  |->  ( y  +  T ) )  e.  ( CC
-cn-> CC ) )
2321, 22syl 17 . . . 4  |-  ( ph  ->  ( y  e.  CC  |->  ( y  +  T
) )  e.  ( CC -cn-> CC ) )
241, 2iccssred 37551 . . . . 5  |-  ( ph  ->  ( A [,] B
)  C_  RR )
25 ax-resscn 9603 . . . . 5  |-  RR  C_  CC
2624, 25syl6ss 3476 . . . 4  |-  ( ph  ->  ( A [,] B
)  C_  CC )
278, 9iccssred 37551 . . . . 5  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  C_  RR )
2827, 25syl6ss 3476 . . . 4  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  C_  CC )
298adantr 466 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( A  +  T )  e.  RR )
309adantr 466 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( B  +  T )  e.  RR )
3124sselda 3464 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  RR )
324adantr 466 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  T  e.  RR )
3331, 32readdcld 9677 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  +  T )  e.  RR )
341adantr 466 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  A  e.  RR )
35 simpr 462 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  ( A [,] B ) )
362adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  B  e.  RR )
37 elicc2 11706 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( y  e.  ( A [,] B )  <-> 
( y  e.  RR  /\  A  <_  y  /\  y  <_  B ) ) )
3834, 36, 37syl2anc 665 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  e.  ( A [,] B
)  <->  ( y  e.  RR  /\  A  <_ 
y  /\  y  <_  B ) ) )
3935, 38mpbid 213 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  e.  RR  /\  A  <_ 
y  /\  y  <_  B ) )
4039simp2d 1018 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  A  <_  y )
4134, 31, 32, 40leadd1dd 10234 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( A  +  T )  <_  (
y  +  T ) )
4239simp3d 1019 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  <_  B )
4331, 36, 32, 42leadd1dd 10234 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  +  T )  <_  ( B  +  T )
)
4429, 30, 33, 41, 43eliccd 37550 . . . 4  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  +  T )  e.  ( ( A  +  T
) [,] ( B  +  T ) ) )
4520, 23, 26, 28, 44cncfmptssg 37687 . . 3  |-  ( ph  ->  ( y  e.  ( A [,] B ) 
|->  ( y  +  T
) )  e.  ( ( A [,] B
) -cn-> ( ( A  +  T ) [,] ( B  +  T
) ) ) )
46 eqeq1 2426 . . . . . . . 8  |-  ( w  =  x  ->  (
w  =  ( z  +  T )  <->  x  =  ( z  +  T
) ) )
4746rexbidv 2936 . . . . . . 7  |-  ( w  =  x  ->  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  <->  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )
48 oveq1 6312 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  +  T )  =  ( y  +  T ) )
4948eqeq2d 2436 . . . . . . . 8  |-  ( z  =  y  ->  (
x  =  ( z  +  T )  <->  x  =  ( y  +  T
) ) )
5049cbvrexv 3055 . . . . . . 7  |-  ( E. z  e.  ( A [,] B ) x  =  ( z  +  T )  <->  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) )
5147, 50syl6bb 264 . . . . . 6  |-  ( w  =  x  ->  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  <->  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) ) )
5251cbvrabv 3079 . . . . 5  |-  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  =  { x  e.  CC  |  E. y  e.  ( A [,] B
) x  =  ( y  +  T ) }
53 ffdm 5760 . . . . . . 7  |-  ( F : RR --> CC  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
5410, 53syl 17 . . . . . 6  |-  ( ph  ->  ( F : dom  F --> CC  /\  dom  F  C_  RR ) )
5554simpld 460 . . . . 5  |-  ( ph  ->  F : dom  F --> CC )
56 simp3 1007 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  w  =  ( z  +  T ) )  ->  w  =  ( z  +  T
) )
5724sselda 3464 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  z  e.  RR )
584adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  T  e.  RR )
5957, 58readdcld 9677 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  +  T )  e.  RR )
60593adant3 1025 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  w  =  ( z  +  T ) )  ->  ( z  +  T )  e.  RR )
6156, 60eqeltrd 2507 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  w  =  ( z  +  T ) )  ->  w  e.  RR )
6261rexlimdv3a 2916 . . . . . . . 8  |-  ( ph  ->  ( E. z  e.  ( A [,] B
) w  =  ( z  +  T )  ->  w  e.  RR ) )
6362ralrimivw 2837 . . . . . . 7  |-  ( ph  ->  A. w  e.  CC  ( E. z  e.  ( A [,] B ) w  =  ( z  +  T )  ->  w  e.  RR )
)
64 rabss 3538 . . . . . . 7  |-  ( { 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 )
)
6563, 64sylibr 215 . . . . . 6  |-  ( ph  ->  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } 
C_  RR )
66 fdm 5750 . . . . . . 7  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
6710, 66syl 17 . . . . . 6  |-  ( ph  ->  dom  F  =  RR )
6865, 67sseqtr4d 3501 . . . . 5  |-  ( ph  ->  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } 
C_  dom  F )
69 itgperiod.fper . . . . 5  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
70 itgperiod.fcn . . . . 5  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> CC ) )
7126, 4, 52, 55, 68, 69, 70cncfperiod 37696 . . . 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 ) )
7247elrab 3228 . . . . . . . . 9  |-  ( x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) }  <->  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )
73 simprr 764 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )  ->  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) )
74 nfv 1755 . . . . . . . . . . . 12  |-  F/ z
ph
75 nfv 1755 . . . . . . . . . . . . 13  |-  F/ z  x  e.  CC
76 nfre1 2883 . . . . . . . . . . . . 13  |-  F/ z E. z  e.  ( A [,] B ) x  =  ( z  +  T )
7775, 76nfan 1988 . . . . . . . . . . . 12  |-  F/ z ( x  e.  CC  /\ 
E. z  e.  ( A [,] B ) x  =  ( z  +  T ) )
7874, 77nfan 1988 . . . . . . . . . . 11  |-  F/ z ( ph  /\  (
x  e.  CC  /\  E. z  e.  ( A [,] B ) x  =  ( z  +  T ) ) )
79 nfv 1755 . . . . . . . . . . 11  |-  F/ z  x  e.  ( ( A  +  T ) [,] ( B  +  T ) )
80 simp3 1007 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  x  =  ( z  +  T
) )
811adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  A  e.  RR )
82 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( A [,] B ) )
832adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  B  e.  RR )
84 elicc2 11706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( z  e.  ( A [,] B )  <-> 
( z  e.  RR  /\  A  <_  z  /\  z  <_  B ) ) )
8581, 83, 84syl2anc 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  e.  ( A [,] B
)  <->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) ) )
8682, 85mpbid 213 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) )
8786simp2d 1018 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  A  <_  z )
8881, 57, 58, 87leadd1dd 10234 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( A  +  T )  <_  (
z  +  T ) )
8986simp3d 1019 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  z  <_  B )
9057, 83, 58, 89leadd1dd 10234 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( z  +  T )  <_  ( B  +  T )
)
9159, 88, 903jca 1185 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( (
z  +  T )  e.  RR  /\  ( A  +  T )  <_  ( z  +  T
)  /\  ( z  +  T )  <_  ( B  +  T )
) )
92913adant3 1025 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( (
z  +  T )  e.  RR  /\  ( A  +  T )  <_  ( z  +  T
)  /\  ( z  +  T )  <_  ( B  +  T )
) )
9383ad2ant1 1026 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( A  +  T )  e.  RR )
9493ad2ant1 1026 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( B  +  T )  e.  RR )
95 elicc2 11706 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
) ) )
9693, 94, 95syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( (
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 )
) ) )
9792, 96mpbird 235 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  ( z  +  T )  e.  ( ( A  +  T
) [,] ( B  +  T ) ) )
9880, 97eqeltrd 2507 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  ( A [,] B )  /\  x  =  ( z  +  T ) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
99983exp 1204 . . . . . . . . . . . 12  |-  ( ph  ->  ( z  e.  ( A [,] B )  ->  ( x  =  ( z  +  T
)  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) ) )
10099adantr 466 . . . . . . . . . . 11  |-  ( (
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 ) ) ) ) )
10178, 79, 100rexlimd 2906 . . . . . . . . . 10  |-  ( (
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 )
) ) )
10273, 101mpd 15 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  CC  /\  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) ) )  ->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )
10372, 102sylan2b 477 . . . . . . . 8  |-  ( (
ph  /\  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )  ->  x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) )
10416recnd 9676 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  CC )
1051adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  e.  RR )
1062adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  B  e.  RR )
1074adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  RR )
10816, 107resubcld 10054 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  e.  RR )
1091recnd 9676 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  CC )
110109, 21pncand 9994 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  +  T )  -  T
)  =  A )
111110eqcomd 2430 . . . . . . . . . . . . 13  |-  ( ph  ->  A  =  ( ( A  +  T )  -  T ) )
112111adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  =  ( ( A  +  T )  -  T ) )
113 elicc2 11706 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  +  T
)  e.  RR  /\  ( B  +  T
)  e.  RR )  ->  ( x  e.  ( ( A  +  T ) [,] ( B  +  T )
)  <->  ( x  e.  RR  /\  ( A  +  T )  <_  x  /\  x  <_  ( B  +  T )
) ) )
11412, 13, 113syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  e.  ( ( A  +  T ) [,] ( B  +  T ) )  <->  ( x  e.  RR  /\  ( A  +  T )  <_  x  /\  x  <_  ( B  +  T )
) ) )
11514, 114mpbid 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  e.  RR  /\  ( A  +  T
)  <_  x  /\  x  <_  ( B  +  T ) ) )
116115simp2d 1018 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  ( A  +  T )  <_  x )
11712, 16, 107, 116lesub1dd 10236 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( A  +  T
)  -  T )  <_  ( x  -  T ) )
118112, 117eqbrtrd 4444 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  A  <_  ( x  -  T
) )
119115simp3d 1019 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  <_  ( B  +  T
) )
12016, 13, 107, 119lesub1dd 10236 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  <_  ( ( B  +  T )  -  T ) )
1212recnd 9676 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  CC )
122121, 21pncand 9994 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  +  T )  -  T
)  =  B )
123122adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( B  +  T
)  -  T )  =  B )
124120, 123breqtrd 4448 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  <_  B )
125105, 106, 108, 118, 124eliccd 37550 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
x  -  T )  e.  ( A [,] B ) )
12621adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  T  e.  CC )
127104, 126npcand 9997 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  (
( x  -  T
)  +  T )  =  x )
128127eqcomd 2430 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  =  ( ( x  -  T )  +  T ) )
129 oveq1 6312 . . . . . . . . . . . 12  |-  ( z  =  ( x  -  T )  ->  (
z  +  T )  =  ( ( x  -  T )  +  T ) )
130129eqeq2d 2436 . . . . . . . . . . 11  |-  ( z  =  ( x  -  T )  ->  (
x  =  ( z  +  T )  <->  x  =  ( ( x  -  T )  +  T
) ) )
131130rspcev 3182 . . . . . . . . . 10  |-  ( ( ( x  -  T
)  e.  ( A [,] B )  /\  x  =  ( (
x  -  T )  +  T ) )  ->  E. z  e.  ( A [,] B ) x  =  ( z  +  T ) )
132125, 128, 131syl2anc 665 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  E. z  e.  ( A [,] B
) x  =  ( z  +  T ) )
133104, 132, 72sylanbrc 668 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) )  ->  x  e.  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) } )
134103, 133impbida 840 . . . . . . 7  |-  ( ph  ->  ( x  e.  {
w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  <->  x  e.  ( ( A  +  T ) [,] ( B  +  T )
) ) )
135134eqrdv 2419 . . . . . 6  |-  ( ph  ->  { w  e.  CC  |  E. z  e.  ( A [,] B ) w  =  ( z  +  T ) }  =  ( ( A  +  T ) [,] ( B  +  T
) ) )
136135reseq2d 5124 . . . . 5  |-  ( ph  ->  ( F  |`  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } )  =  ( F  |`  ( ( A  +  T ) [,] ( B  +  T
) ) ) )
137135, 68eqsstr3d 3499 . . . . . 6  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  C_  dom  F )
13855, 137feqresmpt 5935 . . . . 5  |-  ( ph  ->  ( F  |`  (
( A  +  T
) [,] ( B  +  T ) ) )  =  ( x  e.  ( ( A  +  T ) [,] ( B  +  T
) )  |->  ( F `
 x ) ) )
139136, 138eqtr2d 2464 . . . 4  |-  ( ph  ->  ( x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) 
|->  ( F `  x
) )  =  ( F  |`  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } ) )
1401, 2, 4iccshift 37568 . . . . 5  |-  ( ph  ->  ( ( A  +  T ) [,] ( B  +  T )
)  =  { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } )
141140oveq1d 6320 . . . 4  |-  ( ph  ->  ( ( ( A  +  T ) [,] ( B  +  T
) ) -cn-> CC )  =  ( { w  e.  CC  |  E. z  e.  ( A [,] B
) w  =  ( z  +  T ) } -cn-> CC ) )
14271, 139, 1413eltr4d 2522 . . 3  |-  ( ph  ->  ( x  e.  ( ( A  +  T
) [,] ( B  +  T ) ) 
|->  ( F `  x
) )  e.  ( ( ( A  +  T ) [,] ( B  +  T )
) -cn-> CC ) )
143 ioosscn 37540 . . . . . 6  |-  ( A (,) B )  C_  CC
144143a1i 11 . . . . 5  |-  ( ph  ->  ( A (,) B
)  C_  CC )
145 1cnd 9666 . . . . 5  |-  ( ph  ->  1  e.  CC )
146 ssid 3483 . . . . . 6  |-  CC  C_  CC
147146a1i 11 . . . . 5  |-  ( ph  ->  CC  C_  CC )
148144, 145, 147constcncfg 37688 . . . 4  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  e.  ( ( A (,) B
) -cn-> CC ) )
149 fconstmpt 4897 . . . . 5  |-  ( ( A (,) B )  X.  { 1 } )  =  ( y  e.  ( A (,) B )  |->  1 )
150 ioombl 22516 . . . . . . 7  |-  ( A (,) B )  e. 
dom  vol
151150a1i 11 . . . . . 6  |-  ( ph  ->  ( A (,) B
)  e.  dom  vol )
152 ioovolcl 22520 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A (,) B ) )  e.  RR )
1531, 2, 152syl2anc 665 . . . . . 6  |-  ( ph  ->  ( vol `  ( A (,) B ) )  e.  RR )
154 iblconst 22773 . . . . . 6  |-  ( ( ( A (,) B
)  e.  dom  vol  /\  ( vol `  ( A (,) B ) )  e.  RR  /\  1  e.  CC )  ->  (
( A (,) B
)  X.  { 1 } )  e.  L^1 )
155151, 153, 145, 154syl3anc 1264 . . . . 5  |-  ( ph  ->  ( ( A (,) B )  X.  {
1 } )  e.  L^1 )
156149, 155syl5eqelr 2512 . . . 4  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  e.  L^1 )
157148, 156elind 3650 . . 3  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  1 )  e.  ( ( ( A (,) B ) -cn-> CC )  i^i  L^1 ) )
15824resmptd 5175 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  RR  |->  ( y  +  T ) )  |`  ( A [,] B ) )  =  ( y  e.  ( A [,] B )  |->  ( y  +  T ) ) )
159158eqcomd 2430 . . . . . 6  |-  ( ph  ->  ( y  e.  ( A [,] B ) 
|->  ( y  +  T
) )  =  ( ( y  e.  RR  |->  ( y  +  T
) )  |`  ( A [,] B ) ) )
160159oveq2d 6321 . . . . 5  |-  ( ph  ->  ( RR  _D  (
y  e.  ( A [,] B )  |->  ( y  +  T ) ) )  =  ( RR  _D  ( ( y  e.  RR  |->  ( y  +  T ) )  |`  ( A [,] B ) ) ) )
16125a1i 11 . . . . . 6  |-  ( ph  ->  RR  C_  CC )
162161sselda 3464 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  CC )
16321adantr 466 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  T  e.  CC )
164162, 163addcld 9669 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  T )  e.  CC )
165 eqid 2422 . . . . . . 7  |-  ( y  e.  RR  |->  ( y  +  T ) )  =  ( y  e.  RR  |->  ( y  +  T ) )
166164, 165fmptd 6061 . . . . . 6  |-  ( ph  ->  ( y  e.  RR  |->  ( y  +  T
) ) : RR --> CC )
167 ssid 3483 . . . . . . 7  |-  RR  C_  RR
168167a1i 11 . . . . . 6  |-  ( ph  ->  RR  C_  RR )
169 eqid 2422 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
170169tgioo2 21819 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
171169, 170dvres 22864 . . . . . 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 ) ) ) )
172161, 166, 168, 24, 171syl22anc 1265 . . . . 5  |-  ( ph  ->  ( RR  _D  (
( y  e.  RR  |->  ( y  +  T
) )  |`  ( A [,] B ) ) )  =  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T ) ) )  |`  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A [,] B ) ) ) )
173160, 172eqtrd 2463 . . . 4  |-  ( ph  ->  ( RR  _D  (
y  e.  ( A [,] B )  |->  ( y  +  T ) ) )  =  ( ( RR  _D  (
y  e.  RR  |->  ( y  +  T ) ) )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) ) )
174 iccntr 21837 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
1751, 2, 174syl2anc 665 . . . . 5  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) )  =  ( A (,) B
) )
176175reseq2d 5124 . . . 4  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A [,] B ) ) )  =  ( ( RR 
_D  ( y  e.  RR  |->  ( y  +  T ) ) )  |`  ( A (,) B
) ) )
177 reelprrecn 9638 . . . . . . . 8  |-  RR  e.  { RR ,  CC }
178177a1i 11 . . . . . . 7  |-  ( ph  ->  RR  e.  { RR ,  CC } )
179 1cnd 9666 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  1  e.  CC )
180178dvmptid 22909 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  y ) )  =  ( y  e.  RR  |->  1 ) )
181 0cnd 9643 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  0  e.  CC )
182178, 21dvmptc 22910 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  T ) )  =  ( y  e.  RR  |->  0 ) )
183178, 162, 179, 180, 163, 181, 182dvmptadd 22912 . . . . . 6  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( y  +  T ) ) )  =  ( y  e.  RR  |->  ( 1  +  0 ) ) )
184183reseq1d 5123 . . . . 5  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( A (,) B ) )  =  ( ( y  e.  RR  |->  ( 1  +  0 ) )  |`  ( A (,) B ) ) )
185 ioossre 11703 . . . . . . 7  |-  ( A (,) B )  C_  RR
186185a1i 11 . . . . . 6  |-  ( ph  ->  ( A (,) B
)  C_  RR )
187186resmptd 5175 . . . . 5  |-  ( ph  ->  ( ( y  e.  RR  |->  ( 1  +  0 ) )  |`  ( A (,) B ) )  =  ( y  e.  ( A (,) B )  |->  ( 1  +  0 ) ) )
188 1p0e1 10729 . . . . . . 7  |-  ( 1  +  0 )  =  1
189188mpteq2i 4507 . . . . . 6  |-  ( y  e.  ( A (,) B )  |->  ( 1  +  0 ) )  =  ( y  e.  ( A (,) B
)  |->  1 )
190189a1i 11 . . . . 5  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  ( 1  +  0 ) )  =  ( y  e.  ( A (,) B )  |->  1 ) )
191184, 187, 1903eqtrd 2467 . . . 4  |-  ( ph  ->  ( ( RR  _D  ( y  e.  RR  |->  ( y  +  T
) ) )  |`  ( A (,) B ) )  =  ( y  e.  ( A (,) B )  |->  1 ) )
192173, 176, 1913eqtrd 2467 . . 3  |-  ( ph  ->  ( RR  _D  (
y  e.  ( A [,] B )  |->  ( y  +  T ) ) )  =  ( y  e.  ( A (,) B )  |->  1 ) )
193 fveq2 5881 . . 3  |-  ( x  =  ( y  +  T )  ->  ( F `  x )  =  ( F `  ( y  +  T
) ) )
194 oveq1 6312 . . 3  |-  ( y  =  A  ->  (
y  +  T )  =  ( A  +  T ) )
195 oveq1 6312 . . 3  |-  ( y  =  B  ->  (
y  +  T )  =  ( B  +  T ) )
1961, 2, 5, 45, 142, 157, 192, 193, 194, 195, 8, 9itgsubsticc 37793 . 2  |-  ( ph  ->  S__ [ ( A  +  T )  -> 
( B  +  T
) ] ( F `
 x )  _d x  =  S__ [ A  ->  B ] ( ( F `  (
y  +  T ) )  x.  1 )  _d y )
1975ditgpos 22809 . . 3  |-  ( ph  ->  S__ [ A  ->  B ] ( ( F `
 ( y  +  T ) )  x.  1 )  _d y  =  S. ( A (,) B ) ( ( F `  (
y  +  T ) )  x.  1 )  _d y )
19810adantr 466 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  F : RR
--> CC )
199198, 33ffvelrnd 6038 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  ( y  +  T
) )  e.  CC )
200 1cnd 9666 . . . . 5  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  1  e.  CC )
201199, 200mulcld 9670 . . . 4  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( ( F `  ( y  +  T ) )  x.  1 )  e.  CC )
2021, 2, 201itgioo 22771 . . 3  |-  ( ph  ->  S. ( A (,) B ) ( ( F `  ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( ( F `  ( y  +  T
) )  x.  1 )  _d y )
203 oveq1 6312 . . . . . . 7  |-  ( y  =  x  ->  (
y  +  T )  =  ( x  +  T ) )
204203fveq2d 5885 . . . . . 6  |-  ( y  =  x  ->  ( F `  ( y  +  T ) )  =  ( F `  (
x  +  T ) ) )
205204oveq1d 6320 . . . . 5  |-  ( y  =  x  ->  (
( F `  (
y  +  T ) )  x.  1 )  =  ( ( F `
 ( x  +  T ) )  x.  1 ) )
206205cbvitgv 22732 . . . 4  |-  S. ( A [,] B ) ( ( F `  ( y  +  T
) )  x.  1 )  _d y  =  S. ( A [,] B ) ( ( F `  ( x  +  T ) )  x.  1 )  _d x
20710adantr 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  F : RR
--> CC )
20824sselda 3464 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  x  e.  RR )
2094adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  T  e.  RR )
210208, 209readdcld 9677 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( x  +  T )  e.  RR )
211207, 210ffvelrnd 6038 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  ( x  +  T
) )  e.  CC )
212211mulid1d 9667 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( ( F `  ( x  +  T ) )  x.  1 )  =  ( F `  ( x  +  T ) ) )
213212, 69eqtrd 2463 . . . . 5  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( ( F `  ( x  +  T ) )  x.  1 )  =  ( F `  x ) )
214213itgeq2dv 22737 . . . 4  |-  ( ph  ->  S. ( A [,] B ) ( ( F `  ( x  +  T ) )  x.  1 )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
215206, 214syl5eq 2475 . . 3  |-  ( ph  ->  S. ( A [,] B ) ( ( F `  ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( F `  x
)  _d x )
216197, 202, 2153eqtrd 2467 . 2  |-  ( ph  ->  S__ [ A  ->  B ] ( ( F `
 ( y  +  T ) )  x.  1 )  _d y  =  S. ( A [,] B ) ( F `  x )  _d x )
21719, 196, 2163eqtrd 2467 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   A.wral 2771   E.wrex 2772   {crab 2775    C_ wss 3436   {csn 3998   {cpr 4000   class class class wbr 4423    |-> cmpt 4482    X. cxp 4851   dom cdm 4853   ran crn 4854    |` cres 4855   -->wf 5597   ` cfv 5601  (class class class)co 6305   CCcc 9544   RRcr 9545   0cc0 9546   1c1 9547    + caddc 9549    x. cmul 9551    <_ cle 9683    - cmin 9867   RR+crp 11309   (,)cioo 11642   [,]cicc 11645   TopOpenctopn 15319   topGenctg 15335  ℂfldccnfld 18969   intcnt 20030   -cn->ccncf 21906   volcvol 22413   L^1cibl 22573   S.citg 22574   S__cdit 22799    _D cdv 22816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-inf2 8155  ax-cc 8872  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623  ax-pre-sup 9624  ax-addf 9625  ax-mulf 9626
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-disj 4395  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-ofr 6546  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-2o 7194  df-oadd 7197  df-omul 7198  df-er 7374  df-map 7485  df-pm 7486  df-ixp 7534  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-fsupp 7893  df-fi 7934  df-sup 7965  df-inf 7966  df-oi 8034  df-card 8381  df-acn 8384  df-cda 8605  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-5 10678  df-6 10679  df-7 10680  df-8 10681  df-9 10682  df-10 10683  df-n0 10877  df-z 10945  df-dec 11059  df-uz 11167  df-q 11272  df-rp 11310  df-xneg 11416  df-xadd 11417  df-xmul 11418  df-ioo 11646  df-ioc 11647  df-ico 11648  df-icc 11649  df-fz 11792  df-fzo 11923  df-fl 12034  df-mod 12103  df-seq 12220  df-exp 12279  df-hash 12522  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-limsup 13525  df-clim 13551  df-rlim 13552  df-sum 13752  df-struct 15122  df-ndx 15123  df-slot 15124  df-base 15125  df-sets 15126  df-ress 15127  df-plusg 15202  df-mulr 15203  df-starv 15204  df-sca 15205  df-vsca 15206  df-ip 15207  df-tset 15208  df-ple 15209  df-ds 15211  df-unif 15212  df-hom 15213  df-cco 15214  df-rest 15320  df-topn 15321  df-0g 15339  df-gsum 15340  df-topgen 15341  df-pt 15342  df-prds 15345  df-xrs 15399  df-qtop 15405  df-imas 15406  df-xps 15409  df-mre 15491  df-mrc 15492  df-acs 15494  df-mgm 16487  df-sgrp 16526  df-mnd 16536  df-submnd 16582  df-mulg 16675  df-cntz 16970  df-cmn 17431  df-psmet 18961  df-xmet 18962  df-met 18963  df-bl 18964  df-mopn 18965  df-fbas 18966  df-fg 18967  df-cnfld 18970  df-top 19919  df-bases 19920  df-topon 19921  df-topsp 19922  df-cld 20032  df-ntr 20033  df-cls 20034  df-nei 20112  df-lp 20150  df-perf 20151  df-cn 20241  df-cnp 20242  df-haus 20329  df-cmp 20400  df-tx 20575  df-hmeo 20768  df-fil 20859  df-fm 20951  df-flim 20952  df-flf 20953  df-xms 21333  df-ms 21334  df-tms 21335  df-cncf 21908  df-ovol 22414  df-vol 22416  df-mbf 22575  df-itg1 22576  df-itg2 22577  df-ibl 22578  df-itg 22579  df-0p 22626  df-ditg 22800  df-limc 22819  df-dv 22820
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator