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

Theorem fourierdlem75 31805
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 . . . . . 6  |-  ( ph  ->  X  e.  RR )
21adantr 465 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
32adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  e.  RR )
4 simpl 457 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ph )
5 fourierdlem75.v . . . . . . . . . 10  |-  ( ph  ->  V  e.  ( P `
 M ) )
6 fourierdlem75.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
7 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 ) ) ) } )
87fourierdlem2 31732 . . . . . . . . . . 11  |-  ( M  e.  NN  ->  ( V  e.  ( P `  M )  <->  ( V  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
96, 8syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( V  e.  ( P `  M )  <-> 
( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
105, 9mpbid 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 ) ) ) ) )
1110simpld 459 . . . . . . . 8  |-  ( ph  ->  V  e.  ( RR 
^m  ( 0 ... M ) ) )
12 elmapi 7452 . . . . . . . 8  |-  ( V  e.  ( RR  ^m  ( 0 ... M
) )  ->  V : ( 0 ... M ) --> RR )
1311, 12syl 16 . . . . . . 7  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
144, 13syl 16 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
15 fzofzp1 11889 . . . . . . 7  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
1615adantl 466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
1714, 16ffvelrnd 6033 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
1817adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
19 eqcom 2476 . . . . . . 7  |-  ( ( V `  i )  =  X  <->  X  =  ( V `  i ) )
2019biimpi 194 . . . . . 6  |-  ( ( V `  i )  =  X  ->  X  =  ( V `  i ) )
2120adantl 466 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  =  ( V `  i ) )
2210simprd 463 . . . . . . . 8  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
2322simprd 463 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2423r19.21bi 2836 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2524adantr 465 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( V `  i )  <  ( V `  (
i  +  1 ) ) )
2621, 25eqbrtrd 4473 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  X  <  ( V `  (
i  +  1 ) ) )
27 fourierdlem75.f . . . . . . 7  |-  ( ph  ->  F : RR --> RR )
284, 27syl 16 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> RR )
29 ioossre 11598 . . . . . . 7  |-  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR
3029a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
31 fssres 5757 . . . . . 6  |-  ( ( F : RR --> RR  /\  ( X (,) ( V `
 ( i  +  1 ) ) ) 
C_  RR )  -> 
( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `  ( i  +  1 ) ) ) --> RR )
3228, 30, 31syl2anc 661 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) : ( X (,) ( V `  ( i  +  1 ) ) ) --> RR )
3332adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> RR )
34 limcresi 22157 . . . . . . . 8  |-  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  C_  (
( ( F  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
)
35 fourierdlem75.y . . . . . . . 8  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
3634, 35sseldi 3507 . . . . . . 7  |-  ( ph  ->  Y  e.  ( ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
3736adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( ( F  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
38 pnfxr 11333 . . . . . . . . . 10  |- +oo  e.  RR*
3938a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> +oo  e.  RR* )
4017rexrd 9655 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
41 ltpnf 11343 . . . . . . . . . . 11  |-  ( ( V `  ( i  +  1 ) )  e.  RR  ->  ( V `  ( i  +  1 ) )  < +oo )
4217, 41syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  < +oo )
4340, 39, 42xrltled 31356 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  <_ +oo )
44 iooss2 11577 . . . . . . . . 9  |-  ( ( +oo  e.  RR*  /\  ( V `  ( i  +  1 ) )  <_ +oo )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  ( X (,) +oo )
)
4539, 43, 44syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  ( X (,) +oo ) )
46 resabs1 5308 . . . . . . . 8  |-  ( ( X (,) ( V `
 ( i  +  1 ) ) ) 
C_  ( X (,) +oo )  ->  ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
4745, 46syl 16 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
4847oveq1d 6310 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  X )  =  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
4937, 48eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim
CC  X ) )
5049adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  Y  e.  ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  X ) )
51 eqid 2467 . . . 4  |-  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )  =  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
52 ax-resscn 9561 . . . . . . . . . . 11  |-  RR  C_  CC
5352a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
54 fss 5745 . . . . . . . . . . 11  |-  ( ( F : RR --> RR  /\  RR  C_  CC )  ->  F : RR --> CC )
5527, 53, 54syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> CC )
56 ssid 3528 . . . . . . . . . . 11  |-  RR  C_  RR
5756a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  RR )
5829a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )
59 eqid 2467 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6059tgioo2 21176 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
6159, 60dvres 22183 . . . . . . . . . 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 ) ) ) ) ) )
6253, 55, 57, 58, 61syl22anc 1229 . . . . . . . . 9  |-  ( ph  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) ) )
63 fourierdlem75.g . . . . . . . . . . . 12  |-  G  =  ( RR  _D  F
)
6463eqcomi 2480 . . . . . . . . . . 11  |-  ( RR 
_D  F )  =  G
65 iooretop 21141 . . . . . . . . . . . 12  |-  ( X (,) ( V `  ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )
66 retop 21136 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Top
67 uniretop 21137 . . . . . . . . . . . . . 14  |-  RR  =  U. ( topGen `  ran  (,) )
6867isopn3 19435 . . . . . . . . . . . . 13  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( X (,) ( V `  ( i  +  1 ) ) )  C_  RR )  ->  ( ( X (,) ( V `
 ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
6966, 29, 68mp2an 672 . . . . . . . . . . . 12  |-  ( ( X (,) ( V `
 ( i  +  1 ) ) )  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
7065, 69mpbi 208 . . . . . . . . . . 11  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( X (,) ( V `
 ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) )
7164, 70reseq12i 5277 . . . . . . . . . 10  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) )
7271a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( X (,) ( V `  (
i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
7362, 72eqtrd 2508 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
7473adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( V `  i )  =  X )  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
7574dmeqd 5211 . . . . . 6  |-  ( (
ph  /\  ( V `  i )  =  X )  ->  dom  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )  =  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
7675adantlr 714 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  dom  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
77 fourierdlem75.gcn . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
7877adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC )
79 oveq1 6302 . . . . . . . . . . 11  |-  ( ( V `  i )  =  X  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
8079reseq2d 5279 . . . . . . . . . 10  |-  ( ( V `  i )  =  X  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
8180feq1d 5723 . . . . . . . . 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 ) )
8281adantl 466 . . . . . . . 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 ) )
8378, 82mpbid 210 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
8479adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
8584feq2d 5724 . . . . . . 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 ) )
8683, 85mpbid 210 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) : ( X (,) ( V `
 ( i  +  1 ) ) ) --> CC )
87 fdm 5741 . . . . . 6  |-  ( ( G  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) : ( X (,) ( V `  ( i  +  1 ) ) ) --> CC  ->  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
8886, 87syl 16 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
8976, 88eqtrd 2508 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( X (,) ( V `  ( i  +  1 ) ) ) )
90 limcresi 22157 . . . . . . . 8  |-  ( ( G  |`  ( X (,) +oo ) ) lim CC  X )  C_  (
( ( G  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
)
91 fourierdlem75.e . . . . . . . 8  |-  ( ph  ->  E  e.  ( ( G  |`  ( X (,) +oo ) ) lim CC  X ) )
9290, 91sseldi 3507 . . . . . . 7  |-  ( ph  ->  E  e.  ( ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
9392adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( ( G  |`  ( X (,) +oo )
)  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) lim CC  X
) )
94 resabs1 5308 . . . . . . . . 9  |-  ( ( X (,) ( V `
 ( i  +  1 ) ) ) 
C_  ( X (,) +oo )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
9545, 94syl 16 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) )
964, 73syl 16 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )  =  ( G  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) )
9796eqcomd 2475 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) )  =  ( RR 
_D  ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) ) )
9895, 97eqtrd 2508 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( X (,) +oo ) )  |`  ( X (,) ( V `  ( i  +  1 ) ) ) )  =  ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) )
9998oveq1d 6310 . . . . . 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
) )
10093, 99eleqtrd 2557 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) lim CC  X ) )
101100adantr 465 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  E  e.  ( ( RR  _D  ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) ) lim CC  X ) )
102 eqid 2467 . . . 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 ) )
103 oveq2 6303 . . . . . . 7  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
104103fveq2d 5876 . . . . . 6  |-  ( x  =  s  ->  (
( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `
 ( X  +  x ) )  =  ( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) ) )
105104oveq1d 6310 . . . . 5  |-  ( x  =  s  ->  (
( ( F  |`  ( X (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  x ) )  -  Y )  =  ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  -  Y ) )
106105cbvmptv 4544 . . . 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 ) )
107 id 22 . . . . 5  |-  ( x  =  s  ->  x  =  s )
108107cbvmptv 4544 . . . 4  |-  ( x  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) )  |->  x )  =  ( s  e.  ( 0 (,) (
( V `  (
i  +  1 ) )  -  X ) )  |->  s )
1093, 18, 26, 33, 50, 51, 89, 101, 102, 106, 108fourierdlem61 31791 . . 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 ) )
110 fourierdlem75.a . . . . . 6  |-  A  =  if ( ( V `
 i )  =  X ,  E , 
( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `
 i ) ) )
111 iftrue 3951 . . . . . 6  |-  ( ( V `  i )  =  X  ->  if ( ( V `  i )  =  X ,  E ,  ( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  /  ( Q `
 i ) ) )  =  E )
112110, 111syl5eq 2520 . . . . 5  |-  ( ( V `  i )  =  X  ->  A  =  E )
113112adantl 466 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  A  =  E )
114 fourierdlem75.h . . . . . . . 8  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
115114reseq1i 5275 . . . . . . 7  |-  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
116115a1i 11 . . . . . 6  |-  ( ( ( 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 ) ) ) ) )
117 ioossicc 11622 . . . . . . . . . 10  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
118117a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  (
( Q `  i
) [,] ( Q `
 ( i  +  1 ) ) ) )
119 pire 22718 . . . . . . . . . . . . 13  |-  pi  e.  RR
120119renegcli 9892 . . . . . . . . . . . 12  |-  -u pi  e.  RR
121120rexri 9658 . . . . . . . . . . 11  |-  -u pi  e.  RR*
122121a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
123119rexri 9658 . . . . . . . . . . 11  |-  pi  e.  RR*
124123a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
125120a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  e.  RR )
126119a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  RR )
127120a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
-u pi  e.  RR )
128127, 1jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u pi  e.  RR  /\  X  e.  RR ) )
129 readdcl 9587 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u pi  e.  RR  /\  X  e.  RR )  ->  ( -u pi  +  X )  e.  RR )
130128, 129syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
131119a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  pi  e.  RR )
132131, 1jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( pi  e.  RR  /\  X  e.  RR ) )
133 readdcl 9587 . . . . . . . . . . . . . . . . . 18  |-  ( ( pi  e.  RR  /\  X  e.  RR )  ->  ( pi  +  X
)  e.  RR )
134132, 133syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
135130, 134iccssred 31426 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
136135adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
) [,] ( pi  +  X ) ) 
C_  RR )
1377, 6, 5fourierdlem15 31745 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
138137ffvelrnda 6032 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
139136, 138sseldd 3510 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
1401adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
141139, 140resubcld 9999 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
142127recnd 9634 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u pi  e.  CC )
1431recnd 9634 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  CC )
144142, 143pncand 9943 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
145144eqcomd 2475 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u pi  =  ( ( -u pi  +  X )  -  X
) )
146145adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  =  ( ( -u pi  +  X )  -  X ) )
147130adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  e.  RR )
148134adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
pi  +  X )  e.  RR )
149 elicc2 11601 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -u pi  +  X )  e.  RR  /\  ( pi  +  X
)  e.  RR )  ->  ( ( V `
 i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  <->  ( ( V `
 i )  e.  RR  /\  ( -u pi  +  X )  <_ 
( V `  i
)  /\  ( V `  i )  <_  (
pi  +  X ) ) ) )
150147, 148, 149syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  <-> 
( ( V `  i )  e.  RR  /\  ( -u pi  +  X )  <_  ( V `  i )  /\  ( V `  i
)  <_  ( pi  +  X ) ) ) )
151138, 150mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  RR  /\  ( -u pi  +  X
)  <_  ( V `  i )  /\  ( V `  i )  <_  ( pi  +  X
) ) )
152151simp2d 1009 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  <_  ( V `  i ) )
153147, 139, 140lesub1d 10171 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  <_  ( V `  i )  <->  ( ( -u pi  +  X )  -  X )  <_ 
( ( V `  i )  -  X
) ) )
154152, 153mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  -  X )  <_  ( ( V `
 i )  -  X ) )
155146, 154eqbrtrd 4473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  <_  ( ( V `  i )  -  X
) )
156151simp3d 1010 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  <_  ( pi  +  X
) )
157139, 148, 140lesub1d 10171 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  <_  ( pi  +  X )  <->  ( ( V `  i )  -  X )  <_  (
( pi  +  X
)  -  X ) ) )
158156, 157mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  ( ( pi  +  X )  -  X ) )
159126recnd 9634 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  CC )
160143adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  CC )
161159, 160pncand 9943 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( pi  +  X
)  -  X )  =  pi )
162158, 161breqtrd 4477 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  pi )
163125, 126, 141, 155, 162eliccd 31425 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  ( -u pi [,] pi ) )
164 fourierdlem75.q . . . . . . . . . . . 12  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
165163, 164fmptd 6056 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
166165adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
167 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
168122, 124, 166, 167fourierdlem8 31738 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
169118, 168sstrd 3519 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
170 resmpt 5329 . . . . . . . 8  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  ->  (
( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) ) )
171169, 170syl 16 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) ) )
172171adantr 465 . . . . . 6  |-  ( ( ( 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 ) ) ) )
173 elfzofz 11823 . . . . . . . . 9  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
174 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( 0 ... M
) )
175164fvmpt2 5964 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  ( -u pi [,] pi ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
176174, 163, 175syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
177176adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
178 oveq1 6302 . . . . . . . . . . 11  |-  ( ( V `  i )  =  X  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
179178adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
180143ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  X  e.  CC )
181180subidd 9930 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( X  -  X )  =  0 )
182177, 179, 1813eqtrd 2512 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  0 )
183173, 182sylanl2 651 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( Q `  i )  =  0 )
184 fveq2 5872 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
185184oveq1d 6310 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
186185cbvmptv 4544 . . . . . . . . . . . 12  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
187164, 186eqtri 2496 . . . . . . . . . . 11  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
188187a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
189 fveq2 5872 . . . . . . . . . . . 12  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
190189oveq1d 6310 . . . . . . . . . . 11  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
191190adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
19217, 2resubcld 9999 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
193188, 191, 16, 192fvmptd 5962 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
194193adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
195183, 194oveq12d 6313 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X
) ) )
196 id 22 . . . . . . . . . . . 12  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
197196ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
1984anim1i 568 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  ( ph  /\  s  =  0 ) )
199 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  i  e.  ( 0..^ M ) )
200 fourierdlem75.o . . . . . . . . . . . . . 14  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
2016adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  M  e.  NN )
202127, 131, 1, 7, 200, 6, 5, 164fourierdlem14 31744 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( O `
 M ) )
203202adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  Q  e.  ( O `  M
) )
204 simpr 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  = 
0 )  ->  s  =  0 )
205 fourierdlem75.x . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  e.  ran  V
)
206 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V : ( 0 ... M ) --> ( (
-u pi  +  X
) [,] ( pi  +  X ) )  ->  V  Fn  (
0 ... M ) )
207137, 206syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  V  Fn  ( 0 ... M ) )
208 fvelrnb 5921 . . . . . . . . . . . . . . . . . . . 20  |-  ( V  Fn  ( 0 ... M )  ->  ( X  e.  ran  V  <->  E. i  e.  ( 0 ... M
) ( V `  i )  =  X ) )
209207, 208syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( X  e.  ran  V  <->  E. i  e.  (
0 ... M ) ( V `  i )  =  X ) )
210205, 209mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( V `  i
)  =  X )
211182ex 434 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  =  X  -> 
( Q `  i
)  =  0 ) )
212211reximdva 2942 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E. i  e.  ( 0 ... M
) ( V `  i )  =  X  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 ) )
213210, 212mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 )
214141, 164fmptd 6056 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
215 ffn 5737 . . . . . . . . . . . . . . . . . . 19  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
216214, 215syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
217 fvelrnb 5921 . . . . . . . . . . . . . . . . . 18  |-  ( Q  Fn  ( 0 ... M )  ->  (
0  e.  ran  Q  <->  E. i  e.  ( 0 ... M ) ( Q `  i )  =  0 ) )
218216, 217syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 0  e.  ran  Q  <->  E. i  e.  (
0 ... M ) ( Q `  i )  =  0 ) )
219213, 218mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  ran  Q
)
220219adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  = 
0 )  ->  0  e.  ran  Q )
221204, 220eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  s  e.  ran  Q )
222200, 201, 203, 221fourierdlem12 31742 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  =  0 )  /\  i  e.  ( 0..^ M ) )  ->  -.  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
223198, 199, 222syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
224223adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
225197, 224pm2.65da 576 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
226225adantlr 714 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  s  =  0
)
227 iffalse 3954 . . . . . . . . 9  |-  ( -.  s  =  0  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
228226, 227syl 16 . . . . . . . 8  |-  ( ( ( ( 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 ) )
229183eqcomd 2475 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  0  =  ( Q `  i ) )
230229adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  =  ( Q `
 i ) )
231 elioo3g 11570 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) ) )
232231biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) )
233232simpld 459 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  RR* ) )
234233simp1d 1008 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  e.  RR* )
235233simp2d 1009 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
236 elioo2 11582 . . . . . . . . . . . . . . . 16  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR* )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( s  e.  RR  /\  ( Q `
 i )  < 
s  /\  s  <  ( Q `  ( i  +  1 ) ) ) ) )
237234, 235, 236syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  <->  ( s  e.  RR  /\  ( Q `
 i )  < 
s  /\  s  <  ( Q `  ( i  +  1 ) ) ) ) )
238196, 237mpbid 210 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
s  e.  RR  /\  ( Q `  i )  <  s  /\  s  <  ( Q `  (
i  +  1 ) ) ) )
239238simp2d 1009 . . . . . . . . . . . . 13  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  <  s )
240239adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  s )
241230, 240eqbrtrd 4473 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  <  s )
242 iftrue 3951 . . . . . . . . . . 11  |-  ( 0  <  s  ->  if ( 0  <  s ,  Y ,  W )  =  Y )
243241, 242syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  Y )
244243oveq2d 6311 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
245244oveq1d 6310 . . . . . . . 8  |-  ( ( ( ( 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 ) )
2461rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  RR* )
247246ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR* )
24840adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
249248adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  (
i  +  1 ) )  e.  RR* )
2503adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR )
251 elioore 11571 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
252251adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
253250, 252readdcld 9635 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  RR )
254252, 241elrpd 11266 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR+ )
255250, 254ltaddrpd 11297 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  <  ( X  +  s ) )
256251adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
257214adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
258257, 16ffvelrnd 6033 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
259258adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
2601adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
2614, 260sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
262238simp3d 1010 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
263262adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
264256, 259, 261, 263ltadd2dd 9752 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
265193oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
266143adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
26752, 17sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  CC )
268266, 267pncan3d 9945 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( V `  ( i  +  1 ) )  -  X
) )  =  ( V `  ( i  +  1 ) ) )
269 eqidd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  =  ( V `  ( i  +  1 ) ) )
270265, 268, 2693eqtrd 2512 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
271270adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
272264, 271breqtrd 4477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
273272adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  <  ( V `
 ( i  +  1 ) ) )
274247, 249, 253, 255, 273eliood 31418 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  ( X (,) ( V `  ( i  +  1 ) ) ) )
275 fvres 5886 . . . . . . . . . . . 12  |-  ( ( X  +  s )  e.  ( X (,) ( V `  ( i  +  1 ) ) )  ->  ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  =  ( F `
 ( X  +  s ) ) )
276274, 275syl 16 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) )
277276eqcomd 2475 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) )
278277oveq1d 6310 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
279278oveq1d 6310 . . . . . . . 8  |-  ( ( ( ( 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 ) )
280228, 245, 2793eqtrd 2512 . . . . . . 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 (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  -  Y )  / 
s ) )
281195, 280mpteq12dva 4530 . . . . . 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 ) ) )  =  ( s  e.  ( 0 (,) ( ( V `
 ( i  +  1 ) )  -  X ) )  |->  ( ( ( ( F  |`  ( X (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
)  -  Y )  /  s ) ) )
282116, 172, 2813eqtrd 2512 . . . . 5  |-  ( ( ( 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 ) ) )
283282, 183oveq12d 6313 . . . 4  |-  ( ( ( 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 ) )
284113, 283eleq12d 2549 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  ( A  e.  ( ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) )  <->  E  e.  (
( s  e.  ( 0 (,) ( ( V `  ( i  +  1 ) )  -  X ) ) 
|->  ( ( ( ( F  |`  ( X (,) ( V `  (
i  +  1 ) ) ) ) `  ( X  +  s
) )  -  Y
)  /  s ) ) lim CC  0 ) ) )
285109, 284mpbird 232 . 2  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  =  X )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
286 eqid 2467 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) ) )
287 eqid 2467 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  s )
288 eqid 2467 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
28927adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> RR )
290251adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
291260, 290readdcld 9635 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
292289, 291ffvelrnd 6033 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
29352, 292sseldi 3507 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
294293adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
2952943adantl3 1154 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
296 limccl 22147 . . . . . . . . . . 11  |-  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  C_  CC
297296sseli 3505 . . . . . . . . . 10  |-  ( Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X )  ->  Y  e.  CC )
29835, 297syl 16 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
299 fourierdlem75.w . . . . . . . . . 10  |-  ( ph  ->  W  e.  RR )
30052, 299sseldi 3507 . . . . . . . . 9  |-  ( ph  ->  W  e.  CC )
301298, 300ifcld 3988 . . . . . . . 8  |-  ( ph  ->  if ( 0  < 
s ,  Y ,  W )  e.  CC )
302301adantr 465 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
3033023ad2antl1 1158 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
304295, 303subcld 9942 . . . . 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 )
305251recnd 9634 . . . . . . 7  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  CC )
306305adantl 466 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  CC )
307225neqned 2670 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  0 )
308307neneqd 2669 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
309 elsn 4047 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
310308, 309sylnibr 305 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
3113103adantl3 1154 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
312306, 311eldifd 3492 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 i )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
313 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
314 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  W )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  W )
315 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  W ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) )
316300ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  W  e.  CC )
317 ioossre 11598 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
318317a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
319173adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
320319, 139syldan 470 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
321320rexrd 9655 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR* )
322321adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
323291adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
324 iccssre 11618 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
325120, 119, 324mp2an 672 . . . . . . . . . . . . . . . . . . 19  |-  ( -u pi [,] pi )  C_  RR
326325, 52sstri 3518 . . . . . . . . . . . . . . . . . 18  |-  ( -u pi [,] pi )  C_  CC
327326a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( -u pi [,] pi )  C_  CC )
328176, 163eqeltrd 2555 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  ( -u pi [,] pi ) )
3294, 319, 328syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
330327, 329sseldd 3510 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
331266, 330addcomd 9793 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  i ) )  =  ( ( Q `  i )  +  X ) )
332319, 141syldan 470 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
333164fvmpt2 5964 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
334319, 332, 333syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
335334oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( ( ( V `  i )  -  X
)  +  X ) )
33652, 320sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  CC )
337336, 266npcand 9946 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  i )  -  X )  +  X )  =  ( V `  i ) )
338331, 335, 3373eqtrrd 2513 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  =  ( X  +  ( Q `
 i ) ) )
339338adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
340334, 332eqeltrd 2555 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
341340adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
342239adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
343341, 256, 261, 342ltadd2dd 9752 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
344339, 343eqbrtrd 4473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
345322, 248, 323, 344, 272eliood 31418 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
346 ioossre 11598 . . . . . . . . . . . 12  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
347346a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  RR )
348341, 342gtned 9731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  i
) )
349 fourierdlem75.r . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
350338oveq2d 6311 . . . . . . . . . . . 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 )
) ) )
351349, 350eleqtrd 2557 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  i ) ) ) )
35228, 2, 318, 313, 345, 347, 348, 351, 330fourierdlem53 31783 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  i )
) )
353 ioosscn 31414 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
354353a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
3554, 300syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  CC )
356314, 354, 355, 330constlimc 31489 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  W ) lim CC  ( Q `  i )
) )
357313, 314, 315, 294, 316, 352, 356sublimc 31517 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  -  W )  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  W
) ) lim CC  ( Q `  i )
) )
358357adantr 465 . . . . . . . 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 ) ) )
359 iftrue 3951 . . . . . . . . . . 11  |-  ( ( V `  i )  <  X  ->  if ( ( V `  i )  <  X ,  W ,  Y )  =  W )
360359oveq2d 6311 . . . . . . . . . 10  |-  ( ( V `  i )  <  X  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
361360adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
362251adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
363 0re 9608 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
364363a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
365259adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
366262adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
367193adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
368321ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  i
)  e.  RR* )
36940ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  (
i  +  1 ) )  e.  RR* )
3702adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
X )  ->  X  e.  RR )
371370adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  RR )
372 simplr 754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  ( V `  i
)  <  X )
373 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  -.  ( V `  (
i  +  1 ) )  <_  X )
3742adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  X  e.  RR )
37517adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  -> 
( V `  (
i  +  1 ) )  e.  RR )
376374, 375ltnled 9743 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  -> 
( X  <  ( V `  ( i  +  1 ) )  <->  -.  ( V `  (
i  +  1 ) )  <_  X )
)
377373, 376mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <_  X )  ->  X  <  ( V `  ( i  +  1 ) ) )
378377adantlr 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  <  ( V `
 ( i  +  1 ) ) )
379368, 369, 371, 372, 378eliood 31418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  i )  <  X )  /\  -.  ( V `  (
i  +  1 ) )  <_  X )  ->  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
3807, 6, 5, 205fourierdlem12 31742 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -.  X  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
381380