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

Theorem fourierdlem75 37909
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 731 . . . 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 37835 . . . . . . . . . . 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 214 . . . . . . . . 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 461 . . . . . . . 8  |-  ( ph  ->  V  e.  ( RR 
^m  ( 0 ... M ) ) )
10 elmapi 7499 . . . . . . . 8  |-  ( V  e.  ( RR  ^m  ( 0 ... M
) )  ->  V : ( 0 ... M ) --> RR )
119, 10syl 17 . . . . . . 7  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
1211adantr 467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
13 fzofzp1 12009 . . . . . . 7  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
1413adantl 468 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
1512, 14ffvelrnd 6036 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
1615adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
17 eqcom 2432 . . . . . . 7  |-  ( ( V `  i )  =  X  <->  X  =  ( V `  i ) )
1817biimpi 198 . . . . . 6  |-  ( ( V `  i )  =  X  ->  X  =  ( V `  i ) )
1918adantl 468 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  =  ( V `  i ) )
208simprrd 766 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2120r19.21bi 2795 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2221adantr 467 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( V `  i )  <  ( V `  (
i  +  1 ) ) )
2319, 22eqbrtrd 4442 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  <  ( V `  (
i  +  1 ) ) )
24 fourierdlem75.f . . . . . . 7  |-  ( ph  ->  F : RR --> RR )
2524adantr 467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> RR )
26 ioossre 11698 . . . . . . 7  |-  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR
2726a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
2825, 27fssresd 5765 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) : ( X (,) ( V `  ( i  +  1 ) ) ) --> RR )
2928adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> RR )
30 limcresi 22832 . . . . . . . 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 3463 . . . . . . 7  |-  ( ph  ->  Y  e.  ( ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
3332adantr 467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( ( F  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
34 pnfxr 11414 . . . . . . . . . 10  |- +oo  e.  RR*
3534a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> +oo  e.  RR* )
3615rexrd 9692 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
3715ltpnfd 11425 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  < +oo )
3836, 35, 37xrltled 37370 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  <_ +oo )
39 iooss2 11674 . . . . . . . . 9  |-  ( ( +oo  e.  RR*  /\  ( V `  ( i  +  1 ) )  <_ +oo )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  ( X (,) +oo )
)
4035, 38, 39syl2anc 666 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  ( X (,) +oo ) )
4140resabs1d 5151 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
4241oveq1d 6318 . . . . . 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 2513 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim
CC  X ) )
4443adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  Y  e.  ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  X ) )
45 eqid 2423 . . . 4  |-  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )  =  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
46 ax-resscn 9598 . . . . . . . . . . 11  |-  RR  C_  CC
4746a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
4824, 47fssd 5753 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> CC )
49 ssid 3484 . . . . . . . . . . 11  |-  RR  C_  RR
5049a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  RR )
5126a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
52 eqid 2423 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5352tgioo2 21813 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
5452, 53dvres 22858 . . . . . . . . . 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 1266 . . . . . . . . 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 2436 . . . . . . . . . 10  |-  ( RR 
_D  F )  =  G
58 ioontr 37486 . . . . . . . . . 10  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( X (,) ( V `
 ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) )
5957, 58reseq12i 5120 . . . . . . . . 9  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) )
6055, 59syl6eq 2480 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6160adantr 467 . . . . . . 7  |-  ( (
ph  /\  ( V `  i )  =  X )  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6261dmeqd 5054 . . . . . 6  |-  ( (
ph  /\  ( V `  i )  =  X )  ->  dom  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )  =  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6362adantlr 720 . . . . 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 467 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC )
66 oveq1 6310 . . . . . . . . . . 11  |-  ( ( V `  i )  =  X  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
6766reseq2d 5122 . . . . . . . . . 10  |-  ( ( V `  i )  =  X  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6867feq1d 5730 . . . . . . . . 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 468 . . . . . . . 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 214 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
7166adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
7271feq2d 5731 . . . . . . 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 214 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> CC )
74 fdm 5748 . . . . . 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 2464 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
77 limcresi 22832 . . . . . . . 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 3463 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
8079adantr 467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( ( G  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
8140resabs1d 5151 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
8260adantr 467 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
8381, 82eqtr4d 2467 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) )
8483oveq1d 6318 . . . . . 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 2513 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) lim CC  X ) )
8685adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  E  e.  ( ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) lim CC  X ) )
87 eqid 2423 . . . 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 6311 . . . . . . 7  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
8988fveq2d 5883 . . . . . 6  |-  ( x  =  s  ->  (
( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `
 ( X  +  x ) )  =  ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) ) )
9089oveq1d 6318 . . . . 5  |-  ( x  =  s  ->  (
( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  x ) )  -  Y )  =  ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  -  Y ) )
9190cbvmptv 4514 . . . 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 23 . . . . 5  |-  ( x  =  s  ->  x  =  s )
9392cbvmptv 4514 . . . 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 37895 . . 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 3916 . . . . 5  |-  ( ( V `  i )  =  X  ->  if ( ( V `  i )  =  X ,  E ,  ( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `
 i ) ) )  =  E )
9795, 96syl5eq 2476 . . . 4  |-  ( ( V `  i )  =  X  ->  A  =  E )
9897adantl 468 . . 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 5118 . . . . . 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 11722 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
103 pire 23405 . . . . . . . . . . . 12  |-  pi  e.  RR
104103renegcli 9937 . . . . . . . . . . 11  |-  -u pi  e.  RR
105104rexri 9695 . . . . . . . . . 10  |-  -u pi  e.  RR*
106105a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
107103rexri 9695 . . . . . . . . . 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 9672 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
113103a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  pi  e.  RR )
114113, 1readdcld 9672 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
115112, 114iccssred 37477 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
116115adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
) [,] ( pi  +  X ) ) 
C_  RR )
1175, 4, 3fourierdlem15 37848 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
118117ffvelrnda 6035 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
119116, 118sseldd 3466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
1201adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
121119, 120resubcld 10049 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
122111recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u pi  e.  CC )
1231recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  CC )
124122, 123pncand 9989 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
125124eqcomd 2431 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  =  ( ( -u pi  +  X )  -  X
) )
126125adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  =  ( ( -u pi  +  X )  -  X ) )
127112adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  e.  RR )
128114adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
pi  +  X )  e.  RR )
129 elicc2 11701 . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  RR  /\  ( -u pi  +  X
)  <_  ( V `  i )  /\  ( V `  i )  <_  ( pi  +  X
) ) )
132131simp2d 1019 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  <_  ( V `  i ) )
133127, 119, 120, 132lesub1dd 10231 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  -  X )  <_  ( ( V `
 i )  -  X ) )
134126, 133eqbrtrd 4442 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  <_  ( ( V `  i )  -  X
) )
135131simp3d 1020 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  <_  ( pi  +  X
) )
136119, 128, 120, 135lesub1dd 10231 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  ( ( pi  +  X )  -  X ) )
137110recnd 9671 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  CC )
138123adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  CC )
139137, 138pncand 9989 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( pi  +  X
)  -  X )  =  pi )
140136, 139breqtrd 4446 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  pi )
141109, 110, 121, 134, 140eliccd 37476 . . . . . . . . . . 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 6059 . . . . . . . . . 10  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
144143adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
145 simpr 463 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
146106, 108, 144, 145fourierdlem8 37841 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
147102, 146syl5ss 3476 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
148147resmptd 5173 . . . . . 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 467 . . . . 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 11937 . . . . . . . 8  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
151 simpr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( 0 ... M
) )
152142fvmpt2 5971 . . . . . . . . . . 11  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  ( -u pi [,] pi ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
153151, 141, 152syl2anc 666 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
154153adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
155 oveq1 6310 . . . . . . . . . 10  |-  ( ( V `  i )  =  X  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
156155adantl 468 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
157123ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  X  e.  CC )
158157subidd 9976 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( X  -  X )  =  0 )
159154, 156, 1583eqtrd 2468 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  0 )
160150, 159sylanl2 656 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( Q `  i )  =  0 )
161 fveq2 5879 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
162161oveq1d 6318 . . . . . . . . . . . 12  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
163162cbvmptv 4514 . . . . . . . . . . 11  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
164142, 163eqtri 2452 . . . . . . . . . 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 5879 . . . . . . . . . . 11  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
167166oveq1d 6318 . . . . . . . . . 10  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
168167adantl 468 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
1691adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
17015, 169resubcld 10049 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
171165, 168, 14, 170fvmptd 5968 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
172171adantr 467 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
173160, 172oveq12d 6321 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) ) )
174 simplr 761 . . . . . . . . . 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 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  M  e.  NN )
177111, 113, 1, 5, 175, 4, 3, 142fourierdlem14 37847 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q  e.  ( O `
 M ) )
178177adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  Q  e.  ( O `  M
) )
179 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  s  =  0 )
180 fourierdlem75.x . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  X  e.  ran  V
)
181 ffn 5744 . . . . . . . . . . . . . . . . . . 19  |-  ( V : ( 0 ... M ) --> ( (
-u pi  +  X
) [,] ( pi  +  X ) )  ->  V  Fn  (
0 ... M ) )
182 fvelrnb 5926 . . . . . . . . . . . . . . . . . . 19  |-  ( V  Fn  ( 0 ... M )  ->  ( X  e.  ran  V  <->  E. i  e.  ( 0 ... M
) ( V `  i )  =  X ) )
183117, 181, 1823syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( X  e.  ran  V  <->  E. i  e.  (
0 ... M ) ( V `  i )  =  X ) )
184180, 183mpbid 214 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( V `  i
)  =  X )
185159ex 436 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  =  X  -> 
( Q `  i
)  =  0 ) )
186185reximdva 2901 . . . . . . . . . . . . . . . . 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 6059 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
189 ffn 5744 . . . . . . . . . . . . . . . . 17  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
190 fvelrnb 5926 . . . . . . . . . . . . . . . . 17  |-  ( Q  Fn  ( 0 ... M )  ->  (
0  e.  ran  Q  <->  E. i  e.  ( 0 ... M ) ( Q `  i )  =  0 ) )
191188, 189, 1903syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  e.  ran  Q  <->  E. i  e.  (
0 ... M ) ( Q `  i )  =  0 ) )
192187, 191mpbird 236 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  ran  Q
)
193192adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  0  e.  ran  Q )
194179, 193eqeltrd 2511 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  s  e.  ran  Q )
195175, 176, 178, 194fourierdlem12 37845 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  =  0 )  /\  i  e.  ( 0..^ M ) )  ->  -.  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
196195an32s 812 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
197196adantlr 720 . . . . . . . . . 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 579 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
199198adantlr 720 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  s  =  0
)
200199iffalsed 3921 . . . . . . 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 2431 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  0  =  ( Q `  i ) )
202201adantr 467 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  =  ( Q `
 i ) )
203 elioo3g 11667 . . . . . . . . . . . . . 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 198 . . . . . . . . . . . . 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 764 . . . . . . . . . . . 12  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  <  s )
206205adantl 468 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  s )
207202, 206eqbrtrd 4442 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  <  s )
208207iftrued 3918 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  Y )
209208oveq2d 6319 . . . . . . . 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 6318 . . . . . . 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 9692 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  RR* )
212211ad3antrrr 735 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR* )
21336ad2antrr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  (
i  +  1 ) )  e.  RR* )
214169ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR )
215 elioore 11668 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
216215adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
217214, 216readdcld 9672 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  RR )
218216, 207elrpd 11340 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR+ )
219214, 218ltaddrpd 11373 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  <  ( X  +  s ) )
220215adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
221188adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
222221, 14ffvelrnd 6036 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
223222adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2241ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
225204simprrd 766 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
226225adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
227220, 223, 224, 226ltadd2dd 9796 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
228171oveq2d 6319 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
229123adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
23015recnd 9671 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  CC )
231229, 230pncan3d 9991 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( V `  ( i  +  1 ) )  -  X
) )  =  ( V `  ( i  +  1 ) ) )
232228, 231eqtrd 2464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
233232adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
234227, 233breqtrd 4446 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
235234adantlr 720 . . . . . . . . . . . 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 37470 . . . . . . . . . . 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 5893 . . . . . . . . . . 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 2431 . . . . . . . . 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 6318 . . . . . . . 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 6318 . . . . . . 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 2468 . . . . . 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 4499 . . . . 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 2468 . . . 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 6321 . . 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 2526 . 2  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
247 eqid 2423 . . . . 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 2423 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  s )
249 eqid 2423 . . . . 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 467 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> RR )
2511adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
252215adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
253251, 252readdcld 9672 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
254250, 253ffvelrnd 6036 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
255254recnd 9671 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
256255adantlr 720 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
2572563adantl3 1164 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
258 limccl 22822 . . . . . . . . . 10  |-  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  C_  CC
259258, 31sseldi 3463 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
260 fourierdlem75.w . . . . . . . . . 10  |-  ( ph  ->  W  e.  RR )
261260recnd 9671 . . . . . . . . 9  |-  ( ph  ->  W  e.  CC )
262259, 261ifcld 3953 . . . . . . . 8  |-  ( ph  ->  if ( 0  < 
s ,  Y ,  W )  e.  CC )
263262adantr 467 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
2642633ad2antl1 1168 . . . . . 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 9988 . . . . 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 9671 . . . . . . 7  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  CC )
267266adantl 468 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  CC )
268 elsn 4011 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
269198, 268sylnibr 307 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
2702693adantl3 1164 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
271267, 270eldifd 3448 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
272 eqid 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
273 eqid 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  W )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  W )
274 eqid 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  W ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) )
275261ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  W  e.  CC )
276 ioossre 11698 . . . . . . . . . . . 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 477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
279278rexrd 9692 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR* )
280279adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
28136adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
282253adantlr 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
283 iccssre 11718 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
284104, 103, 283mp2an 677 . . . . . . . . . . . . . . . . . 18  |-  ( -u pi [,] pi )  C_  RR
285284, 46sstri 3474 . . . . . . . . . . . . . . . . 17  |-  ( -u pi [,] pi )  C_  CC
286153, 141eqeltrd 2511 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  ( -u pi [,] pi ) )
287150, 286sylan2 477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
288285, 287sseldi 3463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
289229, 288addcomd 9837 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  i ) )  =  ( ( Q `  i )  +  X ) )
290150adantl 468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
291150, 121sylan2 477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
292142fvmpt2 5971 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
293290, 291, 292syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
294293oveq1d 6318 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( ( ( V `  i )  -  X
)  +  X ) )
295278recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  CC )
296295, 229npcand 9992 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  i )  -  X )  +  X )  =  ( V `  i ) )
297289, 294, 2963eqtrrd 2469 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  =  ( X  +  ( Q `
 i ) ) )
298297adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
299293, 291eqeltrd 2511 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
300299adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
301205adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
302300, 220, 224, 301ltadd2dd 9796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
303298, 302eqbrtrd 4442 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
304280, 281, 282, 303, 234eliood 37470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
305 ioossre 11698 . . . . . . . . . . . 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 9772 . . . . . . . . . . 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 6319 . . . . . . . . . . . 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 2513 . . . . . . . . . . 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 37887 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  i )
) )
312 ioosscn 37466 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
313312a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
314261adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  CC )
315273, 313, 314, 288constlimc 37568 . . . . . . . . . 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 37597 . . . . . . . . 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 467 . . . . . . . 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 3916 . . . . . . . . . 10  |-  ( ( V `  i )  <  X  ->  if ( ( V `  i )  <  X ,  W ,  Y )  =  W )
319318oveq2d 6319 . . . . . . . . 9  |-  ( ( V `  i )  <  X  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
320319adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
321215adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
322 0red 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
323222ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
324225adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
325171adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
326279ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  i
)  e.  RR* )
32736ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  (
i  +  1 ) )  e.  RR* )
328169ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  RR )
329 simplr 761 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  i
)  <  X )
330 simpr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  -.  ( V `  (
i  +  1 ) )  <_  X )
3311ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  X  e.  RR )
33215adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  -> 
( V `  (
i  +  1 ) )  e.  RR )
333331, 332ltnled 9784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  -> 
( X  <  ( V `  ( i  +  1 ) )  <->  -.  ( V `  (
i  +  1 ) )  <_  X )
)
334330, 333mpbird 236 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  X  <  ( V `  ( i  +  1 ) ) )
335334adantlr 720 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  <  ( V `
 ( i  +  1 ) ) )
336326, 327, 328, 329, 335eliood 37470 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
3375, 4, 3, 180fourierdlem12 37845 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -.  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
338337ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  -.  X  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
339336, 338condan 802 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( V `  ( i  +  1 ) )  <_  X )
34015adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
3411ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  X  e.  RR )
342340, 341suble0d 10206 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  (
( ( V `  ( i  +  1 ) )  -  X
)  <_  0  <->  ( V `  ( i  +  1 ) )  <_  X
) )
343339, 342mpbird 236 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  (
( V `  (
i  +  1 ) )  -  X )  <_  0 )
344325, 343eqbrtrd 4442 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( Q `  ( i  +  1 ) )  <_  0 )
345344adantr 467 . . . . . . . . . . . . . 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 9797 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  0 )
347321, 322, 346ltnsymd 9786 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  0  <  s )
348347iffalsed 3921 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
349348oveq2d 6319 . . . . . . . . . 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 4508 . . . . . . . . 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 6318 . . . . . . . 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 2526 . . . . . . 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 1164 . . . . . 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 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  Y )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  Y )
355 eqid 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  Y ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  Y ) )
356259ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  Y  e.  CC )
357259adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  CC )
358354, 313, 357, 288constlimc 37568 . . . . . . . . . 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 37597 . . . . . . . . 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 467 . . . . . . . 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 3919 . . . . . . . . . 10  |-  ( -.  ( V `  i
)  <  X  ->  if ( ( V `  i )  <  X ,  W ,  Y )  =  Y )
362361oveq2d 6319 . . . . . . . . 9  |-  ( -.  ( V `  i
)  <  X  ->  ( R  -  if ( ( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  Y ) )
363362adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  Y ) )
364 0red 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i
)  <  X )  /\  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  0  e.  RR )
365299ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i
)  <  X )  /\  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
366215adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i
)  <  X )  /\  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  s  e.  RR )
3671ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  X  e.  RR )
368278adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  ( V `  i )  e.  RR )
369 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  -.  ( V `  i )  <  X )
370367, 368, 369nltled 9787 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  X  <_  ( V `  i
) )
371368, 367subge0d 10205 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  (
0  <_  ( ( V `  i )  -  X )  <->  X  <_  ( V `  i ) ) )
372370, 371mpbird 236 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  i )  <  X )  ->  0  <_  ( ( V `  i )  -  X
) )
373293eqcomd 2431 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )