Metamath Proof Explorer

Theorem fourierdlem109

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem109.a 
|- ( ph -> A e. RR )
fourierdlem109.b 
|- ( ph -> B e. RR )
fourierdlem109.t 
|- T = ( B - A )
fourierdlem109.x 
|- ( ph -> X e. RR )
fourierdlem109.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 ) ) ) } )
fourierdlem109.m 
|- ( ph -> M e. NN )
fourierdlem109.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem109.f 
|- ( ph -> F : RR --> CC )
fourierdlem109.fper 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem109.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem109.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem109.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem109.o 
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem109.h 
|- H = ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
fourierdlem109.n 
|- N = ( ( # ` H ) - 1 )
fourierdlem109.16 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem109.17 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem109.18 
|- J = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem109.19 
|- I = ( x e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
Assertion fourierdlem109 
|- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step Hyp Ref Expression
1 fourierdlem109.a 
 |-  ( ph -> A e. RR )
2 fourierdlem109.b 
 |-  ( ph -> B e. RR )
3 fourierdlem109.t 
 |-  T = ( B - A )
4 fourierdlem109.x 
 |-  ( ph -> X e. RR )
5 fourierdlem109.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 fourierdlem109.m 
 |-  ( ph -> M e. NN )
7 fourierdlem109.q 
 |-  ( ph -> Q e. ( P ` M ) )
8 fourierdlem109.f 
 |-  ( ph -> F : RR --> CC )
9 fourierdlem109.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
10 fourierdlem109.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem109.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12 fourierdlem109.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
13 fourierdlem109.o 
 |-  O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
14 fourierdlem109.h 
 |-  H = ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
15 fourierdlem109.n 
 |-  N = ( ( # ` H ) - 1 )
16 fourierdlem109.16 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
17 fourierdlem109.17 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
18 fourierdlem109.18 
 |-  J = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
19 fourierdlem109.19 
 |-  I = ( x e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
20 1 adantr 
 |-  ( ( ph /\ 0 < X ) -> A e. RR )
21 2 adantr 
 |-  ( ( ph /\ 0 < X ) -> B e. RR )
22 4 adantr 
 |-  ( ( ph /\ 0 < X ) -> X e. RR )
23 simpr 
 |-  ( ( ph /\ 0 < X ) -> 0 < X )
24 22 23 elrpd 
 |-  ( ( ph /\ 0 < X ) -> X e. RR+ )
25 6 adantr 
 |-  ( ( ph /\ 0 < X ) -> M e. NN )
26 7 adantr 
 |-  ( ( ph /\ 0 < X ) -> Q e. ( P ` M ) )
27 8 adantr 
 |-  ( ( ph /\ 0 < X ) -> F : RR --> CC )
28 9 adantlr 
 |-  ( ( ( ph /\ 0 < X ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
29 10 adantlr 
 |-  ( ( ( ph /\ 0 < X ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
30 11 adantlr 
 |-  ( ( ( ph /\ 0 < X ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
31 12 adantlr 
 |-  ( ( ( ph /\ 0 < X ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
32 20 21 3 24 5 25 26 27 28 29 30 31 fourierdlem108 
 |-  ( ( ph /\ 0 < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
33 oveq2 
 |-  ( X = 0 -> ( A - X ) = ( A - 0 ) )
34 1 recnd 
 |-  ( ph -> A e. CC )
35 34 subid1d 
 |-  ( ph -> ( A - 0 ) = A )
36 33 35 sylan9eqr 
 |-  ( ( ph /\ X = 0 ) -> ( A - X ) = A )
37 oveq2 
 |-  ( X = 0 -> ( B - X ) = ( B - 0 ) )
38 2 recnd 
 |-  ( ph -> B e. CC )
39 38 subid1d 
 |-  ( ph -> ( B - 0 ) = B )
40 37 39 sylan9eqr 
 |-  ( ( ph /\ X = 0 ) -> ( B - X ) = B )
41 36 40 oveq12d 
 |-  ( ( ph /\ X = 0 ) -> ( ( A - X ) [,] ( B - X ) ) = ( A [,] B ) )
42 41 itgeq1d 
 |-  ( ( ph /\ X = 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
43 42 adantlr 
 |-  ( ( ( ph /\ -. 0 < X ) /\ X = 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
44 simpll 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> ph )
45 44 4 syl 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> X e. RR )
46 0red 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> 0 e. RR )
47 simpr 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> -. X = 0 )
48 47 neqned 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> X =/= 0 )
49 simplr 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> -. 0 < X )
50 45 46 48 49 lttri5d 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> X < 0 )
51 4 recnd 
 |-  ( ph -> X e. CC )
52 34 51 subcld 
 |-  ( ph -> ( A - X ) e. CC )
53 52 51 subnegd 
 |-  ( ph -> ( ( A - X ) - -u X ) = ( ( A - X ) + X ) )
54 34 51 npcand 
 |-  ( ph -> ( ( A - X ) + X ) = A )
55 53 54 eqtrd 
 |-  ( ph -> ( ( A - X ) - -u X ) = A )
56 38 51 subcld 
 |-  ( ph -> ( B - X ) e. CC )
57 56 51 subnegd 
 |-  ( ph -> ( ( B - X ) - -u X ) = ( ( B - X ) + X ) )
58 38 51 npcand 
 |-  ( ph -> ( ( B - X ) + X ) = B )
59 57 58 eqtrd 
 |-  ( ph -> ( ( B - X ) - -u X ) = B )
60 55 59 oveq12d 
 |-  ( ph -> ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) = ( A [,] B ) )
61 60 eqcomd 
 |-  ( ph -> ( A [,] B ) = ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) )
62 61 itgeq1d 
 |-  ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) ( F ` x ) _d x )
63 62 adantr 
 |-  ( ( ph /\ X < 0 ) -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) ( F ` x ) _d x )
64 1 4 resubcld 
 |-  ( ph -> ( A - X ) e. RR )
65 64 adantr 
 |-  ( ( ph /\ X < 0 ) -> ( A - X ) e. RR )
66 2 4 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
67 66 adantr 
 |-  ( ( ph /\ X < 0 ) -> ( B - X ) e. RR )
68 eqid 
 |-  ( ( B - X ) - ( A - X ) ) = ( ( B - X ) - ( A - X ) )
69 4 renegcld 
 |-  ( ph -> -u X e. RR )
70 69 adantr 
 |-  ( ( ph /\ X < 0 ) -> -u X e. RR )
71 4 lt0neg1d 
 |-  ( ph -> ( X < 0 <-> 0 < -u X ) )
72 71 biimpa 
 |-  ( ( ph /\ X < 0 ) -> 0 < -u X )
73 70 72 elrpd 
 |-  ( ( ph /\ X < 0 ) -> -u X e. RR+ )
74 fveq2 
 |-  ( i = j -> ( p ` i ) = ( p ` j ) )
75 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
76 75 fveq2d 
 |-  ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
77 74 76 breq12d 
 |-  ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
78 77 cbvralvw 
 |-  ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) )
79 78 anbi2i 
 |-  ( ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
80 79 a1i 
 |-  ( p e. ( RR ^m ( 0 ... m ) ) -> ( ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) ) )
81 80 rabbiia 
 |-  { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) }
82 81 mpteq2i 
 |-  ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ 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 ) = ( B - X ) ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
83 13 82 eqtri 
 |-  O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = ( B - X ) ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
84 5 6 7 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
85 84 simp3d 
 |-  ( ph -> A < B )
86 1 2 4 85 ltsub1dd 
 |-  ( ph -> ( A - X ) < ( B - X ) )
87 3 5 6 7 64 66 86 13 14 15 16 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
88 87 simpld 
 |-  ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
89 88 simpld 
 |-  ( ph -> N e. NN )
90 89 adantr 
 |-  ( ( ph /\ X < 0 ) -> N e. NN )
91 88 simprd 
 |-  ( ph -> S e. ( O ` N ) )
92 91 adantr 
 |-  ( ( ph /\ X < 0 ) -> S e. ( O ` N ) )
93 8 adantr 
 |-  ( ( ph /\ X < 0 ) -> F : RR --> CC )
94 38 34 51 nnncan2d 
 |-  ( ph -> ( ( B - X ) - ( A - X ) ) = ( B - A ) )
95 94 3 eqtr4di 
 |-  ( ph -> ( ( B - X ) - ( A - X ) ) = T )
96 95 oveq2d 
 |-  ( ph -> ( x + ( ( B - X ) - ( A - X ) ) ) = ( x + T ) )
97 96 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( B - X ) - ( A - X ) ) ) = ( x + T ) )
98 97 fveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + ( ( B - X ) - ( A - X ) ) ) ) = ( F ` ( x + T ) ) )
99 98 9 eqtrd 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + ( ( B - X ) - ( A - X ) ) ) ) = ( F ` x ) )
100 99 adantlr 
 |-  ( ( ( ph /\ X < 0 ) /\ x e. RR ) -> ( F ` ( x + ( ( B - X ) - ( A - X ) ) ) ) = ( F ` x ) )
101 6 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> M e. NN )
102 7 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Q e. ( P ` M ) )
103 8 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> F : RR --> CC )
104 9 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
105 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 ) )
106 64 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A - X ) e. RR )
107 64 rexrd 
 |-  ( ph -> ( A - X ) e. RR* )
108 pnfxr 
 |-  +oo e. RR*
109 108 a1i 
 |-  ( ph -> +oo e. RR* )
110 66 ltpnfd 
 |-  ( ph -> ( B - X ) < +oo )
111 107 109 66 86 110 eliood 
 |-  ( ph -> ( B - X ) e. ( ( A - X ) (,) +oo ) )
112 111 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - X ) e. ( ( A - X ) (,) +oo ) )
113 oveq1 
 |-  ( x = y -> ( x + ( k x. T ) ) = ( y + ( k x. T ) ) )
114 113 eleq1d 
 |-  ( x = y -> ( ( x + ( k x. T ) ) e. ran Q <-> ( y + ( k x. T ) ) e. ran Q ) )
115 114 rexbidv 
 |-  ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. T ) ) e. ran Q ) )
116 115 cbvrabv 
 |-  { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } = { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q }
117 116 uneq2i 
 |-  ( { ( A - X ) , ( B - X ) } u. { x e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) = ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
118 14 117 eqtri 
 |-  H = ( { ( A - X ) , ( B - X ) } u. { y e. ( ( A - X ) [,] ( B - X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
119 simpr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) )
120 eqid 
 |-  ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) )
121 eqid 
 |-  ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) = ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) )
122 eqid 
 |-  ( y e. ( ( ( J ` ( E ` ( S ` j ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) (,) ( ( E ` ( S ` ( j + 1 ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) |-> ( ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) ` ( y - ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) ) = ( y e. ( ( ( J ` ( E ` ( S ` j ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) (,) ( ( E ` ( S ` ( j + 1 ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) |-> ( ( F |` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) ` ( y - ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) )
123 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
124 123 breq1d 
 |-  ( j = i -> ( ( Q ` j ) <_ ( J ` ( E ` x ) ) <-> ( Q ` i ) <_ ( J ` ( E ` x ) ) ) )
125 124 cbvrabv 
 |-  { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) }
126 125 supeq1i 
 |-  sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < )
127 126 mpteq2i 
 |-  ( x e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( J ` ( E ` x ) ) } , RR , < ) ) = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
128 19 127 eqtri 
 |-  I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
129 5 3 101 102 103 104 105 106 112 13 118 15 16 17 18 119 120 121 122 128 fourierdlem90 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
130 129 adantlr 
 |-  ( ( ( ph /\ X < 0 ) /\ j e. ( 0 ..^ N ) ) -> ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
131 11 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
132 eqid 
 |-  ( i e. ( 0 ..^ M ) |-> R ) = ( i e. ( 0 ..^ M ) |-> R )
133 5 3 101 102 103 104 105 131 106 112 13 118 15 16 17 18 119 120 128 132 fourierdlem89 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> if ( ( J ` ( E ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` j ) ) ) , ( ( i e. ( 0 ..^ M ) |-> R ) ` ( I ` ( S ` j ) ) ) , ( F ` ( J ` ( E ` ( S ` j ) ) ) ) ) e. ( ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
134 133 adantlr 
 |-  ( ( ( ph /\ X < 0 ) /\ j e. ( 0 ..^ N ) ) -> if ( ( J ` ( E ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` j ) ) ) , ( ( i e. ( 0 ..^ M ) |-> R ) ` ( I ` ( S ` j ) ) ) , ( F ` ( J ` ( E ` ( S ` j ) ) ) ) ) e. ( ( F |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
135 12 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
136 eqid 
 |-  ( i e. ( 0 ..^ M ) |-> L ) = ( i e. ( 0 ..^ M ) |-> L )
137 5 3 101 102 103 104 105 135 106 112 13 118 15 16 17 18 119 120 128 136 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 ) ) ) )
138 137 adantlr 
 |-  ( ( ( ph /\ X < 0 ) /\ 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 ) ) ) )
139 65 67 68 73 83 90 92 93 100 130 134 138 fourierdlem108 
 |-  ( ( ph /\ X < 0 ) -> S. ( ( ( A - X ) - -u X ) [,] ( ( B - X ) - -u X ) ) ( F ` x ) _d x = S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x )
140 63 139 eqtr2d 
 |-  ( ( ph /\ X < 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
141 44 50 140 syl2anc 
 |-  ( ( ( ph /\ -. 0 < X ) /\ -. X = 0 ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
142 43 141 pm2.61dan 
 |-  ( ( ph /\ -. 0 < X ) -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
143 32 142 pm2.61dan 
 |-  ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )