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

Theorem fourierdlem101 37358
Description: Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem101.d  |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  s ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) )
fourierdlem101.p  |-  P  =  ( 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 ) ) ) } )
fourierdlem101.g  |-  G  =  ( t  e.  (
-u pi [,] pi )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )
fourierdlem101.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem101.6  |-  ( ph  ->  M  e.  NN )
fourierdlem101.n  |-  ( ph  ->  N  e.  NN )
fourierdlem101.x  |-  ( ph  ->  X  e.  RR )
fourierdlem101.f  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
fourierdlem101.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem101.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem101.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
Assertion
Ref Expression
fourierdlem101  |-  ( ph  ->  S. ( -u pi [,] pi ) ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) )  _d t  =  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  N ) `  s
) )  _d s )
Distinct variable groups:    D, s,
t    t, F    i, G, s, t    t, L    i, M, s, t    m, M, p, i    n, N, s    t, N    Q, i, s, t    Q, p   
t, R    i, X, s, t    ph, i, s, t    ph, n
Allowed substitution hints:    ph( m, p)    D( i, m, n, p)    P( t, i, m, n, s, p)    Q( m, n)    R( i, m, n, s, p)    F( i, m, n, s, p)    G( m, n, p)    L( i, m, n, s, p)    M( n)    N( i, m, p)    X( m, n, p)

Proof of Theorem fourierdlem101
Dummy variables  r 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 459 . . . . 5  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  t  e.  ( -u pi [,] pi ) )
2 fourierdlem101.f . . . . . . 7  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
32ffvelrnda 6009 . . . . . 6  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
4 fourierdlem101.n . . . . . . . . 9  |-  ( ph  ->  N  e.  NN )
54adantr 463 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  N  e.  NN )
6 pire 23143 . . . . . . . . . . . 12  |-  pi  e.  RR
76renegcli 9916 . . . . . . . . . . 11  |-  -u pi  e.  RR
8 eliccre 36908 . . . . . . . . . . 11  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR  /\  t  e.  ( -u pi [,] pi ) )  -> 
t  e.  RR )
97, 6, 8mp3an12 1316 . . . . . . . . . 10  |-  ( t  e.  ( -u pi [,] pi )  ->  t  e.  RR )
109adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  t  e.  RR )
11 fourierdlem101.x . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
1211adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  X  e.  RR )
1310, 12resubcld 10028 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
t  -  X )  e.  RR )
14 fourierdlem101.d . . . . . . . . 9  |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  s ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) )
1514dirkerre 37245 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( t  -  X
)  e.  RR )  ->  ( ( D `
 N ) `  ( t  -  X
) )  e.  RR )
165, 13, 15syl2anc 659 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  N
) `  ( t  -  X ) )  e.  RR )
1716recnd 9652 . . . . . 6  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  N
) `  ( t  -  X ) )  e.  CC )
183, 17mulcld 9646 . . . . 5  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  N ) `
 ( t  -  X ) ) )  e.  CC )
19 fourierdlem101.g . . . . . 6  |-  G  =  ( t  e.  (
-u pi [,] pi )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )
2019fvmpt2 5941 . . . . 5  |-  ( ( t  e.  ( -u pi [,] pi )  /\  ( ( F `  t )  x.  (
( D `  N
) `  ( t  -  X ) ) )  e.  CC )  -> 
( G `  t
)  =  ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) ) )
211, 18, 20syl2anc 659 . . . 4  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  ( G `  t )  =  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )
2221eqcomd 2410 . . 3  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  N ) `
 ( t  -  X ) ) )  =  ( G `  t ) )
2322itgeq2dv 22480 . 2  |-  ( ph  ->  S. ( -u pi [,] pi ) ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) )  _d t  =  S. (
-u pi [,] pi ) ( G `  t )  _d t )
24 fourierdlem101.p . . 3  |-  P  =  ( 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 ) ) ) } )
25 fveq2 5849 . . . . 5  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
2625oveq1d 6293 . . . 4  |-  ( j  =  i  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 i )  -  X ) )
2726cbvmptv 4487 . . 3  |-  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  -  X ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( Q `
 i )  -  X ) )
28 fourierdlem101.6 . . 3  |-  ( ph  ->  M  e.  NN )
29 fourierdlem101.q . . 3  |-  ( ph  ->  Q  e.  ( P `
 M ) )
3018, 19fmptd 6033 . . 3  |-  ( ph  ->  G : ( -u pi [,] pi ) --> CC )
3119reseq1i 5090 . . . . 5  |-  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( t  e.  (
-u pi [,] pi )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
32 ioossicc 11664 . . . . . . 7  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
337a1i 11 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  e.  RR )
3433rexrd 9673 . . . . . . . . 9  |-  ( ph  -> 
-u pi  e.  RR* )
3534adantr 463 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
366a1i 11 . . . . . . . . . 10  |-  ( ph  ->  pi  e.  RR )
3736rexrd 9673 . . . . . . . . 9  |-  ( ph  ->  pi  e.  RR* )
3837adantr 463 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
3924, 28, 29fourierdlem15 37272 . . . . . . . . 9  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
4039adantr 463 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
41 simpr 459 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
4235, 38, 40, 41fourierdlem8 37265 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
4332, 42syl5ss 3453 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
4443resmptd 5145 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( -u pi [,] pi )  |->  ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  t
)  x.  ( ( D `  N ) `
 ( t  -  X ) ) ) ) )
4531, 44syl5eq 2455 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `  t
)  x.  ( ( D `  N ) `
 ( t  -  X ) ) ) ) )
462adantr 463 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : (
-u pi [,] pi )
--> CC )
4746, 43feqresmpt 5903 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
48 fourierdlem101.fcn . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
4947, 48eqeltrrd 2491 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
50 eqidd 2403 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  e.  RR  |->  ( ( D `  N
) `  s )
)  =  ( s  e.  RR  |->  ( ( D `  N ) `
 s ) ) )
51 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  ( (
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) )  ->  s  =  ( ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) )
52 eqidd 2403 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) )  =  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( t  -  X ) ) )
53 oveq1 6285 . . . . . . . . . . . . . . 15  |-  ( t  =  r  ->  (
t  -  X )  =  ( r  -  X ) )
5453adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  t  =  r )  ->  ( t  -  X
)  =  ( r  -  X ) )
55 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
56 elioore 11612 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  r  e.  RR )
5756adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  r  e.  RR )
5811adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
5957, 58resubcld 10028 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
r  -  X )  e.  RR )
6059adantlr 713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
r  -  X )  e.  RR )
6152, 54, 55, 60fvmptd 5938 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) `  r
)  =  ( r  -  X ) )
6261adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  ( (
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) )  ->  ( (
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r )  =  ( r  -  X ) )
6351, 62eqtrd 2443 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  ( (
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) )  ->  s  =  ( r  -  X
) )
6463fveq2d 5853 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  ( (
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) )  ->  ( ( D `  N ) `  s )  =  ( ( D `  N
) `  ( r  -  X ) ) )
65 elioore 11612 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  t  e.  RR )
6665adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
6711adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
6866, 67resubcld 10028 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
t  -  X )  e.  RR )
6968adantlr 713 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
t  -  X )  e.  RR )
70 eqid 2402 . . . . . . . . . . . 12  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( t  -  X ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) )
7169, 70fmptd 6033 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> RR )
7271ffvelrnda 6009 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) `  r
)  e.  RR )
734ad2antrr 724 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  N  e.  NN )
7414dirkerre 37245 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( r  -  X
)  e.  RR )  ->  ( ( D `
 N ) `  ( r  -  X
) )  e.  RR )
7573, 60, 74syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( r  -  X ) )  e.  RR )
7650, 64, 72, 75fvmptd 5938 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( s  e.  RR  |->  ( ( D `  N ) `  s
) ) `  (
( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) `  r
) )  =  ( ( D `  N
) `  ( r  -  X ) ) )
7776eqcomd 2410 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( r  -  X ) )  =  ( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) ) `  ( ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) ) )
7877mpteq2dva 4481 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( r  -  X
) ) )  =  ( r  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) ) `  ( ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) ) ) )
7953fveq2d 5853 . . . . . . . . 9  |-  ( t  =  r  ->  (
( D `  N
) `  ( t  -  X ) )  =  ( ( D `  N ) `  (
r  -  X ) ) )
8079cbvmptv 4487 . . . . . . . 8  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( t  -  X ) ) )  =  ( r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( r  -  X
) ) )
8180a1i 11 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( t  -  X
) ) )  =  ( r  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
r  -  X ) ) ) )
8214dirkerre 37245 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  s  e.  RR )  ->  ( ( D `  N ) `  s
)  e.  RR )
834, 82sylan 469 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  RR )  ->  ( ( D `  N ) `
 s )  e.  RR )
84 eqid 2402 . . . . . . . . . 10  |-  ( s  e.  RR  |->  ( ( D `  N ) `
 s ) )  =  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )
8583, 84fmptd 6033 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> RR )
8685adantr 463 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) ) : RR --> RR )
87 fcompt 6046 . . . . . . . 8  |-  ( ( ( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> RR  /\  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> RR )  -> 
( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  o.  ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) )  =  ( r  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) ) `  ( ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) `  r ) ) ) )
8886, 71, 87syl2anc 659 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( s  e.  RR  |->  ( ( D `  N ) `
 s ) )  o.  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) )  =  ( r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( s  e.  RR  |->  ( ( D `  N ) `
 s ) ) `
 ( ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( t  -  X ) ) `
 r ) ) ) )
8978, 81, 883eqtr4d 2453 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( t  -  X
) ) )  =  ( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  o.  ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) ) )
90 eqid 2402 . . . . . . . 8  |-  ( t  e.  CC  |->  ( t  -  X ) )  =  ( t  e.  CC  |->  ( t  -  X ) )
91 simpr 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  CC )  ->  t  e.  CC )
9211recnd 9652 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  CC )
9392adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  CC )  ->  X  e.  CC )
9491, 93negsubd 9973 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  CC )  ->  ( t  +  -u X )  =  ( t  -  X
) )
9594eqcomd 2410 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  CC )  ->  ( t  -  X )  =  ( t  +  -u X ) )
9695mpteq2dva 4481 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  CC  |->  ( t  -  X
) )  =  ( t  e.  CC  |->  ( t  +  -u X
) ) )
9792negcld 9954 . . . . . . . . . . 11  |-  ( ph  -> 
-u X  e.  CC )
98 eqid 2402 . . . . . . . . . . . 12  |-  ( t  e.  CC  |->  ( t  +  -u X ) )  =  ( t  e.  CC  |->  ( t  + 
-u X ) )
9998addccncf 21712 . . . . . . . . . . 11  |-  ( -u X  e.  CC  ->  ( t  e.  CC  |->  ( t  +  -u X
) )  e.  ( CC -cn-> CC ) )
10097, 99syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  CC  |->  ( t  +  -u X ) )  e.  ( CC -cn-> CC ) )
10196, 100eqeltrd 2490 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  CC  |->  ( t  -  X
) )  e.  ( CC -cn-> CC ) )
102101adantr 463 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  CC  |->  ( t  -  X ) )  e.  ( CC -cn-> CC ) )
103 ioossre 11640 . . . . . . . . . 10  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
104 ax-resscn 9579 . . . . . . . . . 10  |-  RR  C_  CC
105103, 104sstri 3451 . . . . . . . . 9  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
106105a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
107104a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  CC )
10890, 102, 106, 107, 69cncfmptssg 37040 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> RR ) )
10983recnd 9652 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  RR )  ->  ( ( D `  N ) `
 s )  e.  CC )
110109, 84fmptd 6033 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> CC )
111 ssid 3461 . . . . . . . . . 10  |-  CC  C_  CC
11214dirkerf 37247 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  ( D `  N ) : RR --> RR )
1134, 112syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( D `  N
) : RR --> RR )
114113feqmptd 5902 . . . . . . . . . . 11  |-  ( ph  ->  ( D `  N
)  =  ( s  e.  RR  |->  ( ( D `  N ) `
 s ) ) )
11514dirkercncf 37257 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  ( D `  N )  e.  ( RR -cn-> RR ) )
1164, 115syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( D `  N
)  e.  ( RR
-cn-> RR ) )
117114, 116eqeltrrd 2491 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) )  e.  ( RR -cn-> RR ) )
118 cncffvrn 21694 . . . . . . . . . 10  |-  ( ( CC  C_  CC  /\  (
s  e.  RR  |->  ( ( D `  N
) `  s )
)  e.  ( RR
-cn-> RR ) )  -> 
( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  e.  ( RR -cn-> CC )  <-> 
( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> CC ) )
119111, 117, 118sylancr 661 . . . . . . . . 9  |-  ( ph  ->  ( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  e.  ( RR -cn-> CC )  <-> 
( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> CC ) )
120110, 119mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) )  e.  ( RR -cn-> CC ) )
121120adantr 463 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  e.  ( RR -cn-> CC ) )
122108, 121cncfco 21703 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( s  e.  RR  |->  ( ( D `  N ) `
 s ) )  o.  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
12389, 122eqeltrd 2490 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( t  -  X
) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
12449, 123mulcncf 22151 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
12545, 124eqeltrd 2490 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
126 cncff 21689 . . . . . . . 8  |-  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
12748, 126syl 17 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
128113adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  N ) : RR --> RR )
129 elioore 11612 . . . . . . . . . . . . 13  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
130129adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
13111adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
132130, 131resubcld 10028 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  -  X )  e.  RR )
133128, 132ffvelrnd 6010 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( s  -  X ) )  e.  RR )
134133recnd 9652 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( s  -  X ) )  e.  CC )
135 eqid 2402 . . . . . . . . 9  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) )
136134, 135fmptd 6033 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
137136adantr 463 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC )
138 eqid 2402 . . . . . . 7  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  x.  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) ) `
 t ) ) )  =  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  x.  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) ) `
 t ) ) )
