Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem102.f |
|- ( ph -> F : RR --> RR ) |
2 |
|
fourierdlem102.t |
|- T = ( 2 x. _pi ) |
3 |
|
fourierdlem102.per |
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) |
4 |
|
fourierdlem102.g |
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |
5 |
|
fourierdlem102.dmdv |
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin ) |
6 |
|
fourierdlem102.gcn |
|- ( ph -> G e. ( dom G -cn-> CC ) ) |
7 |
|
fourierdlem102.rlim |
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) ) |
8 |
|
fourierdlem102.llim |
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) ) |
9 |
|
fourierdlem102.x |
|- ( ph -> X e. RR ) |
10 |
|
fourierdlem102.p |
|- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
11 |
|
fourierdlem102.e |
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) ) |
12 |
|
fourierdlem102.h |
|- H = ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) |
13 |
|
fourierdlem102.m |
|- M = ( ( # ` H ) - 1 ) |
14 |
|
fourierdlem102.q |
|- Q = ( iota g g Isom < , < ( ( 0 ... M ) , H ) ) |
15 |
|
2z |
|- 2 e. ZZ |
16 |
15
|
a1i |
|- ( ph -> 2 e. ZZ ) |
17 |
|
tpfi |
|- { -u _pi , _pi , ( E ` X ) } e. Fin |
18 |
17
|
a1i |
|- ( ph -> { -u _pi , _pi , ( E ` X ) } e. Fin ) |
19 |
|
pire |
|- _pi e. RR |
20 |
19
|
renegcli |
|- -u _pi e. RR |
21 |
20
|
rexri |
|- -u _pi e. RR* |
22 |
19
|
rexri |
|- _pi e. RR* |
23 |
|
negpilt0 |
|- -u _pi < 0 |
24 |
|
pipos |
|- 0 < _pi |
25 |
|
0re |
|- 0 e. RR |
26 |
20 25 19
|
lttri |
|- ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi ) |
27 |
23 24 26
|
mp2an |
|- -u _pi < _pi |
28 |
20 19 27
|
ltleii |
|- -u _pi <_ _pi |
29 |
|
prunioo |
|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ -u _pi <_ _pi ) -> ( ( -u _pi (,) _pi ) u. { -u _pi , _pi } ) = ( -u _pi [,] _pi ) ) |
30 |
21 22 28 29
|
mp3an |
|- ( ( -u _pi (,) _pi ) u. { -u _pi , _pi } ) = ( -u _pi [,] _pi ) |
31 |
30
|
difeq1i |
|- ( ( ( -u _pi (,) _pi ) u. { -u _pi , _pi } ) \ dom G ) = ( ( -u _pi [,] _pi ) \ dom G ) |
32 |
|
difundir |
|- ( ( ( -u _pi (,) _pi ) u. { -u _pi , _pi } ) \ dom G ) = ( ( ( -u _pi (,) _pi ) \ dom G ) u. ( { -u _pi , _pi } \ dom G ) ) |
33 |
31 32
|
eqtr3i |
|- ( ( -u _pi [,] _pi ) \ dom G ) = ( ( ( -u _pi (,) _pi ) \ dom G ) u. ( { -u _pi , _pi } \ dom G ) ) |
34 |
|
prfi |
|- { -u _pi , _pi } e. Fin |
35 |
|
diffi |
|- ( { -u _pi , _pi } e. Fin -> ( { -u _pi , _pi } \ dom G ) e. Fin ) |
36 |
34 35
|
mp1i |
|- ( ph -> ( { -u _pi , _pi } \ dom G ) e. Fin ) |
37 |
|
unfi |
|- ( ( ( ( -u _pi (,) _pi ) \ dom G ) e. Fin /\ ( { -u _pi , _pi } \ dom G ) e. Fin ) -> ( ( ( -u _pi (,) _pi ) \ dom G ) u. ( { -u _pi , _pi } \ dom G ) ) e. Fin ) |
38 |
5 36 37
|
syl2anc |
|- ( ph -> ( ( ( -u _pi (,) _pi ) \ dom G ) u. ( { -u _pi , _pi } \ dom G ) ) e. Fin ) |
39 |
33 38
|
eqeltrid |
|- ( ph -> ( ( -u _pi [,] _pi ) \ dom G ) e. Fin ) |
40 |
|
unfi |
|- ( ( { -u _pi , _pi , ( E ` X ) } e. Fin /\ ( ( -u _pi [,] _pi ) \ dom G ) e. Fin ) -> ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) e. Fin ) |
41 |
18 39 40
|
syl2anc |
|- ( ph -> ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) e. Fin ) |
42 |
12 41
|
eqeltrid |
|- ( ph -> H e. Fin ) |
43 |
|
hashcl |
|- ( H e. Fin -> ( # ` H ) e. NN0 ) |
44 |
42 43
|
syl |
|- ( ph -> ( # ` H ) e. NN0 ) |
45 |
44
|
nn0zd |
|- ( ph -> ( # ` H ) e. ZZ ) |
46 |
20 27
|
ltneii |
|- -u _pi =/= _pi |
47 |
|
hashprg |
|- ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi =/= _pi <-> ( # ` { -u _pi , _pi } ) = 2 ) ) |
48 |
20 19 47
|
mp2an |
|- ( -u _pi =/= _pi <-> ( # ` { -u _pi , _pi } ) = 2 ) |
49 |
46 48
|
mpbi |
|- ( # ` { -u _pi , _pi } ) = 2 |
50 |
17
|
elexi |
|- { -u _pi , _pi , ( E ` X ) } e. _V |
51 |
|
ovex |
|- ( -u _pi [,] _pi ) e. _V |
52 |
|
difexg |
|- ( ( -u _pi [,] _pi ) e. _V -> ( ( -u _pi [,] _pi ) \ dom G ) e. _V ) |
53 |
51 52
|
ax-mp |
|- ( ( -u _pi [,] _pi ) \ dom G ) e. _V |
54 |
50 53
|
unex |
|- ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) e. _V |
55 |
12 54
|
eqeltri |
|- H e. _V |
56 |
|
negex |
|- -u _pi e. _V |
57 |
56
|
tpid1 |
|- -u _pi e. { -u _pi , _pi , ( E ` X ) } |
58 |
19
|
elexi |
|- _pi e. _V |
59 |
58
|
tpid2 |
|- _pi e. { -u _pi , _pi , ( E ` X ) } |
60 |
|
prssi |
|- ( ( -u _pi e. { -u _pi , _pi , ( E ` X ) } /\ _pi e. { -u _pi , _pi , ( E ` X ) } ) -> { -u _pi , _pi } C_ { -u _pi , _pi , ( E ` X ) } ) |
61 |
57 59 60
|
mp2an |
|- { -u _pi , _pi } C_ { -u _pi , _pi , ( E ` X ) } |
62 |
|
ssun1 |
|- { -u _pi , _pi , ( E ` X ) } C_ ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) |
63 |
62 12
|
sseqtrri |
|- { -u _pi , _pi , ( E ` X ) } C_ H |
64 |
61 63
|
sstri |
|- { -u _pi , _pi } C_ H |
65 |
|
hashss |
|- ( ( H e. _V /\ { -u _pi , _pi } C_ H ) -> ( # ` { -u _pi , _pi } ) <_ ( # ` H ) ) |
66 |
55 64 65
|
mp2an |
|- ( # ` { -u _pi , _pi } ) <_ ( # ` H ) |
67 |
66
|
a1i |
|- ( ph -> ( # ` { -u _pi , _pi } ) <_ ( # ` H ) ) |
68 |
49 67
|
eqbrtrrid |
|- ( ph -> 2 <_ ( # ` H ) ) |
69 |
|
eluz2 |
|- ( ( # ` H ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` H ) e. ZZ /\ 2 <_ ( # ` H ) ) ) |
70 |
16 45 68 69
|
syl3anbrc |
|- ( ph -> ( # ` H ) e. ( ZZ>= ` 2 ) ) |
71 |
|
uz2m1nn |
|- ( ( # ` H ) e. ( ZZ>= ` 2 ) -> ( ( # ` H ) - 1 ) e. NN ) |
72 |
70 71
|
syl |
|- ( ph -> ( ( # ` H ) - 1 ) e. NN ) |
73 |
13 72
|
eqeltrid |
|- ( ph -> M e. NN ) |
74 |
20
|
a1i |
|- ( ph -> -u _pi e. RR ) |
75 |
19
|
a1i |
|- ( ph -> _pi e. RR ) |
76 |
|
negpitopissre |
|- ( -u _pi (,] _pi ) C_ RR |
77 |
27
|
a1i |
|- ( ph -> -u _pi < _pi ) |
78 |
|
picn |
|- _pi e. CC |
79 |
78
|
2timesi |
|- ( 2 x. _pi ) = ( _pi + _pi ) |
80 |
78 78
|
subnegi |
|- ( _pi - -u _pi ) = ( _pi + _pi ) |
81 |
79 2 80
|
3eqtr4i |
|- T = ( _pi - -u _pi ) |
82 |
74 75 77 81 11
|
fourierdlem4 |
|- ( ph -> E : RR --> ( -u _pi (,] _pi ) ) |
83 |
82 9
|
ffvelrnd |
|- ( ph -> ( E ` X ) e. ( -u _pi (,] _pi ) ) |
84 |
76 83
|
sseldi |
|- ( ph -> ( E ` X ) e. RR ) |
85 |
74 75 84
|
3jca |
|- ( ph -> ( -u _pi e. RR /\ _pi e. RR /\ ( E ` X ) e. RR ) ) |
86 |
|
fvex |
|- ( E ` X ) e. _V |
87 |
56 58 86
|
tpss |
|- ( ( -u _pi e. RR /\ _pi e. RR /\ ( E ` X ) e. RR ) <-> { -u _pi , _pi , ( E ` X ) } C_ RR ) |
88 |
85 87
|
sylib |
|- ( ph -> { -u _pi , _pi , ( E ` X ) } C_ RR ) |
89 |
|
iccssre |
|- ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR ) |
90 |
20 19 89
|
mp2an |
|- ( -u _pi [,] _pi ) C_ RR |
91 |
|
ssdifss |
|- ( ( -u _pi [,] _pi ) C_ RR -> ( ( -u _pi [,] _pi ) \ dom G ) C_ RR ) |
92 |
90 91
|
mp1i |
|- ( ph -> ( ( -u _pi [,] _pi ) \ dom G ) C_ RR ) |
93 |
88 92
|
unssd |
|- ( ph -> ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) C_ RR ) |
94 |
12 93
|
eqsstrid |
|- ( ph -> H C_ RR ) |
95 |
42 94 14 13
|
fourierdlem36 |
|- ( ph -> Q Isom < , < ( ( 0 ... M ) , H ) ) |
96 |
|
isof1o |
|- ( Q Isom < , < ( ( 0 ... M ) , H ) -> Q : ( 0 ... M ) -1-1-onto-> H ) |
97 |
|
f1of |
|- ( Q : ( 0 ... M ) -1-1-onto-> H -> Q : ( 0 ... M ) --> H ) |
98 |
95 96 97
|
3syl |
|- ( ph -> Q : ( 0 ... M ) --> H ) |
99 |
98 94
|
fssd |
|- ( ph -> Q : ( 0 ... M ) --> RR ) |
100 |
|
reex |
|- RR e. _V |
101 |
|
ovex |
|- ( 0 ... M ) e. _V |
102 |
100 101
|
elmap |
|- ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) |
103 |
99 102
|
sylibr |
|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) ) |
104 |
|
fveq2 |
|- ( 0 = i -> ( Q ` 0 ) = ( Q ` i ) ) |
105 |
104
|
adantl |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 = i ) -> ( Q ` 0 ) = ( Q ` i ) ) |
106 |
99
|
ffvelrnda |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR ) |
107 |
106
|
leidd |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ ( Q ` i ) ) |
108 |
107
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 = i ) -> ( Q ` i ) <_ ( Q ` i ) ) |
109 |
105 108
|
eqbrtrd |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 = i ) -> ( Q ` 0 ) <_ ( Q ` i ) ) |
110 |
|
elfzelz |
|- ( i e. ( 0 ... M ) -> i e. ZZ ) |
111 |
110
|
zred |
|- ( i e. ( 0 ... M ) -> i e. RR ) |
112 |
111
|
ad2antlr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. 0 = i ) -> i e. RR ) |
113 |
|
elfzle1 |
|- ( i e. ( 0 ... M ) -> 0 <_ i ) |
114 |
113
|
ad2antlr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. 0 = i ) -> 0 <_ i ) |
115 |
|
neqne |
|- ( -. 0 = i -> 0 =/= i ) |
116 |
115
|
necomd |
|- ( -. 0 = i -> i =/= 0 ) |
117 |
116
|
adantl |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. 0 = i ) -> i =/= 0 ) |
118 |
112 114 117
|
ne0gt0d |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. 0 = i ) -> 0 < i ) |
119 |
|
nnssnn0 |
|- NN C_ NN0 |
120 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
121 |
119 120
|
sseqtri |
|- NN C_ ( ZZ>= ` 0 ) |
122 |
121 73
|
sseldi |
|- ( ph -> M e. ( ZZ>= ` 0 ) ) |
123 |
|
eluzfz1 |
|- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) ) |
124 |
122 123
|
syl |
|- ( ph -> 0 e. ( 0 ... M ) ) |
125 |
98 124
|
ffvelrnd |
|- ( ph -> ( Q ` 0 ) e. H ) |
126 |
94 125
|
sseldd |
|- ( ph -> ( Q ` 0 ) e. RR ) |
127 |
126
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> ( Q ` 0 ) e. RR ) |
128 |
106
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> ( Q ` i ) e. RR ) |
129 |
|
simpr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> 0 < i ) |
130 |
95
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> Q Isom < , < ( ( 0 ... M ) , H ) ) |
131 |
124
|
anim1i |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( 0 e. ( 0 ... M ) /\ i e. ( 0 ... M ) ) ) |
132 |
131
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> ( 0 e. ( 0 ... M ) /\ i e. ( 0 ... M ) ) ) |
133 |
|
isorel |
|- ( ( Q Isom < , < ( ( 0 ... M ) , H ) /\ ( 0 e. ( 0 ... M ) /\ i e. ( 0 ... M ) ) ) -> ( 0 < i <-> ( Q ` 0 ) < ( Q ` i ) ) ) |
134 |
130 132 133
|
syl2anc |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> ( 0 < i <-> ( Q ` 0 ) < ( Q ` i ) ) ) |
135 |
129 134
|
mpbid |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> ( Q ` 0 ) < ( Q ` i ) ) |
136 |
127 128 135
|
ltled |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ 0 < i ) -> ( Q ` 0 ) <_ ( Q ` i ) ) |
137 |
118 136
|
syldan |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. 0 = i ) -> ( Q ` 0 ) <_ ( Q ` i ) ) |
138 |
109 137
|
pm2.61dan |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` 0 ) <_ ( Q ` i ) ) |
139 |
138
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> ( Q ` 0 ) <_ ( Q ` i ) ) |
140 |
|
simpr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> ( Q ` i ) = -u _pi ) |
141 |
139 140
|
breqtrd |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> ( Q ` 0 ) <_ -u _pi ) |
142 |
74
|
rexrd |
|- ( ph -> -u _pi e. RR* ) |
143 |
75
|
rexrd |
|- ( ph -> _pi e. RR* ) |
144 |
|
lbicc2 |
|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ -u _pi <_ _pi ) -> -u _pi e. ( -u _pi [,] _pi ) ) |
145 |
21 22 28 144
|
mp3an |
|- -u _pi e. ( -u _pi [,] _pi ) |
146 |
145
|
a1i |
|- ( ph -> -u _pi e. ( -u _pi [,] _pi ) ) |
147 |
|
ubicc2 |
|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ -u _pi <_ _pi ) -> _pi e. ( -u _pi [,] _pi ) ) |
148 |
21 22 28 147
|
mp3an |
|- _pi e. ( -u _pi [,] _pi ) |
149 |
148
|
a1i |
|- ( ph -> _pi e. ( -u _pi [,] _pi ) ) |
150 |
|
iocssicc |
|- ( -u _pi (,] _pi ) C_ ( -u _pi [,] _pi ) |
151 |
150 83
|
sseldi |
|- ( ph -> ( E ` X ) e. ( -u _pi [,] _pi ) ) |
152 |
|
tpssi |
|- ( ( -u _pi e. ( -u _pi [,] _pi ) /\ _pi e. ( -u _pi [,] _pi ) /\ ( E ` X ) e. ( -u _pi [,] _pi ) ) -> { -u _pi , _pi , ( E ` X ) } C_ ( -u _pi [,] _pi ) ) |
153 |
146 149 151 152
|
syl3anc |
|- ( ph -> { -u _pi , _pi , ( E ` X ) } C_ ( -u _pi [,] _pi ) ) |
154 |
|
difssd |
|- ( ph -> ( ( -u _pi [,] _pi ) \ dom G ) C_ ( -u _pi [,] _pi ) ) |
155 |
153 154
|
unssd |
|- ( ph -> ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) C_ ( -u _pi [,] _pi ) ) |
156 |
12 155
|
eqsstrid |
|- ( ph -> H C_ ( -u _pi [,] _pi ) ) |
157 |
156 125
|
sseldd |
|- ( ph -> ( Q ` 0 ) e. ( -u _pi [,] _pi ) ) |
158 |
|
iccgelb |
|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ ( Q ` 0 ) e. ( -u _pi [,] _pi ) ) -> -u _pi <_ ( Q ` 0 ) ) |
159 |
142 143 157 158
|
syl3anc |
|- ( ph -> -u _pi <_ ( Q ` 0 ) ) |
160 |
159
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> -u _pi <_ ( Q ` 0 ) ) |
161 |
126
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> ( Q ` 0 ) e. RR ) |
162 |
20
|
a1i |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> -u _pi e. RR ) |
163 |
161 162
|
letri3d |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> ( ( Q ` 0 ) = -u _pi <-> ( ( Q ` 0 ) <_ -u _pi /\ -u _pi <_ ( Q ` 0 ) ) ) ) |
164 |
141 160 163
|
mpbir2and |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( Q ` i ) = -u _pi ) -> ( Q ` 0 ) = -u _pi ) |
165 |
63 57
|
sselii |
|- -u _pi e. H |
166 |
|
f1ofo |
|- ( Q : ( 0 ... M ) -1-1-onto-> H -> Q : ( 0 ... M ) -onto-> H ) |
167 |
96 166
|
syl |
|- ( Q Isom < , < ( ( 0 ... M ) , H ) -> Q : ( 0 ... M ) -onto-> H ) |
168 |
|
forn |
|- ( Q : ( 0 ... M ) -onto-> H -> ran Q = H ) |
169 |
95 167 168
|
3syl |
|- ( ph -> ran Q = H ) |
170 |
165 169
|
eleqtrrid |
|- ( ph -> -u _pi e. ran Q ) |
171 |
|
ffn |
|- ( Q : ( 0 ... M ) --> H -> Q Fn ( 0 ... M ) ) |
172 |
|
fvelrnb |
|- ( Q Fn ( 0 ... M ) -> ( -u _pi e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = -u _pi ) ) |
173 |
98 171 172
|
3syl |
|- ( ph -> ( -u _pi e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = -u _pi ) ) |
174 |
170 173
|
mpbid |
|- ( ph -> E. i e. ( 0 ... M ) ( Q ` i ) = -u _pi ) |
175 |
164 174
|
r19.29a |
|- ( ph -> ( Q ` 0 ) = -u _pi ) |
176 |
63 59
|
sselii |
|- _pi e. H |
177 |
176 169
|
eleqtrrid |
|- ( ph -> _pi e. ran Q ) |
178 |
|
fvelrnb |
|- ( Q Fn ( 0 ... M ) -> ( _pi e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = _pi ) ) |
179 |
98 171 178
|
3syl |
|- ( ph -> ( _pi e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = _pi ) ) |
180 |
177 179
|
mpbid |
|- ( ph -> E. i e. ( 0 ... M ) ( Q ` i ) = _pi ) |
181 |
98 156
|
fssd |
|- ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) ) |
182 |
|
eluzfz2 |
|- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) ) |
183 |
122 182
|
syl |
|- ( ph -> M e. ( 0 ... M ) ) |
184 |
181 183
|
ffvelrnd |
|- ( ph -> ( Q ` M ) e. ( -u _pi [,] _pi ) ) |
185 |
|
iccleub |
|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ ( Q ` M ) e. ( -u _pi [,] _pi ) ) -> ( Q ` M ) <_ _pi ) |
186 |
142 143 184 185
|
syl3anc |
|- ( ph -> ( Q ` M ) <_ _pi ) |
187 |
186
|
3ad2ant1 |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> ( Q ` M ) <_ _pi ) |
188 |
|
id |
|- ( ( Q ` i ) = _pi -> ( Q ` i ) = _pi ) |
189 |
188
|
eqcomd |
|- ( ( Q ` i ) = _pi -> _pi = ( Q ` i ) ) |
190 |
189
|
3ad2ant3 |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> _pi = ( Q ` i ) ) |
191 |
107
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i = M ) -> ( Q ` i ) <_ ( Q ` i ) ) |
192 |
|
fveq2 |
|- ( i = M -> ( Q ` i ) = ( Q ` M ) ) |
193 |
192
|
adantl |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i = M ) -> ( Q ` i ) = ( Q ` M ) ) |
194 |
191 193
|
breqtrd |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i = M ) -> ( Q ` i ) <_ ( Q ` M ) ) |
195 |
111
|
ad2antlr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. i = M ) -> i e. RR ) |
196 |
|
elfzel2 |
|- ( i e. ( 0 ... M ) -> M e. ZZ ) |
197 |
196
|
zred |
|- ( i e. ( 0 ... M ) -> M e. RR ) |
198 |
197
|
ad2antlr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. i = M ) -> M e. RR ) |
199 |
|
elfzle2 |
|- ( i e. ( 0 ... M ) -> i <_ M ) |
200 |
199
|
ad2antlr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. i = M ) -> i <_ M ) |
201 |
|
neqne |
|- ( -. i = M -> i =/= M ) |
202 |
201
|
necomd |
|- ( -. i = M -> M =/= i ) |
203 |
202
|
adantl |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. i = M ) -> M =/= i ) |
204 |
195 198 200 203
|
leneltd |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. i = M ) -> i < M ) |
205 |
106
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> ( Q ` i ) e. RR ) |
206 |
90 184
|
sseldi |
|- ( ph -> ( Q ` M ) e. RR ) |
207 |
206
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> ( Q ` M ) e. RR ) |
208 |
|
simpr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> i < M ) |
209 |
95
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> Q Isom < , < ( ( 0 ... M ) , H ) ) |
210 |
|
simpr |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( 0 ... M ) ) |
211 |
183
|
adantr |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> M e. ( 0 ... M ) ) |
212 |
210 211
|
jca |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( i e. ( 0 ... M ) /\ M e. ( 0 ... M ) ) ) |
213 |
212
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> ( i e. ( 0 ... M ) /\ M e. ( 0 ... M ) ) ) |
214 |
|
isorel |
|- ( ( Q Isom < , < ( ( 0 ... M ) , H ) /\ ( i e. ( 0 ... M ) /\ M e. ( 0 ... M ) ) ) -> ( i < M <-> ( Q ` i ) < ( Q ` M ) ) ) |
215 |
209 213 214
|
syl2anc |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> ( i < M <-> ( Q ` i ) < ( Q ` M ) ) ) |
216 |
208 215
|
mpbid |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> ( Q ` i ) < ( Q ` M ) ) |
217 |
205 207 216
|
ltled |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ i < M ) -> ( Q ` i ) <_ ( Q ` M ) ) |
218 |
204 217
|
syldan |
|- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ -. i = M ) -> ( Q ` i ) <_ ( Q ` M ) ) |
219 |
194 218
|
pm2.61dan |
|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ ( Q ` M ) ) |
220 |
219
|
3adant3 |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> ( Q ` i ) <_ ( Q ` M ) ) |
221 |
190 220
|
eqbrtrd |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> _pi <_ ( Q ` M ) ) |
222 |
206
|
3ad2ant1 |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> ( Q ` M ) e. RR ) |
223 |
19
|
a1i |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> _pi e. RR ) |
224 |
222 223
|
letri3d |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> ( ( Q ` M ) = _pi <-> ( ( Q ` M ) <_ _pi /\ _pi <_ ( Q ` M ) ) ) ) |
225 |
187 221 224
|
mpbir2and |
|- ( ( ph /\ i e. ( 0 ... M ) /\ ( Q ` i ) = _pi ) -> ( Q ` M ) = _pi ) |
226 |
225
|
rexlimdv3a |
|- ( ph -> ( E. i e. ( 0 ... M ) ( Q ` i ) = _pi -> ( Q ` M ) = _pi ) ) |
227 |
180 226
|
mpd |
|- ( ph -> ( Q ` M ) = _pi ) |
228 |
|
elfzoelz |
|- ( i e. ( 0 ..^ M ) -> i e. ZZ ) |
229 |
228
|
zred |
|- ( i e. ( 0 ..^ M ) -> i e. RR ) |
230 |
229
|
ltp1d |
|- ( i e. ( 0 ..^ M ) -> i < ( i + 1 ) ) |
231 |
230
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i < ( i + 1 ) ) |
232 |
|
elfzofz |
|- ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) ) |
233 |
|
fzofzp1 |
|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) ) |
234 |
232 233
|
jca |
|- ( i e. ( 0 ..^ M ) -> ( i e. ( 0 ... M ) /\ ( i + 1 ) e. ( 0 ... M ) ) ) |
235 |
|
isorel |
|- ( ( Q Isom < , < ( ( 0 ... M ) , H ) /\ ( i e. ( 0 ... M ) /\ ( i + 1 ) e. ( 0 ... M ) ) ) -> ( i < ( i + 1 ) <-> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) |
236 |
95 234 235
|
syl2an |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i < ( i + 1 ) <-> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) |
237 |
231 236
|
mpbid |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) |
238 |
237
|
ralrimiva |
|- ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) |
239 |
175 227 238
|
jca31 |
|- ( ph -> ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) |
240 |
10
|
fourierdlem2 |
|- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |
241 |
73 240
|
syl |
|- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |
242 |
103 239 241
|
mpbir2and |
|- ( ph -> Q e. ( P ` M ) ) |
243 |
4
|
reseq1i |
|- ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |
244 |
21
|
a1i |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* ) |
245 |
22
|
a1i |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* ) |
246 |
181
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) ) |
247 |
|
simpr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) ) |
248 |
244 245 246 247
|
fourierdlem27 |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi (,) _pi ) ) |
249 |
248
|
resabs1d |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) |
250 |
243 249
|
eqtr2id |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) |
251 |
6 10 73 242 12 169
|
fourierdlem38 |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) |
252 |
250 251
|
eqeltrd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) |
253 |
250
|
oveq1d |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) |
254 |
6
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> G e. ( dom G -cn-> CC ) ) |
255 |
7
|
adantlr |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) ) |
256 |
8
|
adantlr |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) ) |
257 |
95
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q Isom < , < ( ( 0 ... M ) , H ) ) |
258 |
257 96 97
|
3syl |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> H ) |
259 |
84
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E ` X ) e. RR ) |
260 |
257 167 168
|
3syl |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ran Q = H ) |
261 |
254 255 256 257 258 247 237 248 259 12 260
|
fourierdlem46 |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) /\ ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) ) ) |
262 |
261
|
simpld |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) ) |
263 |
253 262
|
eqnetrd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) ) |
264 |
250
|
oveq1d |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) |
265 |
261
|
simprd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) ) |
266 |
264 265
|
eqnetrd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) ) |
267 |
1 2 3 9 10 73 242 252 263 266
|
fourierdlem94 |
|- ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) ) |