Metamath Proof Explorer

Theorem fourierdlem107

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 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)

Ref Expression
Hypotheses 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 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem107.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( 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 fourierdlem107 
|- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step Hyp Ref Expression
1 fourierdlem107.a 
 |-  ( ph -> A e. RR )
2 fourierdlem107.b 
 |-  ( ph -> B e. RR )
3 fourierdlem107.t 
 |-  T = ( B - A )
4 fourierdlem107.x 
 |-  ( ph -> X e. RR+ )
5 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 ) ) ) } )
6 fourierdlem107.m 
 |-  ( ph -> M e. NN )
7 fourierdlem107.q 
 |-  ( ph -> Q e. ( P ` M ) )
8 fourierdlem107.f 
 |-  ( ph -> F : RR --> CC )
9 fourierdlem107.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
10 fourierdlem107.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem107.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12 fourierdlem107.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
13 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 ) ) ) } )
14 fourierdlem107.h 
 |-  H = ( { ( A - X ) , A } u. { y e. ( ( A - X ) [,] A ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
15 fourierdlem107.n 
 |-  N = ( ( # ` H ) - 1 )
16 fourierdlem107.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
17 fourierdlem107.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
18 fourierdlem107.z 
 |-  Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
19 fourierdlem107.i 
 |-  I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
20 3 oveq2i 
 |-  ( ( A - X ) + T ) = ( ( A - X ) + ( B - A ) )
21 1 recnd 
 |-  ( ph -> A e. CC )
22 4 rpred 
 |-  ( ph -> X e. RR )
23 22 recnd 
 |-  ( ph -> X e. CC )
24 2 recnd 
 |-  ( ph -> B e. CC )
25 21 23 24 21 subadd4b 
 |-  ( ph -> ( ( A - X ) + ( B - A ) ) = ( ( A - A ) + ( B - X ) ) )
26 20 25 syl5eq 
 |-  ( ph -> ( ( A - X ) + T ) = ( ( A - A ) + ( B - X ) ) )
27 21 subidd 
 |-  ( ph -> ( A - A ) = 0 )
28 27 oveq1d 
 |-  ( ph -> ( ( A - A ) + ( B - X ) ) = ( 0 + ( B - X ) ) )
29 2 22 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
30 29 recnd 
 |-  ( ph -> ( B - X ) e. CC )
31 30 addid2d 
 |-  ( ph -> ( 0 + ( B - X ) ) = ( B - X ) )
32 26 28 31 3eqtrd 
 |-  ( ph -> ( ( A - X ) + T ) = ( B - X ) )
33 3 oveq2i 
 |-  ( A + T ) = ( A + ( B - A ) )
34 21 24 pncan3d 
 |-  ( ph -> ( A + ( B - A ) ) = B )
35 33 34 syl5eq 
 |-  ( ph -> ( A + T ) = B )
36 32 35 oveq12d 
 |-  ( ph -> ( ( ( A - X ) + T ) [,] ( A + T ) ) = ( ( B - X ) [,] B ) )
37 36 eqcomd 
 |-  ( ph -> ( ( B - X ) [,] B ) = ( ( ( A - X ) + T ) [,] ( A + T ) ) )
38 37 itgeq1d 
 |-  ( ph -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x = S. ( ( ( A - X ) + T ) [,] ( A + T ) ) ( F ` x ) _d x )
39 1 22 resubcld 
 |-  ( ph -> ( A - X ) e. RR )
40 fveq2 
 |-  ( i = j -> ( p ` i ) = ( p ` j ) )
41 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
42 41 fveq2d 
 |-  ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
43 40 42 breq12d 
 |-  ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
44 43 cbvralvw 
 |-  ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) )
45 44 a1i 
 |-  ( m e. NN -> ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
46 45 anbi2d 
 |-  ( 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 ) ) ) ) )
47 46 rabbidv 
 |-  ( 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 ) ) ) } )
48 47 mpteq2ia 
 |-  ( 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 ) ) ) } )
49 13 48 eqtri 
 |-  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 ) ) ) } )
50 1 4 ltsubrpd 
 |-  ( ph -> ( A - X ) < A )
51 3 5 6 7 39 1 50 13 14 15 16 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
52 51 simpld 
 |-  ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
53 52 simpld 
 |-  ( ph -> N e. NN )
54 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
55 3 54 eqeltrid 
 |-  ( ph -> T e. RR )
56 52 simprd 
 |-  ( ph -> S e. ( O ` N ) )
57 39 adantr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> ( A - X ) e. RR )
58 1 adantr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> A e. RR )
59 simpr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> x e. ( ( A - X ) [,] A ) )
60 eliccre 
 |-  ( ( ( A - X ) e. RR /\ A e. RR /\ x e. ( ( A - X ) [,] A ) ) -> x e. RR )
61 57 58 59 60 syl3anc 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> x e. RR )
62 61 9 syldan 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
63 fveq2 
 |-  ( i = j -> ( S ` i ) = ( S ` j ) )
64 63 oveq1d 
 |-  ( i = j -> ( ( S ` i ) + T ) = ( ( S ` j ) + T ) )
65 64 cbvmptv 
 |-  ( i e. ( 0 ... N ) |-> ( ( S ` i ) + T ) ) = ( j e. ( 0 ... N ) |-> ( ( S ` j ) + T ) )
66 eqid 
 |-  ( 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 ) ) ) } )
67 6 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> M e. NN )
68 7 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Q e. ( P ` M ) )
69 8 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> F : RR --> CC )
70 9 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
71 10 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
72 39 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A - X ) e. RR )
73 72 rexrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A - X ) e. RR* )
74 pnfxr 
 |-  +oo e. RR*
75 74 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> +oo e. RR* )
76 1 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR )
77 50 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A - X ) < A )
78 1 ltpnfd 
 |-  ( ph -> A < +oo )
79 78 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A < +oo )
80 73 75 76 77 79 eliood 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. ( ( A - X ) (,) +oo ) )
81 simpr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) )
82 eqid 
 |-  ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) )
83 eqid 
 |-  ( F |` ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) = ( F |` ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) )
84 eqid 
 |-  ( 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 ) ) ) ) ) ) )
85 5 3 67 68 69 70 71 72 80 13 14 15 16 17 18 81 82 83 84 19 fourierdlem90 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
86 11 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
87 eqid 
 |-  ( i e. ( 0 ..^ M ) |-> R ) = ( i e. ( 0 ..^ M ) |-> R )
88 5 3 67 68 69 70 71 86 72 80 13 14 15 16 17 18 81 82 19 87 fourierdlem89 
 |-  ( ( 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 ) ) ) ) limCC ( S ` j ) ) )
89 12 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
90 eqid 
 |-  ( i e. ( 0 ..^ M ) |-> L ) = ( i e. ( 0 ..^ M ) |-> L )
91 5 3 67 68 69 70 71 89 72 80 13 14 15 16 17 18 81 82 19 90 fourierdlem91 
 |-  ( ( 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 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
92 39 1 49 53 55 56 62 65 66 8 85 88 91 fourierdlem92 
 |-  ( ph -> S. ( ( ( A - X ) + T ) [,] ( A + T ) ) ( F ` x ) _d x = S. ( ( A - X ) [,] A ) ( F ` x ) _d x )
93 38 92 eqtrd 
 |-  ( ph -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x = S. ( ( A - X ) [,] A ) ( F ` x ) _d x )
94 8 adantr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> F : RR --> CC )
95 29 adantr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> ( B - X ) e. RR )
96 2 adantr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> B e. RR )
97 simpr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> x e. ( ( B - X ) [,] B ) )
98 eliccre 
 |-  ( ( ( B - X ) e. RR /\ B e. RR /\ x e. ( ( B - X ) [,] B ) ) -> x e. RR )
99 95 96 97 98 syl3anc 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> x e. RR )
100 94 99 ffvelrnd 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] B ) ) -> ( F ` x ) e. CC )
101 29 rexrd 
 |-  ( ph -> ( B - X ) e. RR* )
102 74 a1i 
 |-  ( ph -> +oo e. RR* )
103 2 4 ltsubrpd 
 |-  ( ph -> ( B - X ) < B )
104 2 ltpnfd 
 |-  ( ph -> B < +oo )
105 101 102 2 103 104 eliood 
 |-  ( ph -> B e. ( ( B - X ) (,) +oo ) )
106 5 3 6 7 8 9 10 11 12 29 105 fourierdlem105 
 |-  ( ph -> ( x e. ( ( B - X ) [,] B ) |-> ( F ` x ) ) e. L^1 )
107 100 106 itgcl 
 |-  ( ph -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x e. CC )
108 93 107 eqeltrrd 
 |-  ( ph -> S. ( ( A - X ) [,] A ) ( F ` x ) _d x e. CC )
109 108 subidd 
 |-  ( ph -> ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) = 0 )
110 109 eqcomd 
 |-  ( ph -> 0 = ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) )
111 110 adantr 
 |-  ( ( ph /\ T < X ) -> 0 = ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) )
112 39 adantr 
 |-  ( ( ph /\ T < X ) -> ( A - X ) e. RR )
113 1 adantr 
 |-  ( ( ph /\ T < X ) -> A e. RR )
114 29 adantr 
 |-  ( ( ph /\ T < X ) -> ( B - X ) e. RR )
115 5 6 7 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
116 115 simp3d 
 |-  ( ph -> A < B )
117 1 2 116 ltled 
 |-  ( ph -> A <_ B )
118 117 adantr 
 |-  ( ( ph /\ T < X ) -> A <_ B )
119 1 2 22 lesub1d 
 |-  ( ph -> ( A <_ B <-> ( A - X ) <_ ( B - X ) ) )
120 119 adantr 
 |-  ( ( ph /\ T < X ) -> ( A <_ B <-> ( A - X ) <_ ( B - X ) ) )
121 118 120 mpbid 
 |-  ( ( ph /\ T < X ) -> ( A - X ) <_ ( B - X ) )
122 2 adantr 
 |-  ( ( ph /\ T < X ) -> B e. RR )
123 22 adantr 
 |-  ( ( ph /\ T < X ) -> X e. RR )
124 simpr 
 |-  ( ( ph /\ T < X ) -> T < X )
125 3 124 eqbrtrrid 
 |-  ( ( ph /\ T < X ) -> ( B - A ) < X )
126 122 113 123 125 ltsub23d 
 |-  ( ( ph /\ T < X ) -> ( B - X ) < A )
127 114 113 126 ltled 
 |-  ( ( ph /\ T < X ) -> ( B - X ) <_ A )
128 112 113 114 121 127 eliccd 
 |-  ( ( ph /\ T < X ) -> ( B - X ) e. ( ( A - X ) [,] A ) )
129 8 adantr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> F : RR --> CC )
130 129 61 ffvelrnd 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] A ) ) -> ( F ` x ) e. CC )
131 130 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ x e. ( ( A - X ) [,] A ) ) -> ( F ` x ) e. CC )
132 39 rexrd 
 |-  ( ph -> ( A - X ) e. RR* )
133 1 2 22 116 ltsub1dd 
 |-  ( ph -> ( A - X ) < ( B - X ) )
134 29 ltpnfd 
 |-  ( ph -> ( B - X ) < +oo )
135 132 102 29 133 134 eliood 
 |-  ( ph -> ( B - X ) e. ( ( A - X ) (,) +oo ) )
136 5 3 6 7 8 9 10 11 12 39 135 fourierdlem105 
 |-  ( ph -> ( x e. ( ( A - X ) [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
137 136 adantr 
 |-  ( ( ph /\ T < X ) -> ( x e. ( ( A - X ) [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
138 6 adantr 
 |-  ( ( ph /\ T < X ) -> M e. NN )
139 7 adantr 
 |-  ( ( ph /\ T < X ) -> Q e. ( P ` M ) )
140 8 adantr 
 |-  ( ( ph /\ T < X ) -> F : RR --> CC )
141 9 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
142 10 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
143 11 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
144 12 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
145 101 adantr 
 |-  ( ( ph /\ T < X ) -> ( B - X ) e. RR* )
146 74 a1i 
 |-  ( ( ph /\ T < X ) -> +oo e. RR* )
147 113 ltpnfd 
 |-  ( ( ph /\ T < X ) -> A < +oo )
148 145 146 113 126 147 eliood 
 |-  ( ( ph /\ T < X ) -> A e. ( ( B - X ) (,) +oo ) )
149 5 3 138 139 140 141 142 143 144 114 148 fourierdlem105 
 |-  ( ( ph /\ T < X ) -> ( x e. ( ( B - X ) [,] A ) |-> ( F ` x ) ) e. L^1 )
150 112 113 128 131 137 149 itgspliticc 
 |-  ( ( 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 ) )
151 150 oveq1d 
 |-  ( ( 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 ) )
152 8 adantr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> F : RR --> CC )
153 39 adantr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) e. RR )
154 29 adantr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( B - X ) e. RR )
155 simpr 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> x e. ( ( A - X ) [,] ( B - X ) ) )
156 eliccre 
 |-  ( ( ( A - X ) e. RR /\ ( B - X ) e. RR /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> x e. RR )
157 153 154 155 156 syl3anc 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> x e. RR )
158 152 157 ffvelrnd 
 |-  ( ( ph /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` x ) e. CC )
159 158 136 itgcl 
 |-  ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x e. CC )
160 159 adantr 
 |-  ( ( ph /\ T < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x e. CC )
161 8 adantr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> F : RR --> CC )
162 29 adantr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> ( B - X ) e. RR )
163 1 adantr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> A e. RR )
164 simpr 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> x e. ( ( B - X ) [,] A ) )
165 eliccre 
 |-  ( ( ( B - X ) e. RR /\ A e. RR /\ x e. ( ( B - X ) [,] A ) ) -> x e. RR )
166 162 163 164 165 syl3anc 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> x e. RR )
167 161 166 ffvelrnd 
 |-  ( ( ph /\ x e. ( ( B - X ) [,] A ) ) -> ( F ` x ) e. CC )
168 167 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ x e. ( ( B - X ) [,] A ) ) -> ( F ` x ) e. CC )
169 168 149 itgcl 
 |-  ( ( ph /\ T < X ) -> S. ( ( B - X ) [,] A ) ( F ` x ) _d x e. CC )
170 108 adantr 
 |-  ( ( ph /\ T < X ) -> S. ( ( A - X ) [,] A ) ( F ` x ) _d x e. CC )
171 160 169 170 addsubassd 
 |-  ( ( 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 ) ) )
172 111 151 171 3eqtrd 
 |-  ( ( 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 ) ) )
173 172 oveq2d 
 |-  ( ( 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 ) ) ) )
174 160 subid1d 
 |-  ( ( ph /\ T < X ) -> ( S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x - 0 ) = S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x )
175 159 subidd 
 |-  ( ph -> ( S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x - S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x ) = 0 )
176 175 oveq1d 
 |-  ( 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 ) ) )
177 176 adantr 
 |-  ( ( 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 ) ) )
178 169 170 subcld 
 |-  ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x - S. ( ( A - X ) [,] A ) ( F ` x ) _d x ) e. CC )
179 160 160 178 subsub4d 
 |-  ( ( 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 
 |-  -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 ) )
181 169 170 negsubdi2d 
 |-  ( ( 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 ) )
182 180 181 eqtr3id 
 |-  ( ( 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 ) )
183 177 179 182 3eqtr3d 
 |-  ( ( 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 ) )
184 173 174 183 3eqtr3d 
 |-  ( ( 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 ) )
185 107 subidd 
 |-  ( ph -> ( S. ( ( B - X ) [,] B ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) = 0 )
186 185 eqcomd 
 |-  ( ph -> 0 = ( S. ( ( B - X ) [,] B ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) )
187 186 oveq2d 
 |-  ( 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 ) ) )