139 fourierdlem101.r . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
140 oveq1 6285 . . . . . . . . . . . . . 14  |-  ( t  =  ( Q `  i )  ->  (
t  -  X )  =  ( ( Q `
 i )  -  X ) )
141140fveq2d 5853 . . . . . . . . . . . . 13  |-  ( t  =  ( Q `  i )  ->  (
( D `  N
) `  ( t  -  X ) )  =  ( ( D `  N ) `  (
( Q `  i
)  -  X ) ) )
142141eqcomd 2410 . . . . . . . . . . . 12  |-  ( t  =  ( Q `  i )  ->  (
( D `  N
) `  ( ( Q `  i )  -  X ) )  =  ( ( D `  N ) `  (
t  -  X ) ) )
143142adantl 464 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  t  =  ( Q `  i ) )  -> 
( ( D `  N ) `  (
( Q `  i
)  -  X ) )  =  ( ( D `  N ) `
 ( t  -  X ) ) )
144 eqidd 2403 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `  N
) `  ( s  -  X ) ) ) )
145 oveq1 6285 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
s  -  X )  =  ( t  -  X ) )
146145fveq2d 5853 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
( D `  N
) `  ( s  -  X ) )  =  ( ( D `  N ) `  (
t  -  X ) ) )
147146adantl 464 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  /\  s  =  t )  ->  ( ( D `  N ) `  (
s  -  X ) )  =  ( ( D `  N ) `
 ( t  -  X ) ) )
148 elsn 3986 . . . . . . . . . . . . . . 15  |-  ( t  e.  { ( Q `
 i ) }  <-> 
t  =  ( Q `
 i ) )
149148notbii 294 . . . . . . . . . . . . . 14  |-  ( -.  t  e.  { ( Q `  i ) }  <->  -.  t  =  ( Q `  i ) )
150 elunnel2 36795 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  e.  { ( Q `  i ) } )  ->  t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
151149, 150sylan2br 474 . . . . . . . . . . . . 13  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  =  ( Q `  i ) )  -> 
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
152151adantll 712 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
153113ad2antrr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( D `  N ) : RR --> RR )
154 simpr 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  =  ( Q `  i
) )  ->  t  =  ( Q `  i ) )
1559ssriv 3446 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u pi [,] pi )  C_  RR
156 fzossfz 11877 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0..^ M )  C_  (
0 ... M )
157156, 41sseldi 3440 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
15840, 157ffvelrnd 6010 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
159155, 158sseldi 3440 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
160159adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  =  ( Q `  i
) )  ->  ( Q `  i )  e.  RR )
161154, 160eqeltrd 2490 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  =  ( Q `  i
) )  ->  t  e.  RR )
162161adantlr 713 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  t  =  ( Q `  i ) )  -> 
t  e.  RR )
163152, 65syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
t  e.  RR )
164162, 163pm2.61dan 792 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  t  e.  RR )
16511ad2antrr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  X  e.  RR )
166164, 165resubcld 10028 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( t  -  X )  e.  RR )
167153, 166ffvelrnd 6010 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( ( D `
 N ) `  ( t  -  X
) )  e.  RR )
168167adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
( ( D `  N ) `  (
t  -  X ) )  e.  RR )
169144, 147, 152, 168fvmptd 5938 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) `  t )  =  ( ( D `  N
) `  ( t  -  X ) ) )
170143, 169ifeqda 3918 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  if ( t  =  ( Q `  i ) ,  ( ( D `  N
) `  ( ( Q `  i )  -  X ) ) ,  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) `  t ) )  =  ( ( D `  N ) `  (
t  -  X ) ) )
171170mpteq2dva 4481 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  if ( t  =  ( Q `  i ) ,  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) )  =  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( ( D `  N ) `
 ( t  -  X ) ) ) )
