Metamath Proof Explorer

Theorem fourierdlem89

Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem89.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 ) ) ) } )
fourierdlem89.t 
|- T = ( B - A )
fourierdlem89.m 
|- ( ph -> M e. NN )
fourierdlem89.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem89.f 
|- ( ph -> F : RR --> CC )
fourierdlem89.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem89.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem89.limc 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem89.c 
|- ( ph -> C e. RR )
fourierdlem89.d 
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem89.o 
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem89.12 
|- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
fourierdlem89.n 
|- N = ( ( # ` H ) - 1 )
fourierdlem89.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem89.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem89.z 
|- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem89.j 
|- ( ph -> J e. ( 0 ..^ N ) )
fourierdlem89.u 
|- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
fourierdlem89.20 
|- I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
fourierdlem89.21 
|- V = ( i e. ( 0 ..^ M ) |-> R )
Assertion fourierdlem89 
|- ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) limCC ( S ` J ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem89.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 ) ) ) } )
2 fourierdlem89.t 
 |-  T = ( B - A )
3 fourierdlem89.m 
 |-  ( ph -> M e. NN )
4 fourierdlem89.q 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem89.f 
 |-  ( ph -> F : RR --> CC )
6 fourierdlem89.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
7 fourierdlem89.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
8 fourierdlem89.limc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
9 fourierdlem89.c 
 |-  ( ph -> C e. RR )
10 fourierdlem89.d 
 |-  ( ph -> D e. ( C (,) +oo ) )
11 fourierdlem89.o 
 |-  O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
12 fourierdlem89.12 
 |-  H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
13 fourierdlem89.n 
 |-  N = ( ( # ` H ) - 1 )
14 fourierdlem89.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
15 fourierdlem89.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
16 fourierdlem89.z 
 |-  Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
17 fourierdlem89.j 
 |-  ( ph -> J e. ( 0 ..^ N ) )
18 fourierdlem89.u 
 |-  U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
19 fourierdlem89.20 
 |-  I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
20 fourierdlem89.21 
 |-  V = ( i e. ( 0 ..^ M ) |-> R )
21 1 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 ) ) ) ) ) )
22 3 21 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 ) ) ) ) ) )
23 4 22 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
24 23 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
25 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
26 24 25 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
27 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
28 1 3 4 2 15 16 19 fourierdlem37 
 |-  ( ph -> ( I : RR --> ( 0 ..^ M ) /\ ( x e. RR -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } ) ) )
29 28 simpld 
 |-  ( ph -> I : RR --> ( 0 ..^ M ) )
30 elioore 
 |-  ( D e. ( C (,) +oo ) -> D e. RR )
31 10 30 syl 
 |-  ( ph -> D e. RR )
32 elioo4g 
 |-  ( D e. ( C (,) +oo ) <-> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
33 10 32 sylib 
 |-  ( ph -> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
34 33 simprd 
 |-  ( ph -> ( C < D /\ D < +oo ) )
35 34 simpld 
 |-  ( ph -> C < D )
36 oveq1 
 |-  ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
37 36 eleq1d 
 |-  ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
38 37 rexbidv 
 |-  ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
39 38 cbvrabv 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
40 39 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
41 12 fveq2i 
 |-  ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
42 41 oveq1i 
 |-  ( ( # ` H ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
43 13 42 eqtri 
 |-  N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
44 isoeq5 
 |-  ( H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
45 12 44 ax-mp 
 |-  ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
46 45 iotabii 
 |-  ( iota f f Isom < , < ( ( 0 ... N ) , H ) ) = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
47 14 46 eqtri 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
48 2 1 3 4 9 31 35 11 40 43 47 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
49 48 simpld 
 |-  ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
50 49 simprd 
 |-  ( ph -> S e. ( O ` N ) )
51 49 simpld 
 |-  ( ph -> N e. NN )
52 11 fourierdlem2 
 |-  ( N e. NN -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
53 51 52 syl 
 |-  ( ph -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
54 50 53 mpbid 
 |-  ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
55 54 simpld 
 |-  ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
56 elmapi 
 |-  ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
57 55 56 syl 
 |-  ( ph -> S : ( 0 ... N ) --> RR )
58 elfzofz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ( 0 ... N ) )
59 17 58 syl 
 |-  ( ph -> J e. ( 0 ... N ) )
60 57 59 ffvelrnd 
 |-  ( ph -> ( S ` J ) e. RR )
61 29 60 ffvelrnd 
 |-  ( ph -> ( I ` ( S ` J ) ) e. ( 0 ..^ M ) )
62 27 61 sseldi 
 |-  ( ph -> ( I ` ( S ` J ) ) e. ( 0 ... M ) )
63 26 62 ffvelrnd 
 |-  ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
64 63 rexrd 
 |-  ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
65 64 adantr 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
66 fzofzp1 
 |-  ( ( I ` ( S ` J ) ) e. ( 0 ..^ M ) -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
67 61 66 syl 
 |-  ( ph -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
68 26 67 ffvelrnd 
 |-  ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
69 68 rexrd 
 |-  ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
70 69 adantr 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
71 1 3 4 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
72 71 simp1d 
 |-  ( ph -> A e. RR )
73 71 simp2d 
 |-  ( ph -> B e. RR )
74 72 73 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
75 71 simp3d 
 |-  ( ph -> A < B )
76 72 73 75 16 fourierdlem17 
 |-  ( ph -> Z : ( A (,] B ) --> ( A [,] B ) )
77 72 73 75 2 15 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
78 77 60 ffvelrnd 
 |-  ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
79 76 78 ffvelrnd 
 |-  ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
80 74 79 sseldd 
 |-  ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
81 80 adantr 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
82 63 adantr 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
83 72 rexrd 
 |-  ( ph -> A e. RR* )
84 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
85 83 73 84 syl2anc 
 |-  ( ph -> ( A (,] B ) C_ RR )
86 fzofzp1 
 |-  ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
87 17 86 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... N ) )
88 57 87 ffvelrnd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. RR )
89 77 88 ffvelrnd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
90 85 89 sseldd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
91 54 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
92 fveq2 
 |-  ( i = J -> ( S ` i ) = ( S ` J ) )
93 oveq1 
 |-  ( i = J -> ( i + 1 ) = ( J + 1 ) )
94 93 fveq2d 
 |-  ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
95 92 94 breq12d 
 |-  ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
96 95 rspccva 
 |-  ( ( A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) /\ J e. ( 0 ..^ N ) ) -> ( S ` J ) < ( S ` ( J + 1 ) ) )
97 91 17 96 syl2anc 
 |-  ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
98 60 88 posdifd 
 |-  ( ph -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
99 97 98 mpbid 
 |-  ( ph -> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
100 17 ancli 
 |-  ( ph -> ( ph /\ J e. ( 0 ..^ N ) ) )
101 eleq1 
 |-  ( j = J -> ( j e. ( 0 ..^ N ) <-> J e. ( 0 ..^ N ) ) )
102 101 anbi2d 
 |-  ( j = J -> ( ( ph /\ j e. ( 0 ..^ N ) ) <-> ( ph /\ J e. ( 0 ..^ N ) ) ) )
103 oveq1 
 |-  ( j = J -> ( j + 1 ) = ( J + 1 ) )
104 103 fveq2d 
 |-  ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
105 104 fveq2d 
 |-  ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
106 fveq2 
 |-  ( j = J -> ( S ` j ) = ( S ` J ) )
107 106 fveq2d 
 |-  ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
108 107 fveq2d 
 |-  ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
109 105 108 oveq12d 
 |-  ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
110 104 106 oveq12d 
 |-  ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
111 109 110 eqeq12d 
 |-  ( j = J -> ( ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) <-> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
112 102 111 imbi12d 
 |-  ( j = J -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) <-> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) ) )
113 2 oveq2i 
 |-  ( k x. T ) = ( k x. ( B - A ) )
114 113 oveq2i 
 |-  ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
115 114 eleq1i 
 |-  ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
116 115 rexbii 
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
117 116 rgenw 
 |-  A. y e. ( C [,] D ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
118 rabbi 
 |-  ( A. y e. ( C [,] D ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q ) <-> { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
119 117 118 mpbi 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q }
120 119 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
121 120 fveq2i 
 |-  ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
122 121 oveq1i 
 |-  ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
123 43 122 eqtri 
 |-  N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
124 isoeq5 
 |-  ( ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) ) )
125 120 124 ax-mp 
 |-  ( f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
126 125 iotabii 
 |-  ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
127 47 126 eqtri 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
128 eqid 
 |-  ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
129 1 2 3 4 9 10 11 123 127 15 16 128 fourierdlem65 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
130 112 129 vtoclg 
 |-  ( J e. ( 0 ..^ N ) -> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
131 17 100 130 sylc 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
132 99 131 breqtrrd 
 |-  ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
133 80 90 posdifd 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) <-> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) ) )
134 132 133 mpbird 
 |-  ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
135 id 
 |-  ( ph -> ph )
136 108 105 oveq12d 
 |-  ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
137 106 fveq2d 
 |-  ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
138 137 fveq2d 
 |-  ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
139 137 oveq1d 
 |-  ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
140 139 fveq2d 
 |-  ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
141 138 140 oveq12d 
 |-  ( j = J -> ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
142 136 141 sseq12d 
 |-  ( j = J -> ( ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) <-> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
143 102 142 imbi12d 
 |-  ( j = J -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) ) <-> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
144 eqid 
 |-  ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )
145 2 1 3 4 9 31 35 11 40 43 47 15 16 144 19 fourierdlem79 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )
146 143 145 vtoclg 
 |-  ( J e. ( 0 ..^ N ) -> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
147 146 anabsi7 
 |-  ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
148 135 17 147 syl2anc 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
149 63 68 80 90 134 148 fourierdlem10 
 |-  ( ph -> ( ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) /\ ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
150 149 simpld 
 |-  ( ph -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
151 150 adantr 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
152 neqne 
 |-  ( -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) =/= ( Q ` ( I ` ( S ` J ) ) ) )
153 152 adantl 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) =/= ( Q ` ( I ` ( S ` J ) ) ) )
154 82 81 151 153 leneltd 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( Z ` ( E ` ( S ` J ) ) ) )
155 149 simprd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
156 80 90 68 134 155 ltletrd 
 |-  ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
157 156 adantr 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
158 65 70 81 154 157 eliood 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) e. ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
159 fvres 
 |-  ( ( Z ` ( E ` ( S ` J ) ) ) e. ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) = ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) )
160 158 159 syl 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) = ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) )
161 160 eqcomd 
 |-  ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) )
162 161 ifeq2da 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) ) = if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) )
163 fdm 
 |-  ( F : RR --> CC -> dom F = RR )
164 5 163 syl 
 |-  ( ph -> dom F = RR )
165 164 feq2d 
 |-  ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
166 5 165 mpbird 
 |-  ( ph -> F : dom F --> CC )
167 ioosscn 
 |-  ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC
168 167 a1i 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC )
169 ioossre 
 |-  ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR
170 169 164 sseqtrrid 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ dom F )
171 88 90 resubcld 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
172 18 171 eqeltrid 
 |-  ( ph -> U e. RR )
173 172 recnd 
 |-  ( ph -> U e. CC )
174 eqid 
 |-  { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } = { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) }
175 80 90 172 iooshift 
 |-  ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } )
176 ioossre 
 |-  ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR
177 176 164 sseqtrrid 
 |-  ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F )
178 175 177 eqsstrrd 
 |-  ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F )
179 elioore 
 |-  ( y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> y e. RR )
180 73 72 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
181 2 180 eqeltrid 
 |-  ( ph -> T e. RR )
182 181 recnd 
 |-  ( ph -> T e. CC )
183 72 73 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
184 75 183 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
185 184 2 breqtrrdi 
 |-  ( ph -> 0 < T )
186 185 gt0ne0d 
 |-  ( ph -> T =/= 0 )
187 173 182 186 divcan1d 
 |-  ( ph -> ( ( U / T ) x. T ) = U )
