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

Theorem fourierdlem101 31831
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 461 . . . . 5  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  t  e.  ( -u pi [,] pi ) )
2 fourierdlem101.f . . . . . . 7  |-  ( ph  ->  F : ( -u pi [,] pi ) --> CC )
32ffvelrnda 6032 . . . . . 6  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
4 fourierdlem101.n . . . . . . . . 9  |-  ( ph  ->  N  e.  NN )
54adantr 465 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  N  e.  NN )
6 pire 22718 . . . . . . . . . . . . 13  |-  pi  e.  RR
76renegcli 9892 . . . . . . . . . . . 12  |-  -u pi  e.  RR
87a1i 11 . . . . . . . . . . 11  |-  ( t  e.  ( -u pi [,] pi )  ->  -u pi  e.  RR )
96a1i 11 . . . . . . . . . . 11  |-  ( t  e.  ( -u pi [,] pi )  ->  pi  e.  RR )
10 id 22 . . . . . . . . . . 11  |-  ( t  e.  ( -u pi [,] pi )  ->  t  e.  ( -u pi [,] pi ) )
11 eliccre 31427 . . . . . . . . . . 11  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR  /\  t  e.  ( -u pi [,] pi ) )  -> 
t  e.  RR )
128, 9, 10, 11syl3anc 1228 . . . . . . . . . 10  |-  ( t  e.  ( -u pi [,] pi )  ->  t  e.  RR )
1312adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  t  e.  RR )
14 fourierdlem101.x . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
1514adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  X  e.  RR )
1613, 15resubcld 9999 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
t  -  X )  e.  RR )
17 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 ) ) ) ) ) ) )
1817dirkerre 31718 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( t  -  X
)  e.  RR )  ->  ( ( D `
 N ) `  ( t  -  X
) )  e.  RR )
195, 16, 18syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  N
) `  ( t  -  X ) )  e.  RR )
2019recnd 9634 . . . . . 6  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  N
) `  ( t  -  X ) )  e.  CC )
213, 20mulcld 9628 . . . . 5  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  N ) `
 ( t  -  X ) ) )  e.  CC )
22 fourierdlem101.g . . . . . 6  |-  G  =  ( t  e.  (
-u pi [,] pi )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )
2322fvmpt2 5964 . . . . 5  |-  ( ( t  e.  ( -u pi [,] pi )  /\  ( ( F `  t )  x.  (
( D `  N
) `  ( t  -  X ) ) )  e.  CC )  -> 
( G `  t
)  =  ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) ) )
241, 21, 23syl2anc 661 . . . 4  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  ( G `  t )  =  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )
2524eqcomd 2475 . . 3  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  N ) `
 ( t  -  X ) ) )  =  ( G `  t ) )
2625itgeq2dv 22056 . 2  |-  ( ph  ->  S. ( -u pi [,] pi ) ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) )  _d t  =  S. (
-u pi [,] pi ) ( G `  t )  _d t )
27 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 ) ) ) } )
28 nfcv 2629 . . . 4  |-  F/_ i
( ( Q `  j )  -  X
)
29 nfcv 2629 . . . 4  |-  F/_ j
( ( Q `  i )  -  X
)
30 fveq2 5872 . . . . 5  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
3130oveq1d 6310 . . . 4  |-  ( j  =  i  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 i )  -  X ) )
3228, 29, 31cbvmpt 4543 . . 3  |-  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j )  -  X ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( Q `
 i )  -  X ) )
33 fourierdlem101.6 . . 3  |-  ( ph  ->  M  e.  NN )
34 fourierdlem101.q . . 3  |-  ( ph  ->  Q  e.  ( P `
 M ) )
3521ralrimiva 2881 . . . 4  |-  ( ph  ->  A. t  e.  (
-u pi [,] pi ) ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) )  e.  CC )
3622fmpt 6053 . . . 4  |-  ( A. t  e.  ( -u pi [,] pi ) ( ( F `  t )  x.  ( ( D `
 N ) `  ( t  -  X
) ) )  e.  CC  <->  G : ( -u pi [,] pi ) --> CC )
3735, 36sylib 196 . . 3  |-  ( ph  ->  G : ( -u pi [,] pi ) --> CC )
3822reseq1i 5275 . . . . . 6  |-  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( t  e.  (
-u pi [,] pi )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
3938a1i 11 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( t  e.  (
-u pi [,] pi )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
40 ioossicc 11622 . . . . . . 7  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
417a1i 11 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  e.  RR )
4241rexrd 9655 . . . . . . . . 9  |-  ( ph  -> 
-u pi  e.  RR* )
4342adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
446a1i 11 . . . . . . . . . 10  |-  ( ph  ->  pi  e.  RR )
4544rexrd 9655 . . . . . . . . 9  |-  ( ph  ->  pi  e.  RR* )
4645adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
4727, 33, 34fourierdlem15 31745 . . . . . . . . 9  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
4847adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
49 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
5043, 46, 48, 49fourierdlem8 31738 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
5140, 50syl5ss 3520 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
52 resmpt 5329 . . . . . 6  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  ->  (
( 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 ) ) ) ) )
5351, 52syl 16 . . . . 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 ) ) ) ) )
54 eqidd 2468 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F `
 t )  x.  ( ( D `  N ) `  (
t  -  X ) ) ) )  =  ( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F `  t )  x.  (
( D `  N
) `  ( t  -  X ) ) ) ) )
5539, 53, 543eqtrd 2512 . . . 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 ) ) ) ) )
562adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : (
-u pi [,] pi )
--> CC )
5756, 51feqresmpt 5928 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) ) )
5857eqcomd 2475 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
59 fourierdlem101.fcn . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
6058, 59eqeltrd 2555 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  t ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC ) )
614adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  RR )  ->  N  e.  NN )
62 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  RR )  ->  s  e.  RR )
6317dirkerre 31718 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  s  e.  RR )  ->  ( ( D `  N ) `  s
)  e.  RR )
6461, 62, 63syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  RR )  ->  ( ( D `  N ) `
 s )  e.  RR )
6564ralrimiva 2881 . . . . . . . . . 10  |-  ( ph  ->  A. s  e.  RR  ( ( D `  N ) `  s
)  e.  RR )
66 eqid 2467 . . . . . . . . . . 11  |-  ( s  e.  RR  |->  ( ( D `  N ) `
 s ) )  =  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )
6766fmpt 6053 . . . . . . . . . 10  |-  ( A. s  e.  RR  (
( D `  N
) `  s )  e.  RR  <->  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) ) : RR --> RR )
6865, 67sylib 196 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> RR )
6968adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) ) : RR --> RR )
70 elioore 11571 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  t  e.  RR )
7170adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
7214adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
7371, 72resubcld 9999 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
t  -  X )  e.  RR )
7473adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
t  -  X )  e.  RR )
7574ralrimiva 2881 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( t  -  X
)  e.  RR )
76 eqid 2467 . . . . . . . . . 10  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( t  -  X ) )  =  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) )
7776fmpt 6053 . . . . . . . . 9  |-  ( A. t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ( t  -  X )  e.  RR  <->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> RR )
7875, 77sylib 196 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> RR )
79 fcompt 6068 . . . . . . . 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 ) ) ) )
8069, 78, 79syl2anc 661 . . . . . . 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 ) ) ) )
81 nfcv 2629 . . . . . . . . . 10  |-  F/_ r
( ( D `  N ) `  (
t  -  X ) )
82 nfcv 2629 . . . . . . . . . 10  |-  F/_ t
( ( D `  N ) `  (
r  -  X ) )
83 oveq1 6302 . . . . . . . . . . 11  |-  ( t  =  r  ->  (
t  -  X )  =  ( r  -  X ) )
8483fveq2d 5876 . . . . . . . . . 10  |-  ( t  =  r  ->  (
( D `  N
) `  ( t  -  X ) )  =  ( ( D `  N ) `  (
r  -  X ) ) )
8581, 82, 84cbvmpt 4543 . . . . . . . . 9  |-  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( t  -  X ) ) )  =  ( r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( r  -  X
) ) )
8685a1i 11 . . . . . . . 8  |-  ( (
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 ) ) ) )
87 eqidd 2468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  e.  RR  |->  ( ( D `  N
) `  s )
)  =  ( s  e.  RR  |->  ( ( D `  N ) `
 s ) ) )
88 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
89 eqidd 2468 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
9083adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  t  =  r )  ->  ( t  -  X
)  =  ( r  -  X ) )
91 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
92 elioore 11571 . . . . . . . . . . . . . . . . . 18  |-  ( r  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  r  e.  RR )
9392adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  r  e.  RR )
9414adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
9593, 94resubcld 9999 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
r  -  X )  e.  RR )
9695adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
r  -  X )  e.  RR )
9789, 90, 91, 96fvmptd 5962 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) `  r
)  =  ( r  -  X ) )
9897adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
9988, 98eqtrd 2508 . . . . . . . . . . . 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  =  ( r  -  X
) )
10099fveq2d 5876 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
10178ffvelrnda 6032 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( t  -  X
) ) `  r
)  e.  RR )
1024ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  N  e.  NN )
10317dirkerre 31718 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( r  -  X
)  e.  RR )  ->  ( ( D `
 N ) `  ( r  -  X
) )  e.  RR )
104102, 96, 103syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  r  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( r  -  X ) )  e.  RR )
10587, 100, 101, 104fvmptd 5962 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
106105eqcomd 2475 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
107106mpteq2dva 4539 . . . . . . . 8  |-  ( (
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 ) ) ) )
10886, 107eqtr2d 2509 . . . . . . 7  |-  ( (
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 ) ) )  =  ( t  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( t  -  X ) ) ) )
10980, 108eqtr2d 2509 . . . . . 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
) ) ) )
110 eqid 2467 . . . . . . . 8  |-  ( t  e.  CC  |->  ( t  -  X ) )  =  ( t  e.  CC  |->  ( t  -  X ) )
111 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  CC )  ->  t  e.  CC )
112 ax-resscn 9561 . . . . . . . . . . . . . . 15  |-  RR  C_  CC
113112, 14sseldi 3507 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  CC )
114113adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  CC )  ->  X  e.  CC )
115111, 114negsubd 9948 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  CC )  ->  ( t  +  -u X )  =  ( t  -  X
) )
116115eqcomd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  CC )  ->  ( t  -  X )  =  ( t  +  -u X ) )
117116mpteq2dva 4539 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  CC  |->  ( t  -  X
) )  =  ( t  e.  CC  |->  ( t  +  -u X
) ) )
118113negcld 9929 . . . . . . . . . . 11  |-  ( ph  -> 
-u X  e.  CC )
119 eqid 2467 . . . . . . . . . . . 12  |-  ( t  e.  CC  |->  ( t  +  -u X ) )  =  ( t  e.  CC  |->  ( t  + 
-u X ) )
120119addccncf 21288 . . . . . . . . . . 11  |-  ( -u X  e.  CC  ->  ( t  e.  CC  |->  ( t  +  -u X
) )  e.  ( CC -cn-> CC ) )
121118, 120syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( t  e.  CC  |->  ( t  +  -u X ) )  e.  ( CC -cn-> CC ) )
122117, 121eqeltrd 2555 . . . . . . . . 9  |-  ( ph  ->  ( t  e.  CC  |->  ( t  -  X
) )  e.  ( CC -cn-> CC ) )
123122adantr 465 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  CC  |->  ( t  -  X ) )  e.  ( CC -cn-> CC ) )
124 ioossre 11598 . . . . . . . . . 10  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
125124, 112sstri 3518 . . . . . . . . 9  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
126125a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  CC )
127112a1i 11 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  RR  C_  CC )
128110, 123, 126, 127, 74cncfmptssg 31531 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( t  -  X ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> RR ) )
129112, 64sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  RR )  ->  ( ( D `  N ) `
 s )  e.  CC )
130129, 66fmptd 6056 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> CC )
131 ssid 3528 . . . . . . . . . . 11  |-  CC  C_  CC
132131a1i 11 . . . . . . . . . 10  |-  ( ph  ->  CC  C_  CC )
13317dirkerf 31720 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  ( D `  N ) : RR --> RR )
1344, 133syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D `  N
) : RR --> RR )
135134feqmptd 5927 . . . . . . . . . . . 12  |-  ( ph  ->  ( D `  N
)  =  ( s  e.  RR  |->  ( ( D `  N ) `
 s ) ) )
136135eqcomd 2475 . . . . . . . . . . 11  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) )  =  ( D `  N ) )
13717dirkercncf 31730 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  ( D `  N )  e.  ( RR -cn-> RR ) )
1384, 137syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( D `  N
)  e.  ( RR
-cn-> RR ) )
139136, 138eqeltrd 2555 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) )  e.  ( RR -cn-> RR ) )
140 cncffvrn 21270 . . . . . . . . . 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 ) )
141132, 139, 140syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  e.  ( RR -cn-> CC )  <-> 
( s  e.  RR  |->  ( ( D `  N ) `  s
) ) : RR --> CC ) )
142130, 141mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( s  e.  RR  |->  ( ( D `  N ) `  s
) )  e.  ( RR -cn-> CC ) )
143142adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  RR  |->  ( ( D `
 N ) `  s ) )  e.  ( RR -cn-> CC ) )
144128, 143cncfco 21279 . . . . . 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 ) )
145109, 144eqeltrd 2555 . . . . 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 ) )
14660, 145mulcncf 21727 . . . 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 ) )
14755, 146eqeltrd 2555 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
148 cncff 21265 . . . . . . . 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 )
14959, 148syl 16 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
150134adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( D `  N ) : RR --> RR )
151124sseli 3505 . . . . . . . . . . . . 13  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
152151adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
15314adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
154152, 153resubcld 9999 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  -  X )  e.  RR )
155 ffvelrn 6030 . . . . . . . . . . 11  |-  ( ( ( D `  N
) : RR --> RR  /\  ( s  -  X
)  e.  RR )  ->  ( ( D `
 N ) `  ( s  -  X
) )  e.  RR )
156150, 154, 155syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( s  -  X ) )  e.  RR )
157112, 156sseldi 3507 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( D `  N
) `  ( s  -  X ) )  e.  CC )
158 eqid 2467 . . . . . . . . 9  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( ( D `  N ) `
 ( s  -  X ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) )
159157, 158fmptd 6056 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
160159adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( D `
 N ) `  ( s  -  X
) ) ) : ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) --> CC )
161 eqid 2467 . . . . . . 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 ) ) )
162 fourierdlem101.r . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
163 iftrue 3951 . . . . . . . . . . . . 13  |-  ( t  =  ( 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
) `  ( ( Q `  i )  -  X ) ) )
164163adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  t  =  ( 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
) `  ( ( Q `  i )  -  X ) ) )
165 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( t  =  ( Q `  i )  ->  (
t  -  X )  =  ( ( Q `
 i )  -  X ) )
166165fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( t  =  ( Q `  i )  ->  (
( D `  N
) `  ( t  -  X ) )  =  ( ( D `  N ) `  (
( Q `  i
)  -  X ) ) )
167166eqcomd 2475 . . . . . . . . . . . . 13  |-  ( t  =  ( Q `  i )  ->  (
( D `  N
) `  ( ( Q `  i )  -  X ) )  =  ( ( D `  N ) `  (
t  -  X ) ) )
168167adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
169 eqidd 2468 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  t  =  ( Q `  i ) )  -> 
( ( D `  N ) `  (
t  -  X ) )  =  ( ( D `  N ) `
 ( t  -  X ) ) )
170164, 168, 1693eqtrd 2512 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  t  =  ( 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 ) ) )
171 iffalse 3954 . . . . . . . . . . . . 13  |-  ( -.  t  =  ( Q `
 i )  ->  if ( t  =  ( Q `  i ) ,  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) )  =  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) )
172171adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  ->  if ( t  =  ( Q `  i ) ,  ( ( D `
 N ) `  ( ( Q `  i )  -  X
) ) ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) )  =  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( D `  N ) `  (
s  -  X ) ) ) `  t
) )
173 eqidd 2468 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) )
174 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( s  =  t  ->  (
s  -  X )  =  ( t  -  X ) )
175174fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
( D `  N
) `  ( s  -  X ) )  =  ( ( D `  N ) `  (
t  -  X ) ) )
176175adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 ) ) )
177 simpl 457 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  =  ( Q `  i ) )  -> 
t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )
178 vex 3121 . . . . . . . . . . . . . . . . . . 19  |-  t  e. 
_V
179 elsncg 4056 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  _V  ->  (
t  e.  { ( Q `  i ) }  <->  t  =  ( Q `  i ) ) )
180178, 179ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  { ( Q `
 i ) }  <-> 
t  =  ( Q `
 i ) )
181180notbii 296 . . . . . . . . . . . . . . . . 17  |-  ( -.  t  e.  { ( Q `  i ) }  <->  -.  t  =  ( Q `  i ) )
182181biimpri 206 . . . . . . . . . . . . . . . 16  |-  ( -.  t  =  ( Q `
 i )  ->  -.  t  e.  { ( Q `  i ) } )
183182adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  =  ( Q `  i ) )  ->  -.  t  e.  { ( Q `  i ) } )
184 elun 3650 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } )  <-> 
( t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  \/  t  e.  {
( Q `  i
) } ) )
185184biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } )  ->  ( t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  \/  t  e. 
{ ( Q `  i ) } ) )
186185orcomd 388 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } )  ->  ( t  e. 
{ ( Q `  i ) }  \/  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
187186adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  e.  { ( Q `  i ) } )  ->  ( t  e. 
{ ( Q `  i ) }  \/  t  e.  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
188 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  e.  { ( Q `  i ) } )  ->  -.  t  e.  { ( Q `  i
) } )
189 pm2.53 373 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  { ( Q `  i ) }  \/  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( -.  t  e.  { ( Q `  i ) }  ->  t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
190187, 188, 189sylc 60 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  e.  { ( Q `  i ) } )  ->  t  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
191177, 183, 190syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } )  /\  -.  t  =  ( Q `  i ) )  -> 
t  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
192191adantll 713 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) )
193134ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( D `  N ) : RR --> RR )
194 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  =  ( Q `  i
) )  ->  t  =  ( Q `  i ) )
19512ssriv 3513 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u pi [,] pi )  C_  RR
196 fzossfz 11826 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0..^ M )  C_  (
0 ... M )
197196, 49sseldi 3507 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
198 ffvelrn 6030 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Q : ( 0 ... M ) --> (
-u pi [,] pi )  /\  i  e.  ( 0 ... M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
19948, 197, 198syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
200195, 199sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
201200adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  =  ( Q `  i
) )  ->  ( Q `  i )  e.  RR )
202194, 201eqeltrd 2555 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  =  ( Q `  i
) )  ->  t  e.  RR )
203202adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  t  =  ( Q `  i ) )  -> 
t  e.  RR )
204192, 70syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
t  e.  RR )
205203, 204pm2.61dan 789 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  t  e.  RR )
20614ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  X  e.  RR )
207205, 206resubcld 9999 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( t  -  X )  e.  RR )
208 ffvelrn 6030 . . . . . . . . . . . . . . 15  |-  ( ( ( D `  N
) : RR --> RR  /\  ( t  -  X
)  e.  RR )  ->  ( ( D `
 N ) `  ( t  -  X
) )  e.  RR )
209193, 207, 208syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( ( D `
 N ) `  ( t  -  X
) )  e.  RR )
210209adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
( ( D `  N ) `  (
t  -  X ) )  e.  RR )
211173, 176, 192, 210fvmptd 5962 . . . . . . . . . . . 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
) ) ) `  t )  =  ( ( D `  N
) `  ( t  -  X ) ) )
212 eqidd 2468 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( Q `  i ) )  -> 
( ( D `  N ) `  (
t  -  X ) )  =  ( ( D `  N ) `
 ( t  -  X ) ) )
213172, 211, 2123eqtrd 2512 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  -.  t  =  ( 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 ) ) )
214170, 213pm2.61dan 789 . . . . . . . . . 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 ) ) )
215214mpteq2dva 4539 . . . . . . . . 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 ) ) ) )
216134adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D `  N ) : RR --> RR )
217 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
218 elun 3650 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } )  <-> 
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  \/  s  e.  {
( Q `  i
) } ) )
219217, 218sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  \/  s  e. 
{ ( Q `  i ) } ) )
220219adantlr 714 . . . . . . . . . . . . . . . . . 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 ) } ) )
221151a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  ->  s  e.  RR ) )
222 elsni 4058 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  { ( Q `
 i ) }  ->  s  =  ( Q `  i ) )
223222adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e. 
{ ( Q `  i ) } )  ->  s  =  ( Q `  i ) )
224200adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e. 
{ ( Q `  i ) } )  ->  ( Q `  i )  e.  RR )
225223, 224eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e. 
{ ( Q `  i ) } )  ->  s  e.  RR )
226225ex 434 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e. 
{ ( Q `  i ) }  ->  s  e.  RR ) )
227226adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  e. 
{ ( Q `  i ) }  ->  s  e.  RR ) )
228 pm3.44 511 . . . . . . . . . . . . . . . . . . 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 ) )
229221, 227, 228syl2anc 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 ) )
230220, 229mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  s  e.  RR )
23114ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  X  e.  RR )
232230, 231resubcld 9999 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  ->  ( s  -  X )  e.  RR )
233 eqid 2467 . . . . . . . . . . . . . . . 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 ) )
234232, 233fmptd 6056 . . . . . . . . . . . . . . 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 )
235 fcompt 6068 . . . . . . . . . . . . . . 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
) ) ) )
236216, 234, 235syl2anc 661 . . . . . . . . . . . . . 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 ) ) ) )
237 eqidd 2468 . . . . . . . . . . . . . . . . 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
) ) )
238174adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  t  e.  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  u.  { ( Q `
 i ) } ) )  /\  s  =  t )  -> 
( s  -  X
)  =  ( t  -  X ) )
239 simpr 461 . . . . . . . . . . . . . . . . 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 ) } ) )
240237, 238, 239, 207fvmptd 5962 . . . . . . . . . . . . . . . 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 ) )
241240fveq2d 5876 . . . . . . . . . . . . . . 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 ) ) )
242241mpteq2dva 4539 . . . . . . . . . . . . . 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 ) ) ) )
243236, 242eqtr2d 2509 . . . . . . . . . . . . 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 ) ) ) )
244 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( s  e.  CC  |->  ( s  -  X ) )  =  ( s  e.  CC  |->  ( s  -  X ) )
245 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  CC )  ->  s  e.  CC )
246113adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  CC )  ->  X  e.  CC )
247 negsub 9879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  CC  /\  X  e.  CC )  ->  ( s  +  -u X )  =  ( s  -  X ) )
248245, 246, 247syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  s  e.  CC )  ->  ( s  +  -u X )  =  ( s  -  X
) )
249248eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  s  e.  CC )  ->  ( s  -  X )  =  ( s  +  -u X ) )
250249mpteq2dva 4539 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( s  e.  CC  |->  ( s  -  X
) )  =  ( s  e.  CC  |->  ( s  +  -u X
) ) )
251 eqid 2467 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  CC  |->  ( s  +  -u X ) )  =  ( s  e.  CC  |->  ( s  + 
-u X ) )
252251addccncf 21288 . . . . . . . . . . . . . . . . . . 19  |-  ( -u X  e.  CC  ->  ( s  e.  CC  |->  ( s  +  -u X
) )  e.  ( CC -cn-> CC ) )
253118, 252syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( s  e.  CC  |->  ( s  +  -u X ) )  e.  ( CC -cn-> CC ) )
254250, 253eqeltrd 2555 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( s  e.  CC  |->  ( s  -  X
) )  e.  ( CC -cn-> CC ) )
255254adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  CC  |->  ( s  -  X ) )  e.  ( CC -cn-> CC ) )
256112, 200sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
257256snssd 4178 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  { ( Q `
 i ) } 
C_  CC )
258126, 257jca 532 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC  /\  { ( Q `
 i ) } 
C_  CC ) )
259 unss 3683 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC  /\  {
( Q `  i
) }  C_  CC ) 
<->  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } )  C_  CC )
260258, 259sylib 196 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u. 
{ ( Q `  i ) } ) 
C_  CC )
261244, 255, 260, 127, 232cncfmptssg 31531 . . . . . . . . . . . . . . 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 ) )
262135, 142eqeltrd 2555 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D `  N
)  e.  ( RR
-cn-> CC ) )
263262adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( D `  N )  e.  ( RR -cn-> CC ) )
264261, 263cncfco 21279 . . . . . . . . . . . . . 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 ) )
265131a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  CC  C_  CC )
266 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
267 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  i
) } ) )  =  ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
268266cnfldtop 21159 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  Top
269 unicntop 31336 . . . . . . . . . . . . . . . . . . 19  |-  CC  =  U. ( TopOpen ` fld )
270269restid 14706 . . . . . . . . . . . . . . . . . 18  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
271268, 270ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
272271eqcomi 2480 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
273266, 267, 272cncfcn 21281 . . . . . . . . . . . . . . 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 )
) )
274260, 265, 273syl2anc 661 . . . . . . . . . . . . . 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 )
) )
275264, 274eleqtrd 2557 . . . . . . . . . . . . 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 )
) )
276243, 275eqeltrd 2555 . . . . . . . . . . . 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 ) ) )
277266cnfldtopon 21158 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
278277a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( TopOpen ` fld )  e.  (TopOn `  CC ) )
279 resttopon 19530 . . . . . . . . . . . . . 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 ) } ) ) )
280278, 260, 279syl2anc 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 ) } ) ) )
281 cncnp 19649 . . . . . . . . . . . . 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
) ) ) )
282280, 278, 281syl2anc 661 . . . . . . . . . . . 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 )
) ) )
283276, 282mpbid 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 )
) )
284283simprd 463 . . . . . . . . . 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
) )
285 eqidd 2468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( Q `  i ) )
286 elsncg 4056 . . . . . . . . . . . . . 14  |-  ( ( Q `  i )  e.  RR  ->  (
( Q `  i
)  e.  { ( Q `  i ) }  <->  ( Q `  i )  =  ( Q `  i ) ) )
287200, 286syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e. 
{ ( Q `  i ) }  <->  ( Q `  i )  =  ( Q `  i ) ) )
288285, 287mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  {
( Q `  i
) } )
289288olcd 393 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  \/  ( Q `
 i )  e. 
{ ( Q `  i ) } ) )
290 elun 3650 . . . . . . . . . . 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
) } ) )
291289, 290sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  i ) } ) )
292 fveq2 5872 . . . . . . . . . . . 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 ) ) )
293292eleq2d 2537 . . . . . . . . . . 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 )
) ) )
294293rspccva 3218 . . . . . . . . . 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 ) ) )
295284, 291, 294syl2anc 661 . . . . . . . . 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 ) ) )
296215, 295eqeltrd 2555 . . . . . . . 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