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

Theorem fourierdlem107 31837
Description: The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by any positive value  X. This lemma generalizes fourierdlem92 31822 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem107.a  |-  ( ph  ->  A  e.  RR )
fourierdlem107.b  |-  ( ph  ->  B  e.  RR )
fourierdlem107.t  |-  T  =  ( B  -  A
)
fourierdlem107.x  |-  ( ph  ->  X  e.  RR+ )
fourierdlem107.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem107.m  |-  ( ph  ->  M  e.  NN )
fourierdlem107.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem107.f  |-  ( ph  ->  F : RR --> CC )
fourierdlem107.fper  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fourierdlem107.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem107.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem107.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem107.o  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  -  X
)  /\  ( p `  m )  =  A )  /\  A. i  e.  ( 0..^ m ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) } )
fourierdlem107.h  |-  H  =  ( { ( A  -  X ) ,  A }  u.  {
y  e.  ( ( A  -  X ) [,] A )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )
fourierdlem107.n  |-  N  =  ( ( # `  H
)  -  1 )
fourierdlem107.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
fourierdlem107.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem107.z  |-  Z  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
fourierdlem107.i  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ,  RR ,  <  ) )
Assertion
Ref Expression
fourierdlem107  |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X
) ) ( F `
 x )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
Distinct variable groups:    A, f,
k, y    A, i, x, k, y    A, m, p, i    B, f, k, y    B, i, x    B, m, p    f, E, k, y    i, E, x    i, F, x, y    f, H, y   
x, H    f, I,
k, y    i, I, x    x, L, y    i, M, x, y    m, M, p    f, N, k, y    i, N, x   
m, N, p    Q, f, k, y    Q, i, x    Q, m, p    x, R, y    S, f, k, y    S, i, x    S, p    T, f, k, y    T, i, x    T, m, p    f, X, y   
i, X, m, p   
x, X    i, Z, x, y    ph, f, k, y    ph, i, x
Allowed substitution hints:    ph( m, p)    P( x, y, f, i, k, m, p)    R( f, i, k, m, p)    S( m)    E( m, p)    F( f, k, m, p)    H( i, k, m, p)    I( m, p)    L( f,
i, k, m, p)    M( f, k)    O( x, y, f, i, k, m, p)    X( k)    Z( f, k, m, p)

Proof of Theorem fourierdlem107
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 fourierdlem107.a . . . . . . 7  |-  ( ph  ->  A  e.  RR )
2 fourierdlem107.x . . . . . . . 8  |-  ( ph  ->  X  e.  RR+ )
32rpred 11268 . . . . . . 7  |-  ( ph  ->  X  e.  RR )
41, 3resubcld 9999 . . . . . 6  |-  ( ph  ->  ( A  -  X
)  e.  RR )
54adantr 465 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  ( A  -  X )  e.  RR )
6 fourierdlem107.b . . . . . . 7  |-  ( ph  ->  B  e.  RR )
76, 3resubcld 9999 . . . . . 6  |-  ( ph  ->  ( B  -  X
)  e.  RR )
87adantr 465 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  ( B  -  X )  e.  RR )
91adantr 465 . . . . . . 7  |-  ( (
ph  /\  X  <_  T )  ->  A  e.  RR )
101, 2ltsubrpd 11296 . . . . . . . . 9  |-  ( ph  ->  ( A  -  X
)  <  A )
114, 1, 10ltled 9744 . . . . . . . 8  |-  ( ph  ->  ( A  -  X
)  <_  A )
1211adantr 465 . . . . . . 7  |-  ( (
ph  /\  X  <_  T )  ->  ( A  -  X )  <_  A
)
133adantr 465 . . . . . . . 8  |-  ( (
ph  /\  X  <_  T )  ->  X  e.  RR )
146adantr 465 . . . . . . . 8  |-  ( (
ph  /\  X  <_  T )  ->  B  e.  RR )
15 id 22 . . . . . . . . . 10  |-  ( X  <_  T  ->  X  <_  T )
16 fourierdlem107.t . . . . . . . . . . 11  |-  T  =  ( B  -  A
)
1716breq2i 4461 . . . . . . . . . 10  |-  ( X  <_  T  <->  X  <_  ( B  -  A ) )
1815, 17sylib 196 . . . . . . . . 9  |-  ( X  <_  T  ->  X  <_  ( B  -  A
) )
1918adantl 466 . . . . . . . 8  |-  ( (
ph  /\  X  <_  T )  ->  X  <_  ( B  -  A ) )
2013, 14, 9, 19lesubd 10168 . . . . . . 7  |-  ( (
ph  /\  X  <_  T )  ->  A  <_  ( B  -  X ) )
219, 12, 203jca 1176 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  ( A  e.  RR  /\  ( A  -  X )  <_  A  /\  A  <_  ( B  -  X )
) )
22 elicc2 11601 . . . . . . 7  |-  ( ( ( A  -  X
)  e.  RR  /\  ( B  -  X
)  e.  RR )  ->  ( A  e.  ( ( A  -  X ) [,] ( B  -  X )
)  <->  ( A  e.  RR  /\  ( A  -  X )  <_  A  /\  A  <_  ( B  -  X )
) ) )
235, 8, 22syl2anc 661 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  ( A  e.  ( ( A  -  X ) [,] ( B  -  X )
)  <->  ( A  e.  RR  /\  ( A  -  X )  <_  A  /\  A  <_  ( B  -  X )
) ) )
2421, 23mpbird 232 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  A  e.  ( ( A  -  X ) [,] ( B  -  X )
) )
25 fourierdlem107.f . . . . . . . 8  |-  ( ph  ->  F : RR --> CC )
2625adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  F : RR --> CC )
274adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  ( A  -  X )  e.  RR )
287adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  ( B  -  X )  e.  RR )
29 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )
30 eliccre 31427 . . . . . . . 8  |-  ( ( ( A  -  X
)  e.  RR  /\  ( B  -  X
)  e.  RR  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X
) ) )  ->  x  e.  RR )
3127, 28, 29, 30syl3anc 1228 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  x  e.  RR )
3226, 31ffvelrnd 6033 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  ( F `  x )  e.  CC )
3332adantlr 714 . . . . 5  |-  ( ( ( ph  /\  X  <_  T )  /\  x  e.  ( ( A  -  X ) [,] ( B  -  X )
) )  ->  ( F `  x )  e.  CC )
34 fourierdlem107.p . . . . . . 7  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
35 fourierdlem107.m . . . . . . 7  |-  ( ph  ->  M  e.  NN )
36 fourierdlem107.q . . . . . . 7  |-  ( ph  ->  Q  e.  ( P `
 M ) )
37 fourierdlem107.fper . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
38 fourierdlem107.fcn . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
39 fourierdlem107.r . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
40 fourierdlem107.l . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
414rexrd 9655 . . . . . . . 8  |-  ( ph  ->  ( A  -  X
)  e.  RR* )
42 pnfxr 11333 . . . . . . . . 9  |- +oo  e.  RR*
4342a1i 11 . . . . . . . 8  |-  ( ph  -> +oo  e.  RR* )
44 ltpnf 11343 . . . . . . . . 9  |-  ( A  e.  RR  ->  A  < +oo )
451, 44syl 16 . . . . . . . 8  |-  ( ph  ->  A  < +oo )
4641, 43, 1, 10, 45eliood 31418 . . . . . . 7  |-  ( ph  ->  A  e.  ( ( A  -  X ) (,) +oo ) )
4734, 16, 35, 36, 25, 37, 38, 39, 40, 4, 46fourierdlem105 31835 . . . . . 6  |-  ( ph  ->  ( x  e.  ( ( A  -  X
) [,] A ) 
|->  ( F `  x
) )  e.  L^1 )
4847adantr 465 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  ( x  e.  ( ( A  -  X ) [,] A
)  |->  ( F `  x ) )  e.  L^1 )
491leidd 10131 . . . . . . . 8  |-  ( ph  ->  A  <_  A )
502rpge0d 11272 . . . . . . . . 9  |-  ( ph  ->  0  <_  X )
516, 3subge02d 10156 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  X  <->  ( B  -  X )  <_  B ) )
5250, 51mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( B  -  X
)  <_  B )
53 iccss 11604 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( A  <_  A  /\  ( B  -  X )  <_  B
) )  ->  ( A [,] ( B  -  X ) )  C_  ( A [,] B ) )
541, 6, 49, 52, 53syl22anc 1229 . . . . . . 7  |-  ( ph  ->  ( A [,] ( B  -  X )
)  C_  ( A [,] B ) )
55 iccmbl 21844 . . . . . . . 8  |-  ( ( A  e.  RR  /\  ( B  -  X
)  e.  RR )  ->  ( A [,] ( B  -  X
) )  e.  dom  vol )
561, 7, 55syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( A [,] ( B  -  X )
)  e.  dom  vol )
5725adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  F : RR
--> CC )
581adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  A  e.  RR )
596adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  B  e.  RR )
60 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  x  e.  ( A [,] B ) )
61 eliccre 31427 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  x  e.  RR )
6258, 59, 60, 61syl3anc 1228 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  x  e.  RR )
6357, 62ffvelrnd 6033 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  ( F `  x )  e.  CC )
641, 6iccssred 31426 . . . . . . . . . 10  |-  ( ph  ->  ( A [,] B
)  C_  RR )
6525, 64feqresmpt 5928 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  =  ( x  e.  ( A [,] B
)  |->  ( F `  x ) ) )
6665eqcomd 2475 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( A [,] B ) 
|->  ( F `  x
) )  =  ( F  |`  ( A [,] B ) ) )
6725, 64fssresd 5758 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> CC )
68 ioossicc 11622 . . . . . . . . . . . . 13  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
6968a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
701rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR* )
7170adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  RR* )
726rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  RR* )
7372adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  B  e.  RR* )
7434, 35, 36fourierdlem15 31745 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
7574adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( A [,] B
) )
76 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
7771, 73, 75, 76fourierdlem8 31738 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( A [,] B ) )
7869, 77sstrd 3519 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( A [,] B ) )
79 resabs1 5308 . . . . . . . . . . 11  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( A [,] B )  ->  (
( F  |`  ( A [,] B ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
8078, 79syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( A [,] B
) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
8180, 38eqeltrd 2555 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( A [,] B
) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
8280eqcomd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( F  |`  ( A [,] B ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
8382oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( ( F  |`  ( A [,] B ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
8439, 83eleqtrd 2557 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( ( F  |`  ( A [,] B ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )
8582oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( ( F  |`  ( A [,] B ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
8640, 85eleqtrd 2557 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( ( F  |`  ( A [,] B ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
8734, 35, 36, 67, 81, 84, 86fourierdlem69 31799 . . . . . . . 8  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  L^1 )
8866, 87eqeltrd 2555 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( A [,] B ) 
|->  ( F `  x
) )  e.  L^1 )
8954, 56, 63, 88iblss 22079 . . . . . 6  |-  ( ph  ->  ( x  e.  ( A [,] ( B  -  X ) ) 
|->  ( F `  x
) )  e.  L^1 )
9089adantr 465 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  ( x  e.  ( A [,] ( B  -  X )
)  |->  ( F `  x ) )  e.  L^1 )
915, 8, 24, 33, 48, 90itgspliticc 22111 . . . 4  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  =  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  +  S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x ) )
9250adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  X  <_  T )  ->  0  <_  X )
9351adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  X  <_  T )  ->  ( 0  <_  X  <->  ( B  -  X )  <_  B
) )
9492, 93mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  X  <_  T )  ->  ( B  -  X )  <_  B
)
958, 20, 943jca 1176 . . . . . . . . 9  |-  ( (
ph  /\  X  <_  T )  ->  ( ( B  -  X )  e.  RR  /\  A  <_ 
( B  -  X
)  /\  ( B  -  X )  <_  B
) )
96 elicc2 11601 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( B  -  X )  e.  ( A [,] B )  <-> 
( ( B  -  X )  e.  RR  /\  A  <_  ( B  -  X )  /\  ( B  -  X )  <_  B ) ) )
979, 14, 96syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  X  <_  T )  ->  ( ( B  -  X )  e.  ( A [,] B
)  <->  ( ( B  -  X )  e.  RR  /\  A  <_ 
( B  -  X
)  /\  ( B  -  X )  <_  B
) ) )
9895, 97mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  X  <_  T )  ->  ( B  -  X )  e.  ( A [,] B ) )
9963adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  X  <_  T )  /\  x  e.  ( A [,] B
) )  ->  ( F `  x )  e.  CC )
1006leidd 10131 . . . . . . . . . . 11  |-  ( ph  ->  B  <_  B )
101100adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  X  <_  T )  ->  B  <_  B )
102 iccss 11604 . . . . . . . . . 10  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( A  <_ 
( B  -  X
)  /\  B  <_  B ) )  ->  (
( B  -  X
) [,] B ) 
C_  ( A [,] B ) )
1039, 14, 20, 101, 102syl22anc 1229 . . . . . . . . 9  |-  ( (
ph  /\  X  <_  T )  ->  ( ( B  -  X ) [,] B )  C_  ( A [,] B ) )
104 iccmbl 21844 . . . . . . . . . . 11  |-  ( ( ( B  -  X
)  e.  RR  /\  B  e.  RR )  ->  ( ( B  -  X ) [,] B
)  e.  dom  vol )
1057, 6, 104syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  -  X ) [,] B
)  e.  dom  vol )
106105adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  X  <_  T )  ->  ( ( B  -  X ) [,] B )  e.  dom  vol )
10788adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  X  <_  T )  ->  ( x  e.  ( A [,] B
)  |->  ( F `  x ) )  e.  L^1 )
108103, 106, 99, 107iblss 22079 . . . . . . . 8  |-  ( (
ph  /\  X  <_  T )  ->  ( x  e.  ( ( B  -  X ) [,] B
)  |->  ( F `  x ) )  e.  L^1 )
1099, 14, 98, 99, 90, 108itgspliticc 22111 . . . . . . 7  |-  ( (
ph  /\  X  <_  T )  ->  S. ( A [,] B ) ( F `  x )  _d x  =  ( S. ( A [,] ( B  -  X
) ) ( F `
 x )  _d x  +  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )
110109oveq1d 6310 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  ( S. ( A [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  ( ( S. ( A [,] ( B  -  X
) ) ( F `
 x )  _d x  +  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x )  -  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x ) )
11125adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A [,] ( B  -  X ) ) )  ->  F : RR
--> CC )
1121adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A [,] ( B  -  X ) ) )  ->  A  e.  RR )
1137adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A [,] ( B  -  X ) ) )  ->  ( B  -  X )  e.  RR )
114 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A [,] ( B  -  X ) ) )  ->  x  e.  ( A [,] ( B  -  X ) ) )
115 eliccre 31427 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( B  -  X
)  e.  RR  /\  x  e.  ( A [,] ( B  -  X
) ) )  ->  x  e.  RR )
116112, 113, 114, 115syl3anc 1228 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A [,] ( B  -  X ) ) )  ->  x  e.  RR )
117111, 116ffvelrnd 6033 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A [,] ( B  -  X ) ) )  ->  ( F `  x )  e.  CC )
118117, 89itgcl 22058 . . . . . . . 8  |-  ( ph  ->  S. ( A [,] ( B  -  X
) ) ( F `
 x )  _d x  e.  CC )
11925adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  F : RR --> CC )
1207adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  ( B  -  X )  e.  RR )
1216adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  B  e.  RR )
122 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  x  e.  ( ( B  -  X ) [,] B
) )
123 eliccre 31427 . . . . . . . . . . 11  |-  ( ( ( B  -  X
)  e.  RR  /\  B  e.  RR  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  x  e.  RR )
124120, 121, 122, 123syl3anc 1228 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  x  e.  RR )
125119, 124ffvelrnd 6033 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  ( F `  x )  e.  CC )
1267rexrd 9655 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  X
)  e.  RR* )
1276, 2ltsubrpd 11296 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  X
)  <  B )
128 ltpnf 11343 . . . . . . . . . . . 12  |-  ( B  e.  RR  ->  B  < +oo )
1296, 128syl 16 . . . . . . . . . . 11  |-  ( ph  ->  B  < +oo )
130126, 43, 6, 127, 129eliood 31418 . . . . . . . . . 10  |-  ( ph  ->  B  e.  ( ( B  -  X ) (,) +oo ) )
13134, 16, 35, 36, 25, 37, 38, 39, 40, 7, 130fourierdlem105 31835 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( ( B  -  X
) [,] B ) 
|->  ( F `  x
) )  e.  L^1 )
132125, 131itgcl 22058 . . . . . . . 8  |-  ( ph  ->  S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  e.  CC )
133118, 132, 132addsubassd 9962 . . . . . . 7  |-  ( ph  ->  ( ( S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x  +  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x )  =  ( S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x  +  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) ) )
134133adantr 465 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  ( ( S. ( A [,] ( B  -  X )
) ( F `  x )  _d x  +  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x )  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  ( S. ( A [,] ( B  -  X )
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) ) )
135132subidd 9930 . . . . . . . . 9  |-  ( ph  ->  ( S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  0 )
136135oveq2d 6311 . . . . . . . 8  |-  ( ph  ->  ( S. ( A [,] ( B  -  X ) ) ( F `  x )  _d x  +  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )  =  ( S. ( A [,] ( B  -  X )
) ( F `  x )  _d x  +  0 ) )
137118addid1d 9791 . . . . . . . 8  |-  ( ph  ->  ( S. ( A [,] ( B  -  X ) ) ( F `  x )  _d x  +  0 )  =  S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x )
138136, 137eqtrd 2508 . . . . . . 7  |-  ( ph  ->  ( S. ( A [,] ( B  -  X ) ) ( F `  x )  _d x  +  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )  =  S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x )
139138adantr 465 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  ( S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x  +  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )  =  S. ( A [,] ( B  -  X ) ) ( F `  x
)  _d x )
140110, 134, 1393eqtrrd 2513 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  S. ( A [,] ( B  -  X ) ) ( F `  x )  _d x  =  ( S. ( A [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )
141140oveq2d 6311 . . . 4  |-  ( (
ph  /\  X  <_  T )  ->  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  +  S. ( A [,] ( B  -  X ) ) ( F `  x )  _d x )  =  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  +  ( S. ( A [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) ) )
14216oveq2i 6306 . . . . . . . . . . . . . . 15  |-  ( ( A  -  X )  +  T )  =  ( ( A  -  X )  +  ( B  -  A ) )
143142a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  -  X )  +  T
)  =  ( ( A  -  X )  +  ( B  -  A ) ) )
1441recnd 9634 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  CC )
1453recnd 9634 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  CC )
1466recnd 9634 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  CC )
147144, 145, 146, 144subadd4b 31364 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  -  X )  +  ( B  -  A ) )  =  ( ( A  -  A )  +  ( B  -  X ) ) )
148143, 147eqtrd 2508 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  -  X )  +  T
)  =  ( ( A  -  A )  +  ( B  -  X ) ) )
149144subidd 9930 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  -  A
)  =  0 )
150149oveq1d 6310 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  -  A )  +  ( B  -  X ) )  =  ( 0  +  ( B  -  X ) ) )
1517recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  -  X
)  e.  CC )
152151addid2d 9792 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  ( B  -  X ) )  =  ( B  -  X ) )
153148, 150, 1523eqtrd 2512 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A  -  X )  +  T
)  =  ( B  -  X ) )
15416oveq2i 6306 . . . . . . . . . . . . . 14  |-  ( A  +  T )  =  ( A  +  ( B  -  A ) )
155154a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  T
)  =  ( A  +  ( B  -  A ) ) )
156144, 146pncan3d 9945 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  ( B  -  A ) )  =  B )
157155, 156eqtrd 2508 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  +  T
)  =  B )
158153, 157oveq12d 6313 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A  -  X )  +  T ) [,] ( A  +  T )
)  =  ( ( B  -  X ) [,] B ) )
159158eqcomd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  -  X ) [,] B
)  =  ( ( ( A  -  X
)  +  T ) [,] ( A  +  T ) ) )
160159itgeq1d 31597 . . . . . . . . 9  |-  ( ph  ->  S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  =  S. ( ( ( A  -  X )  +  T
) [,] ( A  +  T ) ) ( F `  x
)  _d x )
161 fourierdlem107.o . . . . . . . . . . 11  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  -  X
)  /\  ( p `  m )  =  A )  /\  A. i  e.  ( 0..^ m ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) ) } )
162 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
p `  i )  =  ( p `  j ) )
163 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
164163fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
p `  ( i  +  1 ) )  =  ( p `  ( j  +  1 ) ) )
165162, 164breq12d 4466 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
( p `  i
)  <  ( p `  ( i  +  1 ) )  <->  ( p `  j )  <  (
p `  ( j  +  1 ) ) ) )
166165cbvralv 3093 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) )  <->  A. j  e.  ( 0..^ m ) ( p `  j )  <  ( p `  ( j  +  1 ) ) )
167166a1i 11 . . . . . . . . . . . . . 14  |-  ( m  e.  NN  ->  ( A. i  e.  (
0..^ m ) ( p `  i )  <  ( p `  ( i  +  1 ) )  <->  A. j  e.  ( 0..^ m ) ( p `  j
)  <  ( p `  ( j  +  1 ) ) ) )
168167anbi2d 703 . . . . . . . . . . . . 13  |-  ( m  e.  NN  ->  (
( ( ( p `
 0 )  =  ( A  -  X
)  /\  ( p `  m )  =  A )  /\  A. i  e.  ( 0..^ m ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) )  <->  ( (
( p `  0
)  =  ( A  -  X )  /\  ( p `  m
)  =  A )  /\  A. j  e.  ( 0..^ m ) ( p `  j
)  <  ( p `  ( j  +  1 ) ) ) ) )
169168rabbidv 3110 . . . . . . . . . . . 12  |-  ( m  e.  NN  ->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  -  X )  /\  (
p `  m )  =  A )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) }  =  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  -  X
)  /\  ( p `  m )  =  A )  /\  A. j  e.  ( 0..^ m ) ( p `  j
)  <  ( p `  ( j  +  1 ) ) ) } )
170169mpteq2ia 4535 . . . . . . . . . . 11  |-  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  -  X )  /\  (
p `  m )  =  A )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( A  -  X )  /\  (
p `  m )  =  A )  /\  A. j  e.  ( 0..^ m ) ( p `
 j )  < 
( p `  (
j  +  1 ) ) ) } )
171161, 170eqtri 2496 . . . . . . . . . 10  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( A  -  X
)  /\  ( p `  m )  =  A )  /\  A. j  e.  ( 0..^ m ) ( p `  j
)  <  ( p `  ( j  +  1 ) ) ) } )
172 fourierdlem107.h . . . . . . . . . . . . 13  |-  H  =  ( { ( A  -  X ) ,  A }  u.  {
y  e.  ( ( A  -  X ) [,] A )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )
173 fourierdlem107.n . . . . . . . . . . . . 13  |-  N  =  ( ( # `  H
)  -  1 )
174 fourierdlem107.s . . . . . . . . . . . . 13  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
17516, 34, 35, 36, 4, 1, 10, 161, 172, 173, 174fourierdlem54 31784 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  e.  NN  /\  S  e.  ( O `  N
) )  /\  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) ) )
176175simpld 459 . . . . . . . . . . 11  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
177176simpld 459 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
1786, 1resubcld 9999 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  A
)  e.  RR )
17916, 178syl5eqel 2559 . . . . . . . . . 10  |-  ( ph  ->  T  e.  RR )
180176simprd 463 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( O `
 N ) )
1814adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  ( A  -  X )  e.  RR )
1821adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  A  e.  RR )
183 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  x  e.  ( ( A  -  X ) [,] A
) )
184 eliccre 31427 . . . . . . . . . . . 12  |-  ( ( ( A  -  X
)  e.  RR  /\  A  e.  RR  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  x  e.  RR )
185181, 182, 183, 184syl3anc 1228 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  x  e.  RR )
186185, 37syldan 470 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
187 fveq2 5872 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( S `  i )  =  ( S `  j ) )
188187oveq1d 6310 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( S `  i
)  +  T )  =  ( ( S `
 j )  +  T ) )
189188cbvmptv 4544 . . . . . . . . . 10  |-  ( i  e.  ( 0 ... N )  |->  ( ( S `  i )  +  T ) )  =  ( j  e.  ( 0 ... N
)  |->  ( ( S `
 j )  +  T ) )
190 eqid 2467 . . . . . . . . . 10  |-  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( ( A  -  X )  +  T )  /\  (
p `  m )  =  ( A  +  T ) )  /\  A. j  e.  ( 0..^ m ) ( p `
 j )  < 
( p `  (
j  +  1 ) ) ) } )  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... m ) )  |  ( ( ( p `  0 )  =  ( ( A  -  X )  +  T )  /\  (
p `  m )  =  ( A  +  T ) )  /\  A. j  e.  ( 0..^ m ) ( p `
 j )  < 
( p `  (
j  +  1 ) ) ) } )
19135adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  M  e.  NN )
19236adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Q  e.  ( P `  M ) )
19325adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  F : RR --> CC )
19437adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
19538adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
1964adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  -  X )  e.  RR )
197196rexrd 9655 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  -  X )  e.  RR* )
19842a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  -> +oo  e.  RR* )
1991adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  A  e.  RR )
20010adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  -  X )  <  A
)
20145adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  A  < +oo )
202197, 198, 199, 200, 201eliood 31418 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  A  e.  ( ( A  -  X
) (,) +oo )
)
203 fourierdlem107.e . . . . . . . . . . 11  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
204 fourierdlem107.z . . . . . . . . . . 11  |-  Z  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
205 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0..^ N ) )
206 eqid 2467 . . . . . . . . . . 11  |-  ( ( S `  ( j  +  1 ) )  -  ( E `  ( S `  ( j  +  1 ) ) ) )  =  ( ( S `  (
j  +  1 ) )  -  ( E `
 ( S `  ( j  +  1 ) ) ) )
207 eqid 2467 . . . . . . . . . . 11  |-  ( F  |`  ( ( Z `  ( E `  ( S `
 j ) ) ) (,) ( E `
 ( S `  ( j  +  1 ) ) ) ) )  =  ( F  |`  ( ( Z `  ( E `  ( S `
 j ) ) ) (,) ( E `
 ( S `  ( j  +  1 ) ) ) ) )
208 eqid 2467 . . . . . . . . . . 11  |-  ( y  e.  ( ( ( Z `  ( E `
 ( S `  j ) ) )  +  ( ( S `
 ( j  +  1 ) )  -  ( E `  ( S `
 ( j  +  1 ) ) ) ) ) (,) (
( E `  ( S `  ( j  +  1 ) ) )  +  ( ( S `  ( j  +  1 ) )  -  ( E `  ( S `  ( j  +  1 ) ) ) ) ) ) 
|->  ( ( F  |`  ( ( Z `  ( E `  ( S `
 j ) ) ) (,) ( E `
 ( S `  ( j  +  1 ) ) ) ) ) `  ( y  -  ( ( S `
 ( j  +  1 ) )  -  ( E `  ( S `
 ( j  +  1 ) ) ) ) ) ) )  =  ( y  e.  ( ( ( Z `
 ( E `  ( S `  j ) ) )  +  ( ( S `  (
j  +  1 ) )  -  ( E `
 ( S `  ( j  +  1 ) ) ) ) ) (,) ( ( E `  ( S `
 ( j  +  1 ) ) )  +  ( ( S `
 ( j  +  1 ) )  -  ( E `  ( S `
 ( j  +  1 ) ) ) ) ) )  |->  ( ( F  |`  (
( Z `  ( E `  ( S `  j ) ) ) (,) ( E `  ( S `  ( j  +  1 ) ) ) ) ) `  ( y  -  (
( S `  (
j  +  1 ) )  -  ( E `
 ( S `  ( j  +  1 ) ) ) ) ) ) )
209 fourierdlem107.i . . . . . . . . . . 11  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ,  RR ,  <  ) )
21034, 16, 191, 192, 193, 194, 195, 196, 202, 161, 172, 173, 174, 203, 204, 205, 206, 207, 208, 209fourierdlem90 31820 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( F  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  e.  ( ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) -cn-> CC ) )
21139adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
212 eqid 2467 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  |->  R )  =  ( i  e.  ( 0..^ M )  |->  R )
21334, 16, 191, 192, 193, 194, 195, 211, 196, 202, 161, 172, 173, 174, 203, 204, 205, 206, 209, 212fourierdlem89 31819 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( Z `  ( E `
 ( S `  j ) ) )  =  ( Q `  ( I `  ( S `  j )
) ) ,  ( ( i  e.  ( 0..^ M )  |->  R ) `  ( I `
 ( S `  j ) ) ) ,  ( F `  ( Z `  ( E `
 ( S `  j ) ) ) ) )  e.  ( ( F  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) lim CC  ( S `
 j ) ) )
21440adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
215 eqid 2467 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  |->  L )  =  ( i  e.  ( 0..^ M )  |->  L )
21634, 16, 191, 192, 193, 194, 195, 214, 196, 202, 161, 172, 173, 174, 203, 204, 205, 206, 209, 215fourierdlem91 31821 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( E `  ( S `
 ( j  +  1 ) ) )  =  ( Q `  ( ( I `  ( S `  j ) )  +  1 ) ) ,  ( ( i  e.  ( 0..^ M )  |->  L ) `
 ( I `  ( S `  j ) ) ) ,  ( F `  ( E `
 ( S `  ( j  +  1 ) ) ) ) )  e.  ( ( F  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) ) )
2174, 1, 171, 177, 179, 180, 186, 189, 190, 25, 210, 213, 216fourierdlem92 31822 . . . . . . . . 9  |-  ( ph  ->  S. ( ( ( A  -  X )  +  T ) [,] ( A  +  T
) ) ( F `
 x )  _d x  =  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x )
218160, 217eqtrd 2508 . . . . . . . 8  |-  ( ph  ->  S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  =  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x )
219218adantr 465 . . . . . . 7  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( B  -  X
) [,] B ) ( F `  x
)  _d x  =  S. ( ( A  -  X ) [,] A ) ( F `
 x )  _d x )
220132adantr 465 . . . . . . 7  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( B  -  X
) [,] B ) ( F `  x
)  _d x  e.  CC )
221219, 220eqeltrrd 2556 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( A  -  X
) [,] A ) ( F `  x
)  _d x  e.  CC )
22299, 107itgcl 22058 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  S. ( A [,] B ) ( F `  x )  _d x  e.  CC )
223219, 221eqeltrd 2555 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( B  -  X
) [,] B ) ( F `  x
)  _d x  e.  CC )
224221, 222, 223addsub12d 9965 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  +  ( S. ( A [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) )  =  ( S. ( A [,] B ) ( F `
 x )  _d x  +  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x ) ) )
225222, 221, 223addsubassd 9962 . . . . . 6  |-  ( (
ph  /\  X  <_  T )  ->  ( ( S. ( A [,] B
) ( F `  x )  _d x  +  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  ( S. ( A [,] B
) ( F `  x )  _d x  +  ( S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) ) )
226225eqcomd 2475 . . . . 5  |-  ( (
ph  /\  X  <_  T )  ->  ( S. ( A [,] B ) ( F `  x
)  _d x  +  ( S. ( ( A  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )  =  ( ( S. ( A [,] B ) ( F `
 x )  _d x  +  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x )  -  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x ) )
227224, 226eqtrd 2508 . . . 4  |-  ( (
ph  /\  X  <_  T )  ->  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  +  ( S. ( A [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) )  =  ( ( S. ( A [,] B ) ( F `  x )  _d x  +  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x )  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )
22891, 141, 2273eqtrd 2512 . . 3  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  =  ( ( S. ( A [,] B ) ( F `  x
)  _d x  +  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x )  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) )
229219oveq2d 6311 . . 3  |-  ( (
ph  /\  X  <_  T )  ->  ( ( S. ( A [,] B
) ( F `  x )  _d x  +  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  ( ( S. ( A [,] B ) ( F `
 x )  _d x  +  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x )  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) )
230222, 221pncand 9943 . . 3  |-  ( (
ph  /\  X  <_  T )  ->  ( ( S. ( A [,] B
) ( F `  x )  _d x  +  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x )  =  S. ( A [,] B ) ( F `  x
)  _d x )
231228, 229, 2303eqtrd 2512 . 2  |-  ( (
ph  /\  X  <_  T )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  =  S. ( A [,] B ) ( F `
 x )  _d x )
232 simpl 457 . . 3  |-  ( (
ph  /\  -.  X  <_  T )  ->  ph )
233 simpr 461 . . . 4  |-  ( (
ph  /\  -.  X  <_  T )  ->  -.  X  <_  T )
234232, 179syl 16 . . . . 5  |-  ( (
ph  /\  -.  X  <_  T )  ->  T  e.  RR )
235232, 3syl 16 . . . . 5  |-  ( (
ph  /\  -.  X  <_  T )  ->  X  e.  RR )
236234, 235ltnled 9743 . . . 4  |-  ( (
ph  /\  -.  X  <_  T )  ->  ( T  <  X  <->  -.  X  <_  T ) )
237233, 236mpbird 232 . . 3  |-  ( (
ph  /\  -.  X  <_  T )  ->  T  <  X )
23834, 35, 36fourierdlem11 31741 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
239238simp3d 1010 . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
2401, 6, 3, 239ltsub1dd 10176 . . . . . . . . . . 11  |-  ( ph  ->  ( A  -  X
)  <  ( B  -  X ) )
241 ltpnf 11343 . . . . . . . . . . . 12  |-  ( ( B  -  X )  e.  RR  ->  ( B  -  X )  < +oo )
2427, 241syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( B  -  X
)  < +oo )
24341, 43, 7, 240, 242eliood 31418 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  X
)  e.  ( ( A  -  X ) (,) +oo ) )
24434, 16, 35, 36, 25, 37, 38, 39, 40, 4, 243fourierdlem105 31835 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( ( A  -  X
) [,] ( B  -  X ) ) 
|->  ( F `  x
) )  e.  L^1 )
24532, 244itgcl 22058 . . . . . . . 8  |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X
) ) ( F `
 x )  _d x  e.  CC )
246245adantr 465 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  e.  CC )
247246subid1d 9931 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  0 )  =  S. ( ( A  -  X ) [,] ( B  -  X
) ) ( F `
 x )  _d x )
248247eqcomd 2475 . . . . 5  |-  ( (
ph  /\  T  <  X )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  =  ( S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  -  0 ) )
249218, 132eqeltrrd 2556 . . . . . . . . . 10  |-  ( ph  ->  S. ( ( A  -  X ) [,] A ) ( F `
 x )  _d x  e.  CC )
250249subidd 9930 . . . . . . . . 9  |-  ( ph  ->  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x )  =  0 )
251250eqcomd 2475 . . . . . . . 8  |-  ( ph  ->  0  =  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) )
252251adantr 465 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  0  =  ( S. ( ( A  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) )
2534adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  ( A  -  X )  e.  RR )
2541adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  A  e.  RR )
2557adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( B  -  X )  e.  RR )
2561, 6, 239ltled 9744 . . . . . . . . . . . . 13  |-  ( ph  ->  A  <_  B )
257256adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  T  <  X )  ->  A  <_  B )
2581, 6, 3lesub1d 10171 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  <_  B  <->  ( A  -  X )  <_  ( B  -  X ) ) )
259258adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  T  <  X )  ->  ( A  <_  B  <->  ( A  -  X )  <_  ( B  -  X )
) )
260257, 259mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( A  -  X )  <_  ( B  -  X )
)
2616adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  T  <  X )  ->  B  e.  RR )
2623adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  T  <  X )  ->  X  e.  RR )
263 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  T  <  X )  ->  T  <  X )
26416, 263syl5eqbrr 4487 . . . . . . . . . . . . 13  |-  ( (
ph  /\  T  <  X )  ->  ( B  -  A )  <  X
)
265261, 254, 262, 264ltsub23d 10169 . . . . . . . . . . . 12  |-  ( (
ph  /\  T  <  X )  ->  ( B  -  X )  <  A
)
266255, 254, 265ltled 9744 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( B  -  X )  <_  A
)
267255, 260, 2663jca 1176 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  ( ( B  -  X )  e.  RR  /\  ( A  -  X )  <_ 
( B  -  X
)  /\  ( B  -  X )  <_  A
) )
268 elicc2 11601 . . . . . . . . . . 11  |-  ( ( ( A  -  X
)  e.  RR  /\  A  e.  RR )  ->  ( ( B  -  X )  e.  ( ( A  -  X
) [,] A )  <-> 
( ( B  -  X )  e.  RR  /\  ( A  -  X
)  <_  ( B  -  X )  /\  ( B  -  X )  <_  A ) ) )
269253, 254, 268syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  ( ( B  -  X )  e.  ( ( A  -  X ) [,] A
)  <->  ( ( B  -  X )  e.  RR  /\  ( A  -  X )  <_ 
( B  -  X
)  /\  ( B  -  X )  <_  A
) ) )
270267, 269mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  ( B  -  X )  e.  ( ( A  -  X
) [,] A ) )
27125adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  F : RR --> CC )
272271, 185ffvelrnd 6033 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  ( F `  x )  e.  CC )
273272adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  T  <  X )  /\  x  e.  ( ( A  -  X ) [,] A
) )  ->  ( F `  x )  e.  CC )
274244adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  ( x  e.  ( ( A  -  X ) [,] ( B  -  X )
)  |->  ( F `  x ) )  e.  L^1 )
27535adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  M  e.  NN )
27636adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  Q  e.  ( P `  M ) )
27725adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  F : RR
--> CC )
27837adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  T  <  X )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
27938adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  T  <  X )  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
28039adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  T  <  X )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
28140adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  T  <  X )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
282126adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( B  -  X )  e.  RR* )
28342a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  -> +oo  e.  RR* )
284254, 44syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  A  < +oo )
285282, 283, 254, 265, 284eliood 31418 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  A  e.  ( ( B  -  X ) (,) +oo ) )
28634, 16, 275, 276, 277, 278, 279, 280, 281, 255, 285fourierdlem105 31835 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  ( x  e.  ( ( B  -  X ) [,] A
)  |->  ( F `  x ) )  e.  L^1 )
287253, 254, 270, 273, 274, 286itgspliticc 22111 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  S. (
( A  -  X
) [,] A ) ( F `  x
)  _d x  =  ( S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  +  S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x ) )
288287oveq1d 6310 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  =  ( ( S. ( ( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  +  S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x )  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) )
28925adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  F : RR --> CC )
2907adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  ( B  -  X )  e.  RR )
2911adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  A  e.  RR )
292 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  x  e.  ( ( B  -  X ) [,] A
) )
293 eliccre 31427 . . . . . . . . . . . 12  |-  ( ( ( B  -  X
)  e.  RR  /\  A  e.  RR  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  x  e.  RR )
294290, 291, 292, 293syl3anc 1228 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  x  e.  RR )
295289, 294ffvelrnd 6033 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  ( F `  x )  e.  CC )
296295adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  T  <  X )  /\  x  e.  ( ( B  -  X ) [,] A
) )  ->  ( F `  x )  e.  CC )
297296, 286itgcl 22058 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  S. (
( B  -  X
) [,] A ) ( F `  x
)  _d x  e.  CC )
298249adantr 465 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  S. (
( A  -  X
) [,] A ) ( F `  x
)  _d x  e.  CC )
299246, 297, 298addsubassd 9962 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  +  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x )  =  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) ) )
300252, 288, 2993eqtrd 2512 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  0  =  ( S. ( ( A  -  X ) [,] ( B  -  X
) ) ( F `
 x )  _d x  +  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) ) )
301300oveq2d 6311 . . . . 5  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  0 )  =  ( S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  -  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) ) ) )
302297, 298subcld 9942 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  e.  CC )
303246, 246, 302subsub4d 9973 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x )  -  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) )  =  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  ( S. ( ( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  +  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) ) ) )
304303eqcomd 2475 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  ( S. ( ( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  +  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) ) )  =  ( ( S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x )  -  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) ) )
305245subidd 9930 . . . . . . . 8  |-  ( ph  ->  ( S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x )  =  0 )
306305oveq1d 6310 . . . . . . 7  |-  ( ph  ->  ( ( S. ( ( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x )  -  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) )  =  ( 0  -  ( S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) ) )
307306adantr 465 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  ( ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x )  -  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) )  =  ( 0  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) ) )
308 df-neg 9820 . . . . . . . . 9  |-  -u ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  =  ( 0  -  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) )
309308eqcomi 2480 . . . . . . . 8  |-  ( 0  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) )  =  -u ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x )
310309a1i 11 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( 0  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) )  =  -u ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) )
311297, 298negsubdi2d 9958 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  -u ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x )  =  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x ) )
312310, 311eqtrd 2508 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  ( 0  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x ) )  =  ( S. ( ( A  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x ) )
313304, 307, 3123eqtrd 2512 . . . . 5  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  -  ( S. ( ( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  +  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x ) ) )  =  ( S. ( ( A  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x ) )
314248, 301, 3133eqtrd 2512 . . . 4  |-  ( (
ph  /\  T  <  X )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  =  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x ) )
315297addid1d 9791 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  0 )  =  S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x )
316315eqcomd 2475 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  S. (
( B  -  X
) [,] A ) ( F `  x
)  _d x  =  ( S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x  +  0 ) )
317135eqcomd 2475 . . . . . . . 8  |-  ( ph  ->  0  =  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x ) )
318317oveq2d 6311 . . . . . . 7  |-  ( ph  ->  ( S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x  +  0 )  =  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) ) )
319318adantr 465 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  0 )  =  ( S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x  +  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x ) ) )
320254, 266, 2573jca 1176 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( A  e.  RR  /\  ( B  -  X )  <_  A  /\  A  <_  B
) )
321 elicc2 11601 . . . . . . . . . . . 12  |-  ( ( ( B  -  X
)  e.  RR  /\  B  e.  RR )  ->  ( A  e.  ( ( B  -  X
) [,] B )  <-> 
( A  e.  RR  /\  ( B  -  X
)  <_  A  /\  A  <_  B ) ) )
322255, 261, 321syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( A  e.  ( ( B  -  X ) [,] B
)  <->  ( A  e.  RR  /\  ( B  -  X )  <_  A  /\  A  <_  B
) ) )
323320, 322mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  A  e.  ( ( B  -  X ) [,] B
) )
324125adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  T  <  X )  /\  x  e.  ( ( B  -  X ) [,] B
) )  ->  ( F `  x )  e.  CC )
32588adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  ( x  e.  ( A [,] B
)  |->  ( F `  x ) )  e.  L^1 )
326255, 261, 323, 324, 286, 325itgspliticc 22111 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  S. (
( B  -  X
) [,] B ) ( F `  x
)  _d x  =  ( S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x  +  S. ( A [,] B ) ( F `  x
)  _d x ) )
327326oveq2d 6311 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x )  =  ( S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x  -  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  S. ( A [,] B ) ( F `  x )  _d x ) ) )
328327oveq2d 6311 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) )  =  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  +  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  +  S. ( A [,] B
) ( F `  x )  _d x ) ) ) )
329132adantr 465 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  S. (
( B  -  X
) [,] B ) ( F `  x
)  _d x  e.  CC )
330326, 329eqeltrrd 2556 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  S. ( A [,] B ) ( F `  x )  _d x )  e.  CC )
331297, 329, 330addsub12d 9965 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x  -  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  +  S. ( A [,] B ) ( F `  x
)  _d x ) ) )  =  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  +  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  +  S. ( A [,] B
) ( F `  x )  _d x ) ) ) )
33263, 88itgcl 22058 . . . . . . . . . . . 12  |-  ( ph  ->  S. ( A [,] B ) ( F `
 x )  _d x  e.  CC )
333332adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  S. ( A [,] B ) ( F `  x )  _d x  e.  CC )
334297, 297, 333subsub4d 9973 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  ( ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( A [,] B
) ( F `  x )  _d x )  =  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  +  S. ( A [,] B
) ( F `  x )  _d x ) ) )
335334eqcomd 2475 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  +  S. ( A [,] B
) ( F `  x )  _d x ) )  =  ( ( S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x )  -  S. ( A [,] B ) ( F `  x
)  _d x ) )
336335oveq2d 6311 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  +  S. ( A [,] B ) ( F `  x
)  _d x ) ) )  =  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  +  ( ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  -  S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x )  -  S. ( A [,] B ) ( F `  x )  _d x ) ) )
337297subidd 9930 . . . . . . . . . . 11  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  =  0 )
338337oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  ( ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( A [,] B
) ( F `  x )  _d x )  =  ( 0  -  S. ( A [,] B ) ( F `  x )  _d x ) )
339 df-neg 9820 . . . . . . . . . . . 12  |-  -u S. ( A [,] B ) ( F `  x
)  _d x  =  ( 0  -  S. ( A [,] B ) ( F `  x
)  _d x )
340339eqcomi 2480 . . . . . . . . . . 11  |-  ( 0  -  S. ( A [,] B ) ( F `  x )  _d x )  = 
-u S. ( A [,] B ) ( F `  x )  _d x
341340a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  T  <  X )  ->  ( 0  -  S. ( A [,] B ) ( F `  x )  _d x )  = 
-u S. ( A [,] B ) ( F `  x )  _d x )
342338, 341eqtrd 2508 . . . . . . . . 9  |-  ( (
ph  /\  T  <  X )  ->  ( ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( A [,] B
) ( F `  x )  _d x )  =  -u S. ( A [,] B ) ( F `  x
)  _d x )
343342oveq2d 6311 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  +  ( ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  -  S. ( A [,] B
) ( F `  x )  _d x ) )  =  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  +  -u S. ( A [,] B ) ( F `  x
)  _d x ) )
344329, 333negsubd 9948 . . . . . . . 8  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  +  -u S. ( A [,] B ) ( F `  x )  _d x )  =  ( S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x  -  S. ( A [,] B ) ( F `  x
)  _d x ) )
345336, 343, 3443eqtrd 2512 . . . . . . 7  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] A ) ( F `  x
)  _d x  -  ( S. ( ( B  -  X ) [,] A ) ( F `
 x )  _d x  +  S. ( A [,] B ) ( F `  x
)  _d x ) ) )  =  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( A [,] B ) ( F `  x
)  _d x ) )
346328, 331, 3453eqtrd 2512 . . . . . 6  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( B  -  X ) [,] A
) ( F `  x )  _d x  +  ( S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x ) )  =  ( S. ( ( B  -  X ) [,] B ) ( F `
 x )  _d x  -  S. ( A [,] B ) ( F `  x
)  _d x ) )
347316, 319, 3463eqtrd 2512 . . . . 5  |-  ( (
ph  /\  T  <  X )  ->  S. (
( B  -  X
) [,] A ) ( F `  x
)  _d x  =  ( S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x  -  S. ( A [,] B ) ( F `  x
)  _d x ) )
348347oveq2d 6311 . . . 4  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] A ) ( F `  x )  _d x )  =  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  -  S. ( A [,] B ) ( F `  x )  _d x ) ) )
349249, 132, 332subsubd 9970 . . . . . 6  |-  ( ph  ->  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  -  S. ( A [,] B ) ( F `  x )  _d x ) )  =  ( ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B ) ( F `  x )  _d x )  +  S. ( A [,] B ) ( F `
 x )  _d x ) )
