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

Theorem fourierdlem104 37342
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 2402 . . 3  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
2 1zzd 10935 . . 3  |-  ( ph  ->  1  e.  ZZ )
3 nfv 1728 . . . . 5  |-  F/ n ph
4 nfmpt1 4483 . . . . 5  |-  F/_ n
( n  e.  NN  |->  S. ( 0 (,) pi ) ( G `  s )  _d s )
5 nfmpt1 4483 . . . . 5  |-  F/_ n
( n  e.  NN  |->  pi )
6 fourierdlem104.e . . . . . 6  |-  E  =  ( n  e.  NN  |->  ( S. ( 0 (,) pi ) ( G `
 s )  _d s  /  pi ) )
7 nfmpt1 4483 . . . . . 6  |-  F/_ n
( n  e.  NN  |->  ( S. ( 0 (,) pi ) ( G `
 s )  _d s  /  pi ) )
86, 7nfcxfr 2562 . . . . 5  |-  F/_ n E
9 nnuz 11161 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
10 elioore 11611 . . . . . . . . . . . . . . . 16  |-  ( d  e.  ( 0 (,) pi )  ->  d  e.  RR )
1110adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  e.  RR )
12 pire 23141 . . . . . . . . . . . . . . . 16  |-  pi  e.  RR
1312a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  e.  RR )
14 fourierdlem104.f . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F : RR --> RR )
15 fourierdlem104.xre . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  X  e.  RR )
16 ioossre 11638 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( X (,) +oo )  C_  RR
1716a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( X (,) +oo )  C_  RR )
1814, 17fssresd 5734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( F  |`  ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
19 ioosscn 36876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X (,) +oo )  C_  CC
2019a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( X (,) +oo )  C_  CC )
21 eqid 2402 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
22 pnfxr 11373 . . . . . . . . . . . . . . . . . . . . . . 23  |- +oo  e.  RR*
2322a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> +oo  e.  RR* )
2415ltpnfd 36832 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  < +oo )
2521, 23, 15, 24lptioo1cn 37001 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( X (,) +oo ) ) )
26 fourierdlem104.y . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
2718, 20, 25, 26limcrecl 36984 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Y  e.  RR )
28 ioossre 11638 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -oo (,) X )  C_  RR
2928a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( -oo (,) X
)  C_  RR )
3014, 29fssresd 5734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( F  |`  ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
31 ioosscn 36876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -oo (,) X )  C_  CC
3231a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( -oo (,) X
)  C_  CC )
33 mnfxr 11375 . . . . . . . . . . . . . . . . . . . . . . 23  |- -oo  e.  RR*
3433a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> -oo  e.  RR* )
3515mnfltd 36841 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> -oo  <  X )
3621, 34, 15, 35lptioo2cn 37000 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( -oo (,) X ) ) )
37 fourierdlem104.w . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
3830, 32, 36, 37limcrecl 36984 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  W  e.  RR )
39 fourierdlem104.h . . . . . . . . . . . . . . . . . . . 20  |-  H  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  / 
s ) ) )
40 fourierdlem104.k . . . . . . . . . . . . . . . . . . . 20  |-  K  =  ( s  e.  (
-u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
41 fourierdlem104.u . . . . . . . . . . . . . . . . . . . 20  |-  U  =  ( s  e.  (
-u pi [,] pi )  |->  ( ( H `
 s )  x.  ( K `  s
) ) )
4214, 15, 27, 38, 39, 40, 41fourierdlem55 37293 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  U : ( -u pi [,] pi ) --> RR )
43 ax-resscn 9578 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  CC
4443a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  RR  C_  CC )
4542, 44fssd 5722 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U : ( -u pi [,] pi ) --> CC )
4645adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  U : ( -u pi [,] pi ) --> CC )
4712renegcli 9915 . . . . . . . . . . . . . . . . . . 19  |-  -u pi  e.  RR
4847a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  -u pi  e.  RR )
4947a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  e.  RR )
50 0red 9626 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( 0 (,) pi )  ->  0  e.  RR )
51 negpilt0 36816 . . . . . . . . . . . . . . . . . . . . . 22  |-  -u pi  <  0
5251a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  <  0 )
53 0xr 9669 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR*
5412rexri 9675 . . . . . . . . . . . . . . . . . . . . . 22  |-  pi  e.  RR*
55 ioogtlb 36877 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  d  e.  ( 0 (,) pi ) )  ->  0  <  d )
5653, 54, 55mp3an12 1316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( 0 (,) pi )  ->  0  <  d )
5749, 50, 10, 52, 56lttrd 9776 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  <  d )
5849, 10, 57ltled 9764 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( 0 (,) pi )  ->  -u pi  <_  d )
5958adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  -u pi  <_  d )
6013leidd 10158 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  <_  pi )
61 iccss 11644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -u pi  e.  RR  /\  pi  e.  RR )  /\  ( -u pi  <_  d  /\  pi  <_  pi ) )  ->  (
d [,] pi ) 
C_  ( -u pi [,] pi ) )
6248, 13, 59, 60, 61syl22anc 1231 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d [,] pi ) 
C_  ( -u pi [,] pi ) )
6346, 62fssresd 5734 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( U  |`  ( d [,] pi ) ) : ( d [,] pi )
--> CC )
64 fourierdlem104.o . . . . . . . . . . . . . . . . . 18  |-  O  =  ( U  |`  (
d [,] pi ) )
6564a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  O  =  ( U  |`  ( d [,] pi ) ) )
6665feq1d 5699 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( O : ( d [,] pi ) --> CC  <->  ( U  |`  ( d [,] pi ) ) : ( d [,] pi ) --> CC ) )
6763, 66mpbird 232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  O : ( d [,] pi ) --> CC )
68 fourierdlem104.n . . . . . . . . . . . . . . . . . 18  |-  N  =  ( ( # `  T
)  -  1 )
6912elexi 3068 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  pi  e.  _V
7069prid2 4080 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  pi  e.  { d ,  pi }
71 elun1 3609 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( pi  e.  { d ,  pi }  ->  pi  e.  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) ) )
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  pi  e.  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
73 fourierdlem104.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  =  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
7472, 73eleqtrri 2489 . . . . . . . . . . . . . . . . . . . . . 22  |-  pi  e.  T
7574ne0ii 3744 . . . . . . . . . . . . . . . . . . . . 21  |-  T  =/=  (/)
7675a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  =/=  (/) )
77 prfi 7828 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { d ,  pi }  e.  Fin
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  { d ,  pi }  e.  Fin )
79 fzfi 12121 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 ... M )  e. 
Fin
80 fourierdlem104.q . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
8180rnmptfi 36802 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
8279, 81ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ran  Q  e.  Fin
83 infi 7777 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  (
d (,) pi ) )  e.  Fin )
8482, 83mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ran  Q  i^i  ( d (,) pi ) )  e.  Fin )
85 unfi 7820 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( { d ,  pi }  e.  Fin  /\  ( ran  Q  i^i  ( d (,) pi ) )  e.  Fin )  -> 
( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )  e.  Fin )
8678, 84, 85syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )  e.  Fin )
8773, 86syl5eqel 2494 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  e.  Fin )
88 hashnncl 12482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T  e.  Fin  ->  (
( # `  T )  e.  NN  <->  T  =/=  (/) ) )
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( # `  T
)  e.  NN  <->  T  =/=  (/) ) )
9076, 89mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( # `  T
)  e.  NN )
91 nnm1nn0 10877 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  T )  e.  NN  ->  ( ( # `
 T )  - 
1 )  e.  NN0 )
9290, 91syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( # `  T
)  -  1 )  e.  NN0 )
9368, 92syl5eqel 2494 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  NN0 )
9493adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  e.  NN0 )
95 0red 9626 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  0  e.  RR )
96 1red 9640 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  1  e.  RR )
9794nn0red 10893 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  e.  RR )
98 0lt1 10114 . . . . . . . . . . . . . . . . . . 19  |-  0  <  1
9998a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  0  <  1 )
100 2re 10645 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
101100a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  2  e.  RR )
10290nnred 10590 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( # `  T
)  e.  RR )
103102adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( # `
 T )  e.  RR )
104 iooltub 36897 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 0  e.  RR*  /\  pi  e.  RR*  /\  d  e.  ( 0 (,) pi ) )  ->  d  <  pi )
10553, 54, 104mp3an12 1316 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( d  e.  ( 0 (,) pi )  ->  d  <  pi )
10610, 105ltned 9752 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( 0 (,) pi )  ->  d  =/=  pi )
107106adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  =/=  pi )
108 hashprg 12507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  RR  /\  pi  e.  RR )  -> 
( d  =/=  pi  <->  (
# `  { d ,  pi } )  =  2 ) )
10911, 12, 108sylancl 660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d  =/=  pi  <->  ( # `  {
d ,  pi }
)  =  2 ) )
110107, 109mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( # `
 { d ,  pi } )  =  2 )
111110eqcomd 2410 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  2  =  ( # `  {
d ,  pi }
) )
11287adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  T  e.  Fin )
113 ssun1 3605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { d ,  pi }  C_  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
114113, 73sseqtr4i 3474 . . . . . . . . . . . . . . . . . . . . . 22  |-  { d ,  pi }  C_  T
115 hashssle 36846 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T  e.  Fin  /\  { d ,  pi }  C_  T )  ->  ( # `
 { d ,  pi } )  <_ 
( # `  T ) )
116112, 114, 115sylancl 660 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( # `
 { d ,  pi } )  <_ 
( # `  T ) )
117111, 116eqbrtrd 4414 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  2  <_  ( # `  T
) )
118101, 103, 96, 117lesub1dd 10207 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
2  -  1 )  <_  ( ( # `  T )  -  1 ) )
119 1e2m1 10691 . . . . . . . . . . . . . . . . . . 19  |-  1  =  ( 2  -  1 )
120118, 119, 683brtr4g 4426 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  1  <_  N )
12195, 96, 97, 99, 120ltletrd 9775 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  0  <  N )
122121gt0ne0d 10156 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  =/=  0 )
123 elnnne0 10849 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  <->  ( N  e.  NN0  /\  N  =/=  0 ) )
12494, 122, 123sylanbrc 662 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  N  e.  NN )
125 fourierdlem104.j . . . . . . . . . . . . . . . . 17  |-  J  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
12611leidd 10158 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  <_  d )
12712a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( 0 (,) pi )  ->  pi  e.  RR )
12810, 127, 105ltled 9764 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  e.  ( 0 (,) pi )  ->  d  <_  pi )
129128adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  <_  pi )
13011, 13, 11, 126, 129eliccd 36887 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  e.  ( d [,] pi ) )
13111, 13, 13, 129, 60eliccd 36887 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  e.  ( d [,] pi ) )
132130, 131jca 530 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d  e.  ( d [,] pi )  /\  pi  e.  ( d [,] pi ) ) )
133 vex 3061 . . . . . . . . . . . . . . . . . . . . 21  |-  d  e. 
_V
134133, 69prss 4125 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( d  e.  ( d [,] pi )  /\  pi  e.  ( d [,] pi ) )  <->  { d ,  pi }  C_  (
d [,] pi ) )
135132, 134sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  { d ,  pi }  C_  ( d [,] pi ) )
136 inss2 3659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  i^i  ( d (,) pi ) )  C_  ( d (,) pi )
137136a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( ran  Q  i^i  ( d (,) pi ) ) 
C_  ( d (,) pi ) )
138 ioossicc 11662 . . . . . . . . . . . . . . . . . . . 20  |-  ( d (,) pi )  C_  ( d [,] pi )
139137, 138syl6ss 3453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( ran  Q  i^i  ( d (,) pi ) ) 
C_  ( d [,] pi ) )
140135, 139unssd 3618 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) ) 
C_  ( d [,] pi ) )
14173, 140syl5eqss 3485 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  T  C_  ( d [,] pi ) )
142133prid1 4079 . . . . . . . . . . . . . . . . . . . 20  |-  d  e. 
{ d ,  pi }
143 elun1 3609 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  { d ,  pi }  ->  d  e.  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) ) )
144142, 143ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  d  e.  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )
145144, 73eleqtrri 2489 . . . . . . . . . . . . . . . . . 18  |-  d  e.  T
146145a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  e.  T )
14774a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  pi  e.  T )
148112, 68, 125, 11, 13, 141, 146, 147fourierdlem52 37290 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
( J : ( 0 ... N ) --> ( d [,] pi )  /\  ( J ` 
0 )  =  d )  /\  ( J `
 N )  =  pi ) )
149148simplld 753 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  J : ( 0 ... N ) --> ( d [,] pi ) )
150148simplrd 755 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( J `  0 )  =  d )
151148simprd 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( J `  N )  =  pi )
152 elfzoelz 11857 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 0..^ N )  ->  k  e.  ZZ )
153152zred 11007 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0..^ N )  ->  k  e.  RR )
154153adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  k  e.  RR )
155154ltp1d 10515 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  k  <  ( k  +  1 ) )
15610, 127jca 530 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  e.  ( 0 (,) pi )  ->  (
d  e.  RR  /\  pi  e.  RR ) )
157133, 69prss 4125 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( d  e.  RR  /\  pi  e.  RR )  <->  { d ,  pi }  C_  RR )
158156, 157sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  e.  ( 0 (,) pi )  ->  { d ,  pi }  C_  RR )
159158adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  { d ,  pi }  C_  RR )
160 ioossre 11638 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d (,) pi )  C_  RR
161136, 160sstri 3450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran 
Q  i^i  ( d (,) pi ) )  C_  RR
162161a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( ran  Q  i^i  ( d (,) pi ) ) 
C_  RR )
163159, 162unssd 3618 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) ) 
C_  RR )
16473, 163syl5eqss 3485 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  T  C_  RR )
165112, 164, 125, 68fourierdlem36 37274 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  J  Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
166165adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  J  Isom  <  ,  <  ( ( 0 ... N ) ,  T ) )
167 elfzofz 11872 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0..^ N )  ->  k  e.  ( 0 ... N
) )
168167adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  k  e.  ( 0 ... N
) )
169 fzofzp1 11944 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0..^ N )  ->  ( k  +  1 )  e.  ( 0 ... N
) )
170169adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( k  +  1 )  e.  ( 0 ... N
) )
171 isorel 6204 . . . . . . . . . . . . . . . . 17  |-  ( ( J  Isom  <  ,  <  ( ( 0 ... N
) ,  T )  /\  ( k  e.  ( 0 ... N
)  /\  ( k  +  1 )  e.  ( 0 ... N
) ) )  -> 
( k  <  (
k  +  1 )  <-> 
( J `  k
)  <  ( J `  ( k  +  1 ) ) ) )
172166, 168, 170, 171syl12anc 1228 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( k  <  ( k  +  1 )  <->  ( J `  k )  <  ( J `  ( k  +  1 ) ) ) )
173155, 172mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  k )  <  ( J `  ( k  +  1 ) ) )
17442adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  U : ( -u pi [,] pi ) --> RR )
175174, 62feqresmpt 5902 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  ( U  |`  ( d [,] pi ) )  =  ( s  e.  ( d [,] pi ) 
|->  ( U `  s
) ) )
17662sselda 3441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  s  e.  ( -u pi [,] pi ) )
17714, 15, 27, 38, 39fourierdlem9 37247 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  H : ( -u pi [,] pi ) --> RR )
178177ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  H : ( -u pi [,] pi ) --> RR )
179178, 176ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( H `  s )  e.  RR )
18040fourierdlem43 37281 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  K :
( -u pi [,] pi )
--> RR
181180a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  K : ( -u pi [,] pi ) --> RR )
182181, 176ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( K `  s )  e.  RR )
183179, 182remulcld 9653 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( H `  s
)  x.  ( K `
 s ) )  e.  RR )
18441fvmpt2 5940 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  e.  ( -u pi [,] pi )  /\  ( ( H `  s )  x.  ( K `  s )
)  e.  RR )  ->  ( U `  s )  =  ( ( H `  s
)  x.  ( K `
 s ) ) )
185176, 183, 184syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( U `  s )  =  ( ( H `
 s )  x.  ( K `  s
) ) )
186 0red 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
0  e.  RR )
18710adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
d  e.  RR )
18812a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  pi  e.  RR )
189 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
s  e.  ( d [,] pi ) )
190 eliccre 36889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  RR  /\  pi  e.  RR  /\  s  e.  ( d [,] pi ) )  ->  s  e.  RR )
191187, 188, 189, 190syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
s  e.  RR )
19256adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
0  <  d )
193187rexrd 9672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
d  e.  RR* )
19454a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  pi  e.  RR* )
195 iccgelb 11633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( d  e.  RR*  /\  pi  e.  RR*  /\  s  e.  ( d [,] pi ) )  ->  d  <_  s )
196193, 194, 189, 195syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
d  <_  s )
197186, 187, 191, 192, 196ltletrd 9775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
0  <  s )
198197gt0ne0d 10156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
s  =/=  0 )
199198adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  s  =/=  0 )
200199neneqd 2605 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  -.  s  =  0 )
201200iffalsed 3895 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )
202197adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  0  <  s )
203202iftrued 3892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  if ( 0  <  s ,  Y ,  W )  =  Y )
204203oveq2d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( F `  ( X  +  s )
)  -  if ( 0  <  s ,  Y ,  W ) )  =  ( ( F `  ( X  +  s ) )  -  Y ) )
205204oveq1d 6292 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s ) )
206201, 205eqtrd 2443 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  =  ( ( ( F `  ( X  +  s )
)  -  Y )  /  s ) )
20714ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  F : RR --> RR )
20815ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  X  e.  RR )
209 iccssre 11658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR )  ->  ( -u pi [,] pi )  C_  RR )
21047, 12, 209mp2an 670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -u pi [,] pi )  C_  RR
211210, 176sseldi 3439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  s  e.  RR )
212208, 211readdcld 9652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( X  +  s )  e.  RR )
213207, 212ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
21427ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  Y  e.  RR )
215213, 214resubcld 10027 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( F `  ( X  +  s )
)  -  Y )  e.  RR )
216215, 211, 199redivcld 10412 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( ( F `  ( X  +  s
) )  -  Y
)  /  s )  e.  RR )
217206, 216eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) )  e.  RR )
21839fvmpt2 5940 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
219176, 217, 218syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( H `  s )  =  if ( s  =  0 ,  0 ,  ( ( ( F `
 ( X  +  s ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )
220219, 201, 2053eqtrd 2447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( H `  s )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s ) )
221188renegcld 10026 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  -u pi  e.  RR )
22251a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  -u pi  <  0 )
223221, 186, 191, 222, 197lttrd 9776 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  -u pi  <  s )
224221, 191, 223ltled 9764 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  -u pi  <_  s )
225 iccleub 11632 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  RR*  /\  pi  e.  RR*  /\  s  e.  ( d [,] pi ) )  ->  s  <_  pi )
226193, 194, 189, 225syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
s  <_  pi )
227221, 188, 191, 224, 226eliccd 36887 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
s  e.  ( -u pi [,] pi ) )
228198neneqd 2605 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  -.  s  =  0
)
229228iffalsed 3895 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
230100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
2  e.  RR )
231191rehalfcld 10825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( s  /  2
)  e.  RR )
232231resincld 14085 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( sin `  (
s  /  2 ) )  e.  RR )
233230, 232remulcld 9653 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  RR )
234 2cnd 10648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
2  e.  CC )
235191recnd 9651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
s  e.  CC )
236235halfcld 10823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( s  /  2
)  e.  CC )
237236sincld 14072 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( sin `  (
s  /  2 ) )  e.  CC )
238 2ne0 10668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  =/=  0
239238a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
2  =/=  0 )
240 fourierdlem44 37282 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
241227, 198, 240syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
242234, 237, 239, 241mulne0d 10241 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  =/=  0 )
243191, 233, 242redivcld 10412 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) )  e.  RR )
244229, 243eqeltrd 2490 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  e.  RR )
24540fvmpt2 5940 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
246227, 244, 245syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( d  e.  ( 0 (,) pi )  /\  s  e.  ( d [,] pi ) )  -> 
( K `  s
)  =  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
247246adantll 712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( K `  s )  =  if ( s  =  0 ,  1 ,  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )
248220, 247oveq12d 6295 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( H `  s
)  x.  ( K `
 s ) )  =  ( ( ( ( F `  ( X  +  s )
)  -  Y )  /  s )  x.  if ( s  =  0 ,  1 ,  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) ) )
249200iffalsed 3895 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
250249oveq2d 6293 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  x.  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  =  ( ( ( ( F `  ( X  +  s
) )  -  Y
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
251185, 248, 2503eqtrd 2447 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( U `  s )  =  ( ( ( ( F `  ( X  +  s )
)  -  Y )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )
252251mpteq2dva 4480 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
s  e.  ( d [,] pi )  |->  ( U `  s ) )  =  ( s  e.  ( d [,] pi )  |->  ( ( ( ( F `  ( X  +  s
) )  -  Y
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
25365, 175, 2523eqtrd 2447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  O  =  ( s  e.  ( d [,] pi )  |->  ( ( ( ( F `  ( X  +  s )
)  -  Y )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) ) )
254253adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  O  =  ( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) )
255254reseq1d 5092 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( O  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  =  ( ( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) )
25614adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  F : RR --> RR )
25715adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  X  e.  RR )
258 fourierdlem104.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 ) ) ) } )
259 fourierdlem104.m . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  NN )
260259adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  M  e.  NN )
261 fourierdlem104.v . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  V  e.  ( P `
 M ) )
262261adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  V  e.  ( P `  M
) )
263 fourierdlem104.fcn . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
264263adantlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
265 fourierdlem104.r . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
266265adantlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  i )
) )
267 fourierdlem104.l . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
268267adantlr 713 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )
269105adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  d  <  pi )
27050, 10ltnled 9763 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  e.  ( 0 (,) pi )  ->  (
0  <  d  <->  -.  d  <_  0 ) )
27156, 270mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  e.  ( 0 (,) pi )  ->  -.  d  <_  0 )
272271intn3an2d 1341 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ( 0 (,) pi )  ->  -.  ( 0  e.  RR  /\  d  <_  0  /\  0  <_  pi ) )
273 elicc2 11641 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( d  e.  RR  /\  pi  e.  RR )  -> 
( 0  e.  ( d [,] pi )  <-> 
( 0  e.  RR  /\  d  <_  0  /\  0  <_  pi ) ) )
27410, 12, 273sylancl 660 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  e.  ( 0 (,) pi )  ->  (
0  e.  ( d [,] pi )  <->  ( 0  e.  RR  /\  d  <_  0  /\  0  <_  pi ) ) )
275272, 274mtbird 299 . . . . . . . . . . . . . . . . . . 19  |-  ( d  e.  ( 0 (,) pi )  ->  -.  0  e.  ( d [,] pi ) )
276275adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  -.  0  e.  ( d [,] pi ) )
27727adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  Y  e.  RR )
278 eqid 2402 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ( d [,] pi )  |->  ( ( ( ( F `  ( X  +  s
) )  -  Y
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  =  ( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
279 eqid 2402 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )  -  Y )  /  ( 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 ) ) ) ) )  -  Y )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )
280 eqid 2402 . . . . . . . . . . . . . . . . . 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 ) ) ) )  -  Y )  /  ( 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 ) ) ) )  -  Y )  /  ( J `  k ) )  x.  ( ( J `  k )  /  (
2  x.  ( sin `  ( ( J `  k )  /  2
) ) ) ) )
281 fveq2 5848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  ( Q `  l )  =  ( Q `  i ) )
282 oveq1 6284 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  i  ->  (
l  +  1 )  =  ( i  +  1 ) )
283282fveq2d 5852 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  ( Q `  ( l  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
284281, 283oveq12d 6295 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  (
( Q `  l
) (,) ( Q `
 ( l  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
285284sseq2d 3469 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
286285cbvriotav 6250 . . . . . . . . . . . . . . . . . 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 ) ) ) )
287256, 257, 258, 260, 262, 264, 266, 268, 11, 13, 269, 62, 276, 277, 278, 80, 73, 68, 125, 279, 280, 286fourierdlem86 37324 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  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 ) ) ) ) )  -  Y )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  e.  ( ( ( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
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 ) ) ) )  -  Y )  /  ( J `  k )
)  x.  ( ( J `  k )  /  ( 2  x.  ( sin `  (
( J `  k
)  /  2 ) ) ) ) )  e.  ( ( ( s  e.  ( d [,] pi )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  k ) ) )  /\  (
( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  e.  ( ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) ) -cn-> CC ) ) )
288287simprd 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( (
s  e.  ( d [,] pi )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  e.  ( ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) ) -cn-> CC ) )
289255, 288eqeltrd 2490 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( O  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  e.  ( ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) -cn-> CC ) )
290287simplld 753 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  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 ) ) ) ) )  -  Y )  /  ( J `  ( k  +  1 ) ) )  x.  ( ( J `  ( k  +  1 ) )  /  (
2  x.  ( sin `  ( ( J `  ( k  +  1 ) )  /  2
) ) ) ) )  e.  ( ( ( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  ( k  +  1 ) ) ) )
291254eqcomd 2410 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( s  e.  ( d [,] pi )  |->  ( ( ( ( F `  ( X  +  s )
)  -  Y )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  =  O )
292291reseq1d 5092 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( (
s  e.  ( d [,] pi )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  =  ( O  |`  (
( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) ) )
293292oveq1d 6292 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( (
( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
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 ) ) ) )
294290, 293eleqtrd 2492 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  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 ) ) ) ) )  -  Y )  /  ( 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 ) ) ) )
295287simplrd 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  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 ) ) ) )  -  Y )  /  ( J `  k )
)  x.  ( ( J `  k )  /  ( 2  x.  ( sin `  (
( J `  k
)  /  2 ) ) ) ) )  e.  ( ( ( s  e.  ( d [,] pi )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) ) lim CC  ( J `  k ) ) )
296292oveq1d 6292 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( (
( s  e.  ( d [,] pi ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
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 ) ) )
297295, 296eleqtrd 2492 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  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 ) ) ) )  -  Y )  /  ( J `  k )
)  x.  ( ( J `  k )  /  ( 2  x.  ( sin `  (
( J `  k
)  /  2 ) ) ) ) )  e.  ( ( O  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) ) lim CC  ( J `  k )
) )
298 eqid 2402 . . . . . . . . . . . . . . 15  |-  ( RR 
_D  O )  =  ( RR  _D  O
)
29967adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  O :
( d [,] pi )
--> CC )
30011ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  d  e.  RR )
30112a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  pi  e.  RR )
302 elioore 11611 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  ->  s  e.  RR )
303302adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  s  e.  RR )
30462, 210syl6ss 3453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( 0 (,) pi ) )  ->  (
d [,] pi ) 
C_  RR )
305304adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( d [,] pi )  C_  RR )
306149adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  J :
( 0 ... N
) --> ( d [,] pi ) )
307306, 168ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  k )  e.  ( d [,] pi ) )
308305, 307sseldd 3442 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  k )  e.  RR )
309308adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( J `  k )  e.  RR )
31011adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  d  e.  RR )
311310rexrd 9672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  d  e.  RR* )
31254a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  pi  e.  RR* )
313 iccgelb 11633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  RR*  /\  pi  e.  RR*  /\  ( J `
 k )  e.  ( d [,] pi ) )  ->  d  <_  ( J `  k
) )
314311, 312, 307, 313syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  d  <_  ( J `  k ) )
315314adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  d  <_  ( J `  k ) )
316309rexrd 9672 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( J `  k )  e.  RR* )
317306, 170ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  ( k  +  1 ) )  e.  ( d [,] pi ) )
318305, 317sseldd 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  ( k  +  1 ) )  e.  RR )
319318rexrd 9672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  ( k  +  1 ) )  e.  RR* )
320319adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( J `  ( k  +  1 ) )  e.  RR* )
321 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )
322 ioogtlb 36877 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( J `  k
)  e.  RR*  /\  ( J `  ( k  +  1 ) )  e.  RR*  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  ( J `  k )  <  s )
323316, 320, 321, 322syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( J `  k )  <  s
)
324300, 309, 303, 315, 323lelttrd 9773 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  d  <  s )
325300, 303, 324ltled 9764 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  d  <_  s )
326318adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( J `  ( k  +  1 ) )  e.  RR )
327 iooltub 36897 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( J `  k
)  e.  RR*  /\  ( J `  ( k  +  1 ) )  e.  RR*  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  s  <  ( J `  (
k  +  1 ) ) )
328316, 320, 321, 327syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  s  <  ( J `  ( k  +  1 ) ) )
329 iccleub 11632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  RR*  /\  pi  e.  RR*  /\  ( J `
 ( k  +  1 ) )  e.  ( d [,] pi ) )  ->  ( J `  ( k  +  1 ) )  <_  pi )
330311, 312, 317, 329syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( J `  ( k  +  1 ) )  <_  pi )
331330adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( J `  ( k  +  1 ) )  <_  pi )
332303, 326, 301, 328, 331ltletrd 9775 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  s  <  pi )
333303, 301, 332ltled 9764 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  s  <_  pi )
334300, 301, 303, 325, 333eliccd 36887 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  s  e.  ( d [,] pi ) )
335334ralrimiva 2817 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  A. s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) s  e.  ( d [,] pi ) )
336 dfss3 3431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
C_  ( d [,] pi )  <->  A. s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) s  e.  ( d [,] pi ) )
337335, 336sylibr 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) )  C_  (
d [,] pi ) )
338299, 337feqresmpt 5902 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  ->  ( O  |`  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  =  ( s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  |->  ( O `  s ) ) )
339 simplll 760 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ph )
340 simpllr 761 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  d  e.  ( 0 (,) pi ) )
34164fveq1i 5849 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( O `
 s )  =  ( ( U  |`  ( d [,] pi ) ) `  s
)
342341a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( O `  s )  =  ( ( U  |`  ( d [,] pi ) ) `  s
) )
343 fvres 5862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( d [,] pi )  ->  (
( U  |`  (
d [,] pi ) ) `  s )  =  ( U `  s ) )
344343adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( U  |`  (
d [,] pi ) ) `  s )  =  ( U `  s ) )
345247, 249eqtrd 2443 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( K `  s )  =  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
346220, 345oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( H `  s
)  x.  ( K `
 s ) )  =  ( ( ( ( F `  ( X  +  s )
)  -  Y )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )
347215recnd 9651 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( F `  ( X  +  s )
)  -  Y )  e.  CC )
348235adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  s  e.  CC )
349 2cnd 10648 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  2  e.  CC )
350348halfcld 10823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
s  /  2 )  e.  CC )
351350sincld 14072 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
352349, 351mulcld 9645 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
353242adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =/=  0 )
354347, 348, 352, 199, 353dmdcan2d 10390 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  (
( ( ( F `
 ( X  +  s ) )  -  Y )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
355185, 346, 3543eqtrd 2447 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( U `  s )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
356342, 344, 3553eqtrd 2447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  s  e.  ( d [,] pi ) )  ->  ( O `  s )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
357339, 340, 334, 356syl21anc 1229 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( O `  s )  =  ( ( ( F `  ( X  +  s
) )  -  Y
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )
358339, 340, 334, 354syl21anc 1229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( (
( ( F `  ( X  +  s
) )  -  Y
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )  =  ( ( ( F `  ( X  +  s
) )  -  Y
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )
359358eqcomd 2410 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  d  e.  ( 0 (,) pi ) )  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) )  ->  ( (
( F `  ( X  +  s )
)  -  Y )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  =  ( ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
360 eqidd 2403 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  (
t  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  |->  ( ( ( F `  ( X  +  t
) )  -  Y
)  /  t ) )  =  ( t  e.  ( ( J `
 k ) (,) ( J `  (
k  +  1 ) ) )  |->  ( ( ( F `  ( X  +  t )
)  -  Y )  /  t ) ) )
361 oveq2 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  s  ->  ( X  +  t )  =  ( X  +  s ) )
362361fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  s  ->  ( F `  ( X  +  t ) )  =  ( F `  ( X  +  s
) ) )
363362oveq1d 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  s  ->  (
( F `  ( X  +  t )
)  -  Y )  =  ( ( F `
 ( X  +  s ) )  -  Y ) )
364 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  s  ->  t  =  s )
365363, 364oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  s  ->  (
( ( F `  ( X  +  t
) )  -  Y
)  /  t )  =  ( ( ( F `  ( X  +  s ) )  -  Y )  / 
s ) )
366365adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  /\  t  =  s )  ->  ( ( ( F `
 ( X  +  t ) )  -  Y )  /  t
)  =  ( ( ( F `  ( X  +  s )
)  -  Y )  /  s ) )
367 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )
368 ovex 6305 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( F `  ( X  +  s )
)  -  Y )  /  s )  e. 
_V
369368a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  (
( ( F `  ( X  +  s
) )  -  Y
)  /  s )  e.  _V )
370360, 366, 367, 369fvmptd 5937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  (
( t  e.  ( ( J `  k
) (,) ( J `
 ( k  +  1 ) ) ) 
|->  ( ( ( F `
 ( X  +  t ) )  -  Y )  /  t
) ) `  s
)  =  ( ( ( F `  ( X  +  s )
)  -  Y )  /  s ) )
371 eqidd 2403 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) )  ->  (
t  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  |->  ( t  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) )  =  ( t  e.  ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) )  |->  ( t  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )
372 oveq1 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  s  ->  (
t  /  2 )  =  ( s  / 
2 ) )
373372fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  s  ->  ( sin `  ( t  / 
2 ) )  =  ( sin `  (
s  /  2 ) ) )
374373oveq2d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  s  ->  (
2  x.  ( sin `  ( t  /  2
) ) )  =  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
375364, 374oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  s  ->  (
t  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) )  =  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
376375adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ N ) )  /\  s  e.  ( ( J `  k ) (,) ( J `  (
k  +  1 ) ) ) )  /\  t  =  s )  ->  ( t  /  (
2  x.  ( sin `  (