Metamath Proof Explorer

Theorem fourierdlem92

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem92.a 
|- ( ph -> A e. RR )
fourierdlem92.b 
|- ( ph -> B e. RR )
fourierdlem92.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 ) ) ) } )
fourierdlem92.m 
|- ( ph -> M e. NN )
fourierdlem92.t 
|- ( ph -> T e. RR )
fourierdlem92.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem92.fper 
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem92.s 
|- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
fourierdlem92.h 
|- H = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem92.f 
|- ( ph -> F : RR --> CC )
fourierdlem92.cncf 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem92.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem92.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem92 
|- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step Hyp Ref Expression
1 fourierdlem92.a 
 |-  ( ph -> A e. RR )
2 fourierdlem92.b 
 |-  ( ph -> B e. RR )
3 fourierdlem92.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 ) ) ) } )
4 fourierdlem92.m 
 |-  ( ph -> M e. NN )
5 fourierdlem92.t 
 |-  ( ph -> T e. RR )
6 fourierdlem92.q 
 |-  ( ph -> Q e. ( P ` M ) )
7 fourierdlem92.fper 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
8 fourierdlem92.s 
 |-  S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
9 fourierdlem92.h 
 |-  H = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
10 fourierdlem92.f 
 |-  ( ph -> F : RR --> CC )
11 fourierdlem92.cncf 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
12 fourierdlem92.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
13 fourierdlem92.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
14 1 adantr 
 |-  ( ( ph /\ 0 < T ) -> A e. RR )
15 2 adantr 
 |-  ( ( ph /\ 0 < T ) -> B e. RR )
16 4 adantr 
 |-  ( ( ph /\ 0 < T ) -> M e. NN )
17 5 adantr 
 |-  ( ( ph /\ 0 < T ) -> T e. RR )
18 simpr 
 |-  ( ( ph /\ 0 < T ) -> 0 < T )
19 17 18 elrpd 
 |-  ( ( ph /\ 0 < T ) -> T e. RR+ )
20 6 adantr 
 |-  ( ( ph /\ 0 < T ) -> Q e. ( P ` M ) )
21 7 adantlr 
 |-  ( ( ( ph /\ 0 < T ) /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
22 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
23 22 oveq1d 
 |-  ( j = i -> ( ( Q ` j ) + T ) = ( ( Q ` i ) + T ) )
24 23 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
25 10 adantr 
 |-  ( ( ph /\ 0 < T ) -> F : RR --> CC )
26 11 adantlr 
 |-  ( ( ( ph /\ 0 < T ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
27 12 adantlr 
 |-  ( ( ( ph /\ 0 < T ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
28 13 adantlr 
 |-  ( ( ( ph /\ 0 < T ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
29 eqeq1 
 |-  ( y = x -> ( y = ( Q ` i ) <-> x = ( Q ` i ) ) )
30 eqeq1 
 |-  ( y = x -> ( y = ( Q ` ( i + 1 ) ) <-> x = ( Q ` ( i + 1 ) ) ) )
31 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
32 30 31 ifbieq2d 
 |-  ( y = x -> if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
33 29 32 ifbieq2d 
 |-  ( y = x -> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
34 33 cbvmptv 
 |-  ( y e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
35 eqid 
 |-  ( x e. ( ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` i ) [,] ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` ( i + 1 ) ) ) |-> ( ( y e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) ` ( x - T ) ) ) = ( x e. ( ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` i ) [,] ( ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) ` ( i + 1 ) ) ) |-> ( ( y e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( y = ( Q ` i ) , R , if ( y = ( Q ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) ` ( x - T ) ) )
36 14 15 3 16 19 20 21 24 25 26 27 28 34 35 fourierdlem81 
 |-  ( ( ph /\ 0 < T ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
37 simpr 
 |-  ( ( ph /\ T = 0 ) -> T = 0 )
38 37 oveq2d 
 |-  ( ( ph /\ T = 0 ) -> ( A + T ) = ( A + 0 ) )
39 1 recnd 
 |-  ( ph -> A e. CC )
40 39 adantr 
 |-  ( ( ph /\ T = 0 ) -> A e. CC )
41 40 addid1d 
 |-  ( ( ph /\ T = 0 ) -> ( A + 0 ) = A )
42 38 41 eqtrd 
 |-  ( ( ph /\ T = 0 ) -> ( A + T ) = A )
43 37 oveq2d 
 |-  ( ( ph /\ T = 0 ) -> ( B + T ) = ( B + 0 ) )
44 2 recnd 
 |-  ( ph -> B e. CC )
45 44 adantr 
 |-  ( ( ph /\ T = 0 ) -> B e. CC )
46 45 addid1d 
 |-  ( ( ph /\ T = 0 ) -> ( B + 0 ) = B )
47 43 46 eqtrd 
 |-  ( ( ph /\ T = 0 ) -> ( B + T ) = B )
48 42 47 oveq12d 
 |-  ( ( ph /\ T = 0 ) -> ( ( A + T ) [,] ( B + T ) ) = ( A [,] B ) )
49 48 itgeq1d 
 |-  ( ( ph /\ T = 0 ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
50 49 adantlr 
 |-  ( ( ( ph /\ -. 0 < T ) /\ T = 0 ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
51 simpll 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ph )
52 simpr 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> -. T = 0 )
53 simplr 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> -. 0 < T )
54 ioran 
 |-  ( -. ( T = 0 \/ 0 < T ) <-> ( -. T = 0 /\ -. 0 < T ) )
55 52 53 54 sylanbrc 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> -. ( T = 0 \/ 0 < T ) )
56 51 5 syl 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> T e. RR )
57 0red 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> 0 e. RR )
58 56 57 lttrid 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ( T < 0 <-> -. ( T = 0 \/ 0 < T ) ) )
59 55 58 mpbird 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> T < 0 )
60 56 lt0neg1d 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> ( T < 0 <-> 0 < -u T ) )
61 59 60 mpbid 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> 0 < -u T )
62 1 5 readdcld 
 |-  ( ph -> ( A + T ) e. RR )
63 62 recnd 
 |-  ( ph -> ( A + T ) e. CC )
64 5 recnd 
 |-  ( ph -> T e. CC )
65 63 64 negsubd 
 |-  ( ph -> ( ( A + T ) + -u T ) = ( ( A + T ) - T ) )
66 39 64 pncand 
 |-  ( ph -> ( ( A + T ) - T ) = A )
67 65 66 eqtrd 
 |-  ( ph -> ( ( A + T ) + -u T ) = A )
68 2 5 readdcld 
 |-  ( ph -> ( B + T ) e. RR )
69 68 recnd 
 |-  ( ph -> ( B + T ) e. CC )
70 69 64 negsubd 
 |-  ( ph -> ( ( B + T ) + -u T ) = ( ( B + T ) - T ) )
71 44 64 pncand 
 |-  ( ph -> ( ( B + T ) - T ) = B )
72 70 71 eqtrd 
 |-  ( ph -> ( ( B + T ) + -u T ) = B )
73 67 72 oveq12d 
 |-  ( ph -> ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) = ( A [,] B ) )
74 73 eqcomd 
 |-  ( ph -> ( A [,] B ) = ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) )
75 74 itgeq1d 
 |-  ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) ( F ` x ) _d x )
76 75 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) ( F ` x ) _d x )
77 1 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> A e. RR )
78 5 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> T e. RR )
79 77 78 readdcld 
 |-  ( ( ph /\ 0 < -u T ) -> ( A + T ) e. RR )
80 2 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> B e. RR )
81 80 78 readdcld 
 |-  ( ( ph /\ 0 < -u T ) -> ( B + T ) e. RR )
82 eqid 
 |-  ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
83 4 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> M e. NN )
84 78 renegcld 
 |-  ( ( ph /\ 0 < -u T ) -> -u T e. RR )
85 simpr 
 |-  ( ( ph /\ 0 < -u T ) -> 0 < -u T )
86 84 85 elrpd 
 |-  ( ( ph /\ 0 < -u T ) -> -u T e. RR+ )
87 3 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
88 4 87 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
89 6 88 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
90 89 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
91 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
92 90 91 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
93 92 ffvelrnda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
94 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> T e. RR )
95 93 94 readdcld 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) + T ) e. RR )
96 95 8 fmptd 
 |-  ( ph -> S : ( 0 ... M ) --> RR )
97 reex 
 |-  RR e. _V
98 97 a1i 
 |-  ( ph -> RR e. _V )
99 ovex 
 |-  ( 0 ... M ) e. _V
100 99 a1i 
 |-  ( ph -> ( 0 ... M ) e. _V )
101 98 100 elmapd 
 |-  ( ph -> ( S e. ( RR ^m ( 0 ... M ) ) <-> S : ( 0 ... M ) --> RR ) )
102 96 101 mpbird 
 |-  ( ph -> S e. ( RR ^m ( 0 ... M ) ) )
103 8 a1i 
 |-  ( ph -> S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) )
104 fveq2 
 |-  ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
105 104 oveq1d 
 |-  ( i = 0 -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
106 105 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
107 0zd 
 |-  ( ph -> 0 e. ZZ )
108 4 nnzd 
 |-  ( ph -> M e. ZZ )
109 107 108 107 3jca 
 |-  ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
110 0le0 
 |-  0 <_ 0
111 110 a1i 
 |-  ( ph -> 0 <_ 0 )
112 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
113 112 nn0ge0d 
 |-  ( M e. NN -> 0 <_ M )
114 4 113 syl 
 |-  ( ph -> 0 <_ M )
115 109 111 114 jca32 
 |-  ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
116 elfz2 
 |-  ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
117 115 116 sylibr 
 |-  ( ph -> 0 e. ( 0 ... M ) )
118 92 117 ffvelrnd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
119 118 5 readdcld 
 |-  ( ph -> ( ( Q ` 0 ) + T ) e. RR )
120 103 106 117 119 fvmptd 
 |-  ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
121 simprll 
 |-  ( ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) -> ( Q ` 0 ) = A )
122 89 121 syl 
 |-  ( ph -> ( Q ` 0 ) = A )
123 122 oveq1d 
 |-  ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
124 120 123 eqtrd 
 |-  ( ph -> ( S ` 0 ) = ( A + T ) )
125 fveq2 
 |-  ( i = M -> ( Q ` i ) = ( Q ` M ) )
126 125 oveq1d 
 |-  ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
127 126 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
128 4 nnnn0d 
 |-  ( ph -> M e. NN0 )
129 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
130 128 129 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
131 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
132 130 131 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
133 92 132 ffvelrnd 
 |-  ( ph -> ( Q ` M ) e. RR )
134 133 5 readdcld 
 |-  ( ph -> ( ( Q ` M ) + T ) e. RR )
135 103 127 132 134 fvmptd 
 |-  ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
136 simprlr 
 |-  ( ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) -> ( Q ` M ) = B )
137 89 136 syl 
 |-  ( ph -> ( Q ` M ) = B )
138 137 oveq1d 
 |-  ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
139 135 138 eqtrd 
 |-  ( ph -> ( S ` M ) = ( B + T ) )
140 124 139 jca 
 |-  ( ph -> ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) )
141 92 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
142 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
143 142 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
144 141 143 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
145 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
146 145 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
147 141 146 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
148 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. RR )
149 89 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
150 149 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
151 144 147 148 150 ltadd1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
152 144 148 readdcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
153 8 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
154 143 152 153 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
155 8 24 eqtr4i 
 |-  S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
156 155 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) )
157 fveq2 
 |-  ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
158 157 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
159 158 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
160 147 148 readdcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
161 156 159 146 160 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
162 151 154 161 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
163 162 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) )
164 102 140 163 jca32 
 |-  ( ph -> ( S e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0 ..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
165 9 fourierdlem2 
 |-  ( M e. NN -> ( S e. ( H ` M ) <-> ( S e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0 ..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
166 4 165 syl 
 |-  ( ph -> ( S e. ( H ` M ) <-> ( S e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) /\ A. i e. ( 0 ..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
167 164 166 mpbird 
 |-  ( ph -> S e. ( H ` M ) )
168 9 fveq1i 
 |-  ( H ` M ) = ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M )
169 167 168 eleqtrdi 
 |-  ( ph -> S e. ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M ) )
170 169 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> S e. ( ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( A + T ) /\ ( p ` m ) = ( B + T ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` M ) )
171 62 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR )
172 68 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR )
173 simpr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
174 eliccre 
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
175 171 172 173 174 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
176 175 recnd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. CC )
177 64 negcld 
 |-  ( ph -> -u T e. CC )
178 177 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> -u T e. CC )
179 176 178 addcld 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. CC )
180 simpl 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ph )
181 1 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A e. RR )
182 2 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> B e. RR )
183 5 renegcld 
 |-  ( ph -> -u T e. RR )
184 183 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> -u T e. RR )
185 175 184 readdcld 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. RR )
186 65 66 eqtr2d 
 |-  ( ph -> A = ( ( A + T ) + -u T ) )
187 186 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A = ( ( A + T ) + -u T ) )
188 171 rexrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR* )
189 172 rexrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR* )
190 iccgelb 
 |-  ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
191 188 189 173 190 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
192 171 175 184 191 leadd1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) + -u T ) <_ ( x + -u T ) )
193 187 192 eqbrtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A <_ ( x + -u T ) )
194 iccleub 
 |-  ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
195 188 189 173 194 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
196 175 172 184 195 leadd1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) <_ ( ( B + T ) + -u T ) )
197 172 recnd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. CC )
198 64 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. CC )
199 197 198 negsubd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) + -u T ) = ( ( B + T ) - T ) )
200 71 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
201 199 200 eqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) + -u T ) = B )
202 196 201 breqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) <_ B )
203 181 182 185 193 202 eliccd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. ( A [,] B ) )
204 180 203 jca 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ph /\ ( x + -u T ) e. ( A [,] B ) ) )
205 eleq1 
 |-  ( y = ( x + -u T ) -> ( y e. ( A [,] B ) <-> ( x + -u T ) e. ( A [,] B ) ) )
206 205 anbi2d 
 |-  ( y = ( x + -u T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x + -u T ) e. ( A [,] B ) ) ) )
207 oveq1 
 |-  ( y = ( x + -u T ) -> ( y + T ) = ( ( x + -u T ) + T ) )
208 207 fveq2d 
 |-  ( y = ( x + -u T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x + -u T ) + T ) ) )
209 fveq2 
 |-  ( y = ( x + -u T ) -> ( F ` y ) = ( F ` ( x + -u T ) ) )
210 208 209 eqeq12d 
 |-  ( y = ( x + -u T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) )
211 206 210 imbi12d 
 |-  ( y = ( x + -u T ) -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ ( x + -u T ) e. ( A [,] B ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) ) )
212 eleq1 
 |-  ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
213 212 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ y e. ( A [,] B ) ) ) )
214 oveq1 
 |-  ( x = y -> ( x + T ) = ( y + T ) )
215 214 fveq2d 
 |-  ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
216 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
217 215 216 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
218 213 217 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
219 218 7 chvarvv 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) )
220 211 219 vtoclg 
 |-  ( ( x + -u T ) e. CC -> ( ( ph /\ ( x + -u T ) e. ( A [,] B ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) )
221 179 204 220 sylc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) )
222 176 198 negsubd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) = ( x - T ) )
223 222 oveq1d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) + T ) = ( ( x - T ) + T ) )
224 176 198 npcand 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
225 223 224 eqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) + T ) = x )
226 225 fveq2d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` x ) )
227 221 226 eqtr3d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x + -u T ) ) = ( F ` x ) )
228 227 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x + -u T ) ) = ( F ` x ) )
229 fveq2 
 |-  ( j = i -> ( S ` j ) = ( S ` i ) )
230 229 oveq1d 
 |-  ( j = i -> ( ( S ` j ) + -u T ) = ( ( S ` i ) + -u T ) )
231 230 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) = ( i e. ( 0 ... M ) |-> ( ( S ` i ) + -u T ) )
232 10 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> F : RR --> CC )
233 10 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> CC )
234 ioossre 
 |-  ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR
235 234 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR )
236 233 235 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
237 154 161 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) = ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
238 144 147 148 iooshift 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } )
239 237 238 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } )
240 239 mpteq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( F ` x ) ) )
241 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ph )
242 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> i e. ( 0 ..^ M ) )
243 238 eleq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) <-> x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) )
244 243 biimpar 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
245 144 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
246 245 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) e. RR* )
247 147 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
248 247 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
249 elioore 
 |-  ( x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) -> x e. RR )
250 249 adantl 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
251 5 adantr 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
252 250 251 resubcld 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
253 252 3adant2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
254 144 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
255 64 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. CC )
256 254 255 pncand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
257 256 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
258 257 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
259 152 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR )
260 250 3adant2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
261 5 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
262 152 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) e. RR* )
263 262 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR* )
264 160 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
265 264 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
266 simp3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
267 ioogtlb 
 |-  ( ( ( ( Q ` i ) + T ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR* /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) < x )
268 263 265 266 267 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) < x )
269 259 260 261 268 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` i ) + T ) - T ) < ( x - T ) )
270 258 269 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) < ( x - T ) )
271 160 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
272 iooltub 
 |-  ( ( ( ( Q ` i ) + T ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR* /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x < ( ( Q ` ( i + 1 ) ) + T ) )
273 263 265 266 272 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x < ( ( Q ` ( i + 1 ) ) + T ) )
274 260 271 261 273 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
275 147 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
276 275 255 pncand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
277 276 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
278 274 277 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
279 246 248 253 270 278 eliood 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
280 241 242 244 279 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
281 fvres 
 |-  ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
282 280 281 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
283 241 244 252 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( x - T ) e. RR )
284 1 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A e. RR )
285 2 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> B e. RR )
286 66 eqcomd 
 |-  ( ph -> A = ( ( A + T ) - T ) )
287 286 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A = ( ( A + T ) - T ) )
288 62 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) e. RR )
289 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR )
290 1 rexrd 
 |-  ( ph -> A e. RR* )
291 290 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR* )
292 2 rexrd 
 |-  ( ph -> B e. RR* )
293 292 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> B e. RR* )
294 3 4 6 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
295 294 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
296 295 143 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( A [,] B ) )
297 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` i ) e. ( A [,] B ) ) -> A <_ ( Q ` i ) )
298 291 293 296 297 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A <_ ( Q ` i ) )
299 289 144 148 298 leadd1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A + T ) <_ ( ( Q ` i ) + T ) )
300 299 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) <_ ( ( Q ` i ) + T ) )
301 288 259 260 300 268 lelttrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) < x )
302 288 260 261 301 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( A + T ) - T ) < ( x - T ) )
303 287 302 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A < ( x - T ) )
304 284 253 303 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A <_ ( x - T ) )
305 147 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
306 295 146 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( A [,] B ) )
307 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` ( i + 1 ) ) e. ( A [,] B ) ) -> ( Q ` ( i + 1 ) ) <_ B )
308 291 293 306 307 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) <_ B )
309 308 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) <_ B )
310 253 305 285 278 309 ltletrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < B )
311 253 285 310 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) <_ B )
312 284 285 253 304 311 eliccd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( A [,] B ) )
313 241 242 244 312 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( x - T ) e. ( A [,] B ) )
314 241 313 jca 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( ph /\ ( x - T ) e. ( A [,] B ) ) )
315 eleq1 
 |-  ( y = ( x - T ) -> ( y e. ( A [,] B ) <-> ( x - T ) e. ( A [,] B ) ) )
316 315 anbi2d 
 |-  ( y = ( x - T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x - T ) e. ( A [,] B ) ) ) )
317 oveq1 
 |-  ( y = ( x - T ) -> ( y + T ) = ( ( x - T ) + T ) )
318 317 fveq2d 
 |-  ( y = ( x - T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x - T ) + T ) ) )
319 fveq2 
 |-  ( y = ( x - T ) -> ( F ` y ) = ( F ` ( x - T ) ) )
320 318 319 eqeq12d 
 |-  ( y = ( x - T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
321 316 320 imbi12d 
 |-  ( y = ( x - T ) -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) ) )
322 321 219 vtoclg 
 |-  ( ( x - T ) e. RR -> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
323 283 314 322 sylc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) )
324 244 249 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> x e. RR )
325 recn 
 |-  ( x e. RR -> x e. CC )
326 325 adantl 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
327 64 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. CC )
328 326 327 npcand 
 |-  ( ( ph /\ x e. RR ) -> ( ( x - T ) + T ) = x )
329 328 fveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` x ) )
330 241 324 329 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` x ) )
331 282 323 330 3eqtr2rd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ( F ` x ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
332 331 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( F ` x ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
333 236 240 332 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
334 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
335 334 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
336 eqeq1 
 |-  ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
337 336 rexbidv 
 |-  ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
338 oveq1 
 |-  ( z = y -> ( z + T ) = ( y + T ) )
339 338 eqeq2d 
 |-  ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
340 339 cbvrexvw 
 |-  ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) )
341 337 340 bitrdi 
 |-  ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) ) )
342 341 cbvrabv 
 |-  { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) }
343 eqid 
 |-  ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) = ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
344 335 255 342 11 343 cncfshift 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) e. ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) )
345 239 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
346 345 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) = ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
347 344 346 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
348 333 347 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
349 348 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
350 ffdm 
 |-  ( F : RR --> CC -> ( F : dom F --> CC /\ dom F C_ RR ) )
351 10 350 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ RR ) )
352 351 simpld 
 |-  ( ph -> F : dom F --> CC )
353 352 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : dom F --> CC )
354 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
355 fdm 
 |-  ( F : RR --> CC -> dom F = RR )
356 233 355 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom F = RR )
357 354 356 sseqtrrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
358 342 eqcomi 
 |-  { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) }
359 235 345 356 3sstr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } C_ dom F )
360 342 359 eqsstrrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } C_ dom F )
361 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
362 361 290 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
363 361 292 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
364 361 294 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
365 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
366 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
367 366 sseli 
 |-  ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
368 367 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
369 362 363 364 365 368 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( A [,] B ) )
370 eleq1 
 |-  ( x = z -> ( x e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
371 370 anbi2d 
 |-  ( x = z -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
372 oveq1 
 |-  ( x = z -> ( x + T ) = ( z + T ) )
373 372 fveq2d 
 |-  ( x = z -> ( F ` ( x + T ) ) = ( F ` ( z + T ) ) )
374 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
375 373 374 eqeq12d 
 |-  ( x = z -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( z + T ) ) = ( F ` z ) ) )
376 371 375 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) ) ) )
377 376 7 chvarvv 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
378 361 369 377 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
379 353 335 357 255 358 360 378 12 limcperiod 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } ) limCC ( ( Q ` i ) + T ) ) )
380 358 345 syl5eq 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
381 380 reseq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } ) = ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
382 154 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
383 381 382 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } ) limCC ( ( Q ` i ) + T ) ) = ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` i ) ) )
384 379 383 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` i ) ) )
385 384 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` i ) ) )
386 353 335 357 255 358 360 378 13 limcperiod 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } ) limCC ( ( Q ` ( i + 1 ) ) + T ) ) )
387 161 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
388 381 387 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } ) limCC ( ( Q ` ( i + 1 ) ) + T ) ) = ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` ( i + 1 ) ) ) )
389 386 388 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` ( i + 1 ) ) ) )
390 389 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` ( i + 1 ) ) ) )
391 eqeq1 
 |-  ( y = x -> ( y = ( S ` i ) <-> x = ( S ` i ) ) )
392 eqeq1 
 |-  ( y = x -> ( y = ( S ` ( i + 1 ) ) <-> x = ( S ` ( i + 1 ) ) ) )
393 392 31 ifbieq2d 
 |-  ( y = x -> if ( y = ( S ` ( i + 1 ) ) , L , ( F ` y ) ) = if ( x = ( S ` ( i + 1 ) ) , L , ( F ` x ) ) )
394 391 393 ifbieq2d 
 |-  ( y = x -> if ( y = ( S ` i ) , R , if ( y = ( S ` ( i + 1 ) ) , L , ( F ` y ) ) ) = if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
395 394 cbvmptv 
 |-  ( y e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( y = ( S ` i ) , R , if ( y = ( S ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
396 eqid 
 |-  ( x e. ( ( ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) ` i ) [,] ( ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) ` ( i + 1 ) ) ) |-> ( ( y e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( y = ( S ` i ) , R , if ( y = ( S ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) ` ( x - -u T ) ) ) = ( x e. ( ( ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) ` i ) [,] ( ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) ` ( i + 1 ) ) ) |-> ( ( y e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( y = ( S ` i ) , R , if ( y = ( S ` ( i + 1 ) ) , L , ( F ` y ) ) ) ) ` ( x - -u T ) ) )
397 79 81 82 83 86 170 228 231 232 349 385 390 395 396 fourierdlem81 
 |-  ( ( ph /\ 0 < -u T ) -> S. ( ( ( A + T ) + -u T ) [,] ( ( B + T ) + -u T ) ) ( F ` x ) _d x = S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x )
398 76 397 eqtr2d 
 |-  ( ( ph /\ 0 < -u T ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
399 51 61 398 syl2anc 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
400 50 399 pm2.61dan 
 |-  ( ( ph /\ -. 0 < T ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
401 36 400 pm2.61dan 
 |-  ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )