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

Theorem fourierdlem111 31841
Description: The fourier partial sum for  F is the sum of two integrals, with the same integrand involving  F and the Dirichlet Kernel 
D, but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem111.a  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( cos `  (
n  x.  t ) ) )  _d t  /  pi ) )
fourierdlem111.b  |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( sin `  (
n  x.  t ) ) )  _d t  /  pi ) )
fourierdlem111.s  |-  S  =  ( m  e.  NN  |->  ( ( ( A `
 0 )  / 
2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )
fourierdlem111.d  |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
fourierdlem111.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 ) ) ) } )
fourierdlem111.m  |-  ( ph  ->  M  e.  NN )
fourierdlem111.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem111.x  |-  ( ph  ->  X  e.  RR )
fourierdlem111.6  |-  ( ph  ->  F : RR --> RR )
fourierdlem111.fper  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fourierdlem111.g  |-  G  =  ( x  e.  RR  |->  ( ( F `  ( X  +  x
) )  x.  (
( D `  n
) `  x )
) )
fourierdlem111.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem111.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem111.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem111.t  |-  T  =  ( 2  x.  pi )
fourierdlem111.o  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  -  X )  /\  (
p `  m )  =  ( pi  -  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem111.14  |-  W  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  -  X
) )
Assertion
Ref Expression
fourierdlem111  |-  ( (
ph  /\  n  e.  NN )  ->  ( S `
 n )  =  ( S. ( -u pi (,) 0 ) ( ( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  _d s  +  S. ( 0 (,) pi ) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) )  _d s ) )
Distinct variable groups:    A, m, n    B, m    D, i, m, y    D, s, t, i, y    x, D, i, s, y    i, F, n, s, t, y   
x, F, n    i, G, s, x    L, s, t    x, L    i, M, m, p    M, s, t, y    x, M    Q, i, p    Q, s, t, y    x, Q    R, s, t    x, R    T, s, x    i, W, m, p    W, s, x, y    i, X, m, n, y    X, p    X, s, t    x, X    ph, i, m, n, y    ph, s, t    ph, x
Allowed substitution hints:    ph( p)    A( x, y, t, i, s, p)    B( x, y, t, i, n, s, p)    D( n, p)    P( x, y, t, i, m, n, s, p)    Q( m, n)    R( y, i, m, n, p)    S( x, y, t, i, m, n, s, p)    T( y,
t, i, m, n, p)    F( m, p)    G( y, t, m, n, p)    L( y, i, m, n, p)    M( n)    O( x, y, t, i, m, n, s, p)    W( t, n)

Proof of Theorem fourierdlem111
Dummy variables  k 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2539 . . . . . 6  |-  ( k  =  n  ->  (
k  e.  NN  <->  n  e.  NN ) )
21anbi2d 703 . . . . 5  |-  ( k  =  n  ->  (
( ph  /\  k  e.  NN )  <->  ( ph  /\  n  e.  NN ) ) )
3 fveq2 5872 . . . . . 6  |-  ( k  =  n  ->  ( S `  k )  =  ( S `  n ) )
4 fveq2 5872 . . . . . . . . . 10  |-  ( k  =  n  ->  ( D `  k )  =  ( D `  n ) )
54fveq1d 5874 . . . . . . . . 9  |-  ( k  =  n  ->  (
( D `  k
) `  ( t  -  X ) )  =  ( ( D `  n ) `  (
t  -  X ) ) )
65oveq2d 6311 . . . . . . . 8  |-  ( k  =  n  ->  (
( F `  t
)  x.  ( ( D `  k ) `
 ( t  -  X ) ) )  =  ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) ) )
76adantr 465 . . . . . . 7  |-  ( ( k  =  n  /\  t  e.  ( -u pi (,) pi ) )  -> 
( ( F `  t )  x.  (
( D `  k
) `  ( t  -  X ) ) )  =  ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) ) )
87itgeq2dv 22056 . . . . . 6  |-  ( k  =  n  ->  S. ( -u pi (,) pi ) ( ( F `
 t )  x.  ( ( D `  k ) `  (
t  -  X ) ) )  _d t  =  S. ( -u pi (,) pi ) ( ( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  _d t )
93, 8eqeq12d 2489 . . . . 5  |-  ( k  =  n  ->  (
( S `  k
)  =  S. (
-u pi (,) pi ) ( ( F `
 t )  x.  ( ( D `  k ) `  (
t  -  X ) ) )  _d t  <-> 
( S `  n
)  =  S. (
-u pi (,) pi ) ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) )  _d t ) )
102, 9imbi12d 320 . . . 4  |-  ( k  =  n  ->  (
( ( ph  /\  k  e.  NN )  ->  ( S `  k
)  =  S. (
-u pi (,) pi ) ( ( F `
 t )  x.  ( ( D `  k ) `  (
t  -  X ) ) )  _d t )  <->  ( ( ph  /\  n  e.  NN )  ->  ( S `  n )  =  S. ( -u pi (,) pi ) ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) )  _d t ) ) )
11 fourierdlem111.6 . . . . . 6  |-  ( ph  ->  F : RR --> RR )
1211adantr 465 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  F : RR
--> RR )
13 eqid 2467 . . . . 5  |-  ( -u pi (,) pi )  =  ( -u pi (,) pi )
14 elioore 11571 . . . . . . . . . 10  |-  ( s  e.  ( -u pi (,) pi )  ->  s  e.  RR )
1514ssriv 3513 . . . . . . . . 9  |-  ( -u pi (,) pi )  C_  RR
1615a1i 11 . . . . . . . 8  |-  ( ph  ->  ( -u pi (,) pi )  C_  RR )
1711, 16feqresmpt 5928 . . . . . . 7  |-  ( ph  ->  ( F  |`  ( -u pi (,) pi ) )  =  ( x  e.  ( -u pi (,) pi )  |->  ( F `
 x ) ) )
18 ioossicc 11622 . . . . . . . . 9  |-  ( -u pi (,) pi )  C_  ( -u pi [,] pi )
1918a1i 11 . . . . . . . 8  |-  ( ph  ->  ( -u pi (,) pi )  C_  ( -u pi [,] pi ) )
20 ioombl 21843 . . . . . . . . 9  |-  ( -u pi (,) pi )  e. 
dom  vol
2120a1i 11 . . . . . . . 8  |-  ( ph  ->  ( -u pi (,) pi )  e.  dom  vol )
2211adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u pi [,] pi ) )  ->  F : RR --> RR )
23 pire 22718 . . . . . . . . . . . . . . . . 17  |-  pi  e.  RR
2423renegcli 9892 . . . . . . . . . . . . . . . 16  |-  -u pi  e.  RR
2524, 23pm3.2i 455 . . . . . . . . . . . . . . 15  |-  ( -u pi  e.  RR  /\  pi  e.  RR )
26 elicc2 11601 . . . . . . . . . . . . . . 15  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( t  e.  ( -u pi [,] pi )  <->  ( t  e.  RR  /\  -u pi  <_  t  /\  t  <_  pi ) ) )
2725, 26ax-mp 5 . . . . . . . . . . . . . 14  |-  ( t  e.  ( -u pi [,] pi )  <->  ( t  e.  RR  /\  -u pi  <_  t  /\  t  <_  pi ) )
2827biimpi 194 . . . . . . . . . . . . 13  |-  ( t  e.  ( -u pi [,] pi )  ->  (
t  e.  RR  /\  -u pi  <_  t  /\  t  <_  pi ) )
2928simp1d 1008 . . . . . . . . . . . 12  |-  ( t  e.  ( -u pi [,] pi )  ->  t  e.  RR )
3029ssriv 3513 . . . . . . . . . . 11  |-  ( -u pi [,] pi )  C_  RR
3130a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi [,] pi )  C_  RR )
3231sselda 3509 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u pi [,] pi ) )  ->  x  e.  RR )
3322, 32ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( -u pi [,] pi ) )  ->  ( F `  x )  e.  RR )
3411, 31feqresmpt 5928 . . . . . . . . . 10  |-  ( ph  ->  ( F  |`  ( -u pi [,] pi ) )  =  ( x  e.  ( -u pi [,] pi )  |->  ( F `
 x ) ) )
3534eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  (
-u pi [,] pi )  |->  ( F `  x ) )  =  ( F  |`  ( -u pi [,] pi ) ) )
36 fourierdlem111.p . . . . . . . . . 10  |-  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 ) ) ) } )
37 fourierdlem111.m . . . . . . . . . 10  |-  ( ph  ->  M  e.  NN )
38 fourierdlem111.q . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( P `
 M ) )
39 ax-resscn 9561 . . . . . . . . . . . . 13  |-  RR  C_  CC
4039a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  CC )
4111, 40fssd 5746 . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> CC )
42 fssres 5757 . . . . . . . . . . 11  |-  ( ( F : RR --> CC  /\  ( -u pi [,] pi )  C_  RR )  -> 
( F  |`  ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
4341, 31, 42syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( F  |`  ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
44 ioossicc 11622 . . . . . . . . . . . . 13  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
4524rexri 9658 . . . . . . . . . . . . . . 15  |-  -u pi  e.  RR*
4645a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
4723rexri 9658 . . . . . . . . . . . . . . 15  |-  pi  e.  RR*
4847a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
4936, 37, 38fourierdlem15 31745 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
5049adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
51 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
5246, 48, 50, 51fourierdlem8 31738 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
5344, 52syl5ss 3520 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
54 resabs1 5308 . . . . . . . . . . . 12  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  ( -u pi [,] pi )  ->  (
( F  |`  ( -u pi [,] pi ) )  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
5553, 54syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
56 fourierdlem111.fcn . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
5755, 56eqeltrd 2555 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
58 fourierdlem111.r . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
5955oveq1d 6310 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )
6059eleq2d 2537 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( R  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) )  <-> 
R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) ) )
6158, 60mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
62 fourierdlem111.l . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
6355oveq1d 6310 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
6463eleq2d 2537 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( L  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) )  <-> 
L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) ) )
6562, 64mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
6636, 37, 38, 43, 57, 61, 65fourierdlem69 31799 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( -u pi [,] pi ) )  e.  L^1 )
6735, 66eqeltrd 2555 . . . . . . . 8  |-  ( ph  ->  ( x  e.  (
-u pi [,] pi )  |->  ( F `  x ) )  e.  L^1 )
6819, 21, 33, 67iblss 22079 . . . . . . 7  |-  ( ph  ->  ( x  e.  (
-u pi (,) pi )  |->  ( F `  x ) )  e.  L^1 )
6917, 68eqeltrd 2555 . . . . . 6  |-  ( ph  ->  ( F  |`  ( -u pi (,) pi ) )  e.  L^1 )
7069adantr 465 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( F  |`  ( -u pi (,) pi ) )  e.  L^1 )
71 fourierdlem111.a . . . . 5  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( cos `  (
n  x.  t ) ) )  _d t  /  pi ) )
72 fourierdlem111.b . . . . 5  |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( sin `  (
n  x.  t ) ) )  _d t  /  pi ) )
73 fourierdlem111.x . . . . . 6  |-  ( ph  ->  X  e.  RR )
7473adantr 465 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  RR )
75 fourierdlem111.s . . . . 5  |-  S  =  ( m  e.  NN  |->  ( ( ( A `
 0 )  / 
2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )
76 fourierdlem111.d . . . . 5  |-  D  =  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
77 simpr 461 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
7812, 13, 70, 71, 72, 74, 75, 76, 77fourierdlem83 31813 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  =  S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( ( D `
 k ) `  ( t  -  X
) ) )  _d t )
7910, 78chvarv 1983 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  ( S `
 n )  =  S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( ( D `
 n ) `  ( t  -  X
) ) )  _d t )
8024a1i 11 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  -u pi  e.  RR )
8123a1i 11 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  pi  e.  RR )
8241adantr 465 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  F : RR --> CC )
8329adantl 466 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  t  e.  RR )
84 ffvelrn 6030 . . . . . . . 8  |-  ( ( F : RR --> CC  /\  t  e.  RR )  ->  ( F `  t
)  e.  CC )
8582, 83, 84syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
8685adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
8776dirkerf 31720 . . . . . . . . . 10  |-  ( n  e.  NN  ->  ( D `  n ) : RR --> RR )
8887adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( D `
 n ) : RR --> RR )
8988adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  ( D `  n ) : RR --> RR )
9073adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  X  e.  RR )
9183, 90resubcld 9999 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
t  -  X )  e.  RR )
9291adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
t  -  X )  e.  RR )
93 ffvelrn 6030 . . . . . . . 8  |-  ( ( ( D `  n
) : RR --> RR  /\  ( t  -  X
)  e.  RR )  ->  ( ( D `
 n ) `  ( t  -  X
) )  e.  RR )
9489, 92, 93syl2anc 661 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  n
) `  ( t  -  X ) )  e.  RR )
9539, 94sseldi 3507 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  n
) `  ( t  -  X ) )  e.  CC )
9686, 95mulcld 9628 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  e.  CC )
9780, 81, 96itgioo 22090 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  S. (
-u pi (,) pi ) ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) )  _d t  =  S. ( -u pi [,] pi ) ( ( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  _d t )
98 fvres 5886 . . . . . . . 8  |-  ( t  e.  ( -u pi [,] pi )  ->  (
( F  |`  ( -u pi [,] pi ) ) `  t )  =  ( F `  t ) )
9998eqcomd 2475 . . . . . . 7  |-  ( t  e.  ( -u pi [,] pi )  ->  ( F `  t )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  t
) )
10099oveq1d 6310 . . . . . 6  |-  ( t  e.  ( -u pi [,] pi )  ->  (
( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  =  ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) ) )
101100adantl 466 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  =  ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) ) )
102101itgeq2dv 22056 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  S. (
-u pi [,] pi ) ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) )  _d t  =  S. ( -u pi [,] pi ) ( ( ( F  |`  ( -u pi [,] pi ) ) `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  _d t )
103 nfcv 2629 . . . . . . . 8  |-  F/_ m
( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
104 nfcv 2629 . . . . . . . 8  |-  F/_ n
( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )
105 simpl 457 . . . . . . . . . . . . 13  |-  ( ( n  =  m  /\  y  e.  RR )  ->  n  =  m )
106105oveq2d 6311 . . . . . . . . . . . 12  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( 2  x.  n
)  =  ( 2  x.  m ) )
107106oveq1d 6310 . . . . . . . . . . 11  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( 2  x.  n )  +  1 )  =  ( ( 2  x.  m )  +  1 ) )
108107oveq1d 6310 . . . . . . . . . 10  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( ( 2  x.  n )  +  1 )  /  (
2  x.  pi ) )  =  ( ( ( 2  x.  m
)  +  1 )  /  ( 2  x.  pi ) ) )
109105oveq1d 6310 . . . . . . . . . . . . 13  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( n  +  ( 1  /  2 ) )  =  ( m  +  ( 1  / 
2 ) ) )
110109oveq1d 6310 . . . . . . . . . . . 12  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( n  +  ( 1  /  2
) )  x.  y
)  =  ( ( m  +  ( 1  /  2 ) )  x.  y ) )
111110fveq2d 5876 . . . . . . . . . . 11  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  =  ( sin `  ( ( m  +  ( 1  /  2
) )  x.  y
) ) )
112111oveq1d 6310 . . . . . . . . . 10  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) )  =  ( ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )
113108, 112ifeq12d 3965 . . . . . . . . 9  |-  ( ( n  =  m  /\  y  e.  RR )  ->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n
)  +  1 )  /  ( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) )  =  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  /  ( 2  x.  pi ) ) ,  ( ( sin `  ( ( m  +  ( 1  /  2
) )  x.  y
) )  /  (
( 2  x.  pi )  x.  ( sin `  ( y  /  2
) ) ) ) ) )
114113mpteq2dva 4539 . . . . . . . 8  |-  ( n  =  m  ->  (
y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) )  =  ( y  e.  RR  |->  if ( ( y  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
115103, 104, 114cbvmpt 4543 . . . . . . 7  |-  ( n  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  (
2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )  =  ( m  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
11676, 115eqtri 2496 . . . . . 6  |-  D  =  ( m  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( m  +  ( 1  /  2 ) )  x.  y ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
y  /  2 ) ) ) ) ) ) )
117 nfcv 2629 . . . . . . 7  |-  F/_ t
( ( ( F  |`  ( -u pi [,] pi ) ) `  s
)  x.  ( ( D `  n ) `
 ( s  -  X ) ) )
118 nfcv 2629 . . . . . . 7  |-  F/_ s
( ( ( F  |`  ( -u pi [,] pi ) ) `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )
119 fveq2 5872 . . . . . . . 8  |-  ( s  =  t  ->  (
( F  |`  ( -u pi [,] pi ) ) `  s )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  t
) )
120 oveq1 6302 . . . . . . . . 9  |-  ( s  =  t  ->  (
s  -  X )  =  ( t  -  X ) )
121120fveq2d 5876 . . . . . . . 8  |-  ( s  =  t  ->  (
( D `  n
) `  ( s  -  X ) )  =  ( ( D `  n ) `  (
t  -  X ) ) )
122119, 121oveq12d 6313 . . . . . . 7  |-  ( s  =  t  ->  (
( ( F  |`  ( -u pi [,] pi ) ) `  s
)  x.  ( ( D `  n ) `
 ( s  -  X ) ) )  =  ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) ) )
123117, 118, 122cbvmpt 4543 . . . . . 6  |-  ( s  e.  ( -u pi [,] pi )  |->  ( ( ( F  |`  ( -u pi [,] pi ) ) `  s )  x.  ( ( D `
 n ) `  ( s  -  X
) ) ) )  =  ( t  e.  ( -u pi [,] pi )  |->  ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  ( ( D `
 n ) `  ( t  -  X
) ) ) )
12438adantr 465 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  Q  e.  ( P `  M
) )
12537adantr 465 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  M  e.  NN )
126 simpr 461 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
12773adantr 465 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  X  e.  RR )
12843adantr 465 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( F  |`  ( -u pi [,] pi ) ) : (
-u pi [,] pi )
--> CC )
12957adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -u pi [,] pi ) )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
13061adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
13165adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
132116, 36, 123, 124, 125, 126, 127, 128, 129, 130, 131fourierdlem101 31831 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  S. (
-u pi [,] pi ) ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) )  _d t  =  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)  _d y )
133 oveq2 6303 . . . . . . . . . 10  |-  ( s  =  y  ->  ( X  +  s )  =  ( X  +  y ) )
134133fveq2d 5876 . . . . . . . . 9  |-  ( s  =  y  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  y
) ) )
135 fveq2 5872 . . . . . . . . 9  |-  ( s  =  y  ->  (
( D `  n
) `  s )  =  ( ( D `
 n ) `  y ) )
136134, 135oveq12d 6313 . . . . . . . 8  |-  ( s  =  y  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  =  ( ( F `
 ( X  +  y ) )  x.  ( ( D `  n ) `  y
) ) )
137 nfcv 2629 . . . . . . . 8  |-  F/_ y
( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
)
138 nfcv 2629 . . . . . . . 8  |-  F/_ s
( ( F `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)
139136, 137, 138cbvitg 22050 . . . . . . 7  |-  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) )  _d s  =  S. ( (
-u pi  -  X
) (,) ( pi 
-  X ) ) ( ( F `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)  _d y
140139a1i 11 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) )  _d s  =  S. ( (
-u pi  -  X
) (,) ( pi 
-  X ) ) ( ( F `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)  _d y )
14124a1i 11 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  e.  RR )
142141, 73jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi  e.  RR  /\  X  e.  RR ) )
143 resubcl 9895 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR  /\  X  e.  RR )  ->  ( -u pi  -  X )  e.  RR )
144142, 143syl 16 . . . . . . . . 9  |-  ( ph  ->  ( -u pi  -  X )  e.  RR )
145144adantr 465 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( -u pi  -  X )  e.  RR )
14623a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  pi  e.  RR )
147146, 73jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( pi  e.  RR  /\  X  e.  RR ) )
148 resubcl 9895 . . . . . . . . . 10  |-  ( ( pi  e.  RR  /\  X  e.  RR )  ->  ( pi  -  X
)  e.  RR )
149147, 148syl 16 . . . . . . . . 9  |-  ( ph  ->  ( pi  -  X
)  e.  RR )
150149adantr 465 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( pi 
-  X )  e.  RR )
15141adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  F : RR --> CC )
15273adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  X  e.  RR )
153 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )
154144adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( -u pi  -  X )  e.  RR )
155149adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
pi  -  X )  e.  RR )
156 elicc2 11601 . . . . . . . . . . . . . . 15  |-  ( ( ( -u pi  -  X )  e.  RR  /\  ( pi  -  X
)  e.  RR )  ->  ( y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
)  <->  ( y  e.  RR  /\  ( -u pi  -  X )  <_ 
y  /\  y  <_  ( pi  -  X ) ) ) )
157154, 155, 156syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
y  e.  ( (
-u pi  -  X
) [,] ( pi 
-  X ) )  <-> 
( y  e.  RR  /\  ( -u pi  -  X )  <_  y  /\  y  <_  ( pi 
-  X ) ) ) )
158153, 157mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
y  e.  RR  /\  ( -u pi  -  X
)  <_  y  /\  y  <_  ( pi  -  X ) ) )
159158simp1d 1008 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  e.  RR )
160152, 159readdcld 9635 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  e.  RR )
161 ffvelrn 6030 . . . . . . . . . . 11  |-  ( ( F : RR --> CC  /\  ( X  +  y
)  e.  RR )  ->  ( F `  ( X  +  y
) )  e.  CC )
162151, 160, 161syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  e.  CC )
163162adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  e.  CC )
16488adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( D `  n ) : RR --> RR )
165159adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  e.  RR )
166 ffvelrn 6030 . . . . . . . . . . 11  |-  ( ( ( D `  n
) : RR --> RR  /\  y  e.  RR )  ->  ( ( D `  n ) `  y
)  e.  RR )
167164, 165, 166syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( D `  n
) `  y )  e.  RR )
16839, 167sseldi 3507 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( D `  n
) `  y )  e.  CC )
169163, 168mulcld 9628 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( F `  ( X  +  y )
)  x.  ( ( D `  n ) `
 y ) )  e.  CC )
170145, 150, 169itgioo 22090 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  y ) )  x.  ( ( D `  n ) `  y
) )  _d y  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( ( F `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)  _d y )
17139, 73sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  X  e.  CC )
17239, 146sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  pi  e.  CC )
173172negcld 9929 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
-u pi  e.  CC )
174171, 173pncan3d 9945 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( X  +  (
-u pi  -  X
) )  =  -u pi )
175174eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u pi  =  ( X  +  ( -u pi  -  X ) ) )
176175adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  -u pi  =  ( X  +  ( -u pi  -  X
) ) )
177158simp2d 1009 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( -u pi  -  X )  <_  y )
178154, 159, 152, 177leadd2dd 10179 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  ( -u pi  -  X ) )  <_ 
( X  +  y ) )
179176, 178eqbrtrd 4473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  -u pi  <_  ( X  +  y ) )
180158simp3d 1010 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  <_  ( pi  -  X
) )
181159, 155, 152, 180leadd2dd 10179 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  <_  ( X  +  ( pi  -  X ) ) )
182171adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  X  e.  CC )
183172adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  pi  e.  CC )
184182, 183pncan3d 9945 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  ( pi  -  X ) )  =  pi )
185181, 184breqtrd 4477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  <_  pi )
186160, 179, 1853jca 1176 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( X  +  y )  e.  RR  /\  -u pi  <_  ( X  +  y )  /\  ( X  +  y
)  <_  pi )
)
18724a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  -u pi  e.  RR )
18823a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  pi  e.  RR )
189 elicc2 11601 . . . . . . . . . . . . . 14  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( ( X  +  y )  e.  ( -u pi [,] pi )  <->  ( ( X  +  y )  e.  RR  /\  -u pi  <_  ( X  +  y )  /\  ( X  +  y )  <_  pi ) ) )
190187, 188, 189syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( X  +  y )  e.  ( -u pi [,] pi )  <->  ( ( X  +  y )  e.  RR  /\  -u pi  <_  ( X  +  y )  /\  ( X  +  y )  <_  pi ) ) )
191186, 190mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  e.  ( -u pi [,] pi ) )
192 fvres 5886 . . . . . . . . . . . 12  |-  ( ( X  +  y )  e.  ( -u pi [,] pi )  ->  (
( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y ) )  =  ( F `  ( X  +  y
) ) )
193191, 192syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y ) )  =  ( F `  ( X  +  y
) ) )
194193eqcomd 2475 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y )
) )
195194adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y )
) )
196195oveq1d 6310 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( F `  ( X  +  y )
)  x.  ( ( D `  n ) `
 y ) )  =  ( ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
) )
197196itgeq2dv 22056 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( ( F `
 ( X  +  y ) )  x.  ( ( D `  n ) `  y
) )  _d y  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y )
)  x.  ( ( D `  n ) `
 y ) )  _d y )
198170, 197eqtrd 2508 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  y ) )  x.  ( ( D `  n ) `  y
) )  _d y  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y )
)  x.  ( ( D `  n ) `
 y ) )  _d y )
199140, 198eqtr2d 2509 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)  _d y  =  S. ( ( -u pi  -  X ) (,) ( pi  -  X
) ) ( ( F `  ( X  +  s ) )  x.  ( ( D `
 n ) `  s ) )  _d s )
200132, 199eqtrd 2508 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  S. (
-u pi [,] pi ) ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) )  _d t  =  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) )  _d s )
20197, 102, 2003eqtrd 2512 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  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 )
202 elioore 11571 . . . . . . . . 9  |-  ( s  e.  ( ( -u pi  -  X ) (,) ( pi  -  X
) )  ->  s  e.  RR )
203202adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  s  e.  RR )
20441adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  F : RR --> CC )
20573adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  X  e.  RR )
206202adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  s  e.  RR )
207205, 206readdcld 9635 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( X  +  s )  e.  RR )
208204, 207ffvelrnd 6033 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( F `  ( X  +  s ) )  e.  CC )
209208adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( F `  ( X  +  s ) )  e.  CC )
21039a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  RR  C_  CC )
21188adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( D `  n ) : RR --> RR )
212211, 203ffvelrnd 6033 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( D `  n
) `  s )  e.  RR )
213210, 212sseldd 3510 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( D `  n
) `  s )  e.  CC )
214209, 213mulcld 9628 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  e.  CC )
215 fourierdlem111.g . . . . . . . . . 10  |-  G  =  ( x  e.  RR  |->  ( ( F `  ( X  +  x
) )  x.  (
( D `  n
) `  x )
) )
216 oveq2 6303 . . . . . . . . . . . . 13  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
217216fveq2d 5876 . . . . . . . . . . . 12  |-  ( x  =  s  ->  ( F `  ( X  +  x ) )  =  ( F `  ( X  +  s )
) )
218 fveq2 5872 . . . . . . . . . . . 12  |-  ( x  =  s  ->  (
( D `  n
) `  x )  =  ( ( D `
 n ) `  s ) )
219217, 218oveq12d 6313 . . . . . . . . . . 11  |-  ( x  =  s  ->  (
( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) )  =  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) )
220219cbvmptv 4544 . . . . . . . . . 10  |-  ( x  e.  RR  |->  ( ( F `  ( X  +  x ) )  x.  ( ( D `
 n ) `  x ) ) )  =  ( s  e.  RR  |->  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) )
221215, 220eqtri 2496 . . . . . . . . 9  |-  G  =  ( s  e.  RR  |->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) )
222221fvmpt2 5964 . . . . . . . 8  |-  ( ( s  e.  RR  /\  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
)  e.  CC )  ->  ( G `  s )  =  ( ( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) ) )
223203, 214, 222syl2anc 661 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( G `  s )  =  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) )
224223eqcomd 2475 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  =  ( G `  s ) )
225224itgeq2dv 22056 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) )  _d s  =  S. ( (
-u pi  -  X
) (,) ( pi 
-  X ) ) ( G `  s
)  _d s )
226 eqidd 2468 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( G `  s )  _d s  =  S. ( (
-u pi  -  X
) (,) ( pi 
-  X ) ) ( G `  s
)  _d s )
22741adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  F : RR
--> CC )
22873adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  X  e.  RR )
229 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
230228, 229readdcld 9635 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( X  +  x )  e.  RR )
231227, 230ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  x ) )  e.  CC )
232231adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  ( X  +  x ) )  e.  CC )
23339a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  RR  C_  CC )
23488ffvelrnda 6032 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  x )  e.  RR )
235233, 234sseldd 3510 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  x )  e.  CC )
236232, 235mulcld 9628 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) )  e.  CC )
237236, 215fmptd 6056 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  G : RR
--> CC )
238237adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  G : RR --> CC )
239144adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( -u pi  -  X )  e.  RR )
240149adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
pi  -  X )  e.  RR )
241 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )
242 eliccre 31427 . . . . . . . . . 10  |-  ( ( ( -u pi  -  X )  e.  RR  /\  ( pi  -  X
)  e.  RR  /\  s  e.  ( ( -u pi  -  X ) [,] ( pi  -  X ) ) )  ->  s  e.  RR )
243239, 240, 241, 242syl3anc 1228 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  s  e.  RR )
244243adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  s  e.  RR )
245238, 244ffvelrnd 6033 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( G `  s )  e.  CC )
246145, 150, 245itgioo 22090 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( G `  s )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( G `  s
)  _d s )
247 fveq2 5872 . . . . . . . 8  |-  ( s  =  x  ->  ( G `  s )  =  ( G `  x ) )
248247cbvitgv 22051 . . . . . . 7  |-  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( G `  s )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( G `  x
)  _d x
249248a1i 11 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( G `  s )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( G `  x
)  _d x )
250246, 249eqtrd 2508 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( G `  s )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( G `  x
)  _d x )
251225, 226, 2503eqtrd 2512 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  S. ( ( -u pi  -  X ) (,) (
pi  -  X )
) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( G `  x
)  _d x )
252 eqid 2467 . . . . . . 7  |-  ( ( pi  -  X )  -  ( -u pi  -  X ) )  =  ( ( pi  -  X )  -  ( -u pi  -  X ) )
253127renegcld 9998 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  -u X  e.  RR )
254 fourierdlem111.o . . . . . . 7  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  -  X )  /\  (
p `  m )  =  ( pi  -  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
25536fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
25637, 255syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
25738, 256mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
258257simpld 459 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
259 elmapi 7452 . . . . . . . . . . . . . . . . 17  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
260258, 259syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
261260adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
262 simpr 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  i  e.  ( 0 ... M
) )
263261, 262ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
26473adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
265263, 264resubcld 9999 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  -  X )  e.  RR )
266265ralrimiva 2881 . . . . . . . . . . . 12  |-  ( ph  ->  A. i  e.  ( 0 ... M ) ( ( Q `  i )  -  X
)  e.  RR )
267 fourierdlem111.14 . . . . . . . . . . . . 13  |-  W  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  -  X
) )
268267fmpt 6053 . . . . . . . . . . . 12  |-  ( A. i  e.  ( 0 ... M ) ( ( Q `  i
)  -  X )  e.  RR  <->  W :
( 0 ... M
) --> RR )
269266, 268sylib 196 . . . . . . . . . . 11  |-  ( ph  ->  W : ( 0 ... M ) --> RR )
270 reex 9595 . . . . . . . . . . . . . 14  |-  RR  e.  _V
271 ovex 6320 . . . . . . . . . . . . . 14  |-  ( 0 ... M )  e. 
_V
272270, 271pm3.2i 455 . . . . . . . . . . . . 13  |-  ( RR  e.  _V  /\  (
0 ... M )  e. 
_V )
273272a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( RR  e.  _V  /\  ( 0 ... M
)  e.  _V )
)
274 elmapg 7445 . . . . . . . . . . . 12  |-  ( ( RR  e.  _V  /\  ( 0 ... M
)  e.  _V )  ->  ( W  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
W : ( 0 ... M ) --> RR ) )
275273, 274syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( W  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
W : ( 0 ... M ) --> RR ) )
276269, 275mpbird 232 . . . . . . . . . 10  |-  ( ph  ->  W  e.  ( RR 
^m  ( 0 ... M ) ) )
277267a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  W  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) ) )
278 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
279278adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  i )  =  ( Q ` 
0 ) )
280257simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
281280simpld 459 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q ` 
0 )  =  -u pi  /\  ( Q `  M )  =  pi ) )
282281simpld 459 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
283282adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  0 )  =  -u pi )
284 eqidd 2468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  = 
0 )  ->  -u pi  =  -u pi )
285279, 283, 2843eqtrd 2512 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  i )  =  -u pi )
286285oveq1d 6310 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( -u pi  -  X ) )
287 0z 10887 . . . . . . . . . . . . . . . . 17  |-  0  e.  ZZ
288287a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  ZZ )
28937nnzd 10977 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ZZ )
290 0re 9608 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
291290a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN  ->  0  e.  RR )
292 nnre 10555 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN  ->  M  e.  RR )
293 nngt0 10577 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN  ->  0  <  M )
294291, 292, 293ltled 9744 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  NN  ->  0  <_  M )
29537, 294syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  M )
296288, 289, 2953jca 1176 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <_  M ) )
297 eluz2 11100 . . . . . . . . . . . . . . 15  |-  ( M  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <_  M ) )
298296, 297sylibr 212 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
299 eluzfz1 11705 . . . . . . . . . . . . . 14  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
300298, 299syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ( 0 ... M ) )
301277, 286, 300, 144fvmptd 5962 . . . . . . . . . . . 12  |-  ( ph  ->  ( W `  0
)  =  ( -u pi  -  X ) )
302 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
303302adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  =  M )  ->  ( Q `  i )  =  ( Q `  M ) )
304281simprd 463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  M
)  =  pi )
305304adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  =  M )  ->  ( Q `  M )  =  pi )
306303, 305eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  =  M )  ->  ( Q `  i )  =  pi )
307306oveq1d 6310 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  -  X )  =  ( pi  -  X ) )
308 eluzfz2 11706 . . . . . . . . . . . . . 14  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
309298, 308syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( 0 ... M ) )
310277, 307, 309, 149fvmptd 5962 . . . . . . . . . . . 12  |-  ( ph  ->  ( W `  M
)  =  ( pi 
-  X ) )
311301, 310jca 532 . . . . . . . . . . 11  |-  ( ph  ->  ( ( W ` 
0 )  =  (
-u pi  -  X
)  /\  ( W `  M )  =  ( pi  -  X ) ) )
312280simprd 463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
313312r19.21bi 2836 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
314260adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
315 elfzofz 11823 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
316315adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
317314, 316ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
318 fzofzp1 11889 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
319318adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
320314, 319ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
32173adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
322317, 320, 321ltsub1d 10173 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  < 
( Q `  (
i  +  1 ) )  <->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) ) )
323313, 322mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) )
324316, 265syldan 470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  e.  RR )
325267fvmpt2 5964 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  -  X
)  e.  RR )  ->  ( W `  i )  =  ( ( Q `  i
)  -  X ) )
326316, 324, 325syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  =  ( ( Q `  i
)  -  X ) )
327 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
328327oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 j )  -  X ) )
329328cbvmptv 4544 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  -  X ) )
330267, 329eqtri 2496 . . . . . . . . . . . . . . . 16  |-  W  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  -  X
) )
331330a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  -  X ) ) )
332 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
333332oveq1d 6310 . . . . . . . . . . . . . . . 16  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
334333adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
335320, 321resubcld 9999 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  X )  e.  RR )
336331, 334, 319, 335fvmptd 5962 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  -  X ) )
337326, 336breq12d 4466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( W `
 i )  < 
( W `  (
i  +  1 ) )  <->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) ) )
338323, 337mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  <  ( W `  ( i  +  1 ) ) )
339338ralrimiva 2881 . . . . . . . . . . 11  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( W `  i )  <  ( W `  ( i  +  1 ) ) )
340311, 339jca 532 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( W `
 0 )  =  ( -u pi  -  X )  /\  ( W `  M )  =  ( pi  -  X ) )  /\  A. i  e.  ( 0..^ M ) ( W `
 i )  < 
( W `  (
i  +  1 ) ) ) )
341276, 340jca 532 . . . . . . . . 9  |-  ( ph  ->  ( W  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( W `  0 )  =  ( -u pi  -  X )  /\  ( W `  M )  =  ( pi  -  X ) )  /\  A. i  e.  ( 0..^ M ) ( W `
 i )  < 
( W `  (
i  +  1 ) ) ) ) )
342254fourierdlem2 31732 . . . . . . . . . 10  |-  ( M  e.  NN  ->  ( W  e.  ( O `  M )  <->  ( W  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( W `  0 )  =  ( -u pi  -  X )  /\  ( W `  M )  =  ( pi  -  X ) )  /\  A. i  e.  ( 0..^ M ) ( W `
 i )  < 
( W `  (
i  +  1 ) ) ) ) ) )
34337, 342syl 16 . . . . . . . . 9  |-  ( ph  ->  ( W  e.  ( O `  M )  <-> 
( W  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( W `  0 )  =  ( -u pi  -  X )  /\  ( W `  M )  =  ( pi  -  X ) )  /\  A. i  e.  ( 0..^ M ) ( W `
 i )  < 
( W `  (
i  +  1 ) ) ) ) ) )
344341, 343mpbird 232 . . . . . . . 8  |-  ( ph  ->  W  e.  ( O `
 M ) )
345344adantr 465 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  W  e.  ( O `  M
) )
346172, 173, 171nnncan2d 9977 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( pi  -  X )  -  ( -u pi  -  X ) )  =  ( pi 
-  -u pi ) )
34739, 23sselii 3506 . . . . . . . . . . . . . 14  |-  pi  e.  CC
348347, 347subnegi 9910 . . . . . . . . . . . . 13  |-  ( pi 
-  -u pi )  =  ( pi  +  pi )
349348a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( pi  -  -u pi )  =  ( pi  +  pi ) )
350 fourierdlem111.t . . . . . . . . . . . . . 14  |-  T  =  ( 2  x.  pi )
3513472timesi 10668 . . . . . . . . . . . . . . 15  |-  ( 2  x.  pi )  =  ( pi  +  pi )
352351, 348eqtr4i 2499 . . . . . . . . . . . . . 14  |-  ( 2  x.  pi )  =  ( pi  -  -u pi )
353350, 352eqtri 2496 . . . . . . . . . . . . 13  |-  T  =  ( pi  -  -u pi )
354353, 349syl5req 2521 . . . . . . . . . . . 12  |-  ( ph  ->  ( pi  +  pi )  =  T )
355346, 349, 3543eqtrd 2512 . . . . . . . . . . 11  |-  ( ph  ->  ( ( pi  -  X )  -  ( -u pi  -  X ) )  =  T )
356355oveq2d 6311 . . . . . . . . . 10  |-  ( ph  ->  ( x  +  ( ( pi  -  X
)  -  ( -u pi  -  X ) ) )  =  ( x  +  T ) )
357356fveq2d 5876 . . . . . . . . 9  |-  ( ph  ->  ( G `  (
x  +  ( ( pi  -  X )  -  ( -u pi  -  X ) ) ) )  =  ( G `
 ( x  +  T ) ) )
358357ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  ( ( pi 
-  X )  -  ( -u pi  -  X
) ) ) )  =  ( G `  ( x  +  T
) ) )
359 simpr 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  x  e.  RR )
360215fvmpt2 5964 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  ( ( F `  ( X  +  x
) )  x.  (
( D `  n
) `  x )
)  e.  CC )  ->  ( G `  x )  =  ( ( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) ) )
361359, 236, 360syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  x )  =  ( ( F `
 ( X  +  x ) )  x.  ( ( D `  n ) `  x
) ) )
362171adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  X  e.  CC )
36339, 229sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
364 2re 10617 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
365364, 23remulcli 9622 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  x.  pi )  e.  RR
366350, 365eqeltri 2551 . . . . . . . . . . . . . . . . . 18  |-  T  e.  RR
367366a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  RR )
36839, 367sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  CC )
369368adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
370362, 363, 369addassd 9630 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( X  +  x )  +  T )  =  ( X  +  ( x  +  T ) ) )
371370eqcomd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( X  +  ( x  +  T ) )  =  ( ( X  +  x )  +  T
) )
372371fveq2d 5876 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  ( x  +  T
) ) )  =  ( F `  (
( X  +  x
)  +  T ) ) )
373 simpl 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ph )
374373, 230jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ph  /\  ( X  +  x
)  e.  RR ) )
375 eleq1 2539 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( X  +  x )  ->  (
s  e.  RR  <->  ( X  +  x )  e.  RR ) )
376375anbi2d 703 . . . . . . . . . . . . . . 15  |-  ( s  =  ( X  +  x )  ->  (
( ph  /\  s  e.  RR )  <->  ( ph  /\  ( X  +  x
)  e.  RR ) ) )
377 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( X  +  x )  ->  (
s  +  T )  =  ( ( X  +  x )  +  T ) )
378377fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( X  +  x )  ->  ( F `  ( s  +  T ) )  =  ( F `  (
( X  +  x
)  +  T ) ) )
379 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( X  +  x )  ->  ( F `  s )  =  ( F `  ( X  +  x
) ) )
380378, 379eqeq12d 2489 . . . . . . . . . . . . . . 15  |-  ( s  =  ( X  +  x )  ->  (
( F `  (
s  +  T ) )  =  ( F `
 s )  <->  ( F `  ( ( X  +  x )  +  T
) )  =  ( F `  ( X  +  x ) ) ) )
381376, 380imbi12d 320 . . . . . . . . . . . . . 14  |-  ( s  =  ( X  +  x )  ->  (
( ( ph  /\  s  e.  RR )  ->  ( F `  (
s  +  T ) )  =  ( F `
 s ) )  <-> 
( ( ph  /\  ( X  +  x
)  e.  RR )  ->  ( F `  ( ( X  +  x )  +  T
) )  =  ( F `  ( X  +  x ) ) ) ) )
382 nfv 1683 . . . . . . . . . . . . . . 15  |-  F/ x
( ( ph  /\  s  e.  RR )  ->  ( F `  (
s  +  T ) )  =  ( F `
 s ) )
383 eleq1 2539 . . . . . . . . . . . . . . . . 17  |-  ( x  =  s  ->  (
x  e.  RR  <->  s  e.  RR ) )
384383anbi2d 703 . . . . . . . . . . . . . . . 16  |-  ( x  =  s  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  s  e.  RR ) ) )
385 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  s  ->  (
x  +  T )  =  ( s  +  T ) )
386385fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( x  =  s  ->  ( F `  ( x  +  T ) )  =  ( F `  (
s  +  T ) ) )
387 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( x  =  s  ->  ( F `  x )  =  ( F `  s ) )
388386, 387eqeq12d 2489 . . . . . . . . . . . . . . . 16  |-  ( x  =  s  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( s  +  T
) )  =  ( F `  s ) ) )
389384, 388imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( x  =  s  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  s  e.  RR )  ->  ( F `  (
s  +  T ) )  =  ( F `
 s ) ) ) )
390 fourierdlem111.fper . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
391382, 389, 390chvar 1982 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  RR )  ->  ( F `
 ( s  +  T ) )  =  ( F `  s
) )
392381, 391vtoclg 3176 . . . . . . . . . . . . 13  |-  ( ( X  +  x )  e.  RR  ->  (
( ph  /\  ( X  +  x )  e.  RR )  ->  ( F `  ( ( X  +  x )  +  T ) )  =  ( F `  ( X  +  x )
) ) )
393230, 374, 392sylc 60 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( ( X  +  x )  +  T ) )  =  ( F `  ( X  +  x )
) )
394372, 393eqtr2d 2509 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  x ) )  =  ( F `  ( X  +  ( x  +  T ) ) ) )
395394adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  ( X  +  x ) )  =  ( F `  ( X  +  ( x  +  T ) ) ) )
39676, 350dirkerper 31719 . . . . . . . . . . . 12  |-  ( ( n  e.  NN  /\  x  e.  RR )  ->  ( ( D `  n ) `  (
x  +  T ) )  =  ( ( D `  n ) `
 x ) )
397396eqcomd 2475 . . . . . . . . . . 11  |-  ( ( n  e.  NN  /\  x  e.  RR )  ->  ( ( D `  n ) `  x
)  =  ( ( D `  n ) `
 ( x  +  T ) ) )
398397adantll 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  x )  =  ( ( D `
 n ) `  ( x  +  T
) ) )
399395, 398oveq12d 6313 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) )  =  ( ( F `
 ( X  +  ( x  +  T
) ) )  x.  ( ( D `  n ) `  (
x  +  T ) ) ) )
400221a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  G  =  ( s  e.  RR  |->  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) ) )
401 oveq2 6303 . . . . . . . . . . . . . 14  |-  ( s  =  ( x  +  T )  ->  ( X  +  s )  =  ( X  +  ( x  +  T
) ) )
402401fveq2d 5876 . . . . . . . . . . . . 13  |-  ( s  =  ( x  +  T )  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  (
x  +  T ) ) ) )
403 fveq2 5872 . . . . . . . . . . . . 13  |-  ( s  =  ( x  +  T )  ->  (
( D `  n
) `  s )  =  ( ( D `
 n ) `  ( x  +  T
) ) )
404402, 403oveq12d 6313 . . . . . . . . . . . 12  |-  ( s  =  ( x  +  T )  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  =  ( ( F `
 ( X  +  ( x  +  T
) ) )  x.  ( ( D `  n ) `  (
x  +  T ) ) ) )
405404adantl 466 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  /\  s  =  ( x  +  T ) )  ->  ( ( F `  ( X  +  s ) )  x.  ( ( D `
 n ) `  s ) )  =  ( ( F `  ( X  +  (
x  +  T ) ) )  x.  (
( D `  n
) `  ( x  +  T ) ) ) )
406367ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  T  e.  RR )
407359, 406readdcld 9635 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  +  T )  e.  RR )
408367adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
409229, 408readdcld 9635 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  T )  e.  RR )
410228, 409readdcld 9635 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( X  +  ( x  +  T ) )  e.  RR )
411227, 410ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  ( x  +  T
) ) )  e.  CC )
412411adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  ( X  +  ( x  +  T ) ) )  e.  CC )
41388adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( D `  n ) : RR --> RR )
414413, 407ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  ( x  +  T ) )  e.  RR )
415233, 414sseldd 3510 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  ( x  +  T ) )  e.  CC )
416412, 415mulcld 9628 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  ( x  +  T ) ) )  x.  ( ( D `
 n ) `  ( x  +  T
) ) )  e.  CC )
417400, 405, 407, 416fvmptd 5962 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  T ) )  =  ( ( F `  ( X  +  (
x  +  T ) ) )  x.  (
( D `  n
) `  ( x  +  T ) ) ) )
418417eqcomd 2475 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  ( x  +  T ) ) )  x.  ( ( D `
 n ) `  ( x  +  T
) ) )  =  ( G `  (
x  +  T ) ) )
419361, 399, 4183eqtrrd 2513 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  T ) )  =  ( G `  x
) )
420358, 419eqtrd 2508 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  ( ( pi 
-  X )  -  ( -u pi  -  X
) ) ) )  =  ( G `  x ) )
421221reseq1i 5275 . . . . . . . . . 10  |-  ( G  |`  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  =  ( ( s  e.  RR  |->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) )  |`  (
( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) )
422421a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  =  ( ( s  e.  RR  |->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) )  |`  (
( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) ) )
423 ioossre 11598 . . . . . . . . . . 11  |-  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) )  C_  RR
424 resmpt 5329 . . . . . . . . . . 11  |-  ( ( ( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) 
C_  RR  ->  ( ( s  e.  RR  |->  ( ( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) ) )  |`  ( ( W `  i ) (,) ( W `  (
i  +  1 ) ) ) )  =  ( s  e.  ( ( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) ) )
425423, 424ax-mp 5 . . . . . . . . . 10  |-  ( ( s  e.  RR  |->  ( ( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) ) )  |`  ( ( W `  i ) (,) ( W `  (
i  +  1 ) ) ) )  =  ( s  e.  ( ( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) )
426425a1i 11 <