Metamath Proof Explorer

Theorem fourierdlem102

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem102.f 
|- ( ph -> F : RR --> RR )
fourierdlem102.t 
|- T = ( 2 x. _pi )
fourierdlem102.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem102.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fourierdlem102.dmdv 
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
fourierdlem102.gcn 
|- ( ph -> G e. ( dom G -cn-> CC ) )
fourierdlem102.rlim 
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourierdlem102.llim 
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourierdlem102.x 
|- ( ph -> X e. RR )
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 ) ) ) } )
fourierdlem102.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
fourierdlem102.h 
|- H = ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) )
fourierdlem102.m 
|- M = ( ( # ` H ) - 1 )
fourierdlem102.q 
|- Q = ( iota g g Isom < , < ( ( 0 ... M ) , H ) )
Assertion fourierdlem102 
|- ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )

Proof

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 ) =/= (/) ) )