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
|
ffvelrnd |
|- ( ph -> ( S ` J ) e. RR ) |
61 |
29 60
|
ffvelrnd |
|- ( ph -> ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) |
62 |
27 61
|
sselid |
|- ( 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 /\ -. ( 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
|
ffvelrnd |
|- ( 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
|
ffvelrnd |
|- ( ph -> ( S ` ( J + 1 ) ) e. RR ) |
82 |
78 81
|
ffvelrnd |
|- ( 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
|
ffvelrnd |
|- ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) ) |
88 |
86 87
|
ffvelrnd |
|- ( 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
|
ffvelrnd |
|- ( 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 ) ) ) ) |