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