172113adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D `  N ) : RR --> RR )
173 simpr 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
174 elun 3584 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } )  <-> 
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  \/  s  e.  {
( Q `  i
) } ) )
175173, 174sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  \/  s  e. 
{ ( Q `  i ) } ) )
176175adantlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  \/  s  e. 
{ ( Q `  i ) } ) )
177 elsni 3997 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  { ( Q `
 i ) }  ->  s  =  ( Q `  i ) )
178177adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e. 
{ ( Q `  i ) } )  ->  s  =  ( Q `  i ) )
179159adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e. 
{ ( Q `  i ) } )  ->  ( Q `  i )  e.  RR )
180178, 179eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e. 
{ ( Q `  i ) } )  ->  s  e.  RR )
181180ex 432 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e. 
{ ( Q `  i ) }  ->  s  e.  RR ) )
182181adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e. 
{ ( Q `  i ) }  ->  s  e.  RR ) )
183 pm3.44 509 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  ->  s  e.  RR )  /\  ( s  e. 
{ ( Q `  i ) }  ->  s  e.  RR ) )  ->  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  \/  s  e.  { ( Q `  i ) } )  ->  s  e.  RR ) )
184129, 182, 183sylancr 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  \/  s  e.  { ( Q `  i ) } )  ->  s  e.  RR ) )
185176, 184mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  s  e.  RR )
18611ad2antrr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  X  e.  RR )
187185, 186resubcld 10028 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  -  X )  e.  RR )
188 eqid 2402 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( s  -  X
) )  =  ( s  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  |->  ( s  -  X ) )
189187, 188fmptd 6033 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( s  -  X ) ) : ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) --> RR )
190 fcompt 6046 . . . . . . . . . . . . . . 15  |-  ( ( ( D `  N
) : RR --> RR  /\  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( s  -  X ) ) : ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) --> RR )  ->  (
( D `  N
)  o.  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( s  -  X
) ) )  =  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( ( D `  N ) `
 ( ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( s  -  X
) ) `  t
) ) ) )
191172, 189, 190syl2anc 659 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( D `
 N )  o.  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( s  -  X ) ) )  =  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( s  -  X ) ) `
 t ) ) ) )
192 eqidd 2403 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( s  -  X ) )  =  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( s  -  X
) ) )
193145adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  s  =  t )  -> 
( s  -  X
)  =  ( t  -  X ) )
194 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
195192, 193, 194, 166fvmptd 5938 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( s  -  X
) ) `  t
)  =  ( t  -  X ) )
196195fveq2d 5853 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( ( D `
 N ) `  ( ( s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( s  -  X ) ) `  t ) )  =  ( ( D `  N ) `
 ( t  -  X ) ) )
197196mpteq2dva 4481 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( (
s  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  |->  ( s  -  X ) ) `  t ) ) )  =  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) ) )
198191, 197eqtr2d 2444 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) )  =  ( ( D `
 N )  o.  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( s  -  X ) ) ) )
199 eqid 2402 . . . . . . . . . . . . . . . 16  |-  ( s  e.  CC  |->  ( s  -  X ) )  =  ( s  e.  CC  |->  ( s  -  X ) )
200 simpr 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  CC )  ->  s  e.  CC )
20192adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  CC )  ->  X  e.  CC )
202200, 201negsubd 9973 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  s  e.  CC )  ->  ( s  +  -u X )  =  ( s  -  X
) )
203202eqcomd 2410 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  s  e.  CC )  ->  ( s  -  X )  =  ( s  +  -u X ) )
204203mpteq2dva 4481 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( s  e.  CC  |->  ( s  -  X
) )  =  ( s  e.  CC  |->  ( s  +  -u X
) ) )
205 eqid 2402 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  CC  |->  ( s  +  -u X ) )  =  ( s  e.  CC  |->  ( s  + 
-u X ) )
206205addccncf 21712 . . . . . . . . . . . . . . . . . . 19  |-  ( -u X  e.  CC  ->  ( s  e.  CC  |->  ( s  +  -u X
) )  e.  ( CC -cn-> CC ) )
20797, 206syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( s  e.  CC  |->  ( s  +  -u X ) )  e.  ( CC -cn-> CC ) )
208204, 207eqeltrd 2490 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( s  e.  CC  |->  ( s  -  X
) )  e.  ( CC -cn-> CC ) )
209208adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  CC  |->  ( s  -  X ) )  e.  ( CC -cn-> CC ) )
210159recnd 9652 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
211210snssd 4117 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { ( Q `
 i ) } 
C_  CC )
212106, 211unssd 3619 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
C_  CC )
213199, 209, 212, 107, 187cncfmptssg 37040 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( s  -  X ) )  e.  ( ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) -cn-> RR ) )
214114, 120eqeltrd 2490 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D `  N
)  e.  ( RR
-cn-> CC ) )
215214adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D `  N )  e.  ( RR -cn-> CC ) )
216213, 215cncfco 21703 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( D `
 N )  o.  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( s  -  X ) ) )  e.  ( ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) -cn-> CC ) )
217 eqid 2402 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
218 eqid 2402 . . . . . . . . . . . . . . . 16  |-  ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  =  ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
219217cnfldtop 21583 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  Top
220 unicntop 36807 . . . . . . . . . . . . . . . . . . 19  |-  CC  =  U. ( TopOpen ` fld )
221220restid 15048 . . . . . . . . . . . . . . . . . 18  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
222219, 221ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
223222eqcomi 2415 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
224217, 218, 223cncfcn 21705 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  C_  CC  /\  CC  C_  CC )  ->  ( ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) -cn-> CC )  =  ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  Cn  ( TopOpen ` fld )
) )
225212, 111, 224sylancl 660 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) -cn-> CC )  =  ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  Cn  ( TopOpen ` fld )
) )
226216, 225eleqtrd 2492 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( D `
 N )  o.  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( s  -  X ) ) )  e.  ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  Cn  ( TopOpen ` fld )
) )
227198, 226eqeltrd 2490 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) )  e.  ( ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  Cn  ( TopOpen ` fld ) ) )
228217cnfldtopon 21582 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
229 resttopon 19955 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  C_  CC )  ->  ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  e.  (TopOn `  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) ) )
230228, 212, 229sylancr 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  e.  (TopOn `  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) ) )
231 cncnp 20074 . . . . . . . . . . . . 13  |-  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  e.  (TopOn `  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  /\  ( TopOpen ` fld )  e.  (TopOn `  CC ) )  -> 
( ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) )  e.  ( ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  Cn  ( TopOpen ` fld ) )  <->  ( (
t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  |->  ( ( D `
 N ) `  ( t  -  X
) ) ) : ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) --> CC 
/\  A. s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  CnP  ( TopOpen ` fld ) ) `  s
) ) ) )
232230, 228, 231sylancl 660 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
t  -  X ) ) )  e.  ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  Cn  ( TopOpen ` fld )
)  <->  ( ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
t  -  X ) ) ) : ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) --> CC  /\  A. s  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  CnP  ( TopOpen ` fld )
) `  s )
) ) )
233227, 232mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
t  -  X ) ) ) : ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) --> CC  /\  A. s  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  CnP  ( TopOpen ` fld )
) `  s )
) )
234233simprd 461 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  CnP  ( TopOpen ` fld ) ) `  s
) )
235 eqidd 2403 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( Q `  i ) )
236 elsncg 3995 . . . . . . . . . . . . . 14  |-  ( ( Q `  i )  e.  RR  ->  (
( Q `  i
)  e.  { ( Q `  i ) }  <->  ( Q `  i )  =  ( Q `  i ) ) )
237159, 236syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e. 
{ ( Q `  i ) }  <->  ( Q `  i )  =  ( Q `  i ) ) )
238235, 237mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  {
( Q `  i
) } )
239238olcd 391 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  \/  ( Q `
 i )  e. 
{ ( Q `  i ) } ) )
240 elun 3584 . . . . . . . . . . 11  |-  ( ( Q `  i )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } )  <-> 
( ( Q `  i )  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  \/  ( Q `  i )  e.  {
( Q `  i
) } ) )
241239, 240sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
242 fveq2 5849 . . . . . . . . . . . 12  |-  ( s  =  ( Q `  i )  ->  (
( ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  CnP  ( TopOpen ` fld ) ) `  s
)  =  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  CnP  ( TopOpen ` fld )
) `  ( Q `  i ) ) )
243242eleq2d 2472 . . . . . . . . . . 11  |-  ( s  =  ( Q `  i )  ->  (
( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( ( D `  N ) `
 ( t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  CnP  ( TopOpen ` fld )
) `  s )  <->  ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  |->  ( ( D `
 N ) `  ( t  -  X
) ) )  e.  ( ( ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  CnP  ( TopOpen ` fld ) ) `  ( Q `  i )
) ) )
244243rspccva 3159 . . . . . . . . . 10  |-  ( ( A. s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  ( ( D `  N ) `  (
t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  CnP  ( TopOpen ` fld ) ) `  s
)  /\  ( Q `  i )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )  -> 
( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } )  |->  ( ( D `  N ) `
 ( t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  CnP  ( TopOpen ` fld )
) `  ( Q `  i ) ) )
245234, 241, 244syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  ( ( D `  N
) `  ( t  -  X ) ) )  e.  ( ( ( ( TopOpen ` fld )t  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) )  CnP  ( TopOpen ` fld )
) `  ( Q `  i ) ) )
246171, 245eqeltrd 2490 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  if ( t  =  ( Q `  i ) ,  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) )  e.  ( ( ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  CnP  ( TopOpen ` fld ) ) `  ( Q `  i )
) )
247 eqid 2402 . . . . . . . . 9  |-  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
|->  if ( t  =  ( Q `  i
) ,  ( ( D `  N ) `
 ( ( Q `
 i )  -  X ) ) ,  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) `  t ) ) )  =  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  if ( t  =  ( Q `  i ) ,  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) )
248218, 217, 247, 137, 106, 210ellimc 22569 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( D `  N ) `
 ( ( Q `
 i )  -  X ) )  e.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) lim CC  ( Q `  i ) )  <->  ( t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  |->  if ( t  =  ( Q `  i ) ,  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) )  e.  ( ( ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  CnP  ( TopOpen ` fld ) ) `  ( Q `  i )
) ) )
249246, 248mpbird 232 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) )  e.  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) lim CC  ( Q `  i )
) )
250127, 137, 138, 139, 249mullimcf 36997 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  x.  ( ( D `  N ) `  (
( Q `  i
)  -  X ) ) )  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  t
)  x.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `  N
) `  ( s  -  X ) ) ) `
 t ) ) ) lim CC  ( Q `
 i ) ) )
251 fvres 5863 . . . . . . . . . 10  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( F `  t ) )
252251adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  =  ( F `  t ) )
253252oveq1d 6293 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) `  t
)  x.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `  N
) `  ( s  -  X ) ) ) `
 t ) )  =  ( ( F `
 t )  x.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) `  t ) ) )
254253mpteq2dva 4481 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) `  t )  x.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) )  =  ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  t )  x.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) ) )
255254oveq1d 6293 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) `  t )  x.  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) ) `
 t ) ) ) lim CC  ( Q `
 i ) )  =  ( ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  t )  x.  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) ) `
 t ) ) ) lim CC  ( Q `
 i ) ) )
256250, 255eleqtrd 2492 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  x.  ( ( D `  N ) `  (
( Q `  i
)  -  X ) ) )  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  t )  x.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) ) ) lim CC  ( Q `  i ) ) )
257 eqidd 2403 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `  N
) `  ( s  -  X ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) )
258 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  t )  ->  s  =  t )
259258oveq1d 6293 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  t )  ->  ( s  -  X
)  =  ( t  -  X ) )
260259fveq2d 5853 . . . . . . . . 9  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  s  =  t )  ->  ( ( D `  N ) `  (
s  -  X ) )  =  ( ( D `  N ) `
 ( t  -  X ) ) )
261 simpr 459 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
262113ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  N ) : RR --> RR )
263262, 69ffvelrnd 6010 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( t  -  X ) )  e.  RR )
264257, 260, 261, 263fvmptd 5938 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
)  =  ( ( D `  N ) `
 ( t  -  X ) ) )
265264oveq2d 6294 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F `  t
)  x.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `  N
) `  ( s  -  X ) ) ) `
 t ) )  =  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )
266265mpteq2dva 4481 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 t )  x.  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) `  t ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) ) )
267266oveq1d 6293 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  t )  x.  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) ) `
 t ) ) ) lim CC  ( Q `
 i ) )  =  ( ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) ) ) lim
CC  ( Q `  i ) ) )
268256, 267eleqtrd 2492 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  x.  ( ( D `  N ) `  (
( Q `  i
)  -  X ) ) )  e.  ( ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  t )  x.  (
( D `  N
) `  ( t  -  X ) ) ) ) lim CC  ( Q `
 i ) ) )
26945eqcomd 2410 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )  =  ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
270269oveq1d 6293 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) ) ) lim
CC  ( Q `  i ) )  =  ( ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
271268, 270eleqtrd 2492 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  x.  ( ( D `  N ) `  (
( Q `  i
)  -  X ) ) )  e.  ( ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
272 fourierdlem101.l . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
273 iftrue 3891 . . . . . . . . . . 11  |-  ( t  =  ( Q `  ( i  +  1 ) )  ->  if ( t  =  ( Q `  ( i  +  1 ) ) ,  ( ( D `
 N ) `  ( ( Q `  ( i  +  1 ) )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) )  =  ( ( D `  N
) `  ( ( Q `  ( i  +  1 ) )  -  X ) ) )
274 oveq1 6285 . . . . . . . . . . . . 13  |-  ( t  =  ( Q `  ( i  +  1 ) )  ->  (
t  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
275274eqcomd 2410 . . . . . . . . . . . 12  |-  ( t  =  ( Q `  ( i  +  1 ) )  ->  (
( Q `  (
i  +  1 ) )  -  X )  =  ( t  -  X ) )
276275fveq2d 5853 . . . . . . . . . . 11  |-  ( t  =  ( Q `  ( i  +  1 ) )  ->  (
( D `  N
) `  ( ( Q `  ( i  +  1 ) )  -  X ) )  =  ( ( D `
 N ) `  ( t  -  X
) ) )
277273, 276