Metamath Proof Explorer

Theorem fourierdlem114

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem114.f 
|- ( ph -> F : RR --> RR )
fourierdlem114.t 
|- T = ( 2 x. _pi )
fourierdlem114.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem114.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fourierdlem114.dmdv 
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
fourierdlem114.gcn 
|- ( ph -> G e. ( dom G -cn-> CC ) )
fourierdlem114.rlim 
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourierdlem114.llim 
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourierdlem114.x 
|- ( ph -> X e. RR )
fourierdlem114.l 
|- ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem114.r 
|- ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem114.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem114.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem114.s 
|- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
fourierdlem114.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 ) ) ) } )
fourierdlem114.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
fourierdlem114.h 
|- H = ( { -u _pi , _pi , ( E ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) )
fourierdlem114.m 
|- M = ( ( # ` H ) - 1 )
fourierdlem114.q 
|- Q = ( iota g g Isom < , < ( ( 0 ... M ) , H ) )
Assertion fourierdlem114 
|- ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )

Proof

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