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
|
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 /\ -. ( 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
|
eqtr3id |
|- ( 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
|
eqtrid |
|- ( 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 ) ) ) |