Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem107 Structured version   Visualization version   Unicode version
Theorem fourierdlem107 38189
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 38174 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.t . . . . . . . . . . . . . . . . 17 |- T = ( B - A )
21oveq2i 6319 . . . . . . . . . . . . . . . 16 |- ( ( A - X ) + T ) = ( ( A - X ) + ( B - A ) )
3 fourierdlem107.a . . . . . . . . . . . . . . . . . 18 |- ( ph -> A e. RR )
43recnd 9687 . . . . . . . . . . . . . . . . 17 |- ( ph -> A e. CC )
5 fourierdlem107.x . . . . . . . . . . . . . . . . . . 19 |- ( ph -> X e. RR+ )
65rpred 11364 . . . . . . . . . . . . . . . . . 18 |- ( ph -> X e. RR )
76recnd 9687 . . . . . . . . . . . . . . . . 17 |- ( ph -> X e. CC )
8 fourierdlem107.b . . . . . . . . . . . . . . . . . 18 |- ( ph -> B e. RR )
98recnd 9687 . . . . . . . . . . . . . . . . 17 |- ( ph -> B e. CC )
104, 7, 9, 4subadd4b 37582 . . . . . . . . . . . . . . . 16 |- ( ph -> ( ( A - X ) + ( B - A ) ) = ( ( A - A ) + ( B - X ) ) )
112, 10syl5eq 2517 . . . . . . . . . . . . . . 15 |- ( ph -> ( ( A - X ) + T ) = ( ( A - A ) + ( B - X ) ) )
124subidd 9993 . . . . . . . . . . . . . . . 16 |- ( ph -> ( A - A ) = 0 )
1312oveq1d 6323 . . . . . . . . . . . . . . 15 |- ( ph -> ( ( A - A ) + ( B - X ) ) = ( 0 + ( B - X ) ) )
148, 6resubcld 10068 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( B - X ) e. RR )
1514recnd 9687 . . . . . . . . . . . . . . . 16 |- ( ph -> ( B - X ) e. CC )
1615addid2d 9852 . . . . . . . . . . . . . . 15 |- ( ph -> ( 0 + ( B - X ) ) = ( B - X ) )
1711, 13, 163eqtrd 2509 . . . . . . . . . . . . . 14 |- ( ph -> ( ( A - X ) + T ) = ( B - X ) )
181oveq2i 6319 . . . . . . . . . . . . . . 15 |- ( A + T ) = ( A + ( B - A ) )
194, 9pncan3d 10008 . . . . . . . . . . . . . . 15 |- ( ph -> ( A + ( B - A ) ) = B )
2018, 19syl5eq 2517 . . . . . . . . . . . . . 14 |- ( ph -> ( A + T ) = B )
2117, 20oveq12d 6326 . . . . . . . . . . . . 13 |- ( ph -> ( ( ( A - X ) + T ) [,] ( A + T ) ) = ( ( B - X ) [,] B ) )
2221eqcomd 2477 . . . . . . . . . . . 12 |- ( ph -> ( ( B - X ) [,] B ) = ( ( ( A - X ) + T ) [,] ( A + T ) ) )
2322itgeq1d 37930 . . . . . . . . . . 11 |- ( ph -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x = S. ( ( ( A - X ) + T ) [,] ( A + T ) ) ( F ` x ) _d x )
243, 6resubcld 10068 . . . . . . . . . . . 12 |- ( ph -> ( A - X ) e. RR )
25 fourierdlem107.o . . . . . . . . . . . . 13 |- 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 ) ) ) } )
26 fveq2 5879 . . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( p ` i ) = ( p ` j ) )
27 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
2827fveq2d 5883 . . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
2926, 28breq12d 4408 . . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
3029cbvralv 3005 . . . . . . . . . . . . . . . . 17 |- ( A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) )
3130a1i 11 . . . . . . . . . . . . . . . 16 |- ( m e. NN -> ( A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
3231anbi2d 718 . . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
3332rabbidv 3022 . . . . . . . . . . . . . 14 |- ( 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 ) ) ) } )
3433mpteq2ia 4478 . . . . . . . . . . . . 13 |- ( 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 ) ) ) } )
3525, 34eqtri 2493 . . . . . . . . . . . 12 |- 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 ) ) ) } )
36 fourierdlem107.p . . . . . . . . . . . . . . 15 |- 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 ) ) ) } )
37 fourierdlem107.m . . . . . . . . . . . . . . 15 |- ( ph -> M e. NN )
38 fourierdlem107.q . . . . . . . . . . . . . . 15 |- ( ph -> Q e. ( P ` M ) )
393, 5ltsubrpd 11393 . . . . . . . . . . . . . . 15 |- ( ph -> ( A - X ) < A )
40 fourierdlem107.h . . . . . . . . . . . . . . 15 |- H = ( { ( A - X ) , A } u. { y e. ( ( A - X ) [,] A ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
41 fourierdlem107.n . . . . . . . . . . . . . . 15 |- N = ( ( # ` H ) - 1 )
42 fourierdlem107.s . . . . . . . . . . . . . . 15 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
431, 36, 37, 38, 24, 3, 39, 25, 40, 41, 42fourierdlem54 38136 . . . . . . . . . . . . . 14 |- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
4443simpld 466 . . . . . . . . . . . . 13 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
4544simpld 466 . . . . . . . . . . . 12 |- ( ph -> N e. NN )
468, 3resubcld 10068 . . . . . . . . . . . . 13 |- ( ph -> ( B - A ) e. RR )
471, 46syl5eqel 2553 . . . . . . . . . . . 12 |- ( ph -> T e. RR )
4844simprd 470 . . . . . . . . . . . 12 |- ( ph -> S e. ( O ` N ) )
4924adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> ( A - X ) e. RR )
503adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> A e. RR )
51 simpr 468 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> x e. ( ( A - X ) [,] A ) )
52 eliccre 37699 . . . . . . . . . . . . . 14 |- ( ( ( A - X ) e. RR /\ A e. RR /\ x e. ( ( A - X ) [,] A ) ) -> x e. RR )
5349, 50, 51, 52syl3anc 1292 . . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> x e. RR )
54 fourierdlem107.fper . . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
5553, 54syldan 478 . . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
56 fveq2 5879 . . . . . . . . . . . . . 14 |- ( i = j -> ( S ` i ) = ( S ` j ) )
5756oveq1d 6323 . . . . . . . . . . . . 13 |- ( i = j -> ( ( S ` i ) + T ) = ( ( S ` j ) + T ) )
5857cbvmptv 4488 . . . . . . . . . . . 12 |- ( i e. ( 0 ... N ) |-> ( ( S ` i ) + T ) ) = ( j e. ( 0 ... N ) |-> ( ( S ` j ) + T ) )
59 eqid 2471 . . . . . . . . . . . 12 |- ( 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 ) ) ) } )
60 fourierdlem107.f . . . . . . . . . . . 12 |- ( ph -> F : RR --> CC )
6137adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> M e. NN )
6238adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> Q e. ( P ` M ) )
6360adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> F : RR --> CC )
6454adantlr 729 . . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
65 fourierdlem107.fcn . . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
6665adantlr 729 . . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
6724adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A - X ) e. RR )
6867rexrd 9708 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A - X ) e. RR* )
69 pnfxr 11435 . . . . . . . . . . . . . . 15 |- +oo e. RR*
7069a1i 11 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> +oo e. RR* )
713adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> A e. RR )
7239adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( A - X ) < A )
733ltpnfd 11446 . . . . . . . . . . . . . . 15 |- ( ph -> A < +oo )
7473adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> A < +oo )
7568, 70, 71, 72, 74eliood 37691 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> A e. ( ( A - X ) (,) +oo ) )
76 fourierdlem107.e . . . . . . . . . . . . 13 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
77 fourierdlem107.z . . . . . . . . . . . . 13 |- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
78 simpr 468 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> j e. ( 0..^ N ) )
79 eqid 2471 . . . . . . . . . . . . 13 |- ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) )
80 eqid 2471 . . . . . . . . . . . . 13 |- ( F |` ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) = ( F |` ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) )
81 eqid 2471 . . . . . . . . . . . . 13 |- ( 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 ) ) ) ) ) ) )
82 fourierdlem107.i . . . . . . . . . . . . 13 |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
8336, 1, 61, 62, 63, 64, 66, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 80, 81, 82fourierdlem90 38172 . . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
84 fourierdlem107.r . . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
8584adantlr 729 . . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
86 eqid 2471 . . . . . . . . . . . . 13 |- ( i e. ( 0..^ M ) |-> R ) = ( i e. ( 0..^ M ) |-> R )
8736, 1, 61, 62, 63, 64, 66, 85, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 86fourierdlem89 38171 . . . . . . . . . . . 12 |- ( ( 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 ) ) )
88 fourierdlem107.l . . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
8988adantlr 729 . . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
90 eqid 2471 . . . . . . . . . . . . 13 |- ( i e. ( 0..^ M ) |-> L ) = ( i e. ( 0..^ M ) |-> L )
9136, 1, 61, 62, 63, 64, 66, 89, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 90fourierdlem91 38173 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
9224, 3, 35, 45, 47, 48, 55, 58, 59, 60, 83, 87, 91fourierdlem92 38174 . . . . . . . . . . 11 |- ( ph -> S. ( ( ( A - X ) + T ) [,] ( A + T ) ) ( F ` x ) _d x = S. ( ( A - X ) [,] A ) ( F ` x ) _d x )
9323, 92eqtrd 2505 . . . . . . . . . 10 |- ( ph -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x = S. ( ( A - X ) [,] A ) ( F ` x ) _d x )
9460adantr 472 . . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> F : RR --> CC )
9514adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> ( B - X ) e. RR )
968adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> B e. RR )
97 simpr 468 . . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> x e. ( ( B - X ) [,] B ) )
98 eliccre 37699 . . . . . . . . . . . . 13 |- ( ( ( B - X ) e. RR /\ B e. RR /\ x e. ( ( B - X ) [,] B ) ) -> x e. RR )
9995, 96, 97, 98syl3anc 1292 . . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> x e. RR )
10094, 99ffvelrnd 6038 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> ( F ` x ) e. CC )
10114rexrd 9708 . . . . . . . . . . . . 13 |- ( ph -> ( B - X ) e. RR* )
10269a1i 11 . . . . . . . . . . . . 13 |- ( ph -> +oo e. RR* )
1038, 5ltsubrpd 11393 . . . . . . . . . . . . 13 |- ( ph -> ( B - X ) < B )
1048ltpnfd 11446 . . . . . . . . . . . . 13 |- ( ph -> B < +oo )
105101, 102, 8, 103, 104eliood 37691 . . . . . . . . . . . 12 |- ( ph -> B e. ( ( B - X ) (,) +oo ) )
10636, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105fourierdlem105 38187 . . . . . . . . . . 11 |- ( ph -> ( x e. ( ( B - X ) [,] B ) |-> ( F ` x ) ) e. L^1 )
107100, 106itgcl 22820 . . . . . . . . . 10 |- ( ph -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x e. CC )
10893, 107eqeltrrd 2550 . . . . . . . . 9 |- ( ph -> S. ( ( A - X ) [,] A ) ( F ` x ) _d x e. CC )
109108subidd 9993 . . . . . . . 8 |- ( ph -> ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) = 0 )
110109eqcomd 2477 . . . . . . 7 |- ( ph -> 0 = ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) )
111110adantr 472 . . . . . 6 |- ( ( ph /\ T < X ) -> 0 = ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) )
11224adantr 472 . . . . . . . 8 |- ( ( ph /\ T < X ) -> ( A - X ) e. RR )
1133adantr 472 . . . . . . . 8 |- ( ( ph /\ T < X ) -> A e. RR )
11414adantr 472 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> ( B - X ) e. RR )
11536, 37, 38fourierdlem11 38092 . . . . . . . . . . . . 13 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
116115simp3d 1044 . . . . . . . . . . . 12 |- ( ph -> A < B )
1173, 8, 116ltled 9800 . . . . . . . . . . 11 |- ( ph -> A <_ B )
118117adantr 472 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> A <_ B )
1193, 8, 6lesub1d 10241 . . . . . . . . . . 11 |- ( ph -> ( A <_ B <-> ( A - X ) <_ ( B - X ) ) )
120119adantr 472 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> ( A <_ B <-> ( A - X ) <_ ( B - X ) ) )
121118, 120mpbid 215 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> ( A - X ) <_ ( B - X ) )
1228adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ T < X ) -> B e. RR )
1236adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ T < X ) -> X e. RR )
124 simpr 468 . . . . . . . . . . . 12 |- ( ( ph /\ T < X ) -> T < X )
1251, 124syl5eqbrr 4430 . . . . . . . . . . 11 |- ( ( ph /\ T < X ) -> ( B - A ) < X )
126122, 113, 123, 125ltsub23d 10239 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> ( B - X ) < A )
127114, 113, 126ltled 9800 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> ( B - X ) <_ A )
128112, 113, 114, 121, 127eliccd 37697 . . . . . . . 8 |- ( ( ph /\ T < X ) -> ( B - X ) e. ( ( A - X ) [,] A ) )
12960adantr 472 . . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> F : RR --> CC )
130129, 53ffvelrnd 6038 . . . . . . . . 9 |- ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> ( F ` x ) e. CC )
131130adantlr 729 . . . . . . . 8 |- ( ( ( ph /\ T < X ) /\ x e. ( ( A - X ) [,] A ) ) -> ( F ` x ) e. CC )
13224rexrd 9708 . . . . . . . . . . 11 |- ( ph -> ( A - X ) e. RR* )
1333, 8, 6, 116ltsub1dd 10246 . . . . . . . . . . 11 |- ( ph -> ( A - X ) < ( B - X ) )
13414ltpnfd 11446 . . . . . . . . . . 11 |- ( ph -> ( B - X ) < +oo )
135132, 102, 14, 133, 134eliood 37691 . . . . . . . . . 10 |- ( ph -> ( B - X ) e. ( ( A - X ) (,) +oo ) )
13636, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135fourierdlem105 38187 . . . . . . . . 9 |- ( ph -> ( x e. ( ( A - X ) [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
137136adantr 472 . . . . . . . 8 |- ( ( ph /\ T < X ) -> ( x e. ( ( A - X ) [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
13837adantr 472 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> M e. NN )
13938adantr 472 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> Q e. ( P ` M ) )
14060adantr 472 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> F : RR --> CC )
14154adantlr 729 . . . . . . . . 9 |- ( ( ( ph /\ T < X ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
14265adantlr 729 . . . . . . . . 9 |- ( ( ( ph /\ T < X ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
14384adantlr 729 . . . . . . . . 9 |- ( ( ( ph /\ T < X ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
14488adantlr 729 . . . . . . . . 9 |- ( ( ( ph /\ T < X ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
145101adantr 472 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> ( B - X ) e. RR* )
14669a1i 11 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> +oo e. RR* )
147113ltpnfd 11446 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> A < +oo )
148145, 146, 113, 126, 147eliood 37691 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> A e. ( ( B - X ) (,) +oo ) )
14936, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148fourierdlem105 38187 . . . . . . . 8 |- ( ( ph /\ T < X ) -> ( x e. ( ( B - X ) [,] A ) |-> ( F ` x ) ) e. L^1 )
150112, 113, 128, 131, 137, 149itgspliticc 22873 . . . . . . 7 |- ( ( 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 ) )
151150oveq1d 6323 . . . . . 6 |- ( ( 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 ) )
15260adantr 472 . . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> F : RR --> CC )
15324adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) e. RR )
15414adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( B - X ) e. RR )
155 simpr 468 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> x e. ( ( A - X ) [,] ( B - X ) ) )
156 eliccre 37699 . . . . . . . . . . 11 |- ( ( ( A - X ) e. RR /\ ( B - X ) e. RR /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> x e. RR )
157153, 154, 155, 156syl3anc 1292 . . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> x e. RR )
158152, 157ffvelrnd 6038 . . . . . . . . 9 |- ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` x ) e. CC )
159158, 136itgcl 22820 . . . . . . . 8 |- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x e. CC )
160159adantr 472 . . . . . . 7 |- ( ( ph /\ T < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x e. CC )
16160adantr 472 . . . . . . . . . 10 |- ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> F : RR --> CC )
16214adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> ( B - X ) e. RR )
1633adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> A e. RR )
164 simpr 468 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> x e. ( ( B - X ) [,] A ) )
165 eliccre 37699 . . . . . . . . . . 11 |- ( ( ( B - X ) e. RR /\ A e. RR /\ x e. ( ( B - X ) [,] A ) ) -> x e. RR )
166162, 163, 164, 165syl3anc 1292 . . . . . . . . . 10 |- ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> x e. RR )
167161, 166ffvelrnd 6038 . . . . . . . . 9 |- ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> ( F ` x ) e. CC )
168167adantlr 729 . . . . . . . 8 |- ( ( ( ph /\ T < X ) /\ x e. ( ( B - X ) [,] A ) ) -> ( F ` x ) e. CC )
169168, 149itgcl 22820 . . . . . . 7 |- ( ( ph /\ T < X ) -> S. ( ( B - X ) [,] A ) ( F ` x ) _d x e. CC )
170108adantr 472 . . . . . . 7 |- ( ( ph /\ T < X ) -> S. ( ( A - X ) [,] A ) ( F ` x ) _d x e. CC )
171160, 169, 170addsubassd 10025 . . . . . 6 |- ( ( 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 ) ) )
172111, 151, 1713eqtrd 2509 . . . . 5 |- ( ( 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 ) ) )
173172oveq2d 6324 . . . 4 |- ( ( 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 ) ) ) )
174160subid1d 9994 . . . 4 |- ( ( ph /\ T < X ) -> ( S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x - 0 ) = S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x )
175159subidd 9993 . . . . . . 7 |- ( ph -> ( S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x - S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x ) = 0 )
176175oveq1d 6323 . . . . . 6 |- ( 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 ) ) )
177176adantr 472 . . . . 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 ) ) = ( 0 - ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) ) )
178169, 170subcld 10005 . . . . . 6 |- ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) e. CC )
179160, 160, 178subsub4d 10036 . . . . 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 ) [,] ( 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 ) ) ) )
180 df-neg 9883 . . . . . 6 |- -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 ) )
181169, 170negsubdi2d 10021 . . . . . 6 |- ( ( 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 ) )
182180, 181syl5eqr 2519 . . . . 5 |- ( ( 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 ) )
183177, 179, 1823eqtr3d 2513 . . . 4 |- ( ( 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 ) )
184173, 174, 1833eqtr3d 2513 . . 3 |- ( ( 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 ) )
185107subidd 9993 . . . . . . . 8 |- ( ph -> ( S. ( ( B - X ) [,] B ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) = 0 )
186185eqcomd 2477 . . . . . . 7 |- ( ph -> 0 = ( S. ( ( B - X ) [,] B ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) )
187186oveq2d 6324 . . . . . 6 |- ( 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 ) ) )
188187adantr 472 . . . . 5 |- ( ( 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 ) ) )
189169addid1d 9851 . . . . 5 |- ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x + 0 ) = S. ( ( B - X ) [,] A ) ( F ` x ) _d x )
190114, 122, 113, 127, 118eliccd 37697 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> A e. ( ( B - X ) [,] B ) )
191100adantlr 729 . . . . . . . . 9 |- ( ( ( ph /\ T < X ) /\ x e. ( ( B - X ) [,] B ) ) -> ( F ` x ) e. CC )
1923, 8iccssred 37698 . . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
19360, 192feqresmpt 5933 . . . . . . . . . . 11 |- ( ph -> ( F |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( F ` x ) ) )
19460, 192fssresd 5762 . . . . . . . . . . . 12 |- ( ph -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> CC )
195 ioossicc 11745 . . . . . . . . . . . . . . 15 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
1963rexrd 9708 . . . . . . . . . . . . . . . . 17 |- ( ph -> A e. RR* )
197196adantr 472 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A e. RR* )
1988rexrd 9708 . . . . . . . . . . . . . . . . 17 |- ( ph -> B e. RR* )
199198adantr 472 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> B e. RR* )
20036, 37, 38fourierdlem15 38096 . . . . . . . . . . . . . . . . 17 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
201200adantr 472 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
202 simpr 468 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
203197, 199, 201, 202fourierdlem8 38089 . . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
204195, 203syl5ss 3429 . . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
205204resabs1d 5140 . . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
206205, 65eqeltrd 2549 . . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
207205eqcomd 2477 . . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
208207oveq1d 6323 . . . . . . . . . . . . 13 |- ( ( 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 ) ) )
20984, 208eleqtrd 2551 . . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
210207oveq1d 6323 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
21188, 210eleqtrd 2551 . . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
21236, 37, 38, 194, 206, 209, 211fourierdlem69 38151 . . . . . . . . . . 11 |- ( ph -> ( F |` ( A [,] B ) ) e. L^1 )
213193, 212eqeltrrd 2550 . . . . . . . . . 10 |- ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. L^1 )
214213adantr 472 . . . . . . . . 9 |- ( ( ph /\ T < X ) -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. L^1 )
215114, 122, 190, 191, 149, 214itgspliticc 22873 . . . . . . . 8 |- ( ( 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 ) )
216215oveq2d 6324 . . . . . . 7 |- ( ( 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 ) ) )
217216oveq2d 6324 . . . . . 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 ) [,] 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 ) ) ) )
218107adantr 472 . . . . . . 7 |- ( ( ph /\ T < X ) -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x e. CC )
219215, 218eqeltrrd 2550 . . . . . . 7 |- ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x + S. ( A [,] B ) ( F ` x ) _d x ) e. CC )
220169, 218, 219addsub12d 10028 . . . . . 6 |- ( ( 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 ) ) ) )
22160adantr 472 . . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A [,] B ) ) -> F : RR --> CC )
2223adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
2238adantr 472 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
224 simpr 468 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
225 eliccre 37699 . . . . . . . . . . . . . 14 |- ( ( A e. RR /\ B e. RR /\ x e. ( A [,] B ) ) -> x e. RR )
226222, 223, 224, 225syl3anc 1292 . . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
227221, 226ffvelrnd 6038 . . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
228227, 213itgcl 22820 . . . . . . . . . . 11 |- ( ph -> S. ( A [,] B ) ( F ` x ) _d x e. CC )
229228adantr 472 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> S. ( A [,] B ) ( F ` x ) _d x e. CC )
230169, 169, 229subsub4d 10036 . . . . . . . . 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 ) ) )
231230eqcomd 2477 . . . . . . . 8 |- ( ( 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 ) )
232231oveq2d 6324 . . . . . . 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. ( ( B - X ) [,] A ) ( F ` x ) _d x - S. ( ( B - X ) [,] A ) ( F ` x ) _d x ) - S. ( A [,] B ) ( F ` x ) _d x ) ) )
233169subidd 9993 . . . . . . . . . 10 |- ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x - S. ( ( B - X ) [,] A ) ( F ` x ) _d x ) = 0 )
234233oveq1d 6323 . . . . . . . . 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 ) = ( 0 - S. ( A [,] B ) ( F ` x ) _d x ) )
235 df-neg 9883 . . . . . . . . 9 |- -u S. ( A [,] B ) ( F ` x ) _d x = ( 0 - S. ( A [,] B ) ( F ` x ) _d x )
236234, 235syl6eqr 2523 . . . . . . . 8 |- ( ( 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 )
237236oveq2d 6324 . . . . . . 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 + -u S. ( A [,] B ) ( F ` x ) _d x ) )
238218, 229negsubd 10011 . . . . . . 7 |- ( ( 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 ) )
239232, 237, 2383eqtrd 2509 . . . . . 6 |- ( ( 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 ) )
240217, 220, 2393eqtrd 2509 . . . . 5 |- ( ( 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 ) )
241188, 189, 2403eqtr3d 2513 . . . 4 |- ( ( 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 ) )
242241oveq2d 6324 . . 3 |- ( ( 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 ) ) )
243108, 107, 228subsubd 10033 . . . . 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 - X ) [,] A ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) + S. ( A [,] B ) ( F ` x ) _d x ) )
24493oveq2d 6324 . . . . . . 7 |- ( 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 ) )
245244, 109eqtrd 2505 . . . . . 6 |- ( ph -> ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) = 0 )
246245oveq1d 6323 . . . . 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 ) = ( 0 + S. ( A [,] B ) ( F ` x ) _d x ) )
247228addid2d 9852 . . . . 5 |- ( ph -> ( 0 + S. ( A [,] B ) ( F ` x ) _d x ) = S. ( A [,] B ) ( F ` x ) _d x )
248243, 246, 2473eqtrd 2509 . . . 4 |- ( 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 )
249248adantr 472 . . 3 |- ( ( 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 )
250184, 242, 2493eqtrd 2509 . 2 |- ( ( ph /\ T < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
25124adantr 472 . . . . 5 |- ( ( ph /\ X <_ T ) -> ( A - X ) e. RR )
25214adantr 472 . . . . 5 |- ( ( ph /\ X <_ T ) -> ( B - X ) e. RR )
2533adantr 472 . . . . . 6 |- ( ( ph /\ X <_ T ) -> A e. RR )
25424, 3, 39ltled 9800 . . . . . . 7 |- ( ph -> ( A - X ) <_ A )
255254adantr 472 . . . . . 6 |- ( ( ph /\ X <_ T ) -> ( A - X ) <_ A )
2566adantr 472 . . . . . . 7 |- ( ( ph /\ X <_ T ) -> X e. RR )
2578adantr 472 . . . . . . 7 |- ( ( ph /\ X <_ T ) -> B e. RR )
258 id 22 . . . . . . . . 9 |- ( X <_ T -> X <_ T )
259258, 1syl6breq 4435 . . . . . . . 8 |- ( X <_ T -> X <_ ( B - A ) )
260259adantl 473 . . . . . . 7 |- ( ( ph /\ X <_ T ) -> X <_ ( B - A ) )
261256, 257, 253, 260lesubd 10238 . . . . . 6 |- ( ( ph /\ X <_ T ) -> A <_ ( B - X ) )
262251, 252, 253, 255, 261eliccd 37697 . . . . 5 |- ( ( ph /\ X <_ T ) -> A e. ( ( A - X ) [,] ( B - X ) ) )
263158adantlr 729 . . . . 5 |- ( ( ( ph /\ X <_ T ) /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` x ) e. CC )
264132, 102, 3, 39, 73eliood 37691 . . . . . . 7 |- ( ph -> A e. ( ( A - X ) (,) +oo ) )
26536, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264fourierdlem105 38187 . . . . . 6 |- ( ph -> ( x e. ( ( A - X ) [,] A ) |-> ( F ` x ) ) e. L^1 )
266265adantr 472 . . . . 5 |- ( ( ph /\ X <_ T ) -> ( x e. ( ( A - X ) [,] A ) |-> ( F ` x ) ) e. L^1 )
2673leidd 10201 . . . . . . . 8 |- ( ph -> A <_ A )
2685rpge0d 11368 . . . . . . . . 9 |- ( ph -> 0 <_ X )
2698, 6subge02d 10226 . . . . . . . . 9 |- ( ph -> ( 0 <_ X <-> ( B - X ) <_ B ) )
270268, 269mpbid 215 . . . . . . . 8 |- ( ph -> ( B - X ) <_ B )
271 iccss 11727 . . . . . . . 8 |- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ A /\ ( B - X ) <_ B ) ) -> ( A [,] ( B - X ) ) C_ ( A [,] B ) )
2723, 8, 267, 270, 271syl22anc 1293 . . . . . . 7 |- ( ph -> ( A [,] ( B - X ) ) C_ ( A [,] B ) )
273 iccmbl 22598 . . . . . . . 8 |- ( ( A e. RR /\ ( B - X ) e. RR ) -> ( A [,] ( B - X ) ) e. dom vol )
2743, 14, 273syl2anc 673 . . . . . . 7 |- ( ph -> ( A [,] ( B - X ) ) e. dom vol )
275272, 274, 227, 213iblss 22841 . . . . . 6 |- ( ph -> ( x e. ( A [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
276275adantr 472 . . . . 5 |- ( ( ph /\ X <_ T ) -> ( x e. ( A [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
277251, 252, 262, 263, 266, 276itgspliticc 22873 . . . 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 ) )
278268adantr 472 . . . . . . . . . 10 |- ( ( ph /\ X <_ T ) -> 0 <_ X )
279269adantr 472 . . . . . . . . . 10 |- ( ( ph /\ X <_ T ) -> ( 0 <_ X <-> ( B - X ) <_ B ) )
280278, 279mpbid 215 . . . . . . . . 9 |- ( ( ph /\ X <_ T ) -> ( B - X ) <_ B )
281253, 257, 252, 261, 280eliccd 37697 . . . . . . . 8 |- ( ( ph /\ X <_ T ) -> ( B - X ) e. ( A [,] B ) )
282227adantlr 729 . . . . . . . 8 |- ( ( ( ph /\ X <_ T ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
2838leidd 10201 . . . . . . . . . . 11 |- ( ph -> B <_ B )
284283adantr 472 . . . . . . . . . 10 |- ( ( ph /\ X <_ T ) -> B <_ B )
285 iccss 11727 . . . . . . . . . 10 |- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ ( B - X ) /\ B <_ B ) ) -> ( ( B - X ) [,] B ) C_ ( A [,] B ) )
286253, 257, 261, 284, 285syl22anc 1293 . . . . . . . . 9 |- ( ( ph /\ X <_ T ) -> ( ( B - X ) [,] B ) C_ ( A [,] B ) )
287 iccmbl 22598 . . . . . . . . . . 11 |- ( ( ( B - X ) e. RR /\ B e. RR ) -> ( ( B - X ) [,] B ) e. dom vol )
28814, 8, 287syl2anc 673 . . . . . . . . . 10 |- ( ph -> ( ( B - X ) [,] B ) e. dom vol )
289288adantr 472 . . . . . . . . 9 |- ( ( ph /\ X <_ T ) -> ( ( B - X ) [,] B ) e. dom vol )
290213adantr 472 . . . . . . . . 9 |- ( ( ph /\ X <_ T ) -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. L^1 )
291286, 289, 282, 290iblss 22841 . . . . . . . 8 |- ( ( ph /\ X <_ T ) -> ( x e. ( ( B - X ) [,] B ) |-> ( F ` x ) ) e. L^1 )
292253, 257, 281, 282, 276, 291itgspliticc 22873 . . . . . . 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 ) )
293292oveq1d 6323 . . . . . 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 ) )
29460adantr 472 . . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> F : RR --> CC )
2953adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> A e. RR )
29614adantr 472 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> ( B - X ) e. RR )
297 simpr 468 . . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> x e. ( A [,] ( B - X ) ) )
298 eliccre 37699 . . . . . . . . . . 11 |- ( ( A e. RR /\ ( B - X ) e. RR /\ x e. ( A [,] ( B - X ) ) ) -> x e. RR )
299295, 296, 297, 298syl3anc 1292 . . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> x e. RR )
300294, 299ffvelrnd 6038 . . . . . . . . 9 |- ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> ( F ` x ) e. CC )
301300, 275itgcl 22820 . . . . . . . 8 |- ( ph -> S. ( A [,] ( B - X ) ) ( F ` x ) _d x e. CC )
302301, 107, 107addsubassd 10025 . . . . . . 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 ) ) )
303302adantr 472 . . . . . 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 ) ) )
304185oveq2d 6324 . . . . . . . 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 ) )
305301addid1d 9851 . . . . . . . 8 |- ( ph -> ( S. ( A [,] ( B - X ) ) ( F ` x ) _d x + 0 ) = S. ( A [,] ( B - X ) ) ( F ` x ) _d x )
306304, 305eqtrd 2505 . . . . . . 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 )
307306adantr 472 . . . . . 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 )
308293, 303, 3073eqtrrd 2510 . . . . 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 ) )
309308oveq2d 6324 . . . 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 ) ) )
31093adantr 472 . . . . . . 7 |- ( ( ph /\ X <_ T ) -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x = S. ( ( A - X ) [,] A ) ( F ` x ) _d x )
311107adantr 472 . . . . . . 7 |- ( ( ph /\ X <_ T ) -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x e. CC )
312310, 311eqeltrrd 2550 . . . . . 6 |- ( ( ph /\ X <_ T ) -> S. ( ( A - X ) [,] A ) ( F ` x ) _d x e. CC )
313282, 290itgcl 22820 . . . . . 6 |- ( ( ph /\ X <_ T ) -> S. ( A [,] B ) ( F ` x ) _d x e. CC )
314312, 313, 311addsub12d 10028 . . . . 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 ) ) )
315313, 312, 311addsubassd 10025 . . . . 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 ) ) )
316314, 315eqtr4d 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 ) )
317277, 309, 3163eqtrd 2509 . . 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 ) )
318310oveq2d 6324 . . 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 ) )
319313, 312pncand 10006 . . 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 )
320317, 318, 3193eqtrd 2509 . 2 |- ( ( ph /\ X <_ T ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
321250, 320, 47, 6ltlecasei 9760 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:   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   A.wral 2756   E.wrex 2757   {crab 2760   u. cun 3388   C_ wss 3390   ifcif 3872   {cpr 3961   class class class wbr 4395   |-> cmpt 4454   dom cdm 4839   ran crn 4840   |` cres 4841   iotacio 5551   -->wf 5585   ` cfv 5589   Isom wiso 5590  (class class class)co 6308   ^m cmap 7490   supcsup 7972   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   x. cmul 9562   +oocpnf 9690   RR*cxr 9692   < clt 9693   <_ cle 9694   - cmin 9880   -ucneg 9881   / cdiv 10291   NNcn 10631   ZZcz 10961   RR+crp 11325   (,)cioo 11660   (,]cioc 11661   [,]cicc 11663   ...cfz 11810  ..^cfzo 11942   |_cfl 12059   #chash 12553   -cn->ccncf 21986   volcvol 22493   L^1cibl 22654   S.citg 22655   lim CC climc 22896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cc 8883  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-omul 7205  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-acn 8394  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-haus 20408  df-cmp 20479  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-ovol 22494  df-vol 22496  df-mbf 22656  df-itg1 22657  df-itg2 22658  df-ibl 22659  df-itg 22660  df-0p 22707  df-ditg 22881  df-limc 22900  df-dv 22901
This theorem is referenced by:  fourierdlem108  38190
  Copyright terms: Public domain W3C validator