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

Theorem fourierdlem75 37313
Description: Given a piecewise smooth function  F, the derived function  H has a limit at the lower bound of each interval of the partition  Q. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem75.xre  |-  ( ph  ->  X  e.  RR )
fourierdlem75.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 ) ) ) } )
fourierdlem75.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem75.x  |-  ( ph  ->  X  e.  ran  V
)
fourierdlem75.y  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
fourierdlem75.w  |-  ( ph  ->  W  e.  RR )
fourierdlem75.h  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
fourierdlem75.m  |-  ( ph  ->  M  e.  NN )
fourierdlem75.v  |-  ( ph  ->  V  e.  ( P `
 M ) )
fourierdlem75.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
fourierdlem75.q  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
fourierdlem75.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 ) ) ) } )
fourierdlem75.g  |-  G  =  ( RR  _D  F
)
fourierdlem75.gcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
fourierdlem75.e  |-  ( ph  ->  E  e.  ( ( G  |`  ( X (,) +oo ) ) lim CC  X ) )
fourierdlem75.a  |-  A  =  if ( ( V `
 i )  =  X ,  E , 
( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `
 i ) ) )
Assertion
Ref Expression
fourierdlem75  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A  e.  ( ( H  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
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 fourierdlem75
Dummy variables  x  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem75.xre . . . . 5  |-  ( ph  ->  X  e.  RR )
21ad2antrr 724 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  e.  RR )
3 fourierdlem75.v . . . . . . . . . 10  |-  ( ph  ->  V  e.  ( P `
 M ) )
4 fourierdlem75.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
5 fourierdlem75.p . . . . . . . . . . . 12  |-  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 ) ) ) } )
65fourierdlem2 37240 . . . . . . . . . . 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 ) ) ) ) ) )
74, 6syl 17 . . . . . . . . . 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 ) ) ) ) ) )
83, 7mpbid 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 ) ) ) ) )
98simpld 457 . . . . . . . 8  |-  ( ph  ->  V  e.  ( RR 
^m  ( 0 ... M ) ) )
10 elmapi 7477 . . . . . . . 8  |-  ( V  e.  ( RR  ^m  ( 0 ... M
) )  ->  V : ( 0 ... M ) --> RR )
119, 10syl 17 . . . . . . 7  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
1211adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
13 fzofzp1 11944 . . . . . . 7  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
1413adantl 464 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
1512, 14ffvelrnd 6009 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
1615adantr 463 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
17 eqcom 2411 . . . . . . 7  |-  ( ( V `  i )  =  X  <->  X  =  ( V `  i ) )
1817biimpi 194 . . . . . 6  |-  ( ( V `  i )  =  X  ->  X  =  ( V `  i ) )
1918adantl 464 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  =  ( V `  i ) )
208simprrd 759 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2120r19.21bi 2772 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2221adantr 463 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( V `  i )  <  ( V `  (
i  +  1 ) ) )
2319, 22eqbrtrd 4414 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  <  ( V `  (
i  +  1 ) ) )
24 fourierdlem75.f . . . . . . 7  |-  ( ph  ->  F : RR --> RR )
2524adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> RR )
26 ioossre 11638 . . . . . . 7  |-  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR
2726a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
2825, 27fssresd 5734 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) : ( X (,) ( V `  ( i  +  1 ) ) ) --> RR )
2928adantr 463 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> RR )
30 limcresi 22579 . . . . . . . 8  |-  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  C_  (
( ( F  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
)
31 fourierdlem75.y . . . . . . . 8  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
3230, 31sseldi 3439 . . . . . . 7  |-  ( ph  ->  Y  e.  ( ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
3332adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( ( F  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
34 pnfxr 11373 . . . . . . . . . 10  |- +oo  e.  RR*
3534a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> +oo  e.  RR* )
3615rexrd 9672 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
3715ltpnfd 36832 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  < +oo )
3836, 35, 37xrltled 36810 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  <_ +oo )
39 iooss2 11617 . . . . . . . . 9  |-  ( ( +oo  e.  RR*  /\  ( V `  ( i  +  1 ) )  <_ +oo )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  ( X (,) +oo )
)
4035, 38, 39syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  ( X (,) +oo ) )
4140resabs1d 5122 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
4241oveq1d 6292 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  X )  =  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
4333, 42eleqtrd 2492 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim
CC  X ) )
4443adantr 463 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  Y  e.  ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  X ) )
45 eqid 2402 . . . 4  |-  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )  =  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
46 ax-resscn 9578 . . . . . . . . . . 11  |-  RR  C_  CC
4746a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
4824, 47fssd 5722 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> CC )
49 ssid 3460 . . . . . . . . . . 11  |-  RR  C_  RR
5049a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  RR )
5126a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
52 eqid 2402 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5352tgioo2 21598 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
5452, 53dvres 22605 . . . . . . . . . 10  |-  ( ( ( RR  C_  CC  /\  F : RR --> CC )  /\  ( RR  C_  RR  /\  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
)  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) ) )
5547, 48, 50, 51, 54syl22anc 1231 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) ) )
56 fourierdlem75.g . . . . . . . . . . 11  |-  G  =  ( RR  _D  F
)
5756eqcomi 2415 . . . . . . . . . 10  |-  ( RR 
_D  F )  =  G
58 ioontr 36898 . . . . . . . . . 10  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( X (,) ( V `
 ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) )
5957, 58reseq12i 5091 . . . . . . . . 9  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) )
6055, 59syl6eq 2459 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6160adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( V `  i )  =  X )  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6261dmeqd 5025 . . . . . 6  |-  ( (
ph  /\  ( V `  i )  =  X )  ->  dom  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )  =  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6362adantlr 713 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  dom  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
64 fourierdlem75.gcn . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
6564adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC )
66 oveq1 6284 . . . . . . . . . . 11  |-  ( ( V `  i )  =  X  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
6766reseq2d 5093 . . . . . . . . . 10  |-  ( ( V `  i )  =  X  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6867feq1d 5699 . . . . . . . . 9  |-  ( ( V `  i )  =  X  ->  (
( G  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC  <->  ( G  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC ) )
6968adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( G  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC  <->  ( G  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC ) )
7065, 69mpbid 210 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
7166adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
7271feq2d 5700 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) --> CC  <->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> CC ) )
7370, 72mpbid 210 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> CC )
74 fdm 5717 . . . . . 6  |-  ( ( G  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) : ( X (,) ( V `  ( i  +  1 ) ) ) --> CC  ->  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
7573, 74syl 17 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
7663, 75eqtrd 2443 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
77 limcresi 22579 . . . . . . . 8  |-  ( ( G  |`  ( X (,) +oo ) ) lim CC  X )  C_  (
( ( G  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
)
78 fourierdlem75.e . . . . . . . 8  |-  ( ph  ->  E  e.  ( ( G  |`  ( X (,) +oo ) ) lim CC  X ) )
7977, 78sseldi 3439 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
8079adantr 463 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( ( G  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
8140resabs1d 5122 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
8260adantr 463 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
8381, 82eqtr4d 2446 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) )
8483oveq1d 6292 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  X )  =  ( ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) ) lim CC  X
) )
8580, 84eleqtrd 2492 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) lim CC  X ) )
8685adantr 463 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  E  e.  ( ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) lim CC  X ) )
87 eqid 2402 . . . 4  |-  ( s  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) )  |->  ( ( ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  -  Y )  / 
s ) )  =  ( s  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X ) ) 
|->  ( ( ( ( F  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) `  ( X  +  s
) )  -  Y
)  /  s ) )
88 oveq2 6285 . . . . . . 7  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
8988fveq2d 5852 . . . . . 6  |-  ( x  =  s  ->  (
( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `
 ( X  +  x ) )  =  ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) ) )
9089oveq1d 6292 . . . . 5  |-  ( x  =  s  ->  (
( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  x ) )  -  Y )  =  ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  -  Y ) )
9190cbvmptv 4486 . . . 4  |-  ( x  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) )  |->  ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `
 ( X  +  x ) )  -  Y ) )  =  ( s  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X ) ) 
|->  ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  -  Y ) )
92 id 22 . . . . 5  |-  ( x  =  s  ->  x  =  s )
9392cbvmptv 4486 . . . 4  |-  ( x  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) )  |->  x )  =  ( s  e.  ( 0 (,) (
( V `  (
i  +  1 ) )  -  X ) )  |->  s )
942, 16, 23, 29, 44, 45, 76, 86, 87, 91, 93fourierdlem61 37299 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  E  e.  ( ( s  e.  ( 0 (,) (
( V `  (
i  +  1 ) )  -  X ) )  |->  ( ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `
 ( X  +  s ) )  -  Y )  /  s
) ) lim CC  0 ) )
95 fourierdlem75.a . . . . 5  |-  A  =  if ( ( V `
 i )  =  X ,  E , 
( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `
 i ) ) )
96 iftrue 3890 . . . . 5  |-  ( ( V `  i )  =  X  ->  if ( ( V `  i )  =  X ,  E ,  ( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `
 i ) ) )  =  E )
9795, 96syl5eq 2455 . . . 4  |-  ( ( V `  i )  =  X  ->  A  =  E )
9897adantl 464 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  A  =  E )
99 fourierdlem75.h . . . . . . 7  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
10099reseq1i 5089 . . . . . 6  |-  ( 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 ) ) ) )
101100a1i 11 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  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 ) ) ) ) )
102 ioossicc 11662 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
103 pire 23141 . . . . . . . . . . . 12  |-  pi  e.  RR
104103renegcli 9915 . . . . . . . . . . 11  |-  -u pi  e.  RR
105104rexri 9675 . . . . . . . . . 10  |-  -u pi  e.  RR*
106105a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
107103rexri 9675 . . . . . . . . . 10  |-  pi  e.  RR*
108107a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
109104a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  e.  RR )
110103a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  RR )
111104a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u pi  e.  RR )
112111, 1readdcld 9652 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
113103a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  pi  e.  RR )
114113, 1readdcld 9652 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
115112, 114iccssred 36888 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
116115adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
) [,] ( pi  +  X ) ) 
C_  RR )
1175, 4, 3fourierdlem15 37253 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
118117ffvelrnda 6008 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
119116, 118sseldd 3442 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
1201adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
121119, 120resubcld 10027 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
122111recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u pi  e.  CC )
1231recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  CC )
124122, 123pncand 9967 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
125124eqcomd 2410 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  =  ( ( -u pi  +  X )  -  X
) )
126125adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  =  ( ( -u pi  +  X )  -  X ) )
127112adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  e.  RR )
128114adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
pi  +  X )  e.  RR )
129 elicc2 11641 . . . . . . . . . . . . . . . . 17  |-  ( ( ( -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 ) ) ) )
130127, 128, 129syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) ) ) )
131118, 130mpbid 210 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  RR  /\  ( -u pi  +  X
)  <_  ( V `  i )  /\  ( V `  i )  <_  ( pi  +  X
) ) )
132131simp2d 1010 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  <_  ( V `  i ) )
133127, 119, 120, 132lesub1dd 10207 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  -  X )  <_  ( ( V `
 i )  -  X ) )
134126, 133eqbrtrd 4414 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  <_  ( ( V `  i )  -  X
) )
135131simp3d 1011 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  <_  ( pi  +  X
) )
136119, 128, 120, 135lesub1dd 10207 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  ( ( pi  +  X )  -  X ) )
137110recnd 9651 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  CC )
138123adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  CC )
139137, 138pncand 9967 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( pi  +  X
)  -  X )  =  pi )
140136, 139breqtrd 4418 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  pi )
141109, 110, 121, 134, 140eliccd 36887 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  ( -u pi [,] pi ) )
142 fourierdlem75.q . . . . . . . . . . 11  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
143141, 142fmptd 6032 . . . . . . . . . 10  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
144143adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
145 simpr 459 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
146106, 108, 144, 145fourierdlem8 37246 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
147102, 146syl5ss 3452 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
148147resmptd 5144 . . . . . 6  |-  ( (
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 ) ) ) )
149148adantr 463 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  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 ) ) ) )
150 elfzofz 11872 . . . . . . . 8  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
151 simpr 459 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( 0 ... M
) )
152142fvmpt2 5940 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  ( -u pi [,] pi ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
153151, 141, 152syl2anc 659 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
154153adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
155 oveq1 6284 . . . . . . . . . 10  |-  ( ( V `  i )  =  X  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
156155adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
157123ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  X  e.  CC )
158157subidd 9954 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( X  -  X )  =  0 )
159154, 156, 1583eqtrd 2447 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  0 )
160150, 159sylanl2 649 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( Q `  i )  =  0 )
161 fveq2 5848 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
162161oveq1d 6292 . . . . . . . . . . . 12  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
163162cbvmptv 4486 . . . . . . . . . . 11  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
164142, 163eqtri 2431 . . . . . . . . . 10  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
165164a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
166 fveq2 5848 . . . . . . . . . . 11  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
167166oveq1d 6292 . . . . . . . . . 10  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
168167adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
1691adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
17015, 169resubcld 10027 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
171165, 168, 14, 170fvmptd 5937 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
172171adantr 463 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
173160, 172oveq12d 6295 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) ) )
174 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
175 fourierdlem75.o . . . . . . . . . . . . 13  |-  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 ) ) ) } )
1764adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  M  e.  NN )
177111, 113, 1, 5, 175, 4, 3, 142fourierdlem14 37252 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q  e.  ( O `
 M ) )
178177adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  Q  e.  ( O `  M
) )
179 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  s  =  0 )
180 fourierdlem75.x . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  X  e.  ran  V
)
181 ffn 5713 . . . . . . . . . . . . . . . . . . 19  |-  ( V : ( 0 ... M ) --> ( (
-u pi  +  X
) [,] ( pi  +  X ) )  ->  V  Fn  (
0 ... M ) )
182 fvelrnb 5895 . . . . . . . . . . . . . . . . . . 19  |-  ( V  Fn  ( 0 ... M )  ->  ( X  e.  ran  V  <->  E. i  e.  ( 0 ... M
) ( V `  i )  =  X ) )
183117, 181, 1823syl 20 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( X  e.  ran  V  <->  E. i  e.  (
0 ... M ) ( V `  i )  =  X ) )
184180, 183mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( V `  i
)  =  X )
185159ex 432 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  =  X  -> 
( Q `  i
)  =  0 ) )
186185reximdva 2878 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E. i  e.  ( 0 ... M
) ( V `  i )  =  X  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 ) )
187184, 186mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 )
188121, 142fmptd 6032 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
189 ffn 5713 . . . . . . . . . . . . . . . . 17  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
190 fvelrnb 5895 . . . . . . . . . . . . . . . . 17  |-  ( Q  Fn  ( 0 ... M )  ->  (
0  e.  ran  Q  <->  E. i  e.  ( 0 ... M ) ( Q `  i )  =  0 ) )
191188, 189, 1903syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  e.  ran  Q  <->  E. i  e.  (
0 ... M ) ( Q `  i )  =  0 ) )
192187, 191mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  ran  Q
)
193192adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  0  e.  ran  Q )
194179, 193eqeltrd 2490 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  s  e.  ran  Q )
195175, 176, 178, 194fourierdlem12 37250 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  =  0 )  /\  i  e.  ( 0..^ M ) )  ->  -.  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
196195an32s 805 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
197196adantlr 713 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
198174, 197pm2.65da 574 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
199198adantlr 713 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  s  =  0
)
200199iffalsed 3895 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  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 ) )
201160eqcomd 2410 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  0  =  ( Q `  i ) )
202201adantr 463 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  =  ( Q `
 i ) )
203 elioo3g 11610 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) )
204203biimpi 194 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) )
205204simprld 757 . . . . . . . . . . . 12  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  <  s )
206205adantl 464 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  s )
207202, 206eqbrtrd 4414 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  <  s )
208207iftrued 3892 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  Y )
209208oveq2d 6293 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  Y ) )
210209oveq1d 6292 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s ) )
2111rexrd 9672 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  RR* )
212211ad3antrrr 728 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR* )
21336ad2antrr 724 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  (
i  +  1 ) )  e.  RR* )
214169ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR )
215 elioore 11611 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
216215adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
217214, 216readdcld 9652 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  RR )
218216, 207elrpd 11300 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR+ )
219214, 218ltaddrpd 11332 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  <  ( X  +  s ) )
220215adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
221188adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
222221, 14ffvelrnd 6009 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
223222adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2241ad2antrr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
225204simprrd 759 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
226225adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
227220, 223, 224, 226ltadd2dd 9774 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
228171oveq2d 6293 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
229123adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
23015recnd 9651 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  CC )
231229, 230pncan3d 9969 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( V `  ( i  +  1 ) )  -  X
) )  =  ( V `  ( i  +  1 ) ) )
232228, 231eqtrd 2443 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
233232adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
234227, 233breqtrd 4418 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
235234adantlr 713 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  <  ( V `
 ( i  +  1 ) ) )
236212, 213, 217, 219, 235eliood 36880 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  ( X (,) ( V `  ( i  +  1 ) ) ) )
237 fvres 5862 . . . . . . . . . . 11  |-  ( ( X  +  s )  e.  ( X (,) ( V `  ( i  +  1 ) ) )  ->  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  =  ( F `
 ( X  +  s ) ) )
238236, 237syl 17 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
239238eqcomd 2410 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( F `  ( X  +  s )
)  =  ( ( F  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) `  ( X  +  s
) ) )
240239oveq1d 6292 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  Y
)  =  ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `
 ( X  +  s ) )  -  Y ) )
241240oveq1d 6292 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  =  ( ( ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  -  Y )  / 
s ) )
242200, 210, 2413eqtrd 2447 . . . . . 6  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  -  Y )  / 
s ) )
243173, 242mpteq12dva 4471 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  =  ( s  e.  ( 0 (,) ( ( V `
 ( i  +  1 ) )  -  X ) )  |->  ( ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  -  Y )  /  s ) ) )
244101, 149, 2433eqtrd 2447 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( s  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X ) ) 
|->  ( ( ( ( F  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) `  ( X  +  s
) )  -  Y
)  /  s ) ) )
245244, 160oveq12d 6295 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( H  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) )  =  ( ( s  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) )  |->  ( ( ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  -  Y )  / 
s ) ) lim CC  0 ) )
24694, 98, 2453eltr4d 2505 . 2  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
247 eqid 2402 . . . . 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 ) ) )
248 eqid 2402 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  s )
249 eqid 2402 . . . . 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 ) )
25024adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> RR )
2511adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
252215adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
253251, 252readdcld 9652 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
254250, 253ffvelrnd 6009 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
255254recnd 9651 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
256255adantlr 713 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
2572563adantl3 1155 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
258 limccl 22569 . . . . . . . . . 10  |-  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  C_  CC
259258, 31sseldi 3439 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
260 fourierdlem75.w . . . . . . . . . 10  |-  ( ph  ->  W  e.  RR )
261260recnd 9651 . . . . . . . . 9  |-  ( ph  ->  W  e.  CC )
262259, 261ifcld 3927 . . . . . . . 8  |-  ( ph  ->  if ( 0  < 
s ,  Y ,  W )  e.  CC )
263262adantr 463 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
2642633ad2antl1 1159 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
265257, 264subcld 9966 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  e.  CC )
266215recnd 9651 . . . . . . 7  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  CC )
267266adantl 464 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  CC )
268 elsn 3985 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
269198, 268sylnibr 303 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
2702693adantl3 1155 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
271267, 270eldifd 3424 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
272 eqid 2402 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
273 eqid 2402 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  W )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  W )
274 eqid 2402 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  W ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) )
275261ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  W  e.  CC )
276 ioossre 11638 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
277276a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
278150, 119sylan2 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
279278rexrd 9672 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR* )
280279adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
28136adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
282253adantlr 713 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
283 iccssre 11658 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
284104, 103, 283mp2an 670 . . . . . . . . . . . . . . . . . 18  |-  ( -u pi [,] pi )  C_  RR
285284, 46sstri 3450 . . . . . . . . . . . . . . . . 17  |-  ( -u pi [,] pi )  C_  CC
286153, 141eqeltrd 2490 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  ( -u pi [,] pi ) )
287150, 286sylan2 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
288285, 287sseldi 3439 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
289229, 288addcomd 9815 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  i ) )  =  ( ( Q `  i )  +  X ) )
290150adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
291150, 121sylan2 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
292142fvmpt2 5940 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
293290, 291, 292syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
294293oveq1d 6292 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( ( ( V `  i )  -  X
)  +  X ) )
295278recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  CC )
296295, 229npcand 9970 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  i )  -  X )  +  X )  =  ( V `  i ) )
297289, 294, 2963eqtrrd 2448 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  =  ( X  +  ( Q `
 i ) ) )
298297adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
299293, 291eqeltrd 2490 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
300299adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
301205adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
302300, 220, 224, 301ltadd2dd 9774 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
303298, 302eqbrtrd 4414 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
304280, 281, 282, 303, 234eliood 36880 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
305 ioossre 11638 . . . . . . . . . . . 12  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
306305a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  RR )
307300, 301gtned 9751 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  i
) )
308 fourierdlem75.r . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
309297oveq2d 6293 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  i )
)  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  i )
) ) )
310308, 309eleqtrd 2492 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  i ) ) ) )
31125, 169, 277, 272, 304, 306, 307, 310, 288fourierdlem53 37291 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  i )
) )
312 ioosscn 36876 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
313312a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
314261adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  CC )
315273, 313, 314, 288constlimc 36979 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  W ) lim CC  ( Q `  i )
) )
316272, 273, 274, 256, 275, 311, 315sublimc 37007 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  -  W )  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  W
) ) lim CC  ( Q `  i )
) )
317316adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( R  -  W )  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) ) lim CC  ( Q `  i ) ) )
318 iftrue 3890 . . . . . . . . . 10  |-  ( ( V `  i )  <  X  ->  if ( ( V `  i )  <  X ,  W ,  Y )  =  W )
319318oveq2d 6293 . . . . . . . . 9  |-  ( ( V `  i )  <  X  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
320319adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
321215adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
322 0red 9626 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
323222ad2antrr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
324225adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
325171adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
326279ad2antrr 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  i
)  e.  RR* )
32736ad2antrr 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  (
i  +  1 ) )  e.  RR* )
328169ad2antrr 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  RR )
329 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  i
)  <  X )
330 simpr 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  -.  ( V `  (
i  +  1 ) )  <_  X )
3311ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  X  e.  RR )
33215adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  -> 
( V `  (
i  +  1 ) )  e.  RR )
333331, 332ltnled 9763 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  -> 
( X  <  ( V `  ( i  +  1 ) )  <->  -.  ( V `  (
i  +  1 ) )  <_  X )
)
334330, 333mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  X  <  ( V `  ( i  +  1 ) ) )
335334adantlr 713 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  <  ( V `
 ( i  +  1 ) ) )
336326, 327, 328, 329, 335eliood 36880 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
3375, 4, 3, 180fourierdlem12 37250 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -.  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
338337ad2antrr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  -.  X  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
339336, 338condan 795 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( V `  ( i  +  1 ) )  <_  X )
34015adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
3411ad2antrr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  X  e.  RR )
342340, 341suble0d 10182 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  (
( ( V `  ( i  +  1 ) )  -  X
)  <_  0  <->  ( V `  ( i  +  1 ) )  <_  X
) )
343339, 342mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  (
( V `  (
i  +  1 ) )  -  X )  <_  0 )
344325, 343eqbrtrd 4414 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( Q `  ( i  +  1 ) )  <_  0 )
345344adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  <_  0 )
346321, 323, 322, 324, 345ltletrd 9775 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  0 )
347321, 322, 346ltnsymd 9765 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  0  <  s )
348347iffalsed 3895 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
349348oveq2d 6293 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  W ) )
350349mpteq2dva 4480 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  (
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 )
)  -  W ) ) )
351350oveq1d 6292 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) ) ) lim CC  ( Q `  i )
)  =  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  W ) ) lim CC  ( Q `
 i ) ) )
352317, 320, 3513eltr4d 2505 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) ) ) lim CC  ( Q `  i )
) )
3533523adantl3 1155 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  ( V `  i )  <  X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) ) ) lim CC  ( Q `  i )
) )
354 eqid 2402 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  Y )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  Y )
355 eqid 2402 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  Y ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  Y ) )
356259ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Y  e.  CC )
357259adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  CC )
358354, 313, 357, 288constlimc 36979 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  Y ) lim CC  ( Q `  i )
) )
359272, 354, 355, 256, 356, 311, 358sublimc 37007 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  -  Y )  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  Y
) ) lim CC  ( Q `  i )
) )
360359adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  ( R  -  Y )  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  Y ) ) lim CC  ( Q `  i ) ) )
361 iffalse 3893 . . . . . . . . . 10  |-  ( -.  ( V `  i
)  <  X  ->  if ( ( V `  i )  <  X ,  W ,  Y )  =  Y )
362361oveq2d 6293 . . . . . . . . 9  |-  ( -.  ( V `  i
)  <  X  ->  ( R  -  if ( ( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  Y ) )
363362adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  Y ) )
364 0red 9626 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i
)  <  X )  /\  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  0  e.  RR )
365299ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i
)  <  X )  /\  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
366215adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i
)  <  X )  /\  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  s  e.  RR )
3671ad2antrr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  X  e.  RR )
368278adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  ( V `  i )  e.  RR )
369 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  -.  ( V `  i )  <  X )
370367, 368, 369nltled 9766 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  X  <_  ( V `  i
) )
371368, 367subge0d 10181 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  (
0  <_  ( ( V `  i )  -  X )  <->  X  <_  ( V `  i ) ) )
372370, 371mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  0  <_  ( ( V `  i )  -  X
) )
373293eqcomd 2410 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `