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

Theorem fourierdlem104 31834
Description: The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem104.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem104.xre  |-  ( ph  ->  X  e.  RR )
fourierdlem104.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem104.m  |-  ( ph  ->  M  e.  NN )
fourierdlem104.v  |-  ( ph  ->  V  e.  ( P `
 M ) )
fourierdlem104.x  |-  ( ph  ->  X  e.  ran  V
)
fourierdlem104.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem104.fbdioo  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. w  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( F `
 t ) )  <_  w )
fourierdlem104.fdvcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> RR ) )
fourierdlem104.fdvbd  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
fourierdlem104.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
fourierdlem104.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
fourierdlem104.h  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
fourierdlem104.k  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
fourierdlem104.u  |-  U  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( H `
 s )  x.  ( K `  s
) ) )
fourierdlem104.s  |-  S  =  ( s  e.  (
-u pi [,] pi )  |->  ( sin `  (
( n  +  ( 1  /  2 ) )  x.  s ) ) )
fourierdlem104.g  |-  G  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( U `
 s )  x.  ( S `  s
) ) )
fourierdlem104.z  |-  Z  =  ( m  e.  NN  |->  S. ( 0 (,) pi ) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  m ) `  s
) )  _d s )
fourierdlem104.e  |-  E  =  ( n  e.  NN  |->  ( S. ( 0 (,) pi ) ( G `
 s )  _d s  /  pi ) )
fourierdlem104.y  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
fourierdlem104.w  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem104.a  |-  ( ph  ->  A  e.  ( ( ( RR  _D  F
)  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem104.b  |-  ( ph  ->  B  e.  ( ( ( RR  _D  F
)  |`  ( X (,) +oo ) ) lim CC  X
) )
fourierdlem104.d  |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  / 
( 2  x.  pi ) ) ,  ( ( sin `  (
( n  +  ( 1  /  2 ) )  x.  s ) )  /  ( ( 2  x.  pi )  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) )
fourierdlem104.o  |-  O  =  ( U  |`  (
d [,] pi ) )
fourierdlem104.t  |-  T  =  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
fourierdlem104.n  |-  N  =  ( ( # `  T
)  -  1 )
fourierdlem104.j  |-  J  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
fourierdlem104.q  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
fourierdlem104.1  |-  C  =  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) )
fourierdlem104.ch  |-  ( ch  <->  ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  NN )  /\  ( abs `  S. ( 0 (,) d ) ( ( U `  s
)  x.  ( sin `  ( ( k  +  ( 1  /  2
) )  x.  s
) ) )  _d s )  <  (
e  /  2 ) )  /\  ( abs `  S. ( d (,) pi ) ( ( U `  s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )
Assertion
Ref Expression
fourierdlem104  |-  ( ph  ->  Z  ~~>  ( Y  / 
2 ) )
Distinct variable groups:    A, s    B, s    C, i, t, w, z    D, i, m, s   
n, E    i, F, k, l, s, t    m, F, k    w, F, z, k, s    e, G, k, s    i, G, t    i, H, s   
k, J, l, s   
f, J, k    i, J, t    m, J    w, J, z    K, s    L, l, s, t    k, M, l, s, i, t   
m, M, p, i   
i, N, k, l, s, t    e, N, l    f, N    m, N    w, N, z    e, O, l, s, k    t, O    Q, l, s    Q, f    Q, i, t    Q, p    R, l, s, t    S, s    T, f    U, d, k, s, l    U, n, k, s    i, V, k, s    V, p   
t, V    W, s    i, X, k, l, s, t    m, X, p   
w, X, z    i, Y, k, l, s, t   
m, Y, n, i   
w, Y, z    n, Z    e, d    i, d,
ph, t, k, l, s    ph, e    ch, s    f, d, ph    w, d, z,
ph    e, n, ph    ph, m
Allowed substitution hints:    ph( p)    ch( z, w, t, e, f, i, k, m, n, p, d, l)    A( z, w, t, e, f, i, k, m, n, p, d, l)    B( z, w, t, e, f, i, k, m, n, p, d, l)    C( e, f, k, m, n, s, p, d, l)    D( z, w, t, e, f, k, n, p, d, l)    P( z, w, t, e, f, i, k, m, n, s, p, d, l)    Q( z, w, e, k, m, n, d)    R( z, w, e, f, i, k, m, n, p, d)    S( z, w, t, e, f, i, k, m, n, p, d, l)    T( z, w, t, e, i, k, m, n, s, p, d, l)    U( z, w, t, e, f, i, m, p)    E( z, w, t, e, f, i, k, m, s, p, d, l)    F( e, f, n, p, d)    G( z, w, f, m, n, p, d, l)    H( z, w, t, e, f, k, m, n, p, d, l)    J( e, n, p, d)    K( z, w, t, e, f, i, k, m, n, p, d, l)    L( z, w, e, f, i, k, m, n, p, d)    M( z, w, e, f, n, d)    N( n, p, d)    O( z, w, f, i, m, n, p, d)    V( z, w, e, f, m, n, d, l)    W( z, w, t, e, f, i, k, m, n, p, d, l)    X( e, f, n, d)    Y( e, f, p, d)    Z( z, w, t, e, f, i, k, m, s, p, d, l)

Proof of Theorem fourierdlem104
Dummy variables  .||  b  r  c  u  j  y  x  h  v  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . . 3  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
2 1z 10906 . . . 4  |-  1  e.  ZZ
32a1i 11 . . 3  |-  ( ph  ->  1  e.  ZZ )
4 nfv 1683 . . . . 5  |-  F/ n ph
5 nfmpt1 4542 . . . . 5  |-  F/_ n
( n  e.  NN  |->  S. ( 0 (,) pi ) ( G `  s )  _d s )
6 nfmpt1 4542 . . . . 5  |-  F/_ n
( n  e.  NN  |->  pi )
7 fourierdlem104.e . . . . . 6  |-  E  =  ( n  e.  NN  |->  ( S. ( 0 (,) pi ) ( G `
 s )  _d s  /  pi ) )
8 nfmpt1 4542 . . . . . 6  |-  F/_ n
( n  e.  NN  |->  ( S. ( 0 (,) pi ) ( G `
 s )  _d s  /  pi ) )
97, 8nfcxfr 2627 . . . . 5  |-  F/_ n E
10 nnuz 11129 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
11 fourierdlem104.f . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
12 fourierdlem104.xre . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
13 ioossre 11598 . . . . . . . . . . . . 13  |-  ( X (,) +oo )  C_  RR
1413a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( X (,) +oo )  C_  RR )
1511, 14fssresd 5758 . . . . . . . . . . 11  |-  ( ph  ->  ( F  |`  ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
16 ioosscn 31414 . . . . . . . . . . . 12  |-  ( X (,) +oo )  C_  CC
1716a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( X (,) +oo )  C_  CC )
18 eqid 2467 . . . . . . . . . . . 12  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
19 pnfxr 11333 . . . . . . . . . . . . 13  |- +oo  e.  RR*
2019a1i 11 . . . . . . . . . . . 12  |-  ( ph  -> +oo  e.  RR* )
2112ltpnfd 31380 . . . . . . . . . . . 12  |-  ( ph  ->  X  < +oo )
2218, 20, 12, 21lptioo1cn 31511 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( X (,) +oo ) ) )
23 fourierdlem104.y . . . . . . . . . . 11  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
2415, 17, 22, 23limcrecl 31494 . . . . . . . . . 10  |-  ( ph  ->  Y  e.  RR )
25 ioossre 11598 . . . . . . . . . . . . 13  |-  ( -oo (,) X )  C_  RR
2625a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( -oo (,) X
)  C_  RR )
2711, 26fssresd 5758 . . . . . . . . . . 11  |-  ( ph  ->  ( F  |`  ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
28 ioosscn 31414 . . . . . . . . . . . 12  |-  ( -oo (,) X )  C_  CC
2928a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( -oo (,) X
)  C_  CC )
30 mnfxr 11335 . . . . . . . . . . . . 13  |- -oo  e.  RR*
3130a1i 11 . . . . . . . . . . . 12  |-  ( ph  -> -oo  e.  RR* )
3212mnfltd 31391 . . . . . . . . . . . 12  |-  ( ph  -> -oo  <  X )
3318, 31, 12, 32lptioo2cn 31510 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( -oo (,) X ) ) )
34 fourierdlem104.w . . . . . . . . . . 11  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
3527, 29, 33, 34limcrecl 31494 . . . . . . . . . 10  |-  ( ph  ->  W  e.  RR )
36 fourierdlem104.h . . . . . . . . . 10  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
37 fourierdlem104.k . . . . . . . . . 10  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
38 fourierdlem104.u . . . . . . . . . 10  |-  U  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( H `
 s )  x.  ( K `  s
) ) )
39 fourierdlem104.s . . . . . . . . . 10  |-  S  =  ( s  e.  (
-u pi [,] pi )  |->  ( sin `  (
( n  +  ( 1  /  2 ) )  x.  s ) ) )
40 fourierdlem104.g . . . . . . . . . 10  |-  G  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( U `
 s )  x.  ( S `  s
) ) )
41 pire 22718 . . . . . . . . . . . . 13  |-  pi  e.  RR
4241renegcli 9892 . . . . . . . . . . . 12  |-  -u pi  e.  RR
4342a1i 11 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  e.  RR )
4441a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  pi  e.  RR )
45 negpilt0 31362 . . . . . . . . . . . . . 14  |-  -u pi  <  0
46 pipos 22720 . . . . . . . . . . . . . 14  |-  0  <  pi
47 0re 9608 . . . . . . . . . . . . . . 15  |-  0  e.  RR
4842, 47, 41lttri 9722 . . . . . . . . . . . . . 14  |-  ( (
-u pi  <  0  /\  0  <  pi )  ->  -u pi  <  pi )
4945, 46, 48mp2an 672 . . . . . . . . . . . . 13  |-  -u pi  <  pi
5042, 41ltlei 9718 . . . . . . . . . . . . 13  |-  ( -u pi  <  pi  ->  -u pi  <_  pi )
5149, 50ax-mp 5 . . . . . . . . . . . 12  |-  -u pi  <_  pi
5251a1i 11 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  <_  pi )
5311, 12, 24, 35, 36fourierdlem9 31739 . . . . . . . . . . 11  |-  ( ph  ->  H : ( -u pi [,] pi ) --> RR )
54 fourierdlem104.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
55 fourierdlem104.v . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  V  e.  ( P `
 M ) )