188 187 eqcomd 
 |-  ( ph -> U = ( ( U / T ) x. T ) )
189 188 oveq2d 
 |-  ( ph -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
190 189 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
191 190 fveq2d 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
192 5 adantr 
 |-  ( ( ph /\ y e. RR ) -> F : RR --> CC )
193 181 adantr 
 |-  ( ( ph /\ y e. RR ) -> T e. RR )
194 90 recnd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
195 88 recnd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. CC )
196 194 195 negsubdi2d 
 |-  ( ph -> -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
197 196 eqcomd 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
198 197 oveq1d 
 |-  ( ph -> ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
199 18 oveq1i 
 |-  ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T )
200 199 a1i 
 |-  ( ph -> ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) )
201 15 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
202 id 
 |-  ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
203 oveq2 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
204 203 oveq1d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
205 204 fveq2d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
206 205 oveq1d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
207 202 206 oveq12d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
208 207 adantl 
 |-  ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
209 73 88 resubcld 
 |-  ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
210 209 181 186 redivcld 
 |-  ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
211 210 flcld 
 |-  ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
212 211 zred 
 |-  ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
213 212 181 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
214 88 213 readdcld 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
215 201 208 88 214 fvmptd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
216 215 oveq1d 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) )
217 212 recnd 
 |-  ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
218 217 182 mulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
219 195 218 pncan2d 
 |-  ( ph -> ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
220 216 219 eqtrd 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
221 220 218 eqeltrd 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
222 221 182 186 divnegd 
 |-  ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
223 198 200 222 3eqtr4d 
 |-  ( ph -> ( U / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
224 220 oveq1d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
225 217 182 186 divcan4d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
226 224 225 eqtrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
227 226 211 eqeltrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
228 227 znegcld 
 |-  ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
229 223 228 eqeltrd 
 |-  ( ph -> ( U / T ) e. ZZ )
230 229 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( U / T ) e. ZZ )
231 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
232 6 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
233 192 193 230 231 232 fperiodmul 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
234 191 233 eqtrd 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
235 179 234 sylan2 
 |-  ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
236 23 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
237 fveq2 
 |-  ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
238 oveq1 
 |-  ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
239 238 fveq2d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
240 237 239 breq12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
241 240 rspccva 
 |-  ( ( A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
242 236 61 241 syl2anc 
 |-  ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
243 61 ancli 
 |-  ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) )
244 eleq1 
 |-  ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0 ..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) )
245 244 anbi2d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) )
246 237 239 oveq12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
247 246 reseq2d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
248 246 oveq1d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
249 247 248 eleq12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) <-> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) )
250 245 249 imbi12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) ) )
251 250 7 vtoclg 
 |-  ( ( I ` ( S ` J ) ) e. ( 0 ..^ M ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) )
252 61 243 251 sylc 
 |-  ( ph -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
253 nfv 
 |-  F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) )
254 nfmpt1 
 |-  F/_ i ( i e. ( 0 ..^ M ) |-> R )
255 20 254 nfcxfr 
 |-  F/_ i V
256 nfcv 
 |-  F/_ i ( I ` ( S ` J ) )
257 255 256 nffv 
 |-  F/_ i ( V ` ( I ` ( S ` J ) ) )
258 257 nfel1 
 |-  F/ i ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) )
259 253 258 nfim 
 |-  F/ i ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) )
260 245 biimpar 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( ph /\ i e. ( 0 ..^ M ) ) )
261 260 3adant2 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( ph /\ i e. ( 0 ..^ M ) ) )
262 261 8 syl 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
263 fveq2 
 |-  ( i = ( I ` ( S ` J ) ) -> ( V ` i ) = ( V ` ( I ` ( S ` J ) ) ) )
264 263 eqcomd 
 |-  ( i = ( I ` ( S ` J ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
265 264 adantr 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
266 260 simprd 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> i e. ( 0 ..^ M ) )
267 elex 
 |-  ( R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) -> R e. _V )
268 260 8 267 3syl 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> R e. _V )
269 20 fvmpt2 
 |-  ( ( i e. ( 0 ..^ M ) /\ R e. _V ) -> ( V ` i ) = R )
270 266 268 269 syl2anc 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( V ` i ) = R )
271 265 270 eqtrd 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
272 271 3adant2 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
273 247 237 oveq12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) )
274 273 eqcomd 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
275 274 3ad2ant1 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
276 262 272 275 3eltr4d 
 |-  ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) )
277 276 3exp 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) ) ) )
278 8 2a1i 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) ) )
279 277 278 impbid 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) ) ) )
280 259 279 8 vtoclg1f 
 |-  ( ( I ` ( S ` J ) ) e. ( 0 ..^ M ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) ) )
281 61 243 280 sylc 
 |-  ( ph -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) limCC ( Q ` ( I ` ( S ` J ) ) ) ) )
282 eqid 
 |-  if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) = if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) )
283 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( Q ` ( I ` ( S ` J ) ) ) [,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( Q ` ( I ` ( S ` J ) ) ) [,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
284 63 68 242 252 281 80 90 134 148 282 283 fourierdlem32 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) limCC ( Z ` ( E ` ( S ` J ) ) ) ) )
285 148 resabs1d 
 |-  ( ph -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) )
286 285 oveq1d 
 |-  ( ph -> ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) limCC ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) limCC ( Z ` ( E ` ( S ` J ) ) ) ) )
287 284 286 eleqtrd 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) limCC ( Z ` ( E ` ( S ` J ) ) ) ) )
288 166 168 170 173 174 178 235 287 limcperiod 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) limCC ( ( Z ` ( E ` ( S ` J ) ) ) + U ) ) )
289 18 oveq2i 
 |-  ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
290 289 a1i 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
291 9 31 iccssred 
 |-  ( ph -> ( C [,] D ) C_ RR )
292 ax-resscn 
 |-  RR C_ CC
293 291 292 sstrdi 
 |-  ( ph -> ( C [,] D ) C_ CC )
294 11 51 50 fourierdlem15 
 |-  ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
295 294 59 ffvelrnd 
 |-  ( ph -> ( S ` J ) e. ( C [,] D ) )
296 293 295 sseldd 
 |-  ( ph -> ( S ` J ) e. CC )
297 195 296 subcld 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
298 80 recnd 
 |-  ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. CC )
299 194 297 298 subsub23d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) <-> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
300 131 299 mpbird 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
301 300 eqcomd 
 |-  ( ph -> ( Z ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
302 301 oveq1d 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
303 194 297 subcld 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
304 303 195 194 addsub12d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
305 194 297 194 sub32d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
306 194 subidd 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = 0 )
307 306 oveq1d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
308 df-neg 
 |-  -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
309 195 296 negsubdi2d 
 |-  ( ph -> -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
310 308 309 syl5eqr 
 |-  ( ph -> ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
311 305 307 310 3eqtrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
312 311 oveq2d 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) + ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) )
313 195 296 pncan3d 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) = ( S ` J ) )
314 304 312 313 3eqtrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` J ) )
315 290 302 314 3eqtrd 
 |-  ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( S ` J ) )
316 315 oveq2d 
 |-  ( ph -> ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) limCC ( ( Z ` ( E ` ( S ` J ) ) ) + U ) ) = ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) limCC ( S ` J ) ) )
317 288 316 eleqtrd 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) limCC ( S ` J ) ) )
318 18 oveq2i 
 |-  ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
319 194 195 pncan3d 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` ( J + 1 ) ) )
320 318 319 syl5eq 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( S ` ( J + 1 ) ) )
321 315 320 oveq12d 
 |-  ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) )
322 175 321 eqtr3d 
 |-  ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } = ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) )
323 322 reseq2d 
 |-  ( ph -> ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) = ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) )
324 323 oveq1d 
 |-  ( ph -> ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) limCC ( S ` J ) ) = ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) limCC ( S ` J ) ) )
325 317 324 eleqtrd 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) limCC ( S ` J ) ) )
326 162 325 eqeltrd 
 |-  ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) limCC ( S ` J ) ) )