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

Theorem fourierdlem111 37945
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 2495 . . . . . 6  |-  ( k  =  n  ->  (
k  e.  NN  <->  n  e.  NN ) )
21anbi2d 709 . . . . 5  |-  ( k  =  n  ->  (
( ph  /\  k  e.  NN )  <->  ( ph  /\  n  e.  NN ) ) )
3 fveq2 5879 . . . . . 6  |-  ( k  =  n  ->  ( S `  k )  =  ( S `  n ) )
4 fveq2 5879 . . . . . . . . . 10  |-  ( k  =  n  ->  ( D `  k )  =  ( D `  n ) )
54fveq1d 5881 . . . . . . . . 9  |-  ( k  =  n  ->  (
( D `  k
) `  ( t  -  X ) )  =  ( ( D `  n ) `  (
t  -  X ) ) )
65oveq2d 6319 . . . . . . . 8  |-  ( k  =  n  ->  (
( F `  t
)  x.  ( ( D `  k ) `
 ( t  -  X ) ) )  =  ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) ) )
76adantr 467 . . . . . . 7  |-  ( ( k  =  n  /\  t  e.  ( -u pi (,) pi ) )  -> 
( ( F `  t )  x.  (
( D `  k
) `  ( t  -  X ) ) )  =  ( ( F `
 t )  x.  ( ( D `  n ) `  (
t  -  X ) ) ) )
87itgeq2dv 22731 . . . . . 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 2445 . . . . 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 322 . . . 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 467 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  F : RR
--> RR )
13 eqid 2423 . . . . 5  |-  ( -u pi (,) pi )  =  ( -u pi (,) pi )
14 ioossre 11698 . . . . . . . . 9  |-  ( -u pi (,) pi )  C_  RR
1514a1i 11 . . . . . . . 8  |-  ( ph  ->  ( -u pi (,) pi )  C_  RR )
1611, 15feqresmpt 5933 . . . . . . 7  |-  ( ph  ->  ( F  |`  ( -u pi (,) pi ) )  =  ( x  e.  ( -u pi (,) pi )  |->  ( F `
 x ) ) )
17 ioossicc 11722 . . . . . . . . 9  |-  ( -u pi (,) pi )  C_  ( -u pi [,] pi )
1817a1i 11 . . . . . . . 8  |-  ( ph  ->  ( -u pi (,) pi )  C_  ( -u pi [,] pi ) )
19 ioombl 22510 . . . . . . . . 9  |-  ( -u pi (,) pi )  e. 
dom  vol
2019a1i 11 . . . . . . . 8  |-  ( ph  ->  ( -u pi (,) pi )  e.  dom  vol )
2111adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u pi [,] pi ) )  ->  F : RR --> RR )
22 pire 23405 . . . . . . . . . . . . . . 15  |-  pi  e.  RR
2322renegcli 9937 . . . . . . . . . . . . . 14  |-  -u pi  e.  RR
2423, 22elicc2i 11702 . . . . . . . . . . . . 13  |-  ( t  e.  ( -u pi [,] pi )  <->  ( t  e.  RR  /\  -u pi  <_  t  /\  t  <_  pi ) )
2524simp1bi 1021 . . . . . . . . . . . 12  |-  ( t  e.  ( -u pi [,] pi )  ->  t  e.  RR )
2625ssriv 3469 . . . . . . . . . . 11  |-  ( -u pi [,] pi )  C_  RR
2726a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( -u pi [,] pi )  C_  RR )
2827sselda 3465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( -u pi [,] pi ) )  ->  x  e.  RR )
2921, 28ffvelrnd 6036 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( -u pi [,] pi ) )  ->  ( F `  x )  e.  RR )
3011, 27feqresmpt 5933 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( -u pi [,] pi ) )  =  ( x  e.  ( -u pi [,] pi )  |->  ( F `
 x ) ) )
31 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 ) ) ) } )
32 fourierdlem111.m . . . . . . . . . 10  |-  ( ph  ->  M  e.  NN )
33 fourierdlem111.q . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( P `
 M ) )
34 ax-resscn 9598 . . . . . . . . . . . . 13  |-  RR  C_  CC
3534a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  CC )
3611, 35fssd 5753 . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> CC )
3736, 27fssresd 5765 . . . . . . . . . 10  |-  ( ph  ->  ( F  |`  ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
38 ioossicc 11722 . . . . . . . . . . . . 13  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  ( ( Q `  i ) [,] ( Q `  ( i  +  1 ) ) )
3923rexri 9695 . . . . . . . . . . . . . . 15  |-  -u pi  e.  RR*
4039a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -u pi  e.  RR* )
4122rexri 9695 . . . . . . . . . . . . . . 15  |-  pi  e.  RR*
4241a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  pi  e.  RR* )
4331, 32, 33fourierdlem15 37848 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
4443adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
45 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
4640, 42, 44, 45fourierdlem8 37841 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) [,] ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
4738, 46syl5ss 3476 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  ( -u pi [,] pi ) )
4847resabs1d 5151 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) )
49 fourierdlem111.fcn . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
5048, 49eqeltrd 2511 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )
51 fourierdlem111.r . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
5248oveq1d 6318 . . . . . . . . . . 11  |-  ( (
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 ) ) )
5351, 52eleqtrrd 2514 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
54 fourierdlem111.l . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
5548oveq1d 6318 . . . . . . . . . . 11  |-  ( (
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 ) ) ) )
5654, 55eleqtrrd 2514 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
5731, 32, 33, 37, 50, 53, 56fourierdlem69 37903 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  ( -u pi [,] pi ) )  e.  L^1 )
5830, 57eqeltrrd 2512 . . . . . . . 8  |-  ( ph  ->  ( x  e.  (
-u pi [,] pi )  |->  ( F `  x ) )  e.  L^1 )
5918, 20, 29, 58iblss 22754 . . . . . . 7  |-  ( ph  ->  ( x  e.  (
-u pi (,) pi )  |->  ( F `  x ) )  e.  L^1 )
6016, 59eqeltrd 2511 . . . . . 6  |-  ( ph  ->  ( F  |`  ( -u pi (,) pi ) )  e.  L^1 )
6160adantr 467 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( F  |`  ( -u pi (,) pi ) )  e.  L^1 )
62 fourierdlem111.a . . . . 5  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( cos `  (
n  x.  t ) ) )  _d t  /  pi ) )
63 fourierdlem111.b . . . . 5  |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( sin `  (
n  x.  t ) ) )  _d t  /  pi ) )
64 fourierdlem111.x . . . . . 6  |-  ( ph  ->  X  e.  RR )
6564adantr 467 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  RR )
66 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 ) ) ) ) ) )
67 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 ) ) ) ) ) ) )
68 simpr 463 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
6912, 13, 61, 62, 63, 65, 66, 67, 68fourierdlem83 37917 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  =  S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( ( D `
 k ) `  ( t  -  X
) ) )  _d t )
7010, 69chvarv 2069 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  ( S `
 n )  =  S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( ( D `
 n ) `  ( t  -  X
) ) )  _d t )
7123a1i 11 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  -u pi  e.  RR )
7222a1i 11 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  pi  e.  RR )
7336adantr 467 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  F : RR --> CC )
7425adantl 468 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  t  e.  RR )
7573, 74ffvelrnd 6036 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
7675adantlr 720 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  ( F `  t )  e.  CC )
7767dirkerf 37823 . . . . . . . . 9  |-  ( n  e.  NN  ->  ( D `  n ) : RR --> RR )
7877ad2antlr 732 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  ( D `  n ) : RR --> RR )
7964adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  X  e.  RR )
8074, 79resubcld 10049 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( -u pi [,] pi ) )  ->  (
t  -  X )  e.  RR )
8180adantlr 720 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
t  -  X )  e.  RR )
8278, 81ffvelrnd 6036 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  n
) `  ( t  -  X ) )  e.  RR )
8382recnd 9671 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( D `  n
) `  ( t  -  X ) )  e.  CC )
8476, 83mulcld 9665 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  t  e.  ( -u pi [,] pi ) )  ->  (
( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  e.  CC )
8571, 72, 84itgioo 22765 . . . 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 )
86 fvres 5893 . . . . . . . 8  |-  ( t  e.  ( -u pi [,] pi )  ->  (
( F  |`  ( -u pi [,] pi ) ) `  t )  =  ( F `  t ) )
8786eqcomd 2431 . . . . . . 7  |-  ( t  e.  ( -u pi [,] pi )  ->  ( F `  t )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  t
) )
8887oveq1d 6318 . . . . . 6  |-  ( t  e.  ( -u pi [,] pi )  ->  (
( F `  t
)  x.  ( ( D `  n ) `
 ( t  -  X ) ) )  =  ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) ) )
8988adantl 468 . . . . 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 ) ) ) )
9089itgeq2dv 22731 . . . 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 )
91 simpl 459 . . . . . . . . . . . . 13  |-  ( ( n  =  m  /\  y  e.  RR )  ->  n  =  m )
9291oveq2d 6319 . . . . . . . . . . . 12  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( 2  x.  n
)  =  ( 2  x.  m ) )
9392oveq1d 6318 . . . . . . . . . . 11  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( 2  x.  n )  +  1 )  =  ( ( 2  x.  m )  +  1 ) )
9493oveq1d 6318 . . . . . . . . . 10  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( ( 2  x.  n )  +  1 )  /  (
2  x.  pi ) )  =  ( ( ( 2  x.  m
)  +  1 )  /  ( 2  x.  pi ) ) )
9591oveq1d 6318 . . . . . . . . . . . . 13  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( n  +  ( 1  /  2 ) )  =  ( m  +  ( 1  / 
2 ) ) )
9695oveq1d 6318 . . . . . . . . . . . 12  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( ( n  +  ( 1  /  2
) )  x.  y
)  =  ( ( m  +  ( 1  /  2 ) )  x.  y ) )
9796fveq2d 5883 . . . . . . . . . . 11  |-  ( ( n  =  m  /\  y  e.  RR )  ->  ( sin `  (
( n  +  ( 1  /  2 ) )  x.  y ) )  =  ( sin `  ( ( m  +  ( 1  /  2
) )  x.  y
) ) )
9897oveq1d 6318 . . . . . . . . . 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 ) ) ) ) )
9994, 98ifeq12d 3930 . . . . . . . . 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
) ) ) ) ) )
10099mpteq2dva 4508 . . . . . . . 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 ) ) ) ) ) ) )
101100cbvmptv 4514 . . . . . . 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 ) ) ) ) ) ) )
10267, 101eqtri 2452 . . . . . 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 ) ) ) ) ) ) )
103 fveq2 5879 . . . . . . . 8  |-  ( s  =  t  ->  (
( F  |`  ( -u pi [,] pi ) ) `  s )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  t
) )
104 oveq1 6310 . . . . . . . . 9  |-  ( s  =  t  ->  (
s  -  X )  =  ( t  -  X ) )
105104fveq2d 5883 . . . . . . . 8  |-  ( s  =  t  ->  (
( D `  n
) `  ( s  -  X ) )  =  ( ( D `  n ) `  (
t  -  X ) ) )
106103, 105oveq12d 6321 . . . . . . 7  |-  ( s  =  t  ->  (
( ( F  |`  ( -u pi [,] pi ) ) `  s
)  x.  ( ( D `  n ) `
 ( s  -  X ) ) )  =  ( ( ( F  |`  ( -u pi [,] pi ) ) `  t )  x.  (
( D `  n
) `  ( t  -  X ) ) ) )
107106cbvmptv 4514 . . . . . 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
) ) ) )
10833adantr 467 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  Q  e.  ( P `  M
) )
10932adantr 467 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  M  e.  NN )
110 simpr 463 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
11164adantr 467 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  X  e.  RR )
11237adantr 467 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( F  |`  ( -u pi [,] pi ) ) : (
-u pi [,] pi )
--> CC )
11350adantlr 720 . . . . . 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 ) )
11453adantlr 720 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( ( F  |`  ( -u pi [,] pi ) )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
11556adantlr 720 . . . . . 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 ) ) ) )
116102, 31, 107, 108, 109, 110, 111, 112, 113, 114, 115fourierdlem101 37935 . . . . 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 )
117 oveq2 6311 . . . . . . . . . 10  |-  ( s  =  y  ->  ( X  +  s )  =  ( X  +  y ) )
118117fveq2d 5883 . . . . . . . . 9  |-  ( s  =  y  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  y
) ) )
119 fveq2 5879 . . . . . . . . 9  |-  ( s  =  y  ->  (
( D `  n
) `  s )  =  ( ( D `
 n ) `  y ) )
120118, 119oveq12d 6321 . . . . . . . 8  |-  ( s  =  y  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  =  ( ( F `
 ( X  +  y ) )  x.  ( ( D `  n ) `  y
) ) )
121120cbvitgv 22726 . . . . . . 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
122121a1i 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 )
12323a1i 11 . . . . . . . . 9  |-  ( ph  -> 
-u pi  e.  RR )
124123, 64resubcld 10049 . . . . . . . 8  |-  ( ph  ->  ( -u pi  -  X )  e.  RR )
125124adantr 467 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( -u pi  -  X )  e.  RR )
12622a1i 11 . . . . . . . . 9  |-  ( ph  ->  pi  e.  RR )
127126, 64resubcld 10049 . . . . . . . 8  |-  ( ph  ->  ( pi  -  X
)  e.  RR )
128127adantr 467 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( pi 
-  X )  e.  RR )
12936adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  F : RR --> CC )
13064adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  X  e.  RR )
131 simpr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )
132124adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( -u pi  -  X )  e.  RR )
133127adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
pi  -  X )  e.  RR )
134 elicc2 11701 . . . . . . . . . . . . . 14  |-  ( ( ( -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 ) ) ) )
135132, 133, 134syl2anc 666 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
136131, 135mpbid 214 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
y  e.  RR  /\  ( -u pi  -  X
)  <_  y  /\  y  <_  ( pi  -  X ) ) )
137136simp1d 1018 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  e.  RR )
138130, 137readdcld 9672 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  e.  RR )
139129, 138ffvelrnd 6036 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  e.  CC )
140139adantlr 720 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  e.  CC )
14177ad2antlr 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( D `  n ) : RR --> RR )
142137adantlr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  e.  RR )
143141, 142ffvelrnd 6036 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( D `  n
) `  y )  e.  RR )
144143recnd 9671 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( D `  n
) `  y )  e.  CC )
145140, 144mulcld 9665 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( F `  ( X  +  y )
)  x.  ( ( D `  n ) `
 y ) )  e.  CC )
146125, 128, 145itgioo 22765 . . . . . 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 `  ( X  +  y
) )  x.  (
( D `  n
) `  y )
)  _d y )
14723a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  -u pi  e.  RR )
14822a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  pi  e.  RR )
14964recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  CC )
150126recnd 9671 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  pi  e.  CC )
151150negcld 9975 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u pi  e.  CC )
152149, 151pncan3d 9991 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  +  (
-u pi  -  X
) )  =  -u pi )
153152eqcomd 2431 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  =  ( X  +  ( -u pi  -  X ) ) )
154153adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  -u pi  =  ( X  +  ( -u pi  -  X
) ) )
155136simp2d 1019 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( -u pi  -  X )  <_  y )
156132, 137, 130, 155leadd2dd 10230 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  ( -u pi  -  X ) )  <_ 
( X  +  y ) )
157154, 156eqbrtrd 4442 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  -u pi  <_  ( X  +  y ) )
158136simp3d 1020 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  y  <_  ( pi  -  X
) )
159137, 133, 130, 158leadd2dd 10230 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  <_  ( X  +  ( pi  -  X ) ) )
160149adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  X  e.  CC )
161150adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  pi  e.  CC )
162160, 161pncan3d 9991 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  ( pi  -  X ) )  =  pi )
163159, 162breqtrd 4446 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  <_  pi )
164147, 148, 138, 157, 163eliccd 37476 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( X  +  y )  e.  ( -u pi [,] pi ) )
165 fvres 5893 . . . . . . . . . . 11  |-  ( ( X  +  y )  e.  ( -u pi [,] pi )  ->  (
( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y ) )  =  ( F `  ( X  +  y
) ) )
166164, 165syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y ) )  =  ( F `  ( X  +  y
) ) )
167166eqcomd 2431 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y )
) )
168167adantlr 720 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( F `  ( X  +  y ) )  =  ( ( F  |`  ( -u pi [,] pi ) ) `  ( X  +  y )
) )
169168oveq1d 6318 . . . . . . 7  |-  ( ( ( 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 )
) )
170169itgeq2dv 22731 . . . . . 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 )
171122, 146, 1703eqtrrd 2469 . . . . 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 )
172116, 171eqtrd 2464 . . . 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 )
17385, 90, 1723eqtrd 2468 . . 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 )
174 elioore 11668 . . . . . . . . 9  |-  ( s  e.  ( ( -u pi  -  X ) (,) ( pi  -  X
) )  ->  s  e.  RR )
175174adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  s  e.  RR )
17636adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  F : RR --> CC )
17764adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  X  e.  RR )
178174adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  s  e.  RR )
179177, 178readdcld 9672 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( X  +  s )  e.  RR )
180176, 179ffvelrnd 6036 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( F `  ( X  +  s ) )  e.  CC )
181180adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( F `  ( X  +  s ) )  e.  CC )
18277ad2antlr 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( D `  n ) : RR --> RR )
183182, 175ffvelrnd 6036 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( D `  n
) `  s )  e.  RR )
184183recnd 9671 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( D `  n
) `  s )  e.  CC )
185181, 184mulcld 9665 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  e.  CC )
186 fourierdlem111.g . . . . . . . . . 10  |-  G  =  ( x  e.  RR  |->  ( ( F `  ( X  +  x
) )  x.  (
( D `  n
) `  x )
) )
187 oveq2 6311 . . . . . . . . . . . . 13  |-  ( x  =  s  ->  ( X  +  x )  =  ( X  +  s ) )
188187fveq2d 5883 . . . . . . . . . . . 12  |-  ( x  =  s  ->  ( F `  ( X  +  x ) )  =  ( F `  ( X  +  s )
) )
189 fveq2 5879 . . . . . . . . . . . 12  |-  ( x  =  s  ->  (
( D `  n
) `  x )  =  ( ( D `
 n ) `  s ) )
190188, 189oveq12d 6321 . . . . . . . . . . 11  |-  ( x  =  s  ->  (
( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) )  =  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) )
191190cbvmptv 4514 . . . . . . . . . 10  |-  ( x  e.  RR  |->  ( ( F `  ( X  +  x ) )  x.  ( ( D `
 n ) `  x ) ) )  =  ( s  e.  RR  |->  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) )
192186, 191eqtri 2452 . . . . . . . . 9  |-  G  =  ( s  e.  RR  |->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) )
193192fvmpt2 5971 . . . . . . . 8  |-  ( ( s  e.  RR  /\  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
)  e.  CC )  ->  ( G `  s )  =  ( ( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) ) )
194175, 185, 193syl2anc 666 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  ( G `  s )  =  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) )
195194eqcomd 2431 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) (,) (
pi  -  X )
) )  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  =  ( G `  s ) )
196195itgeq2dv 22731 . . . . 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 )
19736adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  F : RR
--> CC )
19864adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  X  e.  RR )
199 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
200198, 199readdcld 9672 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( X  +  x )  e.  RR )
201197, 200ffvelrnd 6036 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  x ) )  e.  CC )
202201adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  ( X  +  x ) )  e.  CC )
20377adantl 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( D `
 n ) : RR --> RR )
204203ffvelrnda 6035 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  x )  e.  RR )
205204recnd 9671 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  x )  e.  CC )
206202, 205mulcld 9665 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) )  e.  CC )
207206, 186fmptd 6059 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  G : RR
--> CC )
208207adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  G : RR --> CC )
209124adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( -u pi  -  X )  e.  RR )
210127adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  (
pi  -  X )  e.  RR )
211 simpr 463 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )
212 eliccre 37478 . . . . . . . . . 10  |-  ( ( ( -u pi  -  X )  e.  RR  /\  ( pi  -  X
)  e.  RR  /\  s  e.  ( ( -u pi  -  X ) [,] ( pi  -  X ) ) )  ->  s  e.  RR )
213209, 210, 211, 212syl3anc 1265 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  s  e.  RR )
214213adantlr 720 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  s  e.  RR )
215208, 214ffvelrnd 6036 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  s  e.  ( ( -u pi  -  X ) [,] (
pi  -  X )
) )  ->  ( G `  s )  e.  CC )
216125, 128, 215itgioo 22765 . . . . . 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 )
217 fveq2 5879 . . . . . . 7  |-  ( s  =  x  ->  ( G `  s )  =  ( G `  x ) )
218217cbvitgv 22726 . . . . . 6  |-  S. ( ( -u pi  -  X ) [,] (
pi  -  X )
) ( G `  s )  _d s  =  S. ( (
-u pi  -  X
) [,] ( pi 
-  X ) ) ( G `  x
)  _d x
219216, 218syl6eq 2480 . . . . 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 )
220196, 219eqtrd 2464 . . . 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 )
221 eqid 2423 . . . . . . 7  |-  ( ( pi  -  X )  -  ( -u pi  -  X ) )  =  ( ( pi  -  X )  -  ( -u pi  -  X ) )
222111renegcld 10048 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  -u X  e.  RR )
223 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 ) ) ) } )
22431fourierdlem2 37835 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) ) )
22532, 224syl 17 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) ) )
22633, 225mpbid 214 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
227226simpld 461 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
228 elmapi 7499 . . . . . . . . . . . . . . 15  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
229227, 228syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
230229fnvinran 37240 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( Q `  i )  e.  RR )
23164adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
232230, 231resubcld 10049 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( Q `  i
)  -  X )  e.  RR )
233 fourierdlem111.14 . . . . . . . . . . . 12  |-  W  =  ( i  e.  ( 0 ... M ) 
|->  ( ( Q `  i )  -  X
) )
234232, 233fmptd 6059 . . . . . . . . . . 11  |-  ( ph  ->  W : ( 0 ... M ) --> RR )
235 reex 9632 . . . . . . . . . . . . 13  |-  RR  e.  _V
236 ovex 6331 . . . . . . . . . . . . 13  |-  ( 0 ... M )  e. 
_V
237235, 236pm3.2i 457 . . . . . . . . . . . 12  |-  ( RR  e.  _V  /\  (
0 ... M )  e. 
_V )
238 elmapg 7491 . . . . . . . . . . . 12  |-  ( ( RR  e.  _V  /\  ( 0 ... M
)  e.  _V )  ->  ( W  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
W : ( 0 ... M ) --> RR ) )
239237, 238mp1i 13 . . . . . . . . . . 11  |-  ( ph  ->  ( W  e.  ( RR  ^m  ( 0 ... M ) )  <-> 
W : ( 0 ... M ) --> RR ) )
240234, 239mpbird 236 . . . . . . . . . 10  |-  ( ph  ->  W  e.  ( RR 
^m  ( 0 ... M ) ) )
241233a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  W  =  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) ) )
242 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
243226simprd 465 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
244243simpld 461 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q ` 
0 )  =  -u pi  /\  ( Q `  M )  =  pi ) )
245244simpld 461 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
246242, 245sylan9eqr 2486 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  = 
0 )  ->  ( Q `  i )  =  -u pi )
247246oveq1d 6318 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  = 
0 )  ->  (
( Q `  i
)  -  X )  =  ( -u pi  -  X ) )
248 0zd 10951 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  ZZ )
24932nnzd 11041 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ZZ )
250 0red 9646 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  0  e.  RR )
251 nnre 10618 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  M  e.  RR )
252 nngt0 10640 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  0  <  M )
253250, 251, 252ltled 9785 . . . . . . . . . . . . . . 15  |-  ( M  e.  NN  ->  0  <_  M )
25432, 253syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <_  M )
255 eluz2 11167 . . . . . . . . . . . . . 14  |-  ( M  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <_  M ) )
256248, 249, 254, 255syl3anbrc 1190 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
257 eluzfz1 11808 . . . . . . . . . . . . 13  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
258256, 257syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  0  e.  ( 0 ... M ) )
259241, 247, 258, 124fvmptd 5968 . . . . . . . . . . 11  |-  ( ph  ->  ( W `  0
)  =  ( -u pi  -  X ) )
260 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( Q `  i )  =  ( Q `  M ) )
261244simprd 465 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q `  M
)  =  pi )
262260, 261sylan9eqr 2486 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  =  M )  ->  ( Q `  i )  =  pi )
263262oveq1d 6318 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  =  M )  ->  (
( Q `  i
)  -  X )  =  ( pi  -  X ) )
264 eluzfz2 11809 . . . . . . . . . . . . 13  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
265256, 264syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( 0 ... M ) )
266241, 263, 265, 127fvmptd 5968 . . . . . . . . . . 11  |-  ( ph  ->  ( W `  M
)  =  ( pi 
-  X ) )
267259, 266jca 535 . . . . . . . . . 10  |-  ( ph  ->  ( ( W ` 
0 )  =  (
-u pi  -  X
)  /\  ( W `  M )  =  ( pi  -  X ) ) )
268229adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
269 elfzofz 11937 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
270269adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
271268, 270ffvelrnd 6036 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
272 fzofzp1 12009 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
273272adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
274268, 273ffvelrnd 6036 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
27564adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
276243simprd 465 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
277276r19.21bi 2795 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
278271, 274, 275, 277ltsub1dd 10227 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  <  (
( Q `  (
i  +  1 ) )  -  X ) )
279270, 232syldan 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  -  X )  e.  RR )
280233fvmpt2 5971 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( Q `  i )  -  X
)  e.  RR )  ->  ( W `  i )  =  ( ( Q `  i
)  -  X ) )
281270, 279, 280syl2anc 666 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  =  ( ( Q `  i
)  -  X ) )
282 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
283282oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
( Q `  i
)  -  X )  =  ( ( Q `
 j )  -  X ) )
284283cbvmptv 4514 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0 ... M )  |->  ( ( Q `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( Q `
 j )  -  X ) )
285233, 284eqtri 2452 . . . . . . . . . . . . . 14  |-  W  =  ( j  e.  ( 0 ... M ) 
|->  ( ( Q `  j )  -  X
) )
286285a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  =  ( j  e.  ( 0 ... M )  |->  ( ( Q `  j
)  -  X ) ) )
287 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( j  =  ( i  +  1 )  ->  ( Q `  j )  =  ( Q `  ( i  +  1 ) ) )
288287oveq1d 6318 . . . . . . . . . . . . . 14  |-  ( j  =  ( i  +  1 )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
289288adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( Q `  j
)  -  X )  =  ( ( Q `
 ( i  +  1 ) )  -  X ) )
290274, 275resubcld 10049 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  -  X )  e.  RR )
291286, 289, 273, 290fvmptd 5968 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  ( i  +  1 ) )  =  ( ( Q `  (
i  +  1 ) )  -  X ) )
292278, 281, 2913brtr4d 4452 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  <  ( W `  ( i  +  1 ) ) )
293292ralrimiva 2840 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( W `  i )  <  ( W `  ( i  +  1 ) ) )
294240, 267, 293jca32 538 . . . . . . . . 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 ) ) ) ) )
295223fourierdlem2 37835 . . . . . . . . . 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 ) ) ) ) ) )
29632, 295syl 17 . . . . . . . . 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 ) ) ) ) ) )
297294, 296mpbird 236 . . . . . . . 8  |-  ( ph  ->  W  e.  ( O `
 M ) )
298297adantr 467 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  W  e.  ( O `  M
) )
299150, 151, 149nnncan2d 10023 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( pi  -  X )  -  ( -u pi  -  X ) )  =  ( pi 
-  -u pi ) )
300 picn 23406 . . . . . . . . . . . . . 14  |-  pi  e.  CC
3013002timesi 10732 . . . . . . . . . . . . 13  |-  ( 2  x.  pi )  =  ( pi  +  pi )
302 fourierdlem111.t . . . . . . . . . . . . 13  |-  T  =  ( 2  x.  pi )
303300, 300subnegi 9955 . . . . . . . . . . . . 13  |-  ( pi 
-  -u pi )  =  ( pi  +  pi )
304301, 302, 3033eqtr4i 2462 . . . . . . . . . . . 12  |-  T  =  ( pi  -  -u pi )
305299, 304syl6eqr 2482 . . . . . . . . . . 11  |-  ( ph  ->  ( ( pi  -  X )  -  ( -u pi  -  X ) )  =  T )
306305oveq2d 6319 . . . . . . . . . 10  |-  ( ph  ->  ( x  +  ( ( pi  -  X
)  -  ( -u pi  -  X ) ) )  =  ( x  +  T ) )
307306fveq2d 5883 . . . . . . . . 9  |-  ( ph  ->  ( G `  (
x  +  ( ( pi  -  X )  -  ( -u pi  -  X ) ) ) )  =  ( G `
 ( x  +  T ) ) )
308307ad2antrr 731 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  ( ( pi 
-  X )  -  ( -u pi  -  X
) ) ) )  =  ( G `  ( x  +  T
) ) )
309 simpr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  x  e.  RR )
310186fvmpt2 5971 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  ( ( F `  ( X  +  x
) )  x.  (
( D `  n
) `  x )
)  e.  CC )  ->  ( G `  x )  =  ( ( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) ) )
311309, 206, 310syl2anc 666 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  x )  =  ( ( F `
 ( X  +  x ) )  x.  ( ( D `  n ) `  x
) ) )
312149adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  X  e.  CC )
313199recnd 9671 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
314 2re 10681 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
315314, 22remulcli 9659 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  x.  pi )  e.  RR
316302, 315eqeltri 2507 . . . . . . . . . . . . . . . . . 18  |-  T  e.  RR
317316a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  RR )
318317recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  CC )
319318adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
320312, 313, 319addassd 9667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( X  +  x )  +  T )  =  ( X  +  ( x  +  T ) ) )
321320eqcomd 2431 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( X  +  ( x  +  T ) )  =  ( ( X  +  x )  +  T
) )
322321fveq2d 5883 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  ( x  +  T
) ) )  =  ( F `  (
( X  +  x
)  +  T ) ) )
323 simpl 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ph )
324323, 200jca 535 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ph  /\  ( X  +  x
)  e.  RR ) )
325 eleq1 2495 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( X  +  x )  ->  (
s  e.  RR  <->  ( X  +  x )  e.  RR ) )
326325anbi2d 709 . . . . . . . . . . . . . . 15  |-  ( s  =  ( X  +  x )  ->  (
( ph  /\  s  e.  RR )  <->  ( ph  /\  ( X  +  x
)  e.  RR ) ) )
327 oveq1 6310 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( X  +  x )  ->  (
s  +  T )  =  ( ( X  +  x )  +  T ) )
328327fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( X  +  x )  ->  ( F `  ( s  +  T ) )  =  ( F `  (
( X  +  x
)  +  T ) ) )
329 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( X  +  x )  ->  ( F `  s )  =  ( F `  ( X  +  x
) ) )
330328, 329eqeq12d 2445 . . . . . . . . . . . . . . 15  |-  ( s  =  ( X  +  x )  ->  (
( F `  (
s  +  T ) )  =  ( F `
 s )  <->  ( F `  ( ( X  +  x )  +  T
) )  =  ( F `  ( X  +  x ) ) ) )
331326, 330imbi12d 322 . . . . . . . . . . . . . 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 ) ) ) ) )
332 eleq1 2495 . . . . . . . . . . . . . . . . 17  |-  ( x  =  s  ->  (
x  e.  RR  <->  s  e.  RR ) )
333332anbi2d 709 . . . . . . . . . . . . . . . 16  |-  ( x  =  s  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  s  e.  RR ) ) )
334 oveq1 6310 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  s  ->  (
x  +  T )  =  ( s  +  T ) )
335334fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( x  =  s  ->  ( F `  ( x  +  T ) )  =  ( F `  (
s  +  T ) ) )
336 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( x  =  s  ->  ( F `  x )  =  ( F `  s ) )
337335, 336eqeq12d 2445 . . . . . . . . . . . . . . . 16  |-  ( x  =  s  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( s  +  T
) )  =  ( F `  s ) ) )
338333, 337imbi12d 322 . . . . . . . . . . . . . . 15  |-  ( x  =  s  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  s  e.  RR )  ->  ( F `  (
s  +  T ) )  =  ( F `
 s ) ) ) )
339 fourierdlem111.fper . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
340338, 339chvarv 2069 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  RR )  ->  ( F `
 ( s  +  T ) )  =  ( F `  s
) )
341331, 340vtoclg 3140 . . . . . . . . . . . . 13  |-  ( ( X  +  x )  e.  RR  ->  (
( ph  /\  ( X  +  x )  e.  RR )  ->  ( F `  ( ( X  +  x )  +  T ) )  =  ( F `  ( X  +  x )
) ) )
342200, 324, 341sylc 63 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( ( X  +  x )  +  T ) )  =  ( F `  ( X  +  x )
) )
343322, 342eqtr2d 2465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  x ) )  =  ( F `  ( X  +  ( x  +  T ) ) ) )
344343adantlr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  ( X  +  x ) )  =  ( F `  ( X  +  ( x  +  T ) ) ) )
34567, 302dirkerper 37822 . . . . . . . . . . . 12  |-  ( ( n  e.  NN  /\  x  e.  RR )  ->  ( ( D `  n ) `  (
x  +  T ) )  =  ( ( D `  n ) `
 x ) )
346345eqcomd 2431 . . . . . . . . . . 11  |-  ( ( n  e.  NN  /\  x  e.  RR )  ->  ( ( D `  n ) `  x
)  =  ( ( D `  n ) `
 ( x  +  T ) ) )
347346adantll 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  x )  =  ( ( D `
 n ) `  ( x  +  T
) ) )
348344, 347oveq12d 6321 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  x )
)  x.  ( ( D `  n ) `
 x ) )  =  ( ( F `
 ( X  +  ( x  +  T
) ) )  x.  ( ( D `  n ) `  (
x  +  T ) ) ) )
349192a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  G  =  ( s  e.  RR  |->  ( ( F `
 ( X  +  s ) )  x.  ( ( D `  n ) `  s
) ) ) )
350 oveq2 6311 . . . . . . . . . . . . . 14  |-  ( s  =  ( x  +  T )  ->  ( X  +  s )  =  ( X  +  ( x  +  T
) ) )
351350fveq2d 5883 . . . . . . . . . . . . 13  |-  ( s  =  ( x  +  T )  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  (
x  +  T ) ) ) )
352 fveq2 5879 . . . . . . . . . . . . 13  |-  ( s  =  ( x  +  T )  ->  (
( D `  n
) `  s )  =  ( ( D `
 n ) `  ( x  +  T
) ) )
353351, 352oveq12d 6321 . . . . . . . . . . . 12  |-  ( s  =  ( x  +  T )  ->  (
( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) )  =  ( ( F `
 ( X  +  ( x  +  T
) ) )  x.  ( ( D `  n ) `  (
x  +  T ) ) ) )
354353adantl 468 . . . . . . . . . . 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 ) ) ) )
355316a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  T  e.  RR )
356309, 355readdcld 9672 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
x  +  T )  e.  RR )
357316a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
358199, 357readdcld 9672 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  T )  e.  RR )
359198, 358readdcld 9672 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( X  +  ( x  +  T ) )  e.  RR )
360197, 359ffvelrnd 6036 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( X  +  ( x  +  T
) ) )  e.  CC )
361360adantlr 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  ( X  +  ( x  +  T ) ) )  e.  CC )
36277ad2antlr 732 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( D `  n ) : RR --> RR )
363362, 356ffvelrnd 6036 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  ( x  +  T ) )  e.  RR )
364363recnd 9671 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( D `  n
) `  ( x  +  T ) )  e.  CC )
365361, 364mulcld 9665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  ( x  +  T ) ) )  x.  ( ( D `
 n ) `  ( x  +  T
) ) )  e.  CC )
366349, 354, 356, 365fvmptd 5968 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  T ) )  =  ( ( F `  ( X  +  (
x  +  T ) ) )  x.  (
( D `  n
) `  ( x  +  T ) ) ) )
367366eqcomd 2431 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  ( X  +  ( x  +  T ) ) )  x.  ( ( D `
 n ) `  ( x  +  T
) ) )  =  ( G `  (
x  +  T ) ) )
368311, 348, 3673eqtrrd 2469 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  T ) )  =  ( G `  x
) )
369308, 368eqtrd 2464 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( G `  ( x  +  ( ( pi 
-  X )  -  ( -u pi  -  X
) ) ) )  =  ( G `  x ) )
370192reseq1i 5118 . . . . . . . . . 10  |-  ( G  |`  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  =  ( ( s  e.  RR  |->  ( ( F `  ( X  +  s
) )  x.  (
( D `  n
) `  s )
) )  |`  (
( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) )
371370a1i 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 ) ) ) ) )
372 ioossre 11698 . . . . . . . . . 10  |-  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) )  C_  RR
373 resmpt 5171 . . . . . . . . . 10  |-  ( ( ( 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 )
) ) )
374372, 373ax-mp 5 . . . . . . . . 9  |-  ( ( 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 )
) )
375371, 374syl6eq 2480 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) )  |->  ( ( F `  ( X  +  s )
)  x.  ( ( D `  n ) `
 s ) ) ) )
376271rexrd 9692 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
377376adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
378274rexrd 9692 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
379378adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
38064adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
381 elioore 11668 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( W `
 i ) (,) ( W `  (
i  +  1 ) ) )  ->  s  e.  RR )
382381adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
383380, 382readdcld 9672 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
384383adantlr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
385 eleq1 2495 . . . . . . . . . . . . . . . 16  |-  ( x  =  s  ->  (
x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) )  <->  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) ) )
386385anbi2d 709 . . . . . . . . . . . . . . 15  |-  ( x  =  s  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  (
i  +  1 ) ) ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i
) (,) ( W `
 ( i  +  1 ) ) ) ) ) )
387187breq2d 4433 . . . . . . . . . . . . . . 15  |-  ( x  =  s  ->  (
( Q `  i
)  <  ( X  +  x )  <->  ( Q `  i )  <  ( X  +  s )
) )
388386, 387imbi12d 322 . . . . . . . . . . . . . 14  |-  ( x  =  s  ->  (
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( X  +  x ) )  <->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( X  +  s ) ) ) )
389149adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
390281, 279eqeltrd 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  e.  RR )
391390recnd 9671 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  e.  CC )
392389, 391addcomd 9837 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( X  +  ( W `  i ) )  =  ( ( W `  i )  +  X ) )
393281oveq1d 6318 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( W `
 i )  +  X )  =  ( ( ( Q `  i )  -  X
)  +  X ) )
394271recnd 9671 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  CC )
395394, 389npcand 9992 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  -  X )  +  X )  =  ( Q `  i ) )
396392, 393, 3953eqtrrd 2469 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( X  +  ( W `
 i ) ) )
397396adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  =  ( X  +  ( W `  i ) ) )
398390adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( W `  i )  e.  RR )
399 elioore 11668 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( ( W `
 i ) (,) ( W `  (
i  +  1 ) ) )  ->  x  e.  RR )
400399adantl 468 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  x  e.  RR )
40164ad2antrr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
402390rexrd 9692 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  i )  e.  RR* )
403402adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( W `  i )  e.  RR* )
404291, 290eqeltrd 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  ( i  +  1 ) )  e.  RR )
405404rexrd 9692 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( W `  ( i  +  1 ) )  e.  RR* )
406405adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( W `  ( i  +  1 ) )  e.  RR* )
407 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )
408 ioogtlb 37467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W `  i
)  e.  RR*  /\  ( W `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( W `  i )  <  x )
409403, 406, 407, 408syl3anc 1265 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( W `  i )  <  x )
410398, 400, 401, 409ltadd2dd 9796 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( X  +  ( W `  i ) )  < 
( X  +  x
) )
411397, 410eqbrtrd 4442 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( X  +  x
) )
412388, 411chvarv 2069 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  ( X  +  s ) )
413187breq1d 4431 . . . . . . . . . . . . . . 15  |-  ( x  =  s  ->  (
( X  +  x
)  <  ( Q `  ( i  +  1 ) )  <->  ( X  +  s )  < 
( Q `  (
i  +  1 ) ) ) )
414386, 413imbi12d 322 . . . . . . . . . . . . . 14  |-  ( x  =  s  ->  (
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  (
i  +  1 ) ) ) )  -> 
( X  +  x
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( Q `  (
i  +  1 ) ) ) ) )
415404adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( W `  ( i  +  1 ) )  e.  RR )
416 iooltub 37485 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W `  i
)  e.  RR*  /\  ( W `  ( i  +  1 ) )  e.  RR*  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  x  <  ( W `  (
i  +  1 ) ) )
417403, 406, 407, 416syl3anc 1265 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  x  <  ( W `  (
i  +  1 ) ) )
418400, 415, 401, 417ltadd2dd 9796 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  x  e.  ( ( W `  i ) (,) ( W `  ( i  +  1 ) ) ) )  ->  ( X  +  x )  <  ( X  +  ( W `  ( i  +  1 ) )