188 187 adantr 
 |-  ( ( 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 ) ) )
189 169 addid1d 
 |-  ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x + 0 ) = S. ( ( B - X ) [,] A ) ( F ` x ) _d x )
190 114 122 113 127 118 eliccd 
 |-  ( ( ph /\ T < X ) -> A e. ( ( B - X ) [,] B ) )
191 100 adantlr 
 |-  ( ( ( ph /\ T < X ) /\ x e. ( ( B - X ) [,] B ) ) -> ( F ` x ) e. CC )
192 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
193 8 192 feqresmpt 
 |-  ( ph -> ( F |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( F ` x ) ) )
194 8 192 fssresd 
 |-  ( ph -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> CC )
195 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
196 1 rexrd 
 |-  ( ph -> A e. RR* )
197 196 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR* )
198 2 rexrd 
 |-  ( ph -> B e. RR* )
199 198 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> B e. RR* )
200 5 6 7 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
201 200 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
202 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
203 197 199 201 202 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
204 195 203 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
205 204 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
206 205 10 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
207 205 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
208 207 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
209 11 208 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
210 207 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
211 12 210 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( ( F |` ( A [,] B ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
212 5 6 7 194 206 209 211 fourierdlem69 
 |-  ( ph -> ( F |` ( A [,] B ) ) e. L^1 )
213 193 212 eqeltrrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. L^1 )
214 213 adantr 
 |-  ( ( ph /\ T < X ) -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. L^1 )
215 114 122 190 191 149 214 itgspliticc 
 |-  ( ( 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 ) )
216 215 oveq2d 
 |-  ( ( 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 ) ) )
217 216 oveq2d 
 |-  ( ( 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 ) ) ) )
218 107 adantr 
 |-  ( ( ph /\ T < X ) -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x e. CC )
219 215 218 eqeltrrd 
 |-  ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x + S. ( A [,] B ) ( F ` x ) _d x ) e. CC )
220 169 218 219 addsub12d 
 |-  ( ( 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 ) ) ) )
221 8 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> F : RR --> CC )
222 1 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
223 2 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
224 simpr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
225 eliccre 
 |-  ( ( A e. RR /\ B e. RR /\ x e. ( A [,] B ) ) -> x e. RR )
226 222 223 224 225 syl3anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
227 221 226 ffvelrnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
228 227 213 itgcl 
 |-  ( ph -> S. ( A [,] B ) ( F ` x ) _d x e. CC )
229 228 adantr 
 |-  ( ( ph /\ T < X ) -> S. ( A [,] B ) ( F ` x ) _d x e. CC )
230 169 169 229 subsub4d 
 |-  ( ( 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 ) ) )
231 230 eqcomd 
 |-  ( ( 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 ) )
232 231 oveq2d 
 |-  ( ( 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 ) ) )
233 169 subidd 
 |-  ( ( ph /\ T < X ) -> ( S. ( ( B - X ) [,] A ) ( F ` x ) _d x - S. ( ( B - X ) [,] A ) ( F ` x ) _d x ) = 0 )
234 233 oveq1d 
 |-  ( ( 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 
 |-  -u S. ( A [,] B ) ( F ` x ) _d x = ( 0 - S. ( A [,] B ) ( F ` x ) _d x )
236 234 235 eqtr4di 
 |-  ( ( 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 )
237 236 oveq2d 
 |-  ( ( 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 ) )
238 218 229 negsubd 
 |-  ( ( 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 ) )
239 232 237 238 3eqtrd 
 |-  ( ( 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 ) )
240 217 220 239 3eqtrd 
 |-  ( ( 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 ) )
241 188 189 240 3eqtr3d 
 |-  ( ( 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 ) )
242 241 oveq2d 
 |-  ( ( 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 ) ) )
243 108 107 228 subsubd 
 |-  ( 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 ) )
244 93 oveq2d 
 |-  ( 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 ) )
