Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem74 Structured version   Unicode version

Theorem fourierdlem74 31804
Description: Given a piecewise smooth function  F, the derived function  H has a limit at the upper bound of each interval of the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem74.xre  |-  ( ph  ->  X  e.  RR )
fourierdlem74.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem74.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem74.x  |-  ( ph  ->  X  e.  ran  V
)
fourierdlem74.y  |-  ( ph  ->  Y  e.  RR )
fourierdlem74.w  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem74.h  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
fourierdlem74.m  |-  ( ph  ->  M  e.  NN )
fourierdlem74.v  |-  ( ph  ->  V  e.  ( P `
 M ) )
fourierdlem74.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
fourierdlem74.q  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
fourierdlem74.o  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem74.g  |-  G  =  ( RR  _D  F
)
fourierdlem74.gcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
fourierdlem74.e  |-  ( ph  ->  E  e.  ( ( G  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem74.a  |-  A  =  if ( ( V `
 ( i  +  1 ) )  =  X ,  E , 
( ( R  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  /  ( Q `
 ( i  +  1 ) ) ) )
Assertion
Ref Expression
fourierdlem74  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  ( ( H  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
Distinct variable groups:    E, s    F, s    H, s    i, M, m, p    M, s, i    Q, i, p    Q, s    R, s    i, V, p    V, s    W, s   
i, X, m, p    X, s    Y, s    ph, i,
s
Allowed substitution hints:    ph( m, p)    A( i, m, s, p)    P( i, m, s, p)    Q( m)    R( i, m, p)    E( i, m, p)    F( i, m, p)    G( i, m, s, p)    H( i, m, p)    O( i, m, s, p)    V( m)    W( i, m, p)    Y( i, m, p)

Proof of Theorem fourierdlem74
Dummy variables  x  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzofz 11823 . . . . . . 7  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
21adantl 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
3 pire 22718 . . . . . . . . . . . . 13  |-  pi  e.  RR
43renegcli 9892 . . . . . . . . . . . 12  |-  -u pi  e.  RR
54a1i 11 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  e.  RR )
6 fourierdlem74.xre . . . . . . . . . . 11  |-  ( ph  ->  X  e.  RR )
75, 6jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi  e.  RR  /\  X  e.  RR ) )
8 readdcl 9587 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR  /\  X  e.  RR )  ->  ( -u pi  +  X )  e.  RR )
97, 8syl 16 . . . . . . . . 9  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
103a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  pi  e.  RR )
1110, 6jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( pi  e.  RR  /\  X  e.  RR ) )
12 readdcl 9587 . . . . . . . . . 10  |-  ( ( pi  e.  RR  /\  X  e.  RR )  ->  ( pi  +  X
)  e.  RR )
1311, 12syl 16 . . . . . . . . 9  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
149, 13iccssred 31426 . . . . . . . 8  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
1514adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
) [,] ( pi  +  X ) ) 
C_  RR )
16 fourierdlem74.p . . . . . . . . 9  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
17 fourierdlem74.m . . . . . . . . 9  |-  ( ph  ->  M  e.  NN )
18 fourierdlem74.v . . . . . . . . 9  |-  ( ph  ->  V  e.  ( P `
 M ) )
1916, 17, 18fourierdlem15 31745 . . . . . . . 8  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
2019ffvelrnda 6032 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
2115, 20sseldd 3510 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
222, 21syldan 470 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
2322adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( V `  i )  e.  RR )
246adantr 465 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
2524adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  X  e.  RR )
2616fourierdlem2 31732 . . . . . . . . . . 11  |-  ( M  e.  NN  ->  ( V  e.  ( P `  M )  <->  ( V  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
2717, 26syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( V  e.  ( P `  M )  <-> 
( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
2818, 27mpbid 210 . . . . . . . . 9  |-  ( ph  ->  ( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) )
2928simprd 463 . . . . . . . 8  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
3029simprd 463 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
3130r19.21bi 2836 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
3231adantr 465 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( V `  i )  <  ( V `  (
i  +  1 ) ) )
33 eqcom 2476 . . . . . . 7  |-  ( ( V `  ( i  +  1 ) )  =  X  <->  X  =  ( V `  ( i  +  1 ) ) )
3433biimpi 194 . . . . . 6  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  X  =  ( V `  ( i  +  1 ) ) )
3534adantl 466 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  X  =  ( V `  ( i  +  1 ) ) )
3632, 35breqtrrd 4479 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( V `  i )  <  X )
37 fourierdlem74.f . . . . . 6  |-  ( ph  ->  F : RR --> RR )
38 ioossre 11598 . . . . . . 7  |-  ( ( V `  i ) (,) X )  C_  RR
3938a1i 11 . . . . . 6  |-  ( ph  ->  ( ( V `  i ) (,) X
)  C_  RR )
4037, 39fssresd 5758 . . . . 5  |-  ( ph  ->  ( F  |`  (
( V `  i
) (,) X ) ) : ( ( V `  i ) (,) X ) --> RR )
4140ad2antrr 725 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( F  |`  ( ( V `
 i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR )
42 limcresi 22157 . . . . . . . 8  |-  ( ( F  |`  ( -oo (,) X ) ) lim CC  X )  C_  (
( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X ) ) lim CC  X )
43 fourierdlem74.w . . . . . . . 8  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
4442, 43sseldi 3507 . . . . . . 7  |-  ( ph  ->  W  e.  ( ( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
) )
4544adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X ) ) lim CC  X ) )
46 mnfxr 11335 . . . . . . . . . 10  |- -oo  e.  RR*
4746a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  e.  RR* )
4822rexrd 9655 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR* )
4922mnfltd 31391 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <  ( V `
 i ) )
5047, 48, 49xrltled 31356 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <_  ( V `
 i ) )
51 iooss1 11576 . . . . . . . . 9  |-  ( ( -oo  e.  RR*  /\ -oo  <_  ( V `  i
) )  ->  (
( V `  i
) (,) X ) 
C_  ( -oo (,) X ) )
5247, 50, 51syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i ) (,) X )  C_  ( -oo (,) X ) )
5352resabs1d 5309 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -oo (,) X
) )  |`  (
( V `  i
) (,) X ) )  =  ( F  |`  ( ( V `  i ) (,) X
) ) )
5453oveq1d 6310 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( F  |`  ( ( V `  i ) (,) X ) ) lim CC  X ) )
5545, 54eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( F  |`  (
( V `  i
) (,) X ) ) lim CC  X ) )
5655adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  W  e.  ( ( F  |`  ( ( V `  i ) (,) X
) ) lim CC  X
) )
57 eqid 2467 . . . 4  |-  ( RR 
_D  ( F  |`  ( ( V `  i ) (,) X
) ) )  =  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )
58 ax-resscn 9561 . . . . . . . . . 10  |-  RR  C_  CC
5958a1i 11 . . . . . . . . 9  |-  ( ph  ->  RR  C_  CC )
60 fss 5745 . . . . . . . . . 10  |-  ( ( F : RR --> RR  /\  RR  C_  CC )  ->  F : RR --> CC )
6137, 59, 60syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  F : RR --> CC )
62 ssid 3528 . . . . . . . . . 10  |-  RR  C_  RR
6362a1i 11 . . . . . . . . 9  |-  ( ph  ->  RR  C_  RR )
64 eqid 2467 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6564tgioo2 21176 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
6664, 65dvres 22183 . . . . . . . . 9  |-  ( ( ( RR  C_  CC  /\  F : RR --> CC )  /\  ( RR  C_  RR  /\  ( ( V `
 i ) (,) X )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( ( V `  i ) (,) X
) ) )  =  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) ) )
6759, 61, 63, 39, 66syl22anc 1229 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) ) )
68 fourierdlem74.g . . . . . . . . . . 11  |-  G  =  ( RR  _D  F
)
6968eqcomi 2480 . . . . . . . . . 10  |-  ( RR 
_D  F )  =  G
70 iooretop 21141 . . . . . . . . . . 11  |-  ( ( V `  i ) (,) X )  e.  ( topGen `  ran  (,) )
71 retop 21136 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  Top
72 uniretop 21137 . . . . . . . . . . . . 13  |-  RR  =  U. ( topGen `  ran  (,) )
7372isopn3 19435 . . . . . . . . . . . 12  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( V `  i ) (,) X )  C_  RR )  ->  ( ( ( V `  i
) (,) X )  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( V `  i ) (,) X ) )  =  ( ( V `  i ) (,) X
) ) )
7471, 38, 73mp2an 672 . . . . . . . . . . 11  |-  ( ( ( V `  i
) (,) X )  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( V `  i ) (,) X ) )  =  ( ( V `  i ) (,) X
) )
7570, 74mpbi 208 . . . . . . . . . 10  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( V `  i ) (,) X
) )  =  ( ( V `  i
) (,) X )
7669, 75reseq12i 5277 . . . . . . . . 9  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) )  =  ( G  |`  ( ( V `  i ) (,) X
) )
7776a1i 11 . . . . . . . 8  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) )  =  ( G  |`  ( ( V `  i ) (,) X
) ) )
7867, 77eqtrd 2508 . . . . . . 7  |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  ( G  |`  ( ( V `  i ) (,) X
) ) )
7978dmeqd 5211 . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  ( F  |`  ( ( V `  i ) (,) X ) ) )  =  dom  ( G  |`  ( ( V `
 i ) (,) X ) ) )
8079ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  dom  ( G  |`  ( ( V `  i ) (,) X
) ) )
81 fourierdlem74.gcn . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
8281adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR )
83 oveq2 6303 . . . . . . . . . 10  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( ( V `
 i ) (,) X ) )
8483reseq2d 5279 . . . . . . . . 9  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  =  ( G  |`  (
( V `  i
) (,) X ) ) )
8584, 83feq12d 5726 . . . . . . . 8  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  (
( G  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  <->  ( G  |`  ( ( V `  i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR ) )
8685adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( G  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  <->  ( G  |`  ( ( V `  i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR ) )
8782, 86mpbid 210 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR )
88 fdm 5741 . . . . . 6  |-  ( ( G  |`  ( ( V `  i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR  ->  dom  ( G  |`  ( ( V `  i ) (,) X ) )  =  ( ( V `
 i ) (,) X ) )
8987, 88syl 16 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  dom  ( G  |`  ( ( V `  i ) (,) X ) )  =  ( ( V `
 i ) (,) X ) )
9080, 89eqtrd 2508 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  ( ( V `
 i ) (,) X ) )
91 limcresi 22157 . . . . . . . . 9  |-  ( ( G  |`  ( -oo (,) X ) ) lim CC  X )  C_  (
( ( G  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X ) ) lim CC  X )
9291a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( -oo (,) X
) ) lim CC  X
)  C_  ( (
( G  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
) )
9352resabs1d 5309 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( -oo (,) X
) )  |`  (
( V `  i
) (,) X ) )  =  ( G  |`  ( ( V `  i ) (,) X
) ) )
9493oveq1d 6310 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( G  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( G  |`  ( ( V `  i ) (,) X ) ) lim CC  X ) )
9592, 94sseqtrd 3545 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( -oo (,) X
) ) lim CC  X
)  C_  ( ( G  |`  ( ( V `
 i ) (,) X ) ) lim CC  X ) )
96 fourierdlem74.e . . . . . . . 8  |-  ( ph  ->  E  e.  ( ( G  |`  ( -oo (,) X ) ) lim CC  X ) )
9796adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( G  |`  ( -oo (,) X ) ) lim
CC  X ) )
9895, 97sseldd 3510 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( G  |`  (
( V `  i
) (,) X ) ) lim CC  X ) )
9967, 77eqtr2d 2509 . . . . . . . 8  |-  ( ph  ->  ( G  |`  (
( V `  i
) (,) X ) )  =  ( RR 
_D  ( F  |`  ( ( V `  i ) (,) X
) ) ) )
10099oveq1d 6310 . . . . . . 7  |-  ( ph  ->  ( ( G  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( RR  _D  ( F  |`  ( ( V `  i ) (,) X
) ) ) lim CC  X ) )
101100adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( RR  _D  ( F  |`  ( ( V `  i ) (,) X
) ) ) lim CC  X ) )
10298, 101eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) ) lim
CC  X ) )
103102adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  E  e.  ( ( RR  _D  ( F  |`  ( ( V `  i ) (,) X ) ) ) lim CC  X ) )
104 eqid 2467 . . . 4  |-  ( s  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) )  =  ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  ( ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  -  W )  / 
s ) )
105 oveq2 6303 . . . . . . 7  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
106105fveq2d 5876 . . . . . 6  |-  ( x  =  s  ->  (
( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  x ) )  =  ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
) )
107106oveq1d 6310 . . . . 5  |-  ( x  =  s  ->  (
( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  x )
)  -  W )  =  ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
) )
108107cbvmptv 4544 . . . 4  |-  ( x  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  x ) )  -  W ) )  =  ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
) )
109 id 22 . . . . 5  |-  ( x  =  s  ->  x  =  s )
110109cbvmptv 4544 . . . 4  |-  ( x  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  x )  =  ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  s )
11123, 25, 36, 41, 56, 57, 90, 103, 104, 108, 110fourierdlem60 31790 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  E  e.  ( ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  ( ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  -  W )  / 
s ) ) lim CC  0 ) )
112 fourierdlem74.a . . . . . 6  |-  A  =  if ( ( V `
 ( i  +  1 ) )  =  X ,  E , 
( ( R  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  /  ( Q `
 ( i  +  1 ) ) ) )
113 iftrue 3951 . . . . . 6  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  if ( ( V `  ( i  +  1 ) )  =  X ,  E ,  ( ( R  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  /  ( Q `
 ( i  +  1 ) ) ) )  =  E )
114112, 113syl5eq 2520 . . . . 5  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  A  =  E )
115114adantl 466 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  A  =  E )
116 fourierdlem74.h . . . . . . . 8  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
117116reseq1i 5275 . . . . . . 7  |-  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
118117a1i 11 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
119 ioossicc 11622 . . . . . . . . . 10  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
120119a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
1214rexri 9658 . . . . . . . . . . 11  |-  -u pi  e.  RR*
122121a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
1233rexri 9658 . . . . . . . . . . 11  |-  pi  e.  RR*
124123a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
1254a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  e.  RR )
1263a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  RR )
1276adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
12821, 127resubcld 9999 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
1295recnd 9634 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u pi  e.  CC )
1306recnd 9634 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  CC )
131129, 130pncand 9943 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
132131eqcomd 2475 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u pi  =  ( ( -u pi  +  X )  -  X
) )
133132adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  =  ( ( -u pi  +  X )  -  X ) )
1349adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  e.  RR )
13513adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
pi  +  X )  e.  RR )
136 elicc2 11601 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -u pi  +  X )  e.  RR  /\  ( pi  +  X
)  e.  RR )  ->  ( ( V `
 i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  <->  ( ( V `
 i )  e.  RR  /\  ( -u pi  +  X )  <_ 
( V `  i
)  /\  ( V `  i )  <_  (
pi  +  X ) ) ) )
137134, 135, 136syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  <-> 
( ( V `  i )  e.  RR  /\  ( -u pi  +  X )  <_  ( V `  i )  /\  ( V `  i
)  <_  ( pi  +  X ) ) ) )
13820, 137mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  RR  /\  ( -u pi  +  X
)  <_  ( V `  i )  /\  ( V `  i )  <_  ( pi  +  X
) ) )
139138simp2d 1009 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  <_  ( V `  i ) )
140134, 21, 127lesub1d 10171 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  <_  ( V `  i )  <->  ( ( -u pi  +  X )  -  X )  <_ 
( ( V `  i )  -  X
) ) )
141139, 140mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  -  X )  <_  ( ( V `
 i )  -  X ) )
142133, 141eqbrtrd 4473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  <_  ( ( V `  i )  -  X
) )
143138simp3d 1010 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  <_  ( pi  +  X
) )
14421, 135, 127lesub1d 10171 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  <_  ( pi  +  X )  <->  ( ( V `  i )  -  X )  <_  (
( pi  +  X
)  -  X ) ) )
145143, 144mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  ( ( pi  +  X )  -  X ) )
146126recnd 9634 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  CC )
147130adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  CC )
148146, 147pncand 9943 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( pi  +  X
)  -  X )  =  pi )
149145, 148breqtrd 4477 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  pi )
150125, 126, 128, 142, 149eliccd 31425 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  ( -u pi [,] pi ) )
151 fourierdlem74.q . . . . . . . . . . . 12  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
152150, 151fmptd 6056 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
153152adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
154 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
155122, 124, 153, 154fourierdlem8 31738 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
156120, 155sstrd 3519 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
157 resmpt 5329 . . . . . . . 8  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  ->  (
( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) ) )
158156, 157syl 16 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) ) )
159158adantr 465 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) ) )
1602, 128syldan 470 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
161151fvmpt2 5964 . . . . . . . . . 10  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
1622, 160, 161syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
163162adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
164 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
165164oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
166165cbvmptv 4544 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
167151, 166eqtri 2496 . . . . . . . . . . . 12  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
168167a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
169 fveq2 5872 . . . . . . . . . . . . 13  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
170169oveq1d 6310 . . . . . . . . . . . 12  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
171170adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
172 fzofzp1 11889 . . . . . . . . . . . 12  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
173172adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
174 simpl 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ph )
17528simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  e.  ( RR 
^m  ( 0 ... M ) ) )
176 elmapi 7452 . . . . . . . . . . . . . . 15  |-  ( V  e.  ( RR  ^m  ( 0 ... M
) )  ->  V : ( 0 ... M ) --> RR )
177175, 176syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
178174, 177syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
179178, 173ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
180179, 24resubcld 9999 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
181168, 171, 173, 180fvmptd 5962 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
182181adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
183 oveq1 6302 . . . . . . . . . 10  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  (
( V `  (
i  +  1 ) )  -  X )  =  ( X  -  X ) )
184183adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( V `  (
i  +  1 ) )  -  X )  =  ( X  -  X ) )
185130ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  ( i  +  1 ) )  =  X )  ->  X  e.  CC )
186185subidd 9930 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  ( i  +  1 ) )  =  X )  -> 
( X  -  X
)  =  0 )
1871, 186sylanl2 651 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( X  -  X )  =  0 )
188182, 184, 1873eqtrd 2512 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  0 )
189163, 188oveq12d 6313 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( ( V `  i )  -  X ) (,) 0 ) )
190 id 22 . . . . . . . . . . . 12  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
191190ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
192174anim1i 568 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  ( ph  /\  s  =  0 ) )
193 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  i  e.  ( 0..^ M ) )
194 fourierdlem74.o . . . . . . . . . . . . . 14  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
19517adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  M  e.  NN )
1965, 10, 6, 16, 194, 17, 18, 151fourierdlem14 31744 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( O `
 M ) )
197196adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  Q  e.  ( O `  M
) )
198 simpr 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  = 
0 )  ->  s  =  0 )
199 fourierdlem74.x . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  e.  ran  V
)
200 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V : ( 0 ... M ) --> ( (
-u pi  +  X
) [,] ( pi  +  X ) )  ->  V  Fn  (
0 ... M ) )
20119, 200syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  V  Fn  ( 0 ... M ) )
202 fvelrnb 5921 . . . . . . . . . . . . . . . . . . . 20  |-  ( V  Fn  ( 0 ... M )  ->  ( X  e.  ran  V  <->  E. i  e.  ( 0 ... M
) ( V `  i )  =  X ) )
203201, 202syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( X  e.  ran  V  <->  E. i  e.  (
0 ... M ) ( V `  i )  =  X ) )
204199, 203mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( V `  i
)  =  X )
205 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( 0 ... M
) )
206151fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  ( -u pi [,] pi ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
207205, 150, 206syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
208207adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
209 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( V `  i )  =  X  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
210209adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
211130subidd 9930 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( X  -  X
)  =  0 )
212211ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( X  -  X )  =  0 )
213208, 210, 2123eqtrd 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  0 )
214213ex 434 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  =  X  -> 
( Q `  i
)  =  0 ) )
215214reximdva 2942 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. i  e.  ( 0 ... M
) ( V `  i )  =  X  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 ) )
216204, 215mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 )
217128, 151fmptd 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
218 ffn 5737 . . . . . . . . . . . . . . . . . . 19  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
219217, 218syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
220 fvelrnb 5921 . . . . . . . . . . . . . . . . . 18  |-  ( Q  Fn  ( 0 ... M )  ->  (
0  e.  ran  Q  <->  E. i  e.  ( 0 ... M ) ( Q `  i )  =  0 ) )
221219, 220syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 0  e.  ran  Q  <->  E. i  e.  (
0 ... M ) ( Q `  i )  =  0 ) )
222216, 221mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  ran  Q
)
223222adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  = 
0 )  ->  0  e.  ran  Q )
224198, 223eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  s  e.  ran  Q )
225194, 195, 197, 224fourierdlem12 31742 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  =  0 )  /\  i  e.  ( 0..^ M ) )  ->  -.  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
226192, 193, 225syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
227226adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
228191, 227pm2.65da 576 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
229228adantlr 714 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  s  =  0
)
230229iffalsed 3956 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
231 elioore 11571 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
232231adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
233 0re 9608 . . . . . . . . . . . . . 14  |-  0  e.  RR
234233a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
235 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  <->  ( (
( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  RR* )  /\  (
( Q `  i
)  <  s  /\  s  <  ( Q `  ( i  +  1 ) ) ) ) )
236235biimpi 194 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( ( Q `  i )  e.  RR*  /\  ( Q `  (
i  +  1 ) )  e.  RR*  /\  s  e.  RR* )  /\  (
( Q `  i
)  <  s  /\  s  <  ( Q `  ( i  +  1 ) ) ) ) )
237236simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  RR* ) )
238237simp1d 1008 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  e.  RR* )
239237simp2d 1009 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
240 elioo2 11582 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( s  e.  RR  /\  ( Q `
 i )  < 
s  /\  s  <  ( Q `  ( i  +  1 ) ) ) ) )
241238, 239, 240syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( s  e.  RR  /\  ( Q `
 i )  < 
s  /\  s  <  ( Q `  ( i  +  1 ) ) ) ) )
242190, 241mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
s  e.  RR  /\  ( Q `  i )  <  s  /\  s  <  ( Q `  (
i  +  1 ) ) ) )
243242simp3d 1010 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
244243adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
245188adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  =  0 )
246244, 245breqtrd 4477 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  0 )
247232, 234, 246ltled 9744 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <_  0 )
248232, 234lenltd 9742 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( s  <_  0  <->  -.  0  <  s ) )
249247, 248mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  0  <  s )
250249iffalsed 3956 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
251250oveq2d 6311 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  W ) )
252251oveq1d 6310 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  =  ( ( ( F `  ( X  +  s ) )  -  W )  / 
s ) )
25348ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  i
)  e.  RR* )
2546rexrd 9655 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  RR* )
255254ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR* )
25625adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR )
257256, 232readdcld 9635 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  RR )
258130adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
259 iccssre 11618 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
2604, 3, 259mp2an 672 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u pi [,] pi )  C_  RR
261260, 58sstri 3518 . . . . . . . . . . . . . . . . . . 19  |-  ( -u pi [,] pi )  C_  CC
262261a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( -u pi [,] pi )  C_  CC )
263207, 150eqeltrd 2555 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  ( -u pi [,] pi ) )
264174, 2, 263syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
265262, 264sseldd 3510 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
266258, 265addcomd 9793 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  i ) )  =  ( ( Q `  i )  +  X ) )
267162oveq1d 6310 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( ( ( V `  i )  -  X
)  +  X ) )
26858, 22sseldi 3507 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  CC )
269268, 258npcand 9946 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  i )  -  X )  +  X )  =  ( V `  i ) )
270266, 267, 2693eqtrrd 2513 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  =  ( X  +  ( Q `
 i ) ) )
271270adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
272162, 160eqeltrd 2555 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
273272adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
274231adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
2756adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
276174, 275sylan 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
277242simp2d 1009 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  <  s )
278277adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
279273, 274, 276, 278ltadd2dd 9752 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
280271, 279eqbrtrd 4473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
281280adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  i
)  <  ( X  +  s ) )
282 ltaddneg 31384 . . . . . . . . . . . . . 14  |-  ( ( s  e.  RR  /\  X  e.  RR )  ->  ( s  <  0  <->  ( X  +  s )  <  X ) )
283232, 256, 282syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( s  <  0  <->  ( X  +  s )  <  X ) )
284246, 283mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  <  X )
285253, 255, 257, 281, 284eliood 31418 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  ( ( V `  i ) (,) X ) )
286 fvres 5886 . . . . . . . . . . . 12  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) X )  ->  (
( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
287286eqcomd 2475 . . . . . . . . . . 11  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) X )  ->  ( F `  ( X  +  s ) )  =  ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
) )
288285, 287syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( F `  ( X  +  s )
)  =  ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) ) )
289288oveq1d 6310 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  W
)  =  ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  -  W ) )
290289oveq1d 6310 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  W )  /  s
)  =  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) )
291230, 252, 2903eqtrd 2512 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) )
292189, 291mpteq12dva 4530 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  =  ( s  e.  ( ( ( V `  i
)  -  X ) (,) 0 )  |->  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) ) )
293118, 159, 2923eqtrd 2512 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( s  e.  ( ( ( V `  i )  -  X
) (,) 0 ) 
|->  ( ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
)  /  s ) ) )
294293, 188oveq12d 6313 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( H  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) )  =  ( ( s  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) ) lim
CC  0 ) )
295115, 294eleq12d 2549 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( A  e.  ( ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  <->  E  e.  (
( s  e.  ( ( ( V `  i )  -  X
) (,) 0 ) 
|->  ( ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
)  /  s ) ) lim CC  0 ) ) )
296111, 295mpbird 232 . 2  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
297 eqid 2467 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) ) )
298 eqid 2467 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  s )
299 eqid 2467 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
30037adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> RR )
301231adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
302275, 301readdcld 9635 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
303300, 302ffvelrnd 6033 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
30458, 303sseldi 3507 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
305304adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
3063053adantl3 1154 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
307 fourierdlem74.y . . . . . . . . . 10  |-  ( ph  ->  Y  e.  RR )
30858sseli 3505 . . . . . . . . . 10  |-  ( Y  e.  RR  ->  Y  e.  CC )
309307, 308syl 16 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
310 limccl 22147 . . . . . . . . . 10  |-  ( ( F  |`  ( -oo (,) X ) ) lim CC  X )  C_  CC
311310, 43sseldi 3507 . . . . . . . . 9  |-  ( ph  ->  W  e.  CC )
312309, 311ifcld 3988 . . . . . . . 8  |-  ( ph  ->  if ( 0  < 
s ,  Y ,  W )  e.  CC )
313312adantr 465 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
3143133ad2antl1 1158 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
315306, 314subcld 9942 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  e.  CC )
316231recnd 9634 . . . . . . 7  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  CC )
317316adantl 466 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  CC )
318228neqned 2670 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  0 )
319318neneqd 2669 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
320 elsn 4047 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
321319, 320sylnibr 305 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
3223213adantl3 1154 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
323317, 322eldifd 3492 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
324 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
325 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  W )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  W )
326 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  W ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) )
327311ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  W  e.  CC )
328174, 37syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> RR )
329231ssriv 3513 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
330329a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
33148adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
332179rexrd 9655 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
333332adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
334302adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
335217adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
336335, 173ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
337336adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
338243adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
339274, 337, 276, 338ltadd2dd 9752 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
340181oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
34158, 179sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  CC )
342258, 341pncan3d 9945 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( V `  ( i  +  1 ) )  -  X
) )  =  ( V `  ( i  +  1 ) ) )
343 eqidd 2468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  =  ( V `  ( i  +  1 ) ) )
344340, 342, 3433eqtrd 2512 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
345344adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
346339, 345breqtrd 4477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
347331, 333, 334, 280, 346eliood 31418 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
348 ioossre 11598 . . . . . . . . . . . 12  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
349348a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  RR )
350274, 338ltned 9732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  (
i  +  1 ) ) )
351 fourierdlem74.r . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
352344eqcomd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  =  ( X  +  ( Q `
 ( i  +  1 ) ) ) )
353352oveq2d 6311 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
354351, 353eleqtrd 2557 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
355336recnd 9634 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
356328, 24, 330, 324, 347, 349, 350, 354, 355fourierdlem53 31783 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
357 ioosscn 31414 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
358357a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
359174, 311syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  CC )
360325, 358, 359, 355constlimc 31489 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  W ) lim CC  ( Q `  ( i  +  1 ) ) ) )
361324, 325, 326, 305, 327, 356, 360sublimc 31517 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  -  W )  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  W
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
362361adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( R  -  W )  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
363 iftrue 3951 . . . . . . . . . . 11  |-  ( ( V `  ( i  +  1 ) )  <  X  ->  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y )  =  W )
364363oveq2d 6311 . . . . . . . . . 10  |-  ( ( V `  ( i  +  1 ) )  <  X  ->  ( R  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
365364adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( R  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
366231adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
367233a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
368337adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
369243adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
370181adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
371179adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
37224adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  X  e.  RR )
373 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  <  X )
374371, 372, 373ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  <_  X )
375374ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  /\  -.  X  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  <_  X
)
376 simplr 754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  /\  -.  X  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  ->  -.  ( V `  ( i  +  1 ) )  <_  X )
377375, 376condan 792 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
37816, 17, 18, 199fourierdlem12 31742 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -.  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
379378adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  -.  X  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )
380379adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  -.  X  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
381377, 380condan 792 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  <_  X )
382371, 372suble0d 10155 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  (
( ( V `  ( i  +  1 ) )  -  X
)  <_  0  <->  ( V `  ( i  +  1 ) )  <_  X
) )
383381, 382mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  (
( V `  (
i  +  1 ) )  -  X )  <_  0 )
384370, 383eqbrtrd 4473 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( Q `  ( i  +  1 ) )  <_  0 )
385384adantr 465 . . . . . . . . . . . . . . . 16