Metamath Proof Explorer

Theorem fourierdlem91

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

Ref Expression
Hypotheses fourierdlem91.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 ) ) ) } )
fourierdlem91.t 
|- T = ( B - A )
fourierdlem91.m 
|- ( ph -> M e. NN )
fourierdlem91.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem91.f 
|- ( ph -> F : RR --> CC )
fourierdlem91.6 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem91.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem91.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem91.c 
|- ( ph -> C e. RR )
fourierdlem91.d 
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem91.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 ) ) ) } )
fourierdlem91.h 
|- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
fourierdlem91.n 
|- N = ( ( # ` H ) - 1 )
fourierdlem91.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem91.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem91.J 
|- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem91.17 
|- ( ph -> J e. ( 0 ..^ N ) )
fourierdlem91.u 
|- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
fourierdlem91.i 
|- I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
fourierdlem91.w 
|- W = ( i e. ( 0 ..^ M ) |-> L )
Assertion fourierdlem91 
|- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) limCC ( S ` ( J + 1 ) ) ) )

Proof

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