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 addridd 
 |-  ( ( 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 addridd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 0le0 
 |-  0 <_ 0
110 109 a1i 
 |-  ( ph -> 0 <_ 0 )
111 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
112 111 nn0ge0d 
 |-  ( M e. NN -> 0 <_ M )
113 4 112 syl 
 |-  ( ph -> 0 <_ M )
114 107 108 107 110 113 elfzd 
 |-  ( ph -> 0 e. ( 0 ... M ) )
115 92 114 ffvelcdmd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
116 115 5 readdcld 
 |-  ( ph -> ( ( Q ` 0 ) + T ) e. RR )
117 103 106 114 116 fvmptd 
 |-  ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
118 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 )
119 89 118 syl 
 |-  ( ph -> ( Q ` 0 ) = A )
120 119 oveq1d 
 |-  ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
121 117 120 eqtrd 
 |-  ( ph -> ( S ` 0 ) = ( A + T ) )
122 fveq2 
 |-  ( i = M -> ( Q ` i ) = ( Q ` M ) )
123 122 oveq1d 
 |-  ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
124 123 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
125 4 nnnn0d 
 |-  ( ph -> M e. NN0 )
126 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
127 125 126 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
128 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
129 127 128 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
130 92 129 ffvelcdmd 
 |-  ( ph -> ( Q ` M ) e. RR )
131 130 5 readdcld 
 |-  ( ph -> ( ( Q ` M ) + T ) e. RR )
132 103 124 129 131 fvmptd 
 |-  ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
133 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 )
134 89 133 syl 
 |-  ( ph -> ( Q ` M ) = B )
135 134 oveq1d 
 |-  ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
136 132 135 eqtrd 
 |-  ( ph -> ( S ` M ) = ( B + T ) )
137 121 136 jca 
 |-  ( ph -> ( ( S ` 0 ) = ( A + T ) /\ ( S ` M ) = ( B + T ) ) )
138 92 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
139 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
140 139 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
141 138 140 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
142 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
143 142 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
144 138 143 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
145 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. RR )
146 89 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
147 146 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
148 141 144 145 147 ltadd1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
149 141 145 readdcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
150 8 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
151 140 149 150 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
152 8 24 eqtr4i 
 |-  S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
153 152 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) )
154 fveq2 
 |-  ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
155 154 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
156 155 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
157 144 145 readdcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
158 153 156 143 157 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
159 148 151 158 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
160 159 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( S ` i ) < ( S ` ( i + 1 ) ) )
161 102 137 160 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 ) ) ) ) )
162 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 ) ) ) ) ) )
163 4 162 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 ) ) ) ) ) )
164 161 163 mpbird 
 |-  ( ph -> S e. ( H ` M ) )
165 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 )
166 164 165 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 ) )
167 166 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 ) )
168 62 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR )
169 68 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR )
170 simpr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
171 eliccre 
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
172 168 169 170 171 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
173 172 recnd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. CC )
174 64 negcld 
 |-  ( ph -> -u T e. CC )
175 174 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> -u T e. CC )
176 173 175 addcld 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. CC )
177 simpl 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ph )
178 1 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A e. RR )
179 2 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> B e. RR )
180 5 renegcld 
 |-  ( ph -> -u T e. RR )
181 180 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> -u T e. RR )
182 172 181 readdcld 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. RR )
183 65 66 eqtr2d 
 |-  ( ph -> A = ( ( A + T ) + -u T ) )
184 183 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A = ( ( A + T ) + -u T ) )
185 168 rexrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR* )
186 169 rexrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR* )
187 iccgelb 
 |-  ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
188 185 186 170 187 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
189 168 172 181 188 leadd1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) + -u T ) <_ ( x + -u T ) )
190 184 189 eqbrtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A <_ ( x + -u T ) )
191 iccleub 
 |-  ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
192 185 186 170 191 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
193 172 169 181 192 leadd1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) <_ ( ( B + T ) + -u T ) )
194 169 recnd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. CC )
195 64 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. CC )
196 194 195 negsubd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) + -u T ) = ( ( B + T ) - T ) )
197 71 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
198 196 197 eqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) + -u T ) = B )
199 193 198 breqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) <_ B )
200 178 179 182 190 199 eliccd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) e. ( A [,] B ) )
201 177 200 jca 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ph /\ ( x + -u T ) e. ( A [,] B ) ) )
202 eleq1 
 |-  ( y = ( x + -u T ) -> ( y e. ( A [,] B ) <-> ( x + -u T ) e. ( A [,] B ) ) )
203 202 anbi2d 
 |-  ( y = ( x + -u T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x + -u T ) e. ( A [,] B ) ) ) )
204 oveq1 
 |-  ( y = ( x + -u T ) -> ( y + T ) = ( ( x + -u T ) + T ) )
205 204 fveq2d 
 |-  ( y = ( x + -u T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x + -u T ) + T ) ) )
206 fveq2 
 |-  ( y = ( x + -u T ) -> ( F ` y ) = ( F ` ( x + -u T ) ) )
207 205 206 eqeq12d 
 |-  ( y = ( x + -u T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) )
208 203 207 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 ) ) ) ) )
209 eleq1 
 |-  ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
210 209 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ y e. ( A [,] B ) ) ) )
211 oveq1 
 |-  ( x = y -> ( x + T ) = ( y + T ) )
212 211 fveq2d 
 |-  ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
213 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
214 212 213 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
215 210 214 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
216 215 7 chvarvv 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) )
217 208 216 vtoclg 
 |-  ( ( x + -u T ) e. CC -> ( ( ph /\ ( x + -u T ) e. ( A [,] B ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) ) )
218 176 201 217 sylc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` ( x + -u T ) ) )
219 173 195 negsubd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x + -u T ) = ( x - T ) )
220 219 oveq1d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) + T ) = ( ( x - T ) + T ) )
221 173 195 npcand 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
222 220 221 eqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x + -u T ) + T ) = x )
223 222 fveq2d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( ( x + -u T ) + T ) ) = ( F ` x ) )
224 218 223 eqtr3d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x + -u T ) ) = ( F ` x ) )
225 224 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x + -u T ) ) = ( F ` x ) )
226 fveq2 
 |-  ( j = i -> ( S ` j ) = ( S ` i ) )
227 226 oveq1d 
 |-  ( j = i -> ( ( S ` j ) + -u T ) = ( ( S ` i ) + -u T ) )
228 227 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( ( S ` j ) + -u T ) ) = ( i e. ( 0 ... M ) |-> ( ( S ` i ) + -u T ) )
229 10 adantr 
 |-  ( ( ph /\ 0 < -u T ) -> F : RR --> CC )
230 10 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> CC )
231 ioossre 
 |-  ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR
232 231 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR )
233 230 232 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
234 151 158 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) = ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
235 141 144 145 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 ) } )
236 234 235 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 ) } )
237 236 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 ) ) )
238 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> ph )
239 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 ) )
240 235 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 ) } ) )
241 240 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 ) ) )
242 141 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
243 242 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) e. RR* )
244 144 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
245 244 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
246 elioore 
 |-  ( x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) -> x e. RR )
247 246 adantl 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
248 5 adantr 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
249 247 248 resubcld 
 |-  ( ( ph /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
250 249 3adant2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
251 141 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
252 64 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. CC )
253 251 252 pncand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
254 253 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
255 254 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
256 149 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR )
257 247 3adant2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
258 5 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
259 149 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) e. RR* )
260 259 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR* )
261 157 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
262 261 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
263 simp3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) )
264 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 )
265 260 262 263 264 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) < x )
266 256 257 258 265 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` i ) + T ) - T ) < ( x - T ) )
267 255 266 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) < ( x - T ) )
268 157 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
269 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 ) )
270 260 262 263 269 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x < ( ( Q ` ( i + 1 ) ) + T ) )
271 257 268 258 270 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
272 144 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
273 272 252 pncand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
274 273 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
275 271 274 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
276 243 245 250 267 275 eliood 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
277 238 239 241 276 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 ) ) ) )
278 fvres 
 |-  ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
279 277 278 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 ) ) )
280 238 241 249 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 )
281 1 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A e. RR )
282 2 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> B e. RR )
283 66 eqcomd 
 |-  ( ph -> A = ( ( A + T ) - T ) )
284 283 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A = ( ( A + T ) - T ) )
285 62 3ad2ant1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) e. RR )
286 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR )
287 1 rexrd 
 |-  ( ph -> A e. RR* )
288 287 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR* )
289 2 rexrd 
 |-  ( ph -> B e. RR* )
290 289 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> B e. RR* )
291 3 4 6 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
292 291 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
293 292 140 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( A [,] B ) )
294 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` i ) e. ( A [,] B ) ) -> A <_ ( Q ` i ) )
295 288 290 293 294 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A <_ ( Q ` i ) )
296 286 141 145 295 leadd1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A + T ) <_ ( ( Q ` i ) + T ) )
297 296 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) <_ ( ( Q ` i ) + T ) )
298 285 256 257 297 265 lelttrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( A + T ) < x )
299 285 257 258 298 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( A + T ) - T ) < ( x - T ) )
300 284 299 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A < ( x - T ) )
301 281 250 300 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> A <_ ( x - T ) )
302 144 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
303 292 143 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( A [,] B ) )
304 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` ( i + 1 ) ) e. ( A [,] B ) ) -> ( Q ` ( i + 1 ) ) <_ B )
305 288 290 303 304 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) <_ B )
306 305 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) <_ B )
307 250 302 282 275 306 ltletrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) < B )
308 250 282 307 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) <_ B )
309 281 282 250 301 308 eliccd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ x e. ( ( ( Q ` i ) + T ) (,) ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( A [,] B ) )
310 238 239 241 309 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 ) )
311 238 310 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 ) ) )
312 eleq1 
 |-  ( y = ( x - T ) -> ( y e. ( A [,] B ) <-> ( x - T ) e. ( A [,] B ) ) )
313 312 anbi2d 
 |-  ( y = ( x - T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x - T ) e. ( A [,] B ) ) ) )
314 oveq1 
 |-  ( y = ( x - T ) -> ( y + T ) = ( ( x - T ) + T ) )
315 314 fveq2d 
 |-  ( y = ( x - T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x - T ) + T ) ) )
316 fveq2 
 |-  ( y = ( x - T ) -> ( F ` y ) = ( F ` ( x - T ) ) )
317 315 316 eqeq12d 
 |-  ( y = ( x - T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
318 313 317 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 ) ) ) ) )
319 318 216 vtoclg 
 |-  ( ( x - T ) e. RR -> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
320 280 311 319 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 ) ) )
321 241 246 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 )
322 recn 
 |-  ( x e. RR -> x e. CC )
323 322 adantl 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
324 64 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. CC )
325 323 324 npcand 
 |-  ( ( ph /\ x e. RR ) -> ( ( x - T ) + T ) = x )
326 325 fveq2d 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` x ) )
327 238 321 326 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 ) )
328 279 320 327 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 ) ) )
329 328 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 ) ) ) )
330 233 237 329 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 ) ) ) )
331 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
332 331 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
333 eqeq1 
 |-  ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
334 333 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 ) ) )
335 oveq1 
 |-  ( z = y -> ( z + T ) = ( y + T ) )
336 335 eqeq2d 
 |-  ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
337 336 cbvrexvw 
 |-  ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) )
338 334 337 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 ) ) )
339 338 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 ) }
340 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 ) ) )
341 332 252 339 11 340 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 ) )
342 236 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 ) ) ) )
343 342 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 ) )
344 341 343 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 ) )
345 330 344 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
346 345 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
347 ffdm 
 |-  ( F : RR --> CC -> ( F : dom F --> CC /\ dom F C_ RR ) )
348 10 347 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ RR ) )
349 348 simpld 
 |-  ( ph -> F : dom F --> CC )
350 349 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : dom F --> CC )
351 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
352 fdm 
 |-  ( F : RR --> CC -> dom F = RR )
353 230 352 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom F = RR )
354 351 353 sseqtrrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
355 339 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 ) }
356 232 342 353 3sstr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } C_ dom F )
357 339 356 eqsstrrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } C_ dom F )
358 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
359 358 287 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
360 358 289 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
361 358 291 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
362 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
363 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
364 363 sseli 
 |-  ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
365 364 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
366 359 360 361 362 365 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( A [,] B ) )
367 eleq1 
 |-  ( x = z -> ( x e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
368 367 anbi2d 
 |-  ( x = z -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
369 oveq1 
 |-  ( x = z -> ( x + T ) = ( z + T ) )
370 369 fveq2d 
 |-  ( x = z -> ( F ` ( x + T ) ) = ( F ` ( z + T ) ) )
371 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
372 370 371 eqeq12d 
 |-  ( x = z -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( z + T ) ) = ( F ` z ) ) )
373 368 372 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) ) ) )
374 373 7 chvarvv 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
375 358 366 374 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
376 350 332 354 252 355 357 375 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 ) ) )
377 355 342 eqtrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
378 377 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 ) ) ) ) )
379 151 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
380 378 379 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 ) ) )
381 376 380 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` i ) ) )
382 381 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` i ) ) )
383 350 332 354 252 355 357 375 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 ) ) )
384 158 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
385 378 384 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 ) ) ) )
386 383 385 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` ( i + 1 ) ) ) )
387 386 adantlr 
 |-  ( ( ( ph /\ 0 < -u T ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) limCC ( S ` ( i + 1 ) ) ) )
388 eqeq1 
 |-  ( y = x -> ( y = ( S ` i ) <-> x = ( S ` i ) ) )
389 eqeq1 
 |-  ( y = x -> ( y = ( S ` ( i + 1 ) ) <-> x = ( S ` ( i + 1 ) ) ) )
390 389 31 ifbieq2d 
 |-  ( y = x -> if ( y = ( S ` ( i + 1 ) ) , L , ( F ` y ) ) = if ( x = ( S ` ( i + 1 ) ) , L , ( F ` x ) ) )
391 388 390 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 ) ) ) )
392 391 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 ) ) ) )
393 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 ) ) )
394 79 81 82 83 86 167 225 228 229 346 382 387 392 393 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 )
395 76 394 eqtr2d 
 |-  ( ( ph /\ 0 < -u T ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
396 51 61 395 syl2anc 
 |-  ( ( ( ph /\ -. 0 < T ) /\ -. T = 0 ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
397 50 396 pm2.61dan 
 |-  ( ( ph /\ -. 0 < T ) -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
398 36 397 pm2.61dan 
 |-  ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )