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

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

Proof of Theorem fourierdlem103
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 2429 . . 3  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
2 1zzd 10968 . . 3  |-  ( ph  ->  1  e.  ZZ )
3 nfv 1754 . . . . 5  |-  F/ n ph
4 nfmpt1 4515 . . . . 5  |-  F/_ n
( n  e.  NN  |->  S. ( -u pi (,) 0 ) ( G `
 s )  _d s )
5 nfmpt1 4515 . . . . 5  |-  F/_ n
( n  e.  NN  |->  pi )
6 fourierdlem103.e . . . . . 6  |-  E  =  ( n  e.  NN  |->  ( S. ( -u pi (,) 0 ) ( G `
 s )  _d s  /  pi ) )
7 nfmpt1 4515 . . . . . 6  |-  F/_ n
( n  e.  NN  |->  ( S. ( -u pi (,) 0 ) ( G `
 s )  _d s  /  pi ) )
86, 7nfcxfr 2589 . . . . 5  |-  F/_ n E
9 nnuz 11194 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
10 pire 23278 . . . . . . . . . . . . . . . . 17  |-  pi  e.  RR
1110renegcli 9934 . . . . . . . . . . . . . . . 16  |-  -u pi  e.  RR
1211a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  e.  RR )
13 elioore 11666 . . . . . . . . . . . . . . . 16  |-  ( d  e.  ( -u pi (,) 0 )  ->  d  e.  RR )
1413adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  d  e.  RR )
15 fourierdlem103.f . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F : RR --> RR )
16 fourierdlem103.xre . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  X  e.  RR )
17 ioossre 11696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( X (,) +oo )  C_  RR
1817a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( X (,) +oo )  C_  RR )
1915, 18fssresd 5767 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( F  |`  ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
20 ioosscn 37175 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X (,) +oo )  C_  CC
2120a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( X (,) +oo )  C_  CC )
22 eqid 2429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
23 pnfxr 11412 . . . . . . . . . . . . . . . . . . . . . . 23  |- +oo  e.  RR*
2423a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> +oo  e.  RR* )
2516ltpnfd 11423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  < +oo )
2622, 24, 16, 25lptioo1cn 37298 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( X (,) +oo ) ) )
27 fourierdlem103.y . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
2819, 21, 26, 27limcrecl 37280 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Y  e.  RR )
29 ioossre 11696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -oo (,) X )  C_  RR
3029a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( -oo (,) X
)  C_  RR )
3115, 30fssresd 5767 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( F  |`  ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
32 ioosscn 37175 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -oo (,) X )  C_  CC
3332a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( -oo (,) X
)  C_  CC )
34 mnfxr 11414 . . . . . . . . . . . . . . . . . . . . . . 23  |- -oo  e.  RR*
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> -oo  e.  RR* )
3616mnfltd 11426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> -oo  <  X )
3722, 35, 16, 36lptioo2cn 37297 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( -oo (,) X ) ) )
38 fourierdlem103.w . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
3931, 33, 37, 38limcrecl 37280 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  W  e.  RR )
40 fourierdlem103.h . . . . . . . . . . . . . . . . . . . 20  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
41 fourierdlem103.k . . . . . . . . . . . . . . . . . . . 20  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
42 fourierdlem103.u . . . . . . . . . . . . . . . . . . . 20  |-  U  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( H `
 s )  x.  ( K `  s
) ) )
4315, 16, 28, 39, 40, 41, 42fourierdlem55 37592 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  U : ( -u pi [,] pi ) --> RR )
44 ax-resscn 9595 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  CC
4544a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  C_  CC )
4643, 45fssd 5755 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U : ( -u pi [,] pi ) --> CC )
4746adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  U : ( -u pi [,] pi ) --> CC )
4811a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( -u pi (,) 0 )  ->  -u pi  e.  RR )
4910a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( -u pi (,) 0 )  ->  pi  e.  RR )
5048leidd 10179 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( -u pi (,) 0 )  ->  -u pi  <_ 
-u pi )
51 0red 9643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( -u pi (,) 0 )  ->  0  e.  RR )
5211rexri 9692 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u pi  e.  RR*
53 0xr 9686 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR*
54 iooltub 37194 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  d  e.  ( -u pi (,) 0 ) )  -> 
d  <  0 )
5552, 53, 54mp3an12 1350 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( -u pi (,) 0 )  ->  d  <  0 )
56 pipos 23280 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  pi
5756a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( -u pi (,) 0 )  ->  0  <  pi )
5813, 51, 49, 55, 57lttrd 9795 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ( -u pi (,) 0 )  ->  d  <  pi )
5913, 49, 58ltled 9782 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( -u pi (,) 0 )  ->  d  <_  pi )
60 iccss 11702 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( -u pi  e.  RR  /\  pi  e.  RR )  /\  ( -u pi  <_ 
-u pi  /\  d  <_  pi ) )  -> 
( -u pi [,] d
)  C_  ( -u pi [,] pi ) )
6148, 49, 50, 59, 60syl22anc 1265 . . . . . . . . . . . . . . . . . 18  |-  ( d  e.  ( -u pi (,) 0 )  ->  ( -u pi [,] d ) 
C_  ( -u pi [,] pi ) )
6261adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( -u pi [,] d ) 
C_  ( -u pi [,] pi ) )
6347, 62fssresd 5767 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( U  |`  ( -u pi [,] d ) ) : ( -u pi [,] d ) --> CC )
64 fourierdlem103.o . . . . . . . . . . . . . . . . . 18  |-  O  =  ( U  |`  ( -u pi [,] d ) )
6564a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  O  =  ( U  |`  ( -u pi [,] d
) ) )
6665feq1d 5732 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( O : ( -u pi [,] d ) --> CC  <->  ( U  |`  ( -u pi [,] d ) ) : ( -u pi [,] d ) --> CC ) )
6763, 66mpbird 235 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  O : ( -u pi [,] d ) --> CC )
68 fourierdlem103.n . . . . . . . . . . . . . . . . . . 19  |-  N  =  ( ( # `  T
)  -  1 )
6911elexi 3097 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -u pi  e.  _V
7069prid1 4111 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  -u pi  e.  { -u pi , 
d }
71 elun1 3639 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -u pi  e.  { -u pi ,  d }  ->  -u pi  e.  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d
) ) ) )
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  -u pi  e.  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d ) ) )
73 fourierdlem103.t . . . . . . . . . . . . . . . . . . . . . . . 24  |-  T  =  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d ) ) )
7472, 73eleqtrri 2516 . . . . . . . . . . . . . . . . . . . . . . 23  |-  -u pi  e.  T
7574ne0ii 3774 . . . . . . . . . . . . . . . . . . . . . 22  |-  T  =/=  (/)
7675a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  =/=  (/) )
77 prfi 7852 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { -u pi ,  d }  e.  Fin
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  { -u pi , 
d }  e.  Fin )
79 fzfi 12182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 ... M )  e. 
Fin
80 fourierdlem103.q . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
8180rnmptfi 37056 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
8279, 81ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ran  Q  e.  Fin
8382a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ran  Q  e.  Fin )
84 infi 7801 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( -u pi (,) d ) )  e.  Fin )
8583, 84syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ran  Q  i^i  ( -u pi (,) d
) )  e.  Fin )
86 unfi 7844 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( { -u pi , 
d }  e.  Fin  /\  ( ran  Q  i^i  ( -u pi (,) d
) )  e.  Fin )  ->  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d
) ) )  e. 
Fin )
8778, 85, 86syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d ) ) )  e.  Fin )
8873, 87syl5eqel 2521 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  T  e.  Fin )
89 hashnncl 12544 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T  e.  Fin  ->  (
( # `  T )  e.  NN  <->  T  =/=  (/) ) )
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( # `  T
)  e.  NN  <->  T  =/=  (/) ) )
9176, 90mpbird 235 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( # `  T
)  e.  NN )
92 nnm1nn0 10911 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  T )  e.  NN  ->  ( ( # `
 T )  - 
1 )  e.  NN0 )
9391, 92syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( # `  T
)  -  1 )  e.  NN0 )
9468, 93syl5eqel 2521 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  NN0 )
9594adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  N  e.  NN0 )
96 0red 9643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  0  e.  RR )
97 1red 9657 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  1  e.  RR )
9895nn0red 10926 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  N  e.  RR )
99 0lt1 10135 . . . . . . . . . . . . . . . . . . . 20  |-  0  <  1
10099a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  0  <  1 )
101 2re 10679 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  RR
102101a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  2  e.  RR )
10391nnred 10624 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( # `  T
)  e.  RR )
104103adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( # `
 T )  e.  RR )
105 ioogtlb 37176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  0  e.  RR*  /\  d  e.  ( -u pi (,) 0 ) )  ->  -u pi  <  d )
10652, 53, 105mp3an12 1350 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  e.  ( -u pi (,) 0 )  ->  -u pi  <  d )
10748, 106ltned 9770 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( d  e.  ( -u pi (,) 0 )  ->  -u pi  =/=  d )
108107adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  =/=  d )
109 hashprg 12569 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
-u pi  e.  RR  /\  d  e.  RR )  ->  ( -u pi  =/=  d  <->  ( # `  { -u pi ,  d } )  =  2 ) )
11012, 14, 109syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( -u pi  =/=  d  <->  ( # `  { -u pi ,  d } )  =  2 ) )
111108, 110mpbid 213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( # `
 { -u pi ,  d } )  =  2 )
112111eqcomd 2437 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  2  =  ( # `  { -u pi ,  d } ) )
11388adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  T  e.  Fin )
114 ssun1 3635 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { -u pi ,  d }  C_  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d ) ) )
115114, 73sseqtr4i 3503 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { -u pi ,  d }  C_  T
116 hashssle 37123 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T  e.  Fin  /\  {
-u pi ,  d }  C_  T )  ->  ( # `  { -u pi ,  d } )  <_  ( # `  T
) )
117113, 115, 116sylancl 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( # `
 { -u pi ,  d } )  <_  ( # `  T
) )
118112, 117eqbrtrd 4446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  2  <_  ( # `  T
) )
119102, 104, 97, 118lesub1dd 10228 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  (
2  -  1 )  <_  ( ( # `  T )  -  1 ) )
120 1e2m1 10725 . . . . . . . . . . . . . . . . . . . 20  |-  1  =  ( 2  -  1 )
121119, 120, 683brtr4g 4458 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  1  <_  N )
12296, 97, 98, 100, 121ltletrd 9794 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  0  <  N )
123122gt0ne0d 10177 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  N  =/=  0 )
12495, 123jca 534 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( N  e.  NN0  /\  N  =/=  0 ) )
125 elnnne0 10883 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  <->  ( N  e.  NN0  /\  N  =/=  0 ) )
126124, 125sylibr 215 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  N  e.  NN )
127 fourierdlem103.j . . . . . . . . . . . . . . . . . 18  |-  J  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
12850adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  <_ 
-u pi )
12948, 13, 106ltled 9782 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( -u pi (,) 0 )  ->  -u pi  <_  d )
130129adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  <_  d )
13112, 14, 12, 128, 130eliccd 37185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  e.  ( -u pi [,] d ) )
13214leidd 10179 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  d  <_  d )
13312, 14, 14, 130, 132eliccd 37185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  d  e.  ( -u pi [,] d ) )
134131, 133jca 534 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( -u pi  e.  ( -u pi [,] d )  /\  d  e.  ( -u pi [,] d ) ) )
135 vex 3090 . . . . . . . . . . . . . . . . . . . . . 22  |-  d  e. 
_V
13669, 135prss 4157 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
-u pi  e.  (
-u pi [,] d
)  /\  d  e.  ( -u pi [,] d
) )  <->  { -u pi ,  d }  C_  ( -u pi [,] d
) )
137134, 136sylib 199 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  { -u pi ,  d }  C_  ( -u pi [,] d ) )
138 inss2 3689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran 
Q  i^i  ( -u pi (,) d ) )  C_  ( -u pi (,) d
)
139138a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( ran  Q  i^i  ( -u pi (,) d ) ) 
C_  ( -u pi (,) d ) )
140 ioossicc 11720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -u pi (,) d )  C_  ( -u pi [,] d
)
141139, 140syl6ss 3482 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( ran  Q  i^i  ( -u pi (,) d ) ) 
C_  ( -u pi [,] d ) )
142137, 141unssd 3648 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( { -u pi ,  d }  u.  ( ran 
Q  i^i  ( -u pi (,) d ) ) ) 
C_  ( -u pi [,] d ) )
14373, 142syl5eqss 3514 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  T  C_  ( -u pi [,] d ) )
14474a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  e.  T )
145135prid2 4112 . . . . . . . . . . . . . . . . . . . . 21  |-  d  e. 
{ -u pi ,  d }
146 elun1 3639 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  { -u pi ,  d }  ->  d  e.  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d
) ) ) )
147145, 146ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  d  e.  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d ) ) )
148147, 73eleqtrri 2516 . . . . . . . . . . . . . . . . . . 19  |-  d  e.  T
149148a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  d  e.  T )
150113, 68, 127, 12, 14, 143, 144, 149fourierdlem52 37589 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  (
( J : ( 0 ... N ) --> ( -u pi [,] d )  /\  ( J `  0 )  =  -u pi )  /\  ( J `  N )  =  d ) )
151150simpld 460 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( J : ( 0 ... N ) --> ( -u pi [,] d )  /\  ( J `  0 )  =  -u pi ) )
152151simpld 460 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  J : ( 0 ... N ) --> ( -u pi [,] d ) )
153151simprd 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( J `  0 )  =  -u pi )
154150simprd 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( J `  N )  =  d )
155 elfzoelz 11918 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 0..^ N )  ->  k  e.  ZZ )
156155zred 11040 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0..^ N )  ->  k  e.  RR )
157156adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
k  e.  RR )
158157ltp1d 10537 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
k  <  ( k  +  1 ) )
15948, 13jca 534 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  e.  ( -u pi (,) 0 )  ->  ( -u pi  e.  RR  /\  d  e.  RR )
)
16069, 135prss 4157 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
-u pi  e.  RR  /\  d  e.  RR )  <->  { -u pi ,  d }  C_  RR )
161159, 160sylib 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  e.  ( -u pi (,) 0 )  ->  { -u pi ,  d }  C_  RR )
162161adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  { -u pi ,  d }  C_  RR )
163 ioossre 11696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -u pi (,) d )  C_  RR
164138, 163sstri 3479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran 
Q  i^i  ( -u pi (,) d ) )  C_  RR
165164a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( ran  Q  i^i  ( -u pi (,) d ) ) 
C_  RR )
166162, 165unssd 3648 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( { -u pi ,  d }  u.  ( ran 
Q  i^i  ( -u pi (,) d ) ) ) 
C_  RR )
16773, 166syl5eqss 3514 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  T  C_  RR )
168113, 167, 127, 68fourierdlem36 37573 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  J  Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
169168adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  J  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
170 elfzofz 11933 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0..^ N )  ->  k  e.  ( 0 ... N
) )
171170adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
k  e.  ( 0 ... N ) )
172 fzofzp1 12005 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0..^ N )  ->  ( k  +  1 )  e.  ( 0 ... N
) )
173172adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( k  +  1 )  e.  ( 0 ... N ) )
174 isorel 6232 . . . . . . . . . . . . . . . . 17  |-  ( ( J  Isom  <  ,  <  ( ( 0 ... N
) ,  T )  /\  ( k  e.  ( 0 ... N
)  /\  ( k  +  1 )  e.  ( 0 ... N
) ) )  -> 
( k  <  (
k  +  1 )  <-> 
( J `  k
)  <  ( J `  ( k  +  1 ) ) ) )
175169, 171, 173, 174syl12anc 1262 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( k  <  (
k  +  1 )  <-> 
( J `  k
)  <  ( J `  ( k  +  1 ) ) ) )
176158, 175mpbid 213 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  k
)  <  ( J `  ( k  +  1 ) ) )
17743adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  U : ( -u pi [,] pi ) --> RR )
178177, 62feqresmpt 5935 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( U  |`  ( -u pi [,] d ) )  =  ( s  e.  (
-u pi [,] d
)  |->  ( U `  s ) ) )
17962sselda 3470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  ( -u pi [,] pi ) )
18015, 16, 28, 39, 40fourierdlem9 37546 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  H : ( -u pi [,] pi ) --> RR )
181180ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  H : ( -u pi [,] pi ) --> RR )
182181, 179ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( H `  s
)  e.  RR )
18341fourierdlem43 37580 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  K :
( -u pi [,] pi )
--> RR
184183a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  K : ( -u pi [,] pi ) --> RR )
185184, 179ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( K `  s
)  e.  RR )
186182, 185remulcld 9670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( H `  s )  x.  ( K `  s )
)  e.  RR )
18742fvmpt2 5973 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  e.  ( -u pi [,] pi )  /\  ( ( H `  s )  x.  ( K `  s )
)  e.  RR )  ->  ( U `  s )  =  ( ( H `  s
)  x.  ( K `
 s ) ) )
188179, 186, 187syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( U `  s
)  =  ( ( H `  s )  x.  ( K `  s ) ) )
18911a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  -u pi  e.  RR )
19013adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
d  e.  RR )
191 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  ( -u pi [,] d ) )
192 eliccre 37187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
-u pi  e.  RR  /\  d  e.  RR  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  RR )
193189, 190, 191, 192syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  RR )
194 0red 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
0  e.  RR )
19552a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  -u pi  e.  RR* )
196190rexrd 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
d  e.  RR* )
197 iccleub 11690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
-u pi  e.  RR*  /\  d  e.  RR*  /\  s  e.  ( -u pi [,] d ) )  -> 
s  <_  d )
198195, 196, 191, 197syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  <_  d )
19955adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
d  <  0 )
200193, 190, 194, 198, 199lelttrd 9792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  <  0 )
201193, 200ltned 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  =/=  0 )
202201adantll 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  =/=  0 )
203202neneqd 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  -.  s  =  0
)
204203iffalsed 3926 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
205193, 194, 200ltnsymd 9783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  -.  0  <  s )
206205adantll 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  -.  0  <  s )
207206iffalsed 3926 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( 0  <  s ,  Y ,  W )  =  W )
208207oveq2d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  W ) )
209208oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  =  ( ( ( F `  ( X  +  s ) )  -  W )  / 
s ) )
210204, 209eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  W )  /  s ) )
21115ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  F : RR --> RR )
21216ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  X  e.  RR )
213 iccssre 11716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
21411, 10, 213mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -u pi [,] pi )  C_  RR
215214, 179sseldi 3468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  RR )
216212, 215readdcld 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( X  +  s )  e.  RR )
217211, 216ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( F `  ( X  +  s )
)  e.  RR )
21839ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  W  e.  RR )
219217, 218resubcld 10046 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( F `  ( X  +  s
) )  -  W
)  e.  RR )
220219, 215, 202redivcld 10434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( ( F `
 ( X  +  s ) )  -  W )  /  s
)  e.  RR )
221210, 220eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  e.  RR )
22240fvmpt2 5973 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ( -u pi [,] pi )  /\  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  e.  RR )  ->  ( H `  s )  =  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )
223179, 221, 222syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( H `  s
)  =  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )
224223, 204, 2093eqtrd 2474 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( H `  s
)  =  ( ( ( F `  ( X  +  s )
)  -  W )  /  s ) )
22510a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  pi  e.  RR )
226225renegcld 10045 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  -u pi  e.  RR )
227 iccgelb 11691 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
-u pi  e.  RR*  /\  d  e.  RR*  /\  s  e.  ( -u pi [,] d ) )  ->  -u pi  <_  s )
228195, 196, 191, 227syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  -u pi  <_  s )
22958adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
d  <  pi )
230193, 190, 225, 198, 229lelttrd 9792 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  <  pi )
231193, 225, 230ltled 9782 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  <_  pi )
232226, 225, 193, 228, 231eliccd 37185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  ( -u pi [,] pi ) )
233201neneqd 2632 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  -.  s  =  0
)
234233iffalsed 3926 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
235101a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
2  e.  RR )
236193rehalfcld 10859 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( s  /  2
)  e.  RR )
237236resincld 14175 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( sin `  (
s  /  2 ) )  e.  RR )
238235, 237remulcld 9670 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  RR )
239 2cn 10680 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  e.  CC
240239a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
2  e.  CC )
241193recnd 9668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  CC )
242241halfcld 10857 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( s  /  2
)  e.  CC )
243242sincld 14162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( sin `  (
s  /  2 ) )  e.  CC )
244 2ne0 10702 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  =/=  0
245244a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
2  =/=  0 )
246 fourierdlem44 37581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
247232, 201, 246syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
248240, 243, 245, 247mulne0d 10263 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  =/=  0 )
249193, 238, 248redivcld 10434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) )  e.  RR )
250234, 249eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  e.  RR )
25141fvmpt2 5973 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ( -u pi [,] pi )  /\  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  e.  RR )  -> 
( K `  s
)  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
252232, 250, 251syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( d  e.  ( -u pi (,) 0 )  /\  s  e.  ( -u pi [,] d ) )  -> 
( K `  s
)  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
253252adantll 718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( K `  s
)  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
254224, 253oveq12d 6323 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( H `  s )  x.  ( K `  s )
)  =  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
255203iffalsed 3926 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
256255oveq2d 6321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( ( ( F `  ( X  +  s ) )  -  W )  / 
s )  x.  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  =  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
257188, 254, 2563eqtrd 2474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( U `  s
)  =  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
258257mpteq2dva 4512 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  (
s  e.  ( -u pi [,] d )  |->  ( U `  s ) )  =  ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
25965, 178, 2583eqtrd 2474 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  O  =  ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
260259adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  O  =  ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
261260reseq1d 5124 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( O  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  =  ( ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  W )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) )
26215adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  F : RR --> RR )
26316adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  X  e.  RR )
264 fourierdlem103.p . . . . . . . . . . . . . . . . . 18  |-  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 ) ) ) } )
265 fourierdlem103.m . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  NN )
266265adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  M  e.  NN )
267 fourierdlem103.v . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  V  e.  ( P `
 M ) )
268267adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  V  e.  ( P `  M
) )
269 fourierdlem103.fcn . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
270269adantlr 719 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  i  e.  ( 0..^ M ) )  -> 
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) )
-cn-> CC ) )
271 fourierdlem103.r . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
272271adantlr 719 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )
273 fourierdlem103.l . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
274273adantlr 719 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )
275106adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  <  d )
27652a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -u pi  e.  RR* )
27753a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  0  e.  RR* )
27855adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  d  <  0 )
279276, 14, 277, 278gtnelicc 37181 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  -.  0  e.  ( -u pi [,] d ) )
28039adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  W  e.  RR )
281 eqid 2429 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  =  ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )
282 eqid 2429 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( if ( ( J `  ( k  +  1 ) )  =  ( Q `  ( ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  +  1 ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ L ,  ( F `  ( X  +  ( J `  ( k  +  1 ) ) ) ) )  -  W )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  =  ( ( ( if ( ( J `  ( k  +  1 ) )  =  ( Q `  ( ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  +  1 ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ L ,  ( F `  ( X  +  ( J `  ( k  +  1 ) ) ) ) )  -  W )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )
283 eqid 2429 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( if ( ( J `  k )  =  ( Q `  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) ) ) ,  [_ ( iota_ l  e.  ( 0..^ M ) ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
( Q `  l
) (,) ( Q `
 ( l  +  1 ) ) ) )  /  i ]_ R ,  ( F `  ( X  +  ( J `  k ) ) ) )  -  W )  /  ( J `  k )
)  x.  ( ( J `  k )  /  ( 2  x.  ( sin `  (
( J `  k
)  /  2 ) ) ) ) )  =  ( ( ( if ( ( J `
 k )  =  ( Q `  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  ( l  +  1 ) ) ) ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ R ,  ( F `  ( X  +  ( J `  k ) ) ) )  -  W )  /  ( J `  k ) )  x.  ( ( J `  k )  /  (
2  x.  ( sin `  ( ( J `  k )  /  2
) ) ) ) )
284 fveq2 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  ( Q `  l )  =  ( Q `  i ) )
285 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  i  ->  (
l  +  1 )  =  ( i  +  1 ) )
286285fveq2d 5885 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  ( Q `  ( l  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
287284, 286oveq12d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  (
( Q `  l
) (,) ( Q `
 ( l  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
288287sseq2d 3498 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) )  <->  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
289288cbvriotav 6278 . . . . . . . . . . . . . . . . . 18  |-  ( iota_ l  e.  ( 0..^ M ) ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
( Q `  l
) (,) ( Q `
 ( l  +  1 ) ) ) )  =  ( iota_ i  e.  ( 0..^ M ) ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )
290262, 263, 264, 266, 268, 270, 272, 274, 12, 14, 275, 62, 279, 280, 281, 80, 73, 68, 127, 282, 283, 289fourierdlem86 37623 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( ( ( if ( ( J `  ( k  +  1 ) )  =  ( Q `  ( ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  +  1 ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ L ,  ( F `  ( X  +  ( J `  ( k  +  1 ) ) ) ) )  -  W )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  e.  ( ( ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) lim CC  ( J `
 ( k  +  1 ) ) )  /\  ( ( ( if ( ( J `
 k )  =  ( Q `  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  ( l  +  1 ) ) ) ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ R ,  ( F `  ( X  +  ( J `  k ) ) ) )  -  W )  /  ( J `  k ) )  x.  ( ( J `  k )  /  (
2  x.  ( sin `  ( ( J `  k )  /  2
) ) ) ) )  e.  ( ( ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) lim CC  ( J `
 k ) ) )  /\  ( ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  W )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  e.  ( ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) ) -cn-> CC ) ) )
291290simprd 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  e.  ( ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) -cn-> CC ) )
292261, 291eqeltrd 2517 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( O  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  e.  ( ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) )
-cn-> CC ) )
293290simpld 460 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( ( if ( ( J `
 ( k  +  1 ) )  =  ( Q `  (
( iota_ l  e.  ( 0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) )  +  1 ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ L ,  ( F `  ( X  +  ( J `  ( k  +  1 ) ) ) ) )  -  W )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  e.  ( ( ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) lim CC  ( J `
 ( k  +  1 ) ) )  /\  ( ( ( if ( ( J `
 k )  =  ( Q `  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  ( l  +  1 ) ) ) ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ R ,  ( F `  ( X  +  ( J `  k ) ) ) )  -  W )  /  ( J `  k ) )  x.  ( ( J `  k )  /  (
2  x.  ( sin `  ( ( J `  k )  /  2
) ) ) ) )  e.  ( ( ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) lim CC  ( J `
 k ) ) ) )
294293simpld 460 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( if ( ( J `  ( k  +  1 ) )  =  ( Q `  ( (
iota_ l  e.  (
0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) )  +  1 ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ L ,  ( F `  ( X  +  ( J `  ( k  +  1 ) ) ) ) )  -  W )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  e.  ( ( ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) lim CC  ( J `
 ( k  +  1 ) ) ) )
295260eqcomd 2437 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  =  O )
296295reseq1d 5124 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  =  ( O  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) )
297296oveq1d 6320 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) ) lim CC  ( J `  ( k  +  1 ) ) )  =  ( ( O  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  ( k  +  1 ) ) ) )
298294, 297eleqtrd 2519 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( if ( ( J `  ( k  +  1 ) )  =  ( Q `  ( (
iota_ l  e.  (
0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) )  +  1 ) ) , 
[_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( ( Q `  l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ L ,  ( F `  ( X  +  ( J `  ( k  +  1 ) ) ) ) )  -  W )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  e.  ( ( O  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  ( k  +  1 ) ) ) )
299293simprd 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( if ( ( J `  k )  =  ( Q `  ( iota_ l  e.  ( 0..^ M ) ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
( Q `  l
) (,) ( Q `
 ( l  +  1 ) ) ) ) ) ,  [_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ R ,  ( F `  ( X  +  ( J `  k ) ) ) )  -  W )  /  ( J `  k ) )  x.  ( ( J `  k )  /  (
2  x.  ( sin `  ( ( J `  k )  /  2
) ) ) ) )  e.  ( ( ( s  e.  (
-u pi [,] d
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  W )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) lim CC  ( J `
 k ) ) )
300296oveq1d 6320 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( s  e.  ( -u pi [,] d )  |->  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) ) lim CC  ( J `  k )
)  =  ( ( O  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  k ) ) )
301299, 300eleqtrd 2519 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( ( if ( ( J `  k )  =  ( Q `  ( iota_ l  e.  ( 0..^ M ) ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
( Q `  l
) (,) ( Q `
 ( l  +  1 ) ) ) ) ) ,  [_ ( iota_ l  e.  ( 0..^ M ) ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( ( Q `
 l ) (,) ( Q `  (
l  +  1 ) ) ) )  / 
i ]_ R ,  ( F `  ( X  +  ( J `  k ) ) ) )  -  W )  /  ( J `  k ) )  x.  ( ( J `  k )  /  (
2  x.  ( sin `  ( ( J `  k )  /  2
) ) ) ) )  e.  ( ( O  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  k ) ) )
302 eqid 2429 . . . . . . . . . . . . . . 15  |-  ( RR 
_D  O )  =  ( RR  _D  O
)
30367adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  O : ( -u pi [,] d ) --> CC )
30411a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  ->  -u pi  e.  RR )
30514ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
d  e.  RR )
306 elioore 11666 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  ->  s  e.  RR )
307306adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
s  e.  RR )
30862, 214syl6ss 3482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( -u pi (,) 0
) )  ->  ( -u pi [,] d ) 
C_  RR )
309308adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( -u pi [,] d
)  C_  RR )
310152adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  J : ( 0 ... N ) --> ( -u pi [,] d ) )
311310, 171ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  k
)  e.  ( -u pi [,] d ) )
312309, 311sseldd 3471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  k
)  e.  RR )
313312adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( J `  k
)  e.  RR )
31452a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  -u pi  e.  RR* )
31514adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
d  e.  RR )
316315rexrd 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
d  e.  RR* )
317 iccgelb 11691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  d  e.  RR*  /\  ( J `  k )  e.  ( -u pi [,] d ) )  ->  -u pi  <_  ( J `  k ) )
318314, 316, 311, 317syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  -u pi  <_  ( J `  k ) )
319318adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  ->  -u pi  <_  ( J `  k ) )
320313rexrd 9689 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( J `  k
)  e.  RR* )
321310, 173ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  (
k  +  1 ) )  e.  ( -u pi [,] d ) )
322309, 321sseldd 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  (
k  +  1 ) )  e.  RR )
323322rexrd 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  (
k  +  1 ) )  e.  RR* )
324323adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( J `  (
k  +  1 ) )  e.  RR* )
325 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )
326 ioogtlb 37176 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( J `  k
)  e.  RR*  /\  ( J `  ( k  +  1 ) )  e.  RR*  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  ( J `  k )  <  s )
327320, 324, 325, 326syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( J `  k
)  <  s )
328304, 313, 307, 319, 327lelttrd 9792 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  ->  -u pi  <  s )
329304, 307, 328ltled 9782 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  ->  -u pi  <_  s )
330322adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( J `  (
k  +  1 ) )  e.  RR )
331 iooltub 37194 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( J `  k
)  e.  RR*  /\  ( J `  ( k  +  1 ) )  e.  RR*  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  s  <  ( J `  (
k  +  1 ) ) )
332320, 324, 325, 331syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
s  <  ( J `  ( k  +  1 ) ) )
333 iccleub 11690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
-u pi  e.  RR*  /\  d  e.  RR*  /\  ( J `  ( k  +  1 ) )  e.  ( -u pi [,] d ) )  -> 
( J `  (
k  +  1 ) )  <_  d )
334314, 316, 321, 333syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( J `  (
k  +  1 ) )  <_  d )
335334adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( J `  (
k  +  1 ) )  <_  d )
336307, 330, 305, 332, 335ltletrd 9794 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
s  <  d )
337307, 305, 336ltled 9782 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
s  <_  d )
338304, 305, 307, 329, 337eliccd 37185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
s  e.  ( -u pi [,] d ) )
339338ralrimiva 2846 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  ->  A. s  e.  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) s  e.  ( -u pi [,] d ) )
340 dfss3 3460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( -u pi [,] d )  <->  A. s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) s  e.  (
-u pi [,] d
) )
341339, 340sylibr 215 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  C_  ( -u pi [,] d ) )
342303, 341feqresmpt 5935 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  -> 
( O  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  =  ( s  e.  ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  |->  ( O `
 s ) ) )
343 simplll 766 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  ->  ph )
344 simpllr 767 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
d  e.  ( -u pi (,) 0 ) )
34564fveq1i 5882 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( O `
 s )  =  ( ( U  |`  ( -u pi [,] d
) ) `  s
)
346345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( O `  s
)  =  ( ( U  |`  ( -u pi [,] d ) ) `  s ) )
347 fvres 5895 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( -u pi [,] d )  ->  (
( U  |`  ( -u pi [,] d ) ) `  s )  =  ( U `  s ) )
348347adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( U  |`  ( -u pi [,] d
) ) `  s
)  =  ( U `
 s ) )
349253, 255eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( K `  s
)  =  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )
350224, 349oveq12d 6323 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( H `  s )  x.  ( K `  s )
)  =  ( ( ( ( F `  ( X  +  s
) )  -  W
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
351219recnd 9668 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( F `  ( X  +  s
) )  -  W
)  e.  CC )
352241adantll 718 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
s  e.  CC )
353239a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
2  e.  CC )
354352halfcld 10857 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( s  /  2
)  e.  CC )
355354sincld 14162 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( sin `  (
s  /  2 ) )  e.  CC )
356353, 355mulcld 9662 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  CC )
357248adantll 718 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  =/=  0 )
358351, 352, 356, 202, 357dmdcan2d 10412 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( ( ( ( F `  ( X  +  s ) )  -  W )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( ( ( F `  ( X  +  s ) )  -  W )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
359188, 350, 3583eqtrd 2474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( U `  s
)  =  ( ( ( F `  ( X  +  s )
)  -  W )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )
360346, 348, 3593eqtrd 2474 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  s  e.  ( -u pi [,] d ) )  -> 
( O `  s
)  =  ( ( ( F `  ( X  +  s )
)  -  W )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )
361343, 344, 338, 360syl21anc 1263 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  -> 
( O `  s
)  =  ( ( ( F `  ( X  +  s )
)  -  W )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )
362343, 344, 338, 358syl21anc 1263 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( -u pi (,) 0 ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )