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

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

Proof of Theorem fourierdlem74
Dummy variables  x  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzofz 11937 . . . . . 6  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
2 pire 23405 . . . . . . . . . . . 12  |-  pi  e.  RR
32renegcli 9937 . . . . . . . . . . 11  |-  -u pi  e.  RR
43a1i 11 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  e.  RR )
5 fourierdlem74.xre . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
64, 5readdcld 9672 . . . . . . . . 9  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
72a1i 11 . . . . . . . . . 10  |-  ( ph  ->  pi  e.  RR )
87, 5readdcld 9672 . . . . . . . . 9  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
96, 8iccssred 37477 . . . . . . . 8  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
109adantr 467 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
) [,] ( pi  +  X ) ) 
C_  RR )
11 fourierdlem74.p . . . . . . . . 9  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
12 fourierdlem74.m . . . . . . . . 9  |-  ( ph  ->  M  e.  NN )
13 fourierdlem74.v . . . . . . . . 9  |-  ( ph  ->  V  e.  ( P `
 M ) )
1411, 12, 13fourierdlem15 37848 . . . . . . . 8  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
1514ffvelrnda 6035 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
1610, 15sseldd 3466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
171, 16sylan2 477 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
1817adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( V `  i )  e.  RR )
195ad2antrr 731 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  X  e.  RR )
2011fourierdlem2 37835 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
2112, 20syl 17 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
2213, 21mpbid 214 . . . . . . . 8  |-  ( 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 ) ) ) ) )
2322simprrd 766 . . . . . . 7  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2423r19.21bi 2795 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
2524adantr 467 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( V `  i )  <  ( V `  (
i  +  1 ) ) )
26 eqcom 2432 . . . . . . 7  |-  ( ( V `  ( i  +  1 ) )  =  X  <->  X  =  ( V `  ( i  +  1 ) ) )
2726biimpi 198 . . . . . 6  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  X  =  ( V `  ( i  +  1 ) ) )
2827adantl 468 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  X  =  ( V `  ( i  +  1 ) ) )
2925, 28breqtrrd 4448 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( V `  i )  <  X )
30 fourierdlem74.f . . . . . 6  |-  ( ph  ->  F : RR --> RR )
31 ioossre 11698 . . . . . . 7  |-  ( ( V `  i ) (,) X )  C_  RR
3231a1i 11 . . . . . 6  |-  ( ph  ->  ( ( V `  i ) (,) X
)  C_  RR )
3330, 32fssresd 5765 . . . . 5  |-  ( ph  ->  ( F  |`  (
( V `  i
) (,) X ) ) : ( ( V `  i ) (,) X ) --> RR )
3433ad2antrr 731 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( F  |`  ( ( V `
 i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR )
35 limcresi 22832 . . . . . . . 8  |-  ( ( F  |`  ( -oo (,) X ) ) lim CC  X )  C_  (
( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X ) ) lim CC  X )
36 fourierdlem74.w . . . . . . . 8  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
3735, 36sseldi 3463 . . . . . . 7  |-  ( ph  ->  W  e.  ( ( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
) )
3837adantr 467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X ) ) lim CC  X ) )
39 mnfxr 11416 . . . . . . . . . 10  |- -oo  e.  RR*
4039a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  e.  RR* )
4117rexrd 9692 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR* )
4217mnfltd 11428 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <  ( V `
 i ) )
4340, 41, 42xrltled 37370 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  -> -oo  <_  ( V `
 i ) )
44 iooss1 11673 . . . . . . . . 9  |-  ( ( -oo  e.  RR*  /\ -oo  <_  ( V `  i
) )  ->  (
( V `  i
) (,) X ) 
C_  ( -oo (,) X ) )
4540, 43, 44syl2anc 666 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i ) (,) X )  C_  ( -oo (,) X ) )
4645resabs1d 5151 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -oo (,) X
) )  |`  (
( V `  i
) (,) X ) )  =  ( F  |`  ( ( V `  i ) (,) X
) ) )
4746oveq1d 6318 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( F  |`  ( ( V `  i ) (,) X ) ) lim CC  X ) )
4838, 47eleqtrd 2513 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( F  |`  (
( V `  i
) (,) X ) ) lim CC  X ) )
4948adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  W  e.  ( ( F  |`  ( ( V `  i ) (,) X
) ) lim CC  X
) )
50 eqid 2423 . . . 4  |-  ( RR 
_D  ( F  |`  ( ( V `  i ) (,) X
) ) )  =  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )
51 ax-resscn 9598 . . . . . . . . . 10  |-  RR  C_  CC
5251a1i 11 . . . . . . . . 9  |-  ( ph  ->  RR  C_  CC )
5330, 52fssd 5753 . . . . . . . . 9  |-  ( ph  ->  F : RR --> CC )
54 ssid 3484 . . . . . . . . . 10  |-  RR  C_  RR
5554a1i 11 . . . . . . . . 9  |-  ( ph  ->  RR  C_  RR )
56 eqid 2423 . . . . . . . . . 10  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5756tgioo2 21813 . . . . . . . . . 10  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
5856, 57dvres 22858 . . . . . . . . 9  |-  ( ( ( RR  C_  CC  /\  F : RR --> CC )  /\  ( RR  C_  RR  /\  ( ( V `
 i ) (,) X )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( ( V `  i ) (,) X
) ) )  =  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) ) )
5952, 53, 55, 32, 58syl22anc 1266 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) ) )
60 fourierdlem74.g . . . . . . . . . . 11  |-  G  =  ( RR  _D  F
)
6160eqcomi 2436 . . . . . . . . . 10  |-  ( RR 
_D  F )  =  G
62 ioontr 37486 . . . . . . . . . 10  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( V `  i ) (,) X
) )  =  ( ( V `  i
) (,) X )
6361, 62reseq12i 5120 . . . . . . . . 9  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) )  =  ( G  |`  ( ( V `  i ) (,) X
) )
6463a1i 11 . . . . . . . 8  |-  ( ph  ->  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( V `  i ) (,) X ) ) )  =  ( G  |`  ( ( V `  i ) (,) X
) ) )
6559, 64eqtrd 2464 . . . . . . 7  |-  ( ph  ->  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  ( G  |`  ( ( V `  i ) (,) X
) ) )
6665dmeqd 5054 . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  ( F  |`  ( ( V `  i ) (,) X ) ) )  =  dom  ( G  |`  ( ( V `
 i ) (,) X ) ) )
6766ad2antrr 731 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  dom  ( G  |`  ( ( V `  i ) (,) X
) ) )
68 fourierdlem74.gcn . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
6968adantr 467 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR )
70 oveq2 6311 . . . . . . . . . 10  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  =  ( ( V `
 i ) (,) X ) )
7170reseq2d 5122 . . . . . . . . 9  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  ( G  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  =  ( G  |`  (
( V `  i
) (,) X ) ) )
7271, 70feq12d 5733 . . . . . . . 8  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  (
( G  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  <->  ( G  |`  ( ( V `  i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR ) )
7372adantl 468 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( G  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  <->  ( G  |`  ( ( V `  i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR ) )
7469, 73mpbid 214 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( G  |`  ( ( V `
 i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR )
75 fdm 5748 . . . . . 6  |-  ( ( G  |`  ( ( V `  i ) (,) X ) ) : ( ( V `  i ) (,) X
) --> RR  ->  dom  ( G  |`  ( ( V `  i ) (,) X ) )  =  ( ( V `
 i ) (,) X ) )
7674, 75syl 17 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  dom  ( G  |`  ( ( V `  i ) (,) X ) )  =  ( ( V `
 i ) (,) X ) )
7767, 76eqtrd 2464 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  dom  ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) )  =  ( ( V `
 i ) (,) X ) )
78 limcresi 22832 . . . . . . . 8  |-  ( ( G  |`  ( -oo (,) X ) ) lim CC  X )  C_  (
( ( G  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X ) ) lim CC  X )
7945resabs1d 5151 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( -oo (,) X
) )  |`  (
( V `  i
) (,) X ) )  =  ( G  |`  ( ( V `  i ) (,) X
) ) )
8079oveq1d 6318 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( G  |`  ( -oo (,) X ) )  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( G  |`  ( ( V `  i ) (,) X ) ) lim CC  X ) )
8178, 80syl5sseq 3513 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( -oo (,) X
) ) lim CC  X
)  C_  ( ( G  |`  ( ( V `
 i ) (,) X ) ) lim CC  X ) )
82 fourierdlem74.e . . . . . . . 8  |-  ( ph  ->  E  e.  ( ( G  |`  ( -oo (,) X ) ) lim CC  X ) )
8382adantr 467 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( G  |`  ( -oo (,) X ) ) lim
CC  X ) )
8481, 83sseldd 3466 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( G  |`  (
( V `  i
) (,) X ) ) lim CC  X ) )
8559, 64eqtr2d 2465 . . . . . . . 8  |-  ( ph  ->  ( G  |`  (
( V `  i
) (,) X ) )  =  ( RR 
_D  ( F  |`  ( ( V `  i ) (,) X
) ) ) )
8685oveq1d 6318 . . . . . . 7  |-  ( ph  ->  ( ( G  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( RR  _D  ( F  |`  ( ( V `  i ) (,) X
) ) ) lim CC  X ) )
8786adantr 467 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( G  |`  ( ( V `  i ) (,) X
) ) lim CC  X
)  =  ( ( RR  _D  ( F  |`  ( ( V `  i ) (,) X
) ) ) lim CC  X ) )
8884, 87eleqtrd 2513 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E  e.  ( ( RR  _D  ( F  |`  ( ( V `
 i ) (,) X ) ) ) lim
CC  X ) )
8988adantr 467 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  E  e.  ( ( RR  _D  ( F  |`  ( ( V `  i ) (,) X ) ) ) lim CC  X ) )
90 eqid 2423 . . . 4  |-  ( s  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) )  =  ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  ( ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  -  W )  / 
s ) )
91 oveq2 6311 . . . . . . 7  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
9291fveq2d 5883 . . . . . 6  |-  ( x  =  s  ->  (
( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  x ) )  =  ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
) )
9392oveq1d 6318 . . . . 5  |-  ( x  =  s  ->  (
( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  x )
)  -  W )  =  ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
) )
9493cbvmptv 4514 . . . 4  |-  ( x  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  x ) )  -  W ) )  =  ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
) )
95 id 23 . . . . 5  |-  ( x  =  s  ->  x  =  s )
9695cbvmptv 4514 . . . 4  |-  ( x  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  x )  =  ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  s )
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 37894 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  E  e.  ( ( s  e.  ( ( ( V `
 i )  -  X ) (,) 0
)  |->  ( ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  -  W )  / 
s ) ) lim CC  0 ) )
98 fourierdlem74.a . . . . 5  |-  A  =  if ( ( V `
 ( i  +  1 ) )  =  X ,  E , 
( ( R  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  /  ( Q `
 ( i  +  1 ) ) ) )
99 iftrue 3916 . . . . 5  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  if ( ( V `  ( i  +  1 ) )  =  X ,  E ,  ( ( R  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  /  ( Q `
 ( i  +  1 ) ) ) )  =  E )
10098, 99syl5eq 2476 . . . 4  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  A  =  E )
101100adantl 468 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  A  =  E )
102 fourierdlem74.h . . . . . . 7  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
103102reseq1i 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 ) ) ) )
104103a1i 11 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
105 ioossicc 11722 . . . . . . . 8  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
1063rexri 9695 . . . . . . . . . 10  |-  -u pi  e.  RR*
107106a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
1082rexri 9695 . . . . . . . . . 10  |-  pi  e.  RR*
109108a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
1103a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  e.  RR )
1112a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  RR )
1125adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
11316, 112resubcld 10049 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
1144recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u pi  e.  CC )
1155recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  CC )
116114, 115pncand 9989 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
117116eqcomd 2431 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  =  ( ( -u pi  +  X )  -  X
) )
118117adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  =  ( ( -u pi  +  X )  -  X ) )
1196adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  e.  RR )
1208adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
pi  +  X )  e.  RR )
121 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 ) ) ) )
122119, 120, 121syl2anc 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 ) ) ) )
12315, 122mpbid 214 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  e.  RR  /\  ( -u pi  +  X
)  <_  ( V `  i )  /\  ( V `  i )  <_  ( pi  +  X
) ) )
124123simp2d 1019 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( -u pi  +  X )  <_  ( V `  i ) )
125119, 16, 112, 124lesub1dd 10231 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( -u pi  +  X
)  -  X )  <_  ( ( V `
 i )  -  X ) )