56 fourierdlem104.p . . . . . . . . . . . . . . . . . . 19  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
5756fourierdlem2 31732 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  NN  ->  ( V  e.  ( P `  M )  <->  ( V  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
5854, 57syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( V  e.  ( P `  M )  <-> 
( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
5955, 58mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) )
6059simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  e.  ( RR 
^m  ( 0 ... M ) ) )
61 elmapi 7452 . . . . . . . . . . . . . . 15  |-  ( V  e.  ( RR  ^m  ( 0 ... M
) )  ->  V : ( 0 ... M ) --> RR )
6260, 61syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
6362ffvelrnda 6032 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
6412adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
6563, 64resubcld 9999 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
66 fourierdlem104.q . . . . . . . . . . . 12  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
6765, 66fmptd 6056 . . . . . . . . . . 11  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
6866a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) ) )
69 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( i  =  0  ->  ( V `  i )  =  ( V ` 
0 ) )
7069oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
7170adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  = 
0 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
7254nnnn0d 10864 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN0 )
73 nn0uz 11128 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
7472, 73syl6eleq 2565 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
75 eluzfz1 11705 . . . . . . . . . . . . . 14  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
7674, 75syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ( 0 ... M ) )
7762, 76ffvelrnd 6033 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( V `  0
)  e.  RR )
7877, 12resubcld 9999 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  e.  RR )
7968, 71, 76, 78fvmptd 5962 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q `  0
)  =  ( ( V `  0 )  -  X ) )
8059simprd 463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
8180simpld 459 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( V ` 
0 )  =  (
-u pi  +  X
)  /\  ( V `  M )  =  ( pi  +  X ) ) )
8281simpld 459 . . . . . . . . . . . . 13  |-  ( ph  ->  ( V `  0
)  =  ( -u pi  +  X ) )
8382oveq1d 6310 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  =  ( (
-u pi  +  X
)  -  X ) )
84 ax-resscn 9561 . . . . . . . . . . . . . 14  |-  RR  C_  CC
8584, 43sseldi 3507 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u pi  e.  CC )
8612recnd 9634 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  CC )
8785, 86pncand 9943 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
8879, 83, 873eqtrd 2512 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
89 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) } )  =  ( 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 ) ) ) } )
9043, 44, 12, 56, 89, 54, 55, 66fourierdlem14 31744 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( ( 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 ) ) ) } ) `
 M ) )
9189fourierdlem2 31732 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  ( Q  e.  ( (
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 ) ) ) } ) `
 M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
9254, 91syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Q  e.  ( ( 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 ) ) ) } ) `
 M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
9390, 92mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  -u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
9493simprd 463 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Q `
 0 )  = 
-u pi  /\  ( Q `  M )  =  pi )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
9594simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q ` 
0 )  =  -u pi  /\  ( Q `  M )  =  pi ) )
9695simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  ( Q `  M
)  =  pi )
9794simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
9897r19.21bi 2836 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
9911adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  F : RR --> RR )
10089, 54, 90fourierdlem15 31745 . . . . . . . . . . . . . 14  |-  ( ph  ->  Q : ( 0 ... M ) --> (
-u pi [,] pi ) )
101100adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
102 elfzofz 11823 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
103102adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
104101, 103ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  (
-u pi [,] pi ) )
105 fzofzp1 11889 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
106105adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
107101, 106ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  (
-u pi [,] pi ) )
10812adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
109 fourierdlem104.x . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  ran  V
)
110 ffn 5737 . . . . . . . . . . . . . . . . . 18  |-  ( V : ( 0 ... M ) --> RR  ->  V  Fn  ( 0 ... M ) )
11160, 61, 1103syl 20 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  V  Fn  ( 0 ... M ) )
112 fvelrnb 5921 . . . . . . . . . . . . . . . . 17  |-  ( V  Fn  ( 0 ... M )  ->  ( X  e.  ran  V  <->  E. i  e.  ( 0 ... M
) ( V `  i )  =  X ) )
113111, 112syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  e.  ran  V  <->  E. i  e.  (
0 ... M ) ( V `  i )  =  X ) )
114109, 113mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E. i  e.  ( 0 ... M ) ( V `  i
)  =  X )
115 oveq1 6302 . . . . . . . . . . . . . . . . . . 19  |-  ( ( V `  i )  =  X  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
116115adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  (
( V `  i
)  -  X )  =  ( X  -  X ) )
11786subidd 9930 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( X  -  X
)  =  0 )
118117ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  ( X  -  X )  =  0 )
119116, 118eqtr2d 2509 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0 ... M
) )  /\  ( V `  i )  =  X )  ->  0  =  ( ( V `
 i )  -  X ) )
120119ex 434 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  =  X  -> 
0  =  ( ( V `  i )  -  X ) ) )
121120reximdva 2942 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E. i  e.  ( 0 ... M
) ( V `  i )  =  X  ->  E. i  e.  ( 0 ... M ) 0  =  ( ( V `  i )  -  X ) ) )
122114, 121mpd 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  E. i  e.  ( 0 ... M ) 0  =  ( ( V `  i )  -  X ) )
12366elrnmpt 5255 . . . . . . . . . . . . . . 15  |-  ( 0  e.  RR  ->  (
0  e.  ran  Q  <->  E. i  e.  ( 0 ... M ) 0  =  ( ( V `
 i )  -  X ) ) )
12447, 123ax-mp 5 . . . . . . . . . . . . . 14  |-  ( 0  e.  ran  Q  <->  E. i  e.  ( 0 ... M
) 0  =  ( ( V `  i
)  -  X ) )
125122, 124sylibr 212 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ran  Q
)
12689, 54, 90, 125fourierdlem12 31742 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  -.  0  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
127 fourierdlem104.fcn . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
12862adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
129128, 103ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
130129, 108resubcld 9999 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
13166fvmpt2 5964 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
132103, 130, 131syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
133132oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( ( ( V `  i )  -  X
)  +  X ) )
13484, 129sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  CC )
13586adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  CC )
136134, 135npcand 9946 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  i )  -  X )  +  X )  =  ( V `  i ) )
137133, 136eqtrd 2508 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  +  X )  =  ( V `  i ) )
138 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  i  ->  ( V `  j )  =  ( V `  i ) )
139138oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  i  ->  (
( V `  j
)  -  X )  =  ( ( V `
 i )  -  X ) )
140139cbvmptv 4544 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... M )  |->  ( ( V `  j )  -  X ) )  =  ( i  e.  ( 0 ... M
)  |->  ( ( V `
 i )  -  X ) )
14166, 140eqtr4i 2499 . . . . . . . . . . . . . . . . . . . 20  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
142141a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
143 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
144143oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
145144adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
146128, 106ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
147146, 108resubcld 9999 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
148142, 145, 106, 147fvmptd 5962 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
149148oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  X )  =  ( ( ( V `  ( i  +  1 ) )  -  X
)  +  X ) )
15084, 146sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  CC )
151150, 135npcand 9946 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( V `  ( i  +  1 ) )  -  X )  +  X )  =  ( V `  ( i  +  1 ) ) )
152149, 151eqtrd 2508 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 ( i  +  1 ) )  +  X )  =  ( V `  ( i  +  1 ) ) )
153137, 152oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( Q `  i )  +  X ) (,) ( ( Q `  ( i  +  1 ) )  +  X
) )  =  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
154153reseq2d 5279 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( ( Q `
 i )  +  X ) (,) (
( Q `  (
i  +  1 ) )  +  X ) ) )  =  ( F  |`  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ) )
155153oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( ( Q `  i
)  +  X ) (,) ( ( Q `
 ( i  +  1 ) )  +  X ) ) -cn-> CC )  =  ( ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) )
-cn-> CC ) )
156154, 155eleq12d 2549 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( F  |`  ( ( ( Q `
 i )  +  X ) (,) (
( Q `  (
i  +  1 ) )  +  X ) ) )  e.  ( ( ( ( Q `
 i )  +  X ) (,) (
( Q `  (
i  +  1 ) )  +  X ) ) -cn-> CC )  <->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) ) )
157127, 156mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( ( Q `
 i )  +  X ) (,) (
( Q `  (
i  +  1 ) )  +  X ) ) )  e.  ( ( ( ( Q `
 i )  +  X ) (,) (
( Q `  (
i  +  1 ) )  +  X ) ) -cn-> CC ) )
15824adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Y  e.  RR )
15935adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  W  e.  RR )
16099, 104, 107, 108, 126, 157, 158, 159, 36fourierdlem40 31770 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
161 fourierdlem104.r . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
162 eqid 2467 . . . . . . . . . . . 12  |-  ( RR 
_D  F )  =  ( RR  _D  F
)
163 fourierdlem104.fdvcn . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> RR ) )
164 cncff 21265 . . . . . . . . . . . . 13  |-  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  e.  ( ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) -cn-> RR )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
165 id 22 . . . . . . . . . . . . . 14  |-  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  ->  (
( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR )
16684a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  ->  RR  C_  CC )
167 fss 5745 . . . . . . . . . . . . . 14  |-  ( ( ( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR 
/\  RR  C_  CC )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
168165, 166, 167syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR  ->  (
( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC )
169163, 164, 1683syl 20 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
170 fourierdlem104.b . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  ( ( ( RR  _D  F
)  |`  ( X (,) +oo ) ) lim CC  X
) )
171 eqid 2467 . . . . . . . . . . . 12  |-  if ( ( V `  i
)  =  X ,  B ,  ( ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  /  ( Q `
 i ) ) )  =  if ( ( V `  i
)  =  X ,  B ,  ( ( R  -  if (
( V `  i
)  <  X ,  W ,  Y )
)  /  ( Q `
 i ) ) )
17212, 56, 11, 109, 23, 35, 36, 54, 55, 161, 66, 89, 162, 169, 170, 171fourierdlem75 31805 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  if ( ( V `  i )  =  X ,  B ,  ( ( R  -  if ( ( V `  i )  <  X ,  W ,  Y ) )  / 
( Q `  i
) ) )  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
173 fourierdlem104.l . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
174163, 164syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
175 fourierdlem104.a . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  ( ( ( RR  _D  F
)  |`  ( -oo (,) X ) ) lim CC  X ) )
176 eqid 2467 . . . . . . . . . . . 12  |-  if ( ( V `  (
i  +  1 ) )  =  X ,  A ,  ( ( L  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  /  ( Q `
 ( i  +  1 ) ) ) )  =  if ( ( V `  (
i  +  1 ) )  =  X ,  A ,  ( ( L  -  if (
( V `  (
i  +  1 ) )  <  X ,  W ,  Y )
)  /  ( Q `
 ( i  +  1 ) ) ) )
17712, 56, 11, 109, 24, 34, 36, 54, 55, 173, 66, 89, 162, 174, 175, 176fourierdlem74 31804 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  if ( ( V `  ( i  +  1 ) )  =  X ,  A ,  ( ( L  -  if ( ( V `  ( i  +  1 ) )  <  X ,  W ,  Y ) )  / 
( Q `  (
i  +  1 ) ) ) )  e.  ( ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
178 fveq2 5872 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  ( Q `  j )  =  ( Q `  i ) )
179 oveq1 6302 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
180179fveq2d 5876 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  ( Q `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
181178, 180oveq12d 6313 . . . . . . . . . . . 12  |-  ( j  =  i  ->  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
182181cbvmptv 4544 . . . . . . . . . . 11  |-  ( j  e.  ( 0..^ M )  |->  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )  =  ( i  e.  ( 0..^ M )  |->  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
18343, 44, 52, 53, 54, 67, 88, 96, 98, 160, 172, 177, 182fourierdlem70 31800 . . . . . . . . . 10  |-  ( ph  ->  E. x  e.  RR  A. s  e.  ( -u pi [,] pi ) ( abs `  ( H `
 s ) )  <_  x )
18411adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  F : RR
--> RR )
185109adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  X  e. 
ran  V )
18623adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  Y  e.  ( ( F  |`  ( X (,) +oo )
) lim CC  X )
)
18734adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
188 nnre 10555 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  n  e.  RR )
189188adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  RR )
19054adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  M  e.  NN )
19155adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  V  e.  ( P `  M
) )
192127adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
193161adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  i )
) )
194173adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )
195174adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
196175adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  A  e.  ( ( ( RR 
_D  F )  |`  ( -oo (,) X ) ) lim CC  X ) )
197170adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  B  e.  ( ( ( RR 
_D  F )  |`  ( X (,) +oo )
) lim CC  X )
)
19856, 184, 185, 186, 187, 36, 37, 38, 189, 39, 40, 190, 191, 192, 193, 194, 140, 89, 162, 195, 196, 197fourierdlem88 31818 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  G  e.  L^1 )
199 eqid 2467 . . . . . . . . . 10  |-  ( ( e  /  3 )  /  y )  =  ( ( e  / 
3 )  /  y
)
200 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  s  ->  ( G `  t )  =  ( G `  s ) )
201200fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( t  =  s  ->  ( abs `  ( G `  t ) )  =  ( abs `  ( G `  s )
) )
202201breq1d 4463 . . . . . . . . . . . . . . . 16  |-  ( t  =  s  ->  (
( abs `  ( G `  t )
)  <_  y  <->  ( abs `  ( G `  s
) )  <_  y
) )
203202cbvralv 3093 . . . . . . . . . . . . . . 15  |-  ( A. t  e.  ( -u pi [,] pi ) ( abs `  ( G `  t
) )  <_  y  <->  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `
 s ) )  <_  y )
204203ralbii 2898 . . . . . . . . . . . . . 14  |-  ( A. n  e.  NN  A. t  e.  ( -u pi [,] pi ) ( abs `  ( G `  t )
)  <_  y  <->  A. n  e.  NN  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `  s )
)  <_  y )
2052043anbi3i 1189 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. t  e.  ( -u pi [,] pi ) ( abs `  ( G `  t )
)  <_  y )  <->  ( ( ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `  s )
)  <_  y )
)
206205anbi1i 695 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. t  e.  ( -u pi [,] pi ) ( abs `  ( G `  t )
)  <_  y )  /\  u  e.  dom  vol )  <->  ( ( (
ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `  s )
)  <_  y )  /\  u  e.  dom  vol ) )
207206anbi1i 695 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. t  e.  ( -u pi [,] pi ) ( abs `  ( G `  t )
)  <_  y )  /\  u  e.  dom  vol )  /\  ( u 
C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
( ( e  / 
3 )  /  y
) ) )  <->  ( (
( ( ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `  s )
)  <_  y )  /\  u  e.  dom  vol )  /\  ( u 
C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
( ( e  / 
3 )  /  y
) ) ) )
208207anbi1i 695 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. t  e.  ( -u pi [,] pi ) ( abs `  ( G `  t )
)  <_  y )  /\  u  e.  dom  vol )  /\  ( u 
C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
( ( e  / 
3 )  /  y
) ) )  /\  n  e.  NN )  <->  ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  y  e.  RR+  /\  A. n  e.  NN  A. s  e.  ( -u pi [,] pi ) ( abs `  ( G `  s )
)  <_  y )  /\  u  e.  dom  vol )  /\  ( u 
C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
( ( e  / 
3 )  /  y
) ) )  /\  n  e.  NN )
)
20911, 12, 24, 35, 36, 37, 38, 39, 40, 183, 198, 199, 208fourierdlem87 31817 . . . . . . . . 9  |-  ( (
ph  /\  e  e.  RR+ )  ->  E. c  e.  RR+  A. u  e. 
dom  vol ( ( u 
C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )
210 iftrue 3951 . . . . . . . . . . . . . . . 16  |-  ( c  <_  ( pi  / 
2 )  ->  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  =  c )
211210adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  =  c )
212 0xr 9652 . . . . . . . . . . . . . . . . 17  |-  0  e.  RR*
213212a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  0  e.  RR* )
21441rexri 9658 . . . . . . . . . . . . . . . . 17  |-  pi  e.  RR*
215214a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  pi  e.  RR* )
216 rpre 11238 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  RR+  ->  c  e.  RR )
217216adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  c  e.  RR )
218 rpgt0 11243 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  RR+  ->  0  < 
c )
219218adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  0  <  c )
22041rehalfcli 10799 . . . . . . . . . . . . . . . . . . 19  |-  ( pi 
/  2 )  e.  RR
221220a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  ( pi 
/  2 )  e.  RR )
222221adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  (
pi  /  2 )  e.  RR )
22341a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  pi  e.  RR )
224 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  c  <_  ( pi  /  2
) )
225 halfpos 10781 . . . . . . . . . . . . . . . . . . . 20  |-  ( pi  e.  RR  ->  (
0  <  pi  <->  ( pi  /  2 )  <  pi ) )
22641, 225ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  <  pi  <->  ( pi  /  2 )  <  pi )
22746, 226mpbi 208 . . . . . . . . . . . . . . . . . 18  |-  ( pi 
/  2 )  < 
pi
228227a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  (
pi  /  2 )  <  pi )
229217, 222, 223, 224, 228lelttrd 9751 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  c  <  pi )
230213, 215, 217, 219, 229eliood 31418 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  c  e.  ( 0 (,) pi ) )
231211, 230eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  e.  ( 0 (,) pi ) )
232 iffalse 3954 . . . . . . . . . . . . . . . 16  |-  ( -.  c  <_  ( pi  /  2 )  ->  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  =  ( pi 
/  2 ) )
233 2pos 10639 . . . . . . . . . . . . . . . . . . 19  |-  0  <  2
234 2re 10617 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
23541, 234divgt0i 10466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  <  pi  /\  0  <  2 )  -> 
0  <  ( pi  /  2 ) )
23646, 233, 235mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  0  <  ( pi  /  2
)
237 elioo2 11582 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  RR*  /\  pi  e.  RR* )  ->  (
( pi  /  2
)  e.  ( 0 (,) pi )  <->  ( (
pi  /  2 )  e.  RR  /\  0  <  ( pi  /  2
)  /\  ( pi  /  2 )  <  pi ) ) )
238212, 214, 237mp2an 672 . . . . . . . . . . . . . . . . . 18  |-  ( ( pi  /  2 )  e.  ( 0 (,) pi )  <->  ( (
pi  /  2 )  e.  RR  /\  0  <  ( pi  /  2
)  /\  ( pi  /  2 )  <  pi ) )
239220, 236, 227, 238mpbir3an 1178 . . . . . . . . . . . . . . . . 17  |-  ( pi 
/  2 )  e.  ( 0 (,) pi )
240239a1i 11 . . . . . . . . . . . . . . . 16  |-  ( -.  c  <_  ( pi  /  2 )  ->  (
pi  /  2 )  e.  ( 0 (,) pi ) )
241232, 240eqeltrd 2555 . . . . . . . . . . . . . . 15  |-  ( -.  c  <_  ( pi  /  2 )  ->  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  e.  ( 0 (,) pi ) )
242241adantl 466 . . . . . . . . . . . . . 14  |-  ( ( c  e.  RR+  /\  -.  c  <_  ( pi  / 
2 ) )  ->  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  e.  ( 0 (,) pi ) )
243231, 242pm2.61dan 789 . . . . . . . . . . . . 13  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  e.  ( 0 (,) pi ) )
2442433ad2ant2 1018 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  c  e.  RR+  /\  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )  ->  if (
c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  e.  ( 0 (,) pi ) )
245 ioombl 21843 . . . . . . . . . . . . . . . 16  |-  ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) )  e.  dom  vol
246245a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  RR+  /\  A. u  e.  dom  vol (
( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )  -> 
( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) )  e.  dom  vol )
247 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  RR+  /\  A. u  e.  dom  vol (
( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )  ->  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )
248246, 247jca 532 . . . . . . . . . . . . . 14  |-  ( ( c  e.  RR+  /\  A. u  e.  dom  vol (
( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )  -> 
( ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  e. 
dom  vol  /\  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) ) )
249 ioossicc 11622 . . . . . . . . . . . . . . . . . 18  |-  ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( 0 [,]
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )
250249a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  RR+  ->  ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( 0 [,]
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) )
25142a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  -u pi  e.  RR )
25241a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  pi  e.  RR )
25342, 47ltlei 9718 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u pi  <  0  ->  -u pi  <_  0 )
25445, 253ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  -u pi  <_  0
255254a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  -u pi  <_  0 )
256 elioore 11571 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( 0 (,) pi )  ->  s  e.  RR )
257256ssriv 3513 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) pi )  C_  RR
258257, 243sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  e.  RR )
259 min2 11402 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c  e.  RR  /\  ( pi  /  2
)  e.  RR )  ->  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  <_ 
( pi  /  2
) )
260216, 221, 259syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  <_ 
( pi  /  2
) )
261227a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  e.  RR+  ->  ( pi 
/  2 )  < 
pi )
262258, 221, 252, 260, 261lelttrd 9751 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  < 
pi )
263258, 252, 262ltled 9744 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  <_  pi )
264 iccss 11604 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -u pi  e.  RR  /\  pi  e.  RR )  /\  ( -u pi  <_  0  /\  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  <_  pi ) )  ->  (
0 [,] if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( -u pi [,] pi ) )
265251, 252, 255, 263, 264syl22anc 1229 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  RR+  ->  ( 0 [,] if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( -u pi [,] pi ) )
266250, 265sstrd 3519 . . . . . . . . . . . . . . . 16  |-  ( c  e.  RR+  ->  ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( -u pi [,] pi ) )
26747a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  RR+  ->  0  e.  RR )
268219, 211breqtrrd 4479 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c  e.  RR+  /\  c  <_  ( pi  /  2
) )  ->  0  <  if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )
269236, 232syl5breqr 4489 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  c  <_  ( pi  /  2 )  ->  0  <  if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )
270269adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c  e.  RR+  /\  -.  c  <_  ( pi  / 
2 ) )  -> 
0  <  if (
c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) )
271268, 270pm2.61dan 789 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  e.  RR+  ->  0  < 
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )
272267, 258, 271ltled 9744 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  RR+  ->  0  <_  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) )
273 volioo 31589 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  RR  /\  if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  e.  RR  /\  0  <_  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) )  ->  ( vol `  (
0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) )  =  ( if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  -  0 ) )
274267, 258, 272, 273syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  ( vol `  ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) )  =  ( if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  - 
0 ) )
27584, 258sseldi 3507 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  e.  CC )
276275subid1d 9931 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  RR+  ->  ( if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) )  -  0 )  =  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) )
277274, 276eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  RR+  ->  ( vol `  ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) )  =  if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )
278 min1 11401 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  e.  RR  /\  ( pi  /  2
)  e.  RR )  ->  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  <_ 
c )
279216, 221, 278syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  RR+  ->  if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) )  <_ 
c )
280277, 279eqbrtrd 4473 . . . . . . . . . . . . . . . 16  |-  ( c  e.  RR+  ->  ( vol `  ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) )  <_ 
c )
281266, 280jca 532 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  ( ( 0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( -u pi [,] pi )  /\  ( vol `  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) )  <_  c ) )
282281adantr 465 . . . . . . . . . . . . . 14  |-  ( ( c  e.  RR+  /\  A. u  e.  dom  vol (
( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )  -> 
( ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  C_  ( -u pi [,] pi )  /\  ( vol `  (
0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) )  <_  c )
)
283 sseq1 3530 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( u  C_  ( -u pi [,] pi )  <-> 
( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) )  C_  ( -u pi [,] pi ) ) )
284 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( vol `  u
)  =  ( vol `  ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) ) )
285284breq1d 4463 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( ( vol `  u
)  <_  c  <->  ( vol `  ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) )  <_ 
c ) )
286283, 285anbi12d 710 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  <->  ( ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) )  C_  ( -u pi [,] pi )  /\  ( vol `  (
0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) )  <_  c )
) )
287 itgeq1 22047 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  ->  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s  =  S. ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )
288287fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  =  ( abs `  S. ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) ( ( U `  s
)  x.  ( sin `  ( ( k  +  ( 1  /  2
) )  x.  s
) ) )  _d s ) )
289288breq1d 4463 . . . . . . . . . . . . . . . . 17  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 )  <->  ( abs `  S. ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) ( ( U `  s
)  x.  ( sin `  ( ( k  +  ( 1  /  2
) )  x.  s
) ) )  _d s )  <  (
e  /  2 ) ) )
290289ralbidv 2906 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 )  <->  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) ( ( U `  s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )
291286, 290imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( u  =  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) )  -> 
( ( ( u 
C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) )  <-> 
( ( ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( -u pi [,] pi )  /\  ( vol `  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) )  <_  c )  ->  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) ) )
292291rspcva 3217 . . . . . . . . . . . . . 14  |-  ( ( ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) )  e.  dom  vol 
/\  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )  -> 
( ( ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) 
C_  ( -u pi [,] pi )  /\  ( vol `  ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) )  <_  c )  ->  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )
293248, 282, 292sylc 60 . . . . . . . . . . . . 13  |-  ( ( c  e.  RR+  /\  A. u  e.  dom  vol (
( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )  ->  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  ( pi  /  2 ) ,  c ,  ( pi  / 
2 ) ) ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) )
2942933adant1 1014 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  c  e.  RR+  /\  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )  ->  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) ( ( U `  s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) )
295 oveq2 6303 . . . . . . . . . . . . . . . . 17  |-  ( d  =  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  -> 
( 0 (,) d
)  =  ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) )
296295itgeq1d 31597 . . . . . . . . . . . . . . . 16  |-  ( d  =  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  ->  S. ( 0 (,) d
) ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s  =  S. ( 0 (,) if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) ) ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )
297296fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( d  =  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  -> 
( abs `  S. ( 0 (,) d
) ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  =  ( abs `  S. ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) ( ( U `  s
)  x.  ( sin `  ( ( k  +  ( 1  /  2
) )  x.  s
) ) )  _d s ) )
298297breq1d 4463 . . . . . . . . . . . . . 14  |-  ( d  =  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  -> 
( ( abs `  S. ( 0 (,) d
) ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 )  <->  ( abs `  S. ( 0 (,)
if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) ) ) ( ( U `  s
)  x.  ( sin `  ( ( k  +  ( 1  /  2
) )  x.  s
) ) )  _d s )  <  (
e  /  2 ) ) )
299298ralbidv 2906 . . . . . . . . . . . . 13  |-  ( d  =  if ( c  <_  ( pi  / 
2 ) ,  c ,  ( pi  / 
2 ) )  -> 
( A. k  e.  NN  ( abs `  S. ( 0 (,) d
) ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 )  <->  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) ( ( U `  s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )
300299rspcev 3219 . . . . . . . . . . . 12  |-  ( ( if ( c  <_ 
( pi  /  2
) ,  c ,  ( pi  /  2
) )  e.  ( 0 (,) pi )  /\  A. k  e.  NN  ( abs `  S. ( 0 (,) if ( c  <_  (
pi  /  2 ) ,  c ,  ( pi  /  2 ) ) ) ( ( U `  s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) )  ->  E. d  e.  ( 0 (,) pi ) A. k  e.  NN  ( abs `  S. ( 0 (,) d ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) )
301244, 294, 300syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  c  e.  RR+  /\  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) ) )  ->  E. d  e.  ( 0 (,) pi ) A. k  e.  NN  ( abs `  S. ( 0 (,) d ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) )
3023013exp 1195 . . . . . . . . . 10  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( c  e.  RR+  ->  ( A. u  e.  dom  vol (
( u  C_  ( -u pi [,] pi )  /\  ( vol `  u
)  <_  c )  ->  A. k  e.  NN  ( abs `  S. u
( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) )  ->  E. d  e.  ( 0 (,) pi ) A. k  e.  NN  ( abs `  S. ( 0 (,) d ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) ) )
303302rexlimdv 2957 . . . . . . . . 9  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( E. c  e.  RR+  A. u  e.  dom  vol ( ( u  C_  ( -u pi [,] pi )  /\  ( vol `  u )  <_ 
c )  ->  A. k  e.  NN  ( abs `  S. u ( ( U `
 s )  x.  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )  _d s )  <  ( e  /  2 ) )  ->  E. d  e.  ( 0 (,) pi ) A. k  e.  NN  ( abs `  S. ( 0 (,) d ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) ) )
304209, 303mpd 15 . . . . . . . 8  |-  ( (
ph  /\  e  e.  RR+ )  ->  E. d  e.  ( 0 (,) pi ) A. k  e.  NN  ( abs `  S. ( 0 (,) d ) ( ( U `  s )  x.  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  s ) ) )  _d s )  < 
( e  /  2
) )
305257sseli 3505 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( 0 (,) pi )  ->  d  e.  RR )
306305adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  e.  RR )
30741a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  e.  RR )
30811, 12, 24, 35, 36, 37, 38fourierdlem55 31785 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  U : ( -u pi [,] pi ) --> RR )
30984a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  RR  C_  CC )
310308, 309fssd 5746 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U : ( -u pi [,] pi ) --> CC )
311310adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  U : ( -u pi [,] pi ) --> CC )
31242a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  -u pi  e.  RR )
31342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  e.  RR )
31447a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( 0 (,) pi )  ->  0  e.  RR )
31545a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  <  0 )
316 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  d  e.  ( 0 (,) pi ) )  ->  0  <  d )
317212, 214, 316mp3an12 1314 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( 0 (,) pi )  ->  0  <  d )
318313, 314, 305, 315, 317lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  <  d )
319313, 305, 318ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  <_  d )
320319adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  -u pi  <_  d )
321307leidd 10131 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  <_  pi )
322 iccss 11604 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( -u pi  e.  RR  /\  pi  e.  RR )  /\  ( -u pi  <_  d  /\  pi  <_  pi ) )  ->  (
d [,] pi ) 
C_  ( -u pi [,] pi ) )
323312, 307, 320, 321, 322syl22anc 1229 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d [,] pi ) 
C_  ( -u pi [,] pi ) )
324311, 323fssresd 5758 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( U  |`  ( d [,] pi ) ) : ( d [,] pi )
--> CC )
325 fourierdlem104.o . . . . . . . . . . . . . . . . . . . . 21  |-  O  =  ( U  |`  (
d [,] pi ) )
326325a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  O  =  ( U  |`  ( d [,] pi ) ) )
327326feq1d 5723 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( O : ( d [,] pi ) --> CC  <->  ( U  |`  ( d [,] pi ) ) : ( d [,] pi ) --> CC ) )
328324, 327mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  O : ( d [,] pi ) --> CC )
329 fourierdlem104.n . . . . . . . . . . . . . . . . . . . . . 22  |-  N  =  ( ( # `  T
)  -  1 )
33041elexi 3128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  pi  e.  _V
331330prid2 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  pi  e.  { d ,  pi }
332 elun1 3676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( pi  e.  { d ,  pi }  ->  pi  e.  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) ) )
333331, 332ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  pi  e.  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
334 fourierdlem104.t . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  T  =  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
335334eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )  =  T
336333, 335eleqtri 2553 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  pi  e.  T
337 ne0i 3796 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( pi  e.  T  ->  T  =/=  (/) )
338336, 337ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  T  =/=  (/)
339338a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  T  =/=  (/) )
340 prfi 7807 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { d ,  pi }  e.  Fin
341340a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  { d ,  pi }  e.  Fin )
342 fzfi 12062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 0 ... M )  e. 
Fin
34366rnmptfi 31348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
344342, 343ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ran  Q  e.  Fin
345344a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ran  Q  e.  Fin )
346 infi 7755 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  (
d (,) pi ) )  e.  Fin )
347345, 346syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ran  Q  i^i  ( d (,) pi ) )  e.  Fin )
348 unfi 7799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( { d ,  pi }  e.  Fin  /\  ( ran  Q  i^i  ( d (,) pi ) )  e.  Fin )  -> 
( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )  e.  Fin )
349341, 347, 348syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )  e.  Fin )
350334, 349syl5eqel 2559 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  T  e.  Fin )
351 hashnncl 12416 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T  e.  Fin  ->  (
( # `  T )  e.  NN  <->  T  =/=  (/) ) )
352350, 351syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( # `  T
)  e.  NN  <->  T  =/=  (/) ) )
353339, 352mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( # `  T
)  e.  NN )
354 nnm1nn0 10849 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
# `  T )  e.  NN  ->  ( ( # `
 T )  - 
1 )  e.  NN0 )
355353, 354syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( # `  T
)  -  1 )  e.  NN0 )
356329, 355syl5eqel 2559 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  NN0 )
357356adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  e.  NN0 )
35847a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  0  e.  RR )
359 1re 9607 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR
360359a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  1  e.  RR )
361357nn0red 10865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  e.  RR )
362 0lt1 10087 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  1
363362a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  0  <  1 )
364 2m1e1 10662 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 2  -  1 )  =  1
365364eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 2  -  1 )
366365a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  1  =  ( 2  -  1 ) )
367234a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  2  e.  RR )
368353nnred 10563 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( # `  T
)  e.  RR )
369368adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( # `
 T )  e.  RR )
370 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  d  e.  ( 0 (,) pi ) )  ->  d  <  pi )
371212, 214, 370mp3an12 1314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  e.  ( 0 (,) pi )  ->  d  <  pi )
372305, 371ltned 9732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  e.  ( 0 (,) pi )  ->  d  =/=  pi )
373372adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  =/=  pi )
374 hashprg 12440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  e.  RR  /\  pi  e.  RR )  -> 
( d  =/=  pi  <->  (
# `  { d ,  pi } )  =  2 ) )
375306, 307, 374syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d  =/=  pi  <->  ( # `  {
d ,  pi }
)  =  2 ) )
376373, 375mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( # `
 { d ,  pi } )  =  2 )
377376eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  2  =  ( # `  {
d ,  pi }
) )
378350adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  T  e.  Fin )
379 ssun1 3672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  { d ,  pi }  C_  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
380379, 335sseqtri 3541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { d ,  pi }  C_  T
381380a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  { d ,  pi }  C_  T )
382 hashssle 31397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T  e.  Fin  /\  { d ,  pi }  C_  T )  ->  ( # `
 { d ,  pi } )  <_ 
( # `  T ) )
383378, 381, 382syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( # `
 { d ,  pi } )  <_ 
( # `  T ) )
384377, 383eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  2  <_  ( # `  T
) )
385367, 369, 360, 384lesub1dd 10180 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
2  -  1 )  <_  ( ( # `  T )  -  1 ) )
386366, 385eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  1  <_  ( ( # `  T
)  -  1 ) )
387329eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  T )  -  1 )  =  N
388387a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
( # `  T )  -  1 )  =  N )
389386, 388breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  1  <_  N )
390358, 360, 361, 363, 389ltletrd 9753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  0  <  N )
391358, 390gtned 9731 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  =/=  0 )
392357, 391jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( N  e.  NN0  /\  N  =/=  0 ) )
393 elnnne0 10821 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  <->  ( N  e.  NN0  /\  N  =/=  0 ) )
394392, 393sylibr 212 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  e.  NN )
395 fourierdlem104.j . . . . . . . . . . . . . . . . . . . . 21  |-  J  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
396306leidd 10131 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  <_  d )
39741a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  e.  ( 0 (,) pi )  ->  pi  e.  RR )
398305, 397, 371ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( d  e.  ( 0 (,) pi )  ->  d  <_  pi )
399398adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  <_  pi )
400306, 307, 306, 396, 399eliccd 31425 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  e.  ( d [,] pi ) )
401306, 307, 307, 399, 321eliccd 31425 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  e.  ( d [,] pi ) )
402400, 401jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d  e.  ( d [,] pi )  /\  pi  e.  ( d [,] pi ) ) )
403 vex 3121 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  d  e. 
_V
404403, 330prss 4187 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  ( d [,] pi )  /\  pi  e.  ( d [,] pi ) )  <->  { d ,  pi }  C_  (
d [,] pi ) )
405402, 404sylib 196 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  { d ,  pi }  C_  ( d [,] pi ) )
406 inss2 3724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ran 
Q  i^i  ( d (,) pi ) )  C_  ( d (,) pi )
407406a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( ran  Q  i^i  ( d (,) pi ) ) 
C_  ( d (,) pi ) )
408 ioossicc 11622 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( d (,) pi )  C_  ( d [,] pi )
409408a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d (,) pi ) 
C_  ( d [,] pi ) )
410407, 409sstrd 3519 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( ran  Q  i^i  ( d (,) pi ) ) 
C_  ( d [,] pi ) )
411405, 410unssd 3685 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) ) 
C_  ( d [,] pi ) )
412334, 411syl5eqss 3553 . . . . . . . . . . . . . . .