350218oveq2d 6311 . . . . . . . 8  |-  ( ph  ->  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x ) )
351350, 250eqtrd 2508 . . . . . . 7  |-  ( ph  ->  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  =  0 )
352351oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( S. ( ( A  -  X
) [,] A ) ( F `  x
)  _d x  -  S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x )  +  S. ( A [,] B ) ( F `  x
)  _d x )  =  ( 0  +  S. ( A [,] B ) ( F `
 x )  _d x ) )
353332addid2d 9792 . . . . . 6  |-  ( ph  ->  ( 0  +  S. ( A [,] B ) ( F `  x
)  _d x )  =  S. ( A [,] B ) ( F `  x )  _d x )
354349, 352, 3533eqtrd 2512 . . . . 5  |-  ( ph  ->  ( S. ( ( A  -  X ) [,] A ) ( F `  x )  _d x  -  ( S. ( ( B  -  X ) [,] B
) ( F `  x )  _d x  -  S. ( A [,] B ) ( F `  x )  _d x ) )  =  S. ( A [,] B ) ( F `  x )  _d x )
355354adantr 465 . . . 4  |-  ( (
ph  /\  T  <  X )  ->  ( S. ( ( A  -  X ) [,] A
) ( F `  x )  _d x  -  ( S. ( ( B  -  X
) [,] B ) ( F `  x
)  _d x  -  S. ( A [,] B
) ( F `  x )  _d x ) )  =  S. ( A [,] B
) ( F `  x )  _d x )
356314, 348, 3553eqtrd 2512 . . 3  |-  ( (
ph  /\  T  <  X )  ->  S. (
( A  -  X
) [,] ( B  -  X ) ) ( F `  x
)  _d x  =  S. ( A [,] B ) ( F `
 x )  _d x )
357232, 237, 356syl2anc 661 . 2  |-  ( (
ph  /\  -.  X  <_  T )  ->  S. ( ( A  -  X ) [,] ( B  -  X )
) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
358231, 357pm2.61dan 789 1  |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X
) ) ( F `
 x )  _d x  =  S. ( A [,] B ) ( F `  x
)  _d x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818   {crab 2821    u. cun 3479    C_ wss 3481   ifcif 3945   {cpr 4035   class class class wbr 4453    |-> cmpt 4511   dom cdm 5005   ran crn 5006    |` cres 5007   iotacio 5555   -->wf 5590   ` cfv 5594    Isom wiso 5595  (class class class)co 6295    ^m cmap 7432   supcsup 7912   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505    + caddc 9507    x. cmul 9509   +oocpnf 9637   RR*cxr 9639    < clt 9640    <_ cle 9641    - cmin 9817   -ucneg 9818    / cdiv 10218   NNcn 10548   ZZcz 10876   RR+crp 11232   (,)cioo 11541   (,]cioc 11542   [,]cicc 11544   ...cfz 11684  ..^cfzo 11804   |_cfl 11907   #chash 12385   -cn->ccncf 21248   volcvol 21743   L^1cibl 21894   S.citg 21895   lim CC climc 22134
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-