126118, 125eqbrtrd 4442 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  -u pi  <_  ( ( V `  i )  -  X
) )
127123simp3d 1020 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  <_  ( pi  +  X
) )
12816, 120, 112, 127lesub1dd 10231 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  ( ( pi  +  X )  -  X ) )
129111recnd 9671 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  pi  e.  CC )
130115adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  CC )
131129, 130pncand 9989 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( pi  +  X
)  -  X )  =  pi )
132128, 131breqtrd 4446 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  <_  pi )
133110, 111, 113, 126, 132eliccd 37476 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  ( -u pi [,] pi ) )
134 fourierdlem74.q . . . . . . . . . . 11  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
135133, 134fmptd 6059 . . . . . . . . . 10  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
136135adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
137 simpr 463 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
138107, 109, 136, 137fourierdlem8 37841 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
139105, 138syl5ss 3476 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
140139resmptd 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 ) ) ) )
141140adantr 467 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) ) )
1421adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
1431, 113sylan2 477 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
144134fvmpt2 5971 . . . . . . . . 9  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
145142, 143, 144syl2anc 666 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
146145adantr 467 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
147 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
148147oveq1d 6318 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
149148cbvmptv 4514 . . . . . . . . . . . 12  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
150134, 149eqtri 2452 . . . . . . . . . . 11  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
151150a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
152 fveq2 5879 . . . . . . . . . . . 12  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
153152oveq1d 6318 . . . . . . . . . . 11  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
154153adantl 468 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
155 fzofzp1 12009 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
156155adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
15722simpld 461 . . . . . . . . . . . . . 14  |-  ( ph  ->  V  e.  ( RR 
^m  ( 0 ... M ) ) )
158 elmapi 7499 . . . . . . . . . . . . . 14  |-  ( V  e.  ( RR  ^m  ( 0 ... M
) )  ->  V : ( 0 ... M ) --> RR )
159157, 158syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
160159adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
161160, 156ffvelrnd 6036 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
1625adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
163161, 162resubcld 10049 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
164151, 154, 156, 163fvmptd 5968 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
165164adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
166 oveq1 6310 . . . . . . . . 9  |-  ( ( V `  ( i  +  1 ) )  =  X  ->  (
( V `  (
i  +  1 ) )  -  X )  =  ( X  -  X ) )
167166adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( V `  (
i  +  1 ) )  -  X )  =  ( X  -  X ) )
168115ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  ( i  +  1 ) )  =  X )  ->  X  e.  CC )
169168subidd 9976 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  ( i  +  1 ) )  =  X )  -> 
( X  -  X
)  =  0 )
1701, 169sylanl2 656 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( X  -  X )  =  0 )
171165, 167, 1703eqtrd 2468 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( Q `  ( i  +  1 ) )  =  0 )
172146, 171oveq12d 6321 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( ( V `  i )  -  X ) (,) 0 ) )
173 simplr 761 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
174 fourierdlem74.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 ) ) ) } )
17512adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  M  e.  NN )
1764, 7, 5, 11, 174, 12, 13, 134fourierdlem14 37847 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q  e.  ( O `
 M ) )
177176adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  Q  e.  ( O `  M
) )
178 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  s  =  0 )
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  X  e.  ran  V
)
180 ffn 5744 . . . . . . . . . . . . . . . . . . 19  |-  ( V : ( 0 ... M ) --> ( (
-u pi  +  X
) [,] ( pi  +  X ) )  ->  V  Fn  (
0 ... M ) )
181 fvelrnb 5926 . . . . . . . . . . . . . . . . . . 19  |-  ( V  Fn  ( 0 ... M )  ->  ( X  e.  ran  V  <->  E. i  e.  ( 0 ... M
) ( V `  i )  =  X ) )
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( X  e.  ran  V  <->  E. i  e.  (
0 ... M ) ( V `  i )  =  X ) )
183179, 182mpbid 214 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( V `  i
)  =  X )
184 simpr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( 0 ... M
) )
185134fvmpt2 5971 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  ( -u pi [,] pi ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
186184, 133, 185syl2anc 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
187186adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  ( ( V `
 i )  -  X ) )
188 oveq1 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( V `  i )  =  X  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
189188adantl 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
190115subidd 9976 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( X  -  X
)  =  0 )
191190ad2antrr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( X  -  X )  =  0 )
192187, 189, 1913eqtrd 2468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( Q `  i )  =  0 )
193192ex 436 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  =  X  -> 
( Q `  i
)  =  0 ) )
194193reximdva 2901 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E. i  e.  ( 0 ... M
) ( V `  i )  =  X  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 ) )
195183, 194mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( Q `  i
)  =  0 )
196113, 134fmptd 6059 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
197 ffn 5744 . . . . . . . . . . . . . . . . 17  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
198 fvelrnb 5926 . . . . . . . . . . . . . . . . 17  |-  ( Q  Fn  ( 0 ... M )  ->  (
0  e.  ran  Q  <->  E. i  e.  ( 0 ... M ) ( Q `  i )  =  0 ) )
199196, 197, 1983syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  e.  ran  Q  <->  E. i  e.  (
0 ... M ) ( Q `  i )  =  0 ) )
200195, 199mpbird 236 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  ran  Q
)
201200adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  = 
0 )  ->  0  e.  ran  Q )
202178, 201eqeltrd 2511 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  = 
0 )  ->  s  e.  ran  Q )
203174, 175, 177, 202fourierdlem12 37845 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  =  0 )  /\  i  e.  ( 0..^ M ) )  ->  -.  s  e.  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
204203an32s 812 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
205204adantlr 720 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  0 )  ->  -.  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
206173, 205pm2.65da 579 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  =  0 )
207206adantlr 720 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  s  =  0
)
208207iffalsed 3921 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
209 elioore 11668 . . . . . . . . . . . 12  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
210209adantl 468 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
211 0red 9646 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
212 elioo3g 11667 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) ) )
213212biimpi 198 . . . . . . . . . . . . . 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 ) ) ) ) )
214213simprrd 766 . . . . . . . . . . . . 13  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
215214adantl 468 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
216171adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  =  0 )
217215, 216breqtrd 4446 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  0 )
218210, 211, 217ltnsymd 9786 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  0  <  s )
219218iffalsed 3921 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
220219oveq2d 6319 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  W ) )
221220oveq1d 6318 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  =  ( ( ( F `  ( X  +  s ) )  -  W )  / 
s ) )
22241ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  i
)  e.  RR* )
2235rexrd 9692 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  RR* )
224223ad3antrrr 735 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR* )
225162ad2antrr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  X  e.  RR )
226225, 210readdcld 9672 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  RR )
227115adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
228 iccssre 11718 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
2293, 2, 228mp2an 677 . . . . . . . . . . . . . . . . . 18  |-  ( -u pi [,] pi )  C_  RR
230229, 51sstri 3474 . . . . . . . . . . . . . . . . 17  |-  ( -u pi [,] pi )  C_  CC
231186, 133eqeltrd 2511 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  ( -u pi [,] pi ) )
2321, 231sylan2 477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
233230, 232sseldi 3463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
234227, 233addcomd 9837 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  i ) )  =  ( ( Q `  i )  +  X ) )
235145oveq1d 6318 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( ( ( V `  i )  -  X
)  +  X ) )
23617recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  CC )
237236, 227npcand 9992 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  i )  -  X )  +  X )  =  ( V `  i ) )
238234, 235, 2373eqtrrd 2469 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  =  ( X  +  ( Q `
 i ) ) )
239238adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
240145, 143eqeltrd 2511 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
241240adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
242209adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
2435ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
244213simprld 764 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  ( Q `  i )  <  s )
245244adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
246241, 242, 243, 245ltadd2dd 9796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
247239, 246eqbrtrd 4442 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
248247adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( V `  i
)  <  ( X  +  s ) )
249 ltaddneg 37394 . . . . . . . . . . . . 13  |-  ( ( s  e.  RR  /\  X  e.  RR )  ->  ( s  <  0  <->  ( X  +  s )  <  X ) )
250210, 225, 249syl2anc 666 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( s  <  0  <->  ( X  +  s )  <  X ) )
251217, 250mpbid 214 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  <  X )
252222, 224, 226, 248, 251eliood 37470 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( X  +  s )  e.  ( ( V `  i ) (,) X ) )
253 fvres 5893 . . . . . . . . . . 11  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) X )  ->  (
( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
254253eqcomd 2431 . . . . . . . . . 10  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) X )  ->  ( F `  ( X  +  s ) )  =  ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
) )
255252, 254syl 17 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( F `  ( X  +  s )
)  =  ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) ) )
256255oveq1d 6318 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  W
)  =  ( ( ( F  |`  (
( V `  i
) (,) X ) ) `  ( X  +  s ) )  -  W ) )
257256oveq1d 6318 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  W )  /  s
)  =  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) )
258208, 221, 2573eqtrd 2468 . . . . . 6  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) )
259172, 258mpteq12dva 4499 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )  =  ( s  e.  ( ( ( V `  i
)  -  X ) (,) 0 )  |->  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) ) )
260104, 141, 2593eqtrd 2468 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  ( H  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( s  e.  ( ( ( V `  i )  -  X
) (,) 0 ) 
|->  ( ( ( ( F  |`  ( ( V `  i ) (,) X ) ) `  ( X  +  s
) )  -  W
)  /  s ) ) )
261260, 171oveq12d 6321 . . 3  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  (
( H  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) )  =  ( ( s  e.  ( ( ( V `  i )  -  X ) (,) 0 )  |->  ( ( ( ( F  |`  ( ( V `  i ) (,) X
) ) `  ( X  +  s )
)  -  W )  /  s ) ) lim
CC  0 ) )
26297, 101, 2613eltr4d 2526 . 2  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  =  X )  ->  A  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
263 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 ) ) )
264 eqid 2423 . . . . 5  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  s )
265 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 ) )
26630adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  F : RR --> RR )
2675adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
268209adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
269267, 268readdcld 9672 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
270266, 269ffvelrnd 6036 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
271270recnd 9671 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
272271adantlr 720 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
2732723adantl3 1164 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
274 fourierdlem74.y . . . . . . . . . 10  |-  ( ph  ->  Y  e.  RR )
275274recnd 9671 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
276 limccl 22822 . . . . . . . . . 10  |-  ( ( F  |`  ( -oo (,) X ) ) lim CC  X )  C_  CC
277276, 36sseldi 3463 . . . . . . . . 9  |-  ( ph  ->  W  e.  CC )
278275, 277ifcld 3953 . . . . . . . 8  |-  ( ph  ->  if ( 0  < 
s ,  Y ,  W )  e.  CC )
279278adantr 467 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
2802793ad2antl1 1168 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
281273, 280subcld 9988 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  e.  CC )
282209recnd 9671 . . . . . . 7  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  CC )
283282adantl 468 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  CC )
284 elsn 4011 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
285206, 284sylnibr 307 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
2862853adantl3 1164 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
287283, 286eldifd 3448 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
288 eqid 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
289 eqid 2423 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  W )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  W )
290 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 ) )
291277ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  W  e.  CC )
29230adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> RR )
293 ioossre 11698 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
294293a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
29541adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
296161rexrd 9692 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
297296adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
298269adantlr 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
299196adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
300299, 156ffvelrnd 6036 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
301300adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
302214adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
303242, 301, 243, 302ltadd2dd 9796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
304164oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
305161recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  CC )
306227, 305pncan3d 9991 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( ( V `  ( i  +  1 ) )  -  X
) )  =  ( V `  ( i  +  1 ) ) )
307304, 306eqtrd 2464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
308307adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
309303, 308breqtrd 4446 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
310295, 297, 298, 247, 309eliood 37470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
311 ioossre 11698 . . . . . . . . . . . 12  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
312311a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  RR )
313242, 302ltned 9773 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  (
i  +  1 ) ) )
314 fourierdlem74.r . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
315307eqcomd 2431 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  =  ( X  +  ( Q `
 ( i  +  1 ) ) ) )
316315oveq2d 6319 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
317314, 316eleqtrd 2513 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
318300recnd 9671 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  CC )
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 37887 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
320 ioosscn 37466 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
321320a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
322277adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  CC )
323289, 321, 322, 318constlimc 37568 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  W ) lim CC  ( Q `  ( i  +  1 ) ) ) )
324288, 289, 290, 272, 291, 319, 323sublimc 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  +  1 ) ) ) )
325324adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( R  -  W )  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  W ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
326 iftrue 3916 . . . . . . . . . 10  |-  ( ( V `  ( i  +  1 ) )  <  X  ->  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y )  =  W )
327326oveq2d 6319 . . . . . . . . 9  |-  ( ( V `  ( i  +  1 ) )  <  X  ->  ( R  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
328327adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( R  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  =  ( R  -  W ) )
329209adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  e.  RR )
330 0red 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
0  e.  RR )
331300ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
332214adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  ( Q `  ( i  +  1 ) ) )
333164adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
334161adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  e.  RR )
3355ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  X  e.  RR )
336 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  <  X )
337334, 335, 336ltled 9785 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( V `  ( i  +  1 ) )  <_  X )
338334, 335suble0d 10206 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  (
( ( V `  ( i  +  1 ) )  -  X
)  <_  0  <->  ( V `  ( i  +  1 ) )  <_  X
) )
339337, 338mpbird 236 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  (
( V `  (
i  +  1 ) )  -  X )  <_  0 )
340333, 339eqbrtrd 4442 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( Q `  ( i  +  1 ) )  <_  0 )
341340adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  <_  0 )
342329, 331, 330, 332, 341ltletrd 9797 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
s  <  0 )
343329, 330, 342ltnsymd 9786 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  -.  0  <  s )
344343iffalsed 3921 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
345344oveq2d 6319 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `  ( i  +  1 ) )  <  X )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  W ) )
346345mpteq2dva 4508 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  W ) ) )
347346oveq1d 6318 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  W ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
348325, 328, 3473eltr4d 2526 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 ( i  +  1 ) )  < 
X )  ->  ( R  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
3493483adantl3 1164 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  ( V `  ( i  +  1 ) )  <  X )  -> 
( R  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
350 simpl1 1009 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  ->  ph )
351 simpl2 1010 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  -> 
i  e.  ( 0..^ M ) )
3525ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  ->  X  e.  RR )
3533523adantl3 1164 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  ->  X  e.  RR )
354161adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  -> 
( V `  (
i  +  1 ) )  e.  RR )
3553543adantl3 1164 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  -> 
( V `  (
i  +  1 ) )  e.  RR )
356 neqne 37279 . . . . . . . . . . 11  |-  ( -.  ( V `  (
i  +  1 ) )  =  X  -> 
( V `  (
i  +  1 ) )  =/=  X )
357356necomd 2696 . . . . . . . . . 10  |-  ( -.  ( V `  (
i  +  1 ) )  =  X  ->  X  =/=  ( V `  ( i  +  1 ) ) )
358357adantr 467 . . . . . . . . 9  |-  ( ( -.  ( V `  ( i  +  1 ) )  =  X  /\  -.  ( V `
 ( i  +  1 ) )  < 
X )  ->  X  =/=  ( V `  (
i  +  1 ) ) )
3593583ad2antl3 1170 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  ->  X  =/=  ( V `  ( i  +  1 ) ) )
360 simpr 463 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  ->  -.  ( V `  (
i  +  1 ) )  <  X )
361353, 355, 359, 360lttri5d 37403 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )  /\  -.  ( V `
 ( i  +  1 ) )  =  X )  /\  -.  ( V `  ( i  +  1 ) )  <  X )  ->  X  <  ( V `  ( i  +  1 ) ) )
362 eqid 2423 . . . . . . . 8  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  if ( 0  <  s ,  Y ,  W ) )  =  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  if ( 0  <  s ,  Y ,  W ) )
363272adantlr 720 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  <  ( V `  ( i  +  1 ) ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( F `  ( X  +  s )
)  e.  CC )
364278ad3antrrr 735 . . . . . . . 8  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  <  ( V `  ( i  +  1 ) ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  if ( 0  <  s ,  Y ,  W )  e.  CC )
365319adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  R  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
366 eqid 2423 . . . . . . . . . . 11  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  Y )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  Y )
367275adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  CC )
368366, 321, 367, 318constlimc 37568 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  Y ) lim CC  ( Q `  ( i  +  1 ) ) ) )
369368adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  Y  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  Y ) lim CC  ( Q `  ( i  +  1 ) ) ) )
3705ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  X  e.  RR )
371161adantr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
372 simpr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  X  <  ( V `  (
i  +  1 ) ) )
373370, 371, 372ltnsymd 9786 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  -.  ( V `  ( i  +  1 ) )  <  X )
374373iffalsed 3921 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  < 
( V `  (
i  +  1 ) ) )  ->  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y )  =  Y )
375 0red 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  X  <  ( V `  ( i  +  1 ) ) )  /\  s  e.