245 244 109 eqtrd 
 |-  ( ph -> ( S. ( ( A - X ) [,] A ) ( F ` x ) _d x - S. ( ( B - X ) [,] B ) ( F ` x ) _d x ) = 0 )
246 245 oveq1d 
 |-  ( 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 ) )
247 228 addid2d 
 |-  ( ph -> ( 0 + S. ( A [,] B ) ( F ` x ) _d x ) = S. ( A [,] B ) ( F ` x ) _d x )
248 243 246 247 3eqtrd 
 |-  ( 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 )
249 248 adantr 
 |-  ( ( 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 )
250 184 242 249 3eqtrd 
 |-  ( ( ph /\ T < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
251 39 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( A - X ) e. RR )
252 29 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( B - X ) e. RR )
253 1 adantr 
 |-  ( ( ph /\ X <_ T ) -> A e. RR )
254 39 1 50 ltled 
 |-  ( ph -> ( A - X ) <_ A )
255 254 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( A - X ) <_ A )
256 22 adantr 
 |-  ( ( ph /\ X <_ T ) -> X e. RR )
257 2 adantr 
 |-  ( ( ph /\ X <_ T ) -> B e. RR )
258 id 
 |-  ( X <_ T -> X <_ T )
259 258 3 breqtrdi 
 |-  ( X <_ T -> X <_ ( B - A ) )
260 259 adantl 
 |-  ( ( ph /\ X <_ T ) -> X <_ ( B - A ) )
261 256 257 253 260 lesubd 
 |-  ( ( ph /\ X <_ T ) -> A <_ ( B - X ) )
262 251 252 253 255 261 eliccd 
 |-  ( ( ph /\ X <_ T ) -> A e. ( ( A - X ) [,] ( B - X ) ) )
263 158 adantlr 
 |-  ( ( ( ph /\ X <_ T ) /\ x e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` x ) e. CC )
264 132 102 1 50 78 eliood 
 |-  ( ph -> A e. ( ( A - X ) (,) +oo ) )
265 5 3 6 7 8 9 10 11 12 39 264 fourierdlem105 
 |-  ( ph -> ( x e. ( ( A - X ) [,] A ) |-> ( F ` x ) ) e. L^1 )
266 265 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( x e. ( ( A - X ) [,] A ) |-> ( F ` x ) ) e. L^1 )
267 1 leidd 
 |-  ( ph -> A <_ A )
268 4 rpge0d 
 |-  ( ph -> 0 <_ X )
269 2 22 subge02d 
 |-  ( ph -> ( 0 <_ X <-> ( B - X ) <_ B ) )
270 268 269 mpbid 
 |-  ( ph -> ( B - X ) <_ B )
271 iccss 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ A /\ ( B - X ) <_ B ) ) -> ( A [,] ( B - X ) ) C_ ( A [,] B ) )
272 1 2 267 270 271 syl22anc 
 |-  ( ph -> ( A [,] ( B - X ) ) C_ ( A [,] B ) )
273 iccmbl 
 |-  ( ( A e. RR /\ ( B - X ) e. RR ) -> ( A [,] ( B - X ) ) e. dom vol )
274 1 29 273 syl2anc 
 |-  ( ph -> ( A [,] ( B - X ) ) e. dom vol )
275 272 274 227 213 iblss 
 |-  ( ph -> ( x e. ( A [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
276 275 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( x e. ( A [,] ( B - X ) ) |-> ( F ` x ) ) e. L^1 )
277 251 252 262 263 266 276 itgspliticc 
 |-  ( ( 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 ) )
278 268 adantr 
 |-  ( ( ph /\ X <_ T ) -> 0 <_ X )
279 269 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( 0 <_ X <-> ( B - X ) <_ B ) )
280 278 279 mpbid 
 |-  ( ( ph /\ X <_ T ) -> ( B - X ) <_ B )
281 253 257 252 261 280 eliccd 
 |-  ( ( ph /\ X <_ T ) -> ( B - X ) e. ( A [,] B ) )
282 227 adantlr 
 |-  ( ( ( ph /\ X <_ T ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
283 2 leidd 
 |-  ( ph -> B <_ B )
284 283 adantr 
 |-  ( ( ph /\ X <_ T ) -> B <_ B )
285 iccss 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ ( B - X ) /\ B <_ B ) ) -> ( ( B - X ) [,] B ) C_ ( A [,] B ) )
286 253 257 261 284 285 syl22anc 
 |-  ( ( ph /\ X <_ T ) -> ( ( B - X ) [,] B ) C_ ( A [,] B ) )
287 iccmbl 
 |-  ( ( ( B - X ) e. RR /\ B e. RR ) -> ( ( B - X ) [,] B ) e. dom vol )
288 29 2 287 syl2anc 
 |-  ( ph -> ( ( B - X ) [,] B ) e. dom vol )
289 288 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( ( B - X ) [,] B ) e. dom vol )
290 213 adantr 
 |-  ( ( ph /\ X <_ T ) -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. L^1 )
291 286 289 282 290 iblss 
 |-  ( ( ph /\ X <_ T ) -> ( x e. ( ( B - X ) [,] B ) |-> ( F ` x ) ) e. L^1 )
292 253 257 281 282 276 291 itgspliticc 
 |-  ( ( 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 ) )
293 292 oveq1d 
 |-  ( ( 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 ) )
294 8 adantr 
 |-  ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> F : RR --> CC )
295 1 adantr 
 |-  ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> A e. RR )
296 29 adantr 
 |-  ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> ( B - X ) e. RR )
297 simpr 
 |-  ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> x e. ( A [,] ( B - X ) ) )
298 eliccre 
 |-  ( ( A e. RR /\ ( B - X ) e. RR /\ x e. ( A [,] ( B - X ) ) ) -> x e. RR )
299 295 296 297 298 syl3anc 
 |-  ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> x e. RR )
300 294 299 ffvelrnd 
 |-  ( ( ph /\ x e. ( A [,] ( B - X ) ) ) -> ( F ` x ) e. CC )
301 300 275 itgcl 
 |-  ( ph -> S. ( A [,] ( B - X ) ) ( F ` x ) _d x e. CC )
302 301 107 107 addsubassd 
 |-  ( 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 ) ) )
303 302 adantr 
 |-  ( ( 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 ) ) )
304 185 oveq2d 
 |-  ( 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 ) )
305 301 addid1d 
 |-  ( ph -> ( S. ( A [,] ( B - X ) ) ( F ` x ) _d x + 0 ) = S. ( A [,] ( B - X ) ) ( F ` x ) _d x )
306 304 305 eqtrd 
 |-  ( 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 )
307 306 adantr 
 |-  ( ( 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 )
308 293 303 307 3eqtrrd 
 |-  ( ( 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 ) )
309 308 oveq2d 
 |-  ( ( 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 ) ) )
310 93 adantr 
 |-  ( ( ph /\ X <_ T ) -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x = S. ( ( A - X ) [,] A ) ( F ` x ) _d x )
311 107 adantr 
 |-  ( ( ph /\ X <_ T ) -> S. ( ( B - X ) [,] B ) ( F ` x ) _d x e. CC )
312 310 311 eqeltrrd 
 |-  ( ( ph /\ X <_ T ) -> S. ( ( A - X ) [,] A ) ( F ` x ) _d x e. CC )
313 282 290 itgcl 
 |-  ( ( ph /\ X <_ T ) -> S. ( A [,] B ) ( F ` x ) _d x e. CC )
314 312 313 311 addsub12d 
 |-  ( ( 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 ) ) )
315 313 312 311 addsubassd 
 |-  ( ( 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 ) ) )
316 314 315 eqtr4d 
 |-  ( ( 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 ) )
317 277 309 316 3eqtrd 
 |-  ( ( 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 ) )
318 310 oveq2d 
 |-  ( ( 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 ) )
319 313 312 pncand 
 |-  ( ( 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 )
320 317 318 319 3eqtrd 
 |-  ( ( ph /\ X <_ T ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
321 250 320 55 22 ltlecasei 
 |-  ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )