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

Theorem fourierdlem80 37876
Description: The derivative of  O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem80.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem80.xre  |-  ( ph  ->  X  e.  RR )
fourierdlem80.a  |-  ( ph  ->  A  e.  RR )
fourierdlem80.b  |-  ( ph  ->  B  e.  RR )
fourierdlem80.ab  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
fourierdlem80.n0  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
fourierdlem80.c  |-  ( ph  ->  C  e.  RR )
fourierdlem80.o  |-  O  =  ( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
fourierdlem80.i  |-  I  =  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )
fourierdlem80.fbdioo  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  I  ( abs `  ( F `
 t ) )  <_  w )
fourierdlem80.fdvbdioo  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z )
fourierdlem80.sf  |-  ( ph  ->  S : ( 0 ... N ) --> ( A [,] B ) )
fourierdlem80.slt  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
fourierdlem80.sjss  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) [,] ( S `  (
j  +  1 ) ) )  C_  ( A [,] B ) )
fourierdlem80.relioo  |-  ( ( ( ph  /\  r  e.  ( A [,] B
) )  /\  -.  r  e.  ran  S )  ->  E. k  e.  ( 0..^ N ) r  e.  ( ( S `
 k ) (,) ( S `  (
k  +  1 ) ) ) )
fdv  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : I --> RR )
fourierdlem80.y  |-  Y  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
fourierdlem80.ch  |-  ( ch  <->  ( ( ( ( (
ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t )
)  <_  w )  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z ) )
Assertion
Ref Expression
fourierdlem80  |-  ( ph  ->  E. b  e.  RR  A. s  e.  dom  ( RR  _D  O ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  b )
Distinct variable groups:    A, b,
r, s, t    B, b, r, s, t    C, b, r, s, t    F, b, r, s, t    w, F, z, s, t    w, I, z    N, b, j, r, s    k, N, j, r    w, N, z, j    O, b, j, r    w, O, z    S, b, j, r, s, t    S, k   
w, S, z    X, b, r, s, t    Y, s    ph, b, j, r, s    ch, s, t    ph, w, z
Allowed substitution hints:    ph( t, k)    ch( z, w, j, k, r, b)    A( z, w, j, k)    B( z, w, j, k)    C( z, w, j, k)    F( j, k)    I( t, j, k, s, r, b)    N( t)    O( t, k, s)    X( z, w, j, k)    Y( z, w, t, j, k, r, b)

Proof of Theorem fourierdlem80
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 fourierdlem80.o . . . . . . . . 9  |-  O  =  ( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
2 oveq2 6311 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  ( X  +  s )  =  ( X  +  t ) )
32fveq2d 5883 . . . . . . . . . . . 12  |-  ( s  =  t  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  t
) ) )
43oveq1d 6318 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
( F `  ( X  +  s )
)  -  C )  =  ( ( F `
 ( X  +  t ) )  -  C ) )
5 oveq1 6310 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
s  /  2 )  =  ( t  / 
2 ) )
65fveq2d 5883 . . . . . . . . . . . 12  |-  ( s  =  t  ->  ( sin `  ( s  / 
2 ) )  =  ( sin `  (
t  /  2 ) ) )
76oveq2d 6319 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =  ( 2  x.  ( sin `  ( t  / 
2 ) ) ) )
84, 7oveq12d 6321 . . . . . . . . . 10  |-  ( s  =  t  ->  (
( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  =  ( ( ( F `
 ( X  +  t ) )  -  C )  /  (
2  x.  ( sin `  ( t  /  2
) ) ) ) )
98cbvmptv 4514 . . . . . . . . 9  |-  ( s  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) )
101, 9eqtr2i 2453 . . . . . . . 8  |-  ( t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t )
)  -  C )  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) )  =  O
1110oveq2i 6314 . . . . . . 7  |-  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )  =  ( RR  _D  O
)
1211dmeqi 5053 . . . . . 6  |-  dom  ( RR  _D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )  =  dom  ( RR  _D  O )
1312ineq2i 3662 . . . . 5  |-  ( ran 
S  i^i  dom  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) ) )  =  ( ran  S  i^i  dom  ( RR  _D  O ) )
1413sneqi 4008 . . . 4  |-  { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  =  { ( ran  S  i^i  dom  ( RR  _D  O ) ) }
1514uneq1i 3617 . . 3  |-  ( { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  =  ( { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
16 snfi 7655 . . . . 5  |-  { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  e.  Fin
17 fzofi 12188 . . . . . 6  |-  ( 0..^ N )  e.  Fin
18 eqid 2423 . . . . . . 7  |-  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  =  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
1918rnmptfi 37290 . . . . . 6  |-  ( ( 0..^ N )  e. 
Fin  ->  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  e.  Fin )
2017, 19ax-mp 5 . . . . 5  |-  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  e.  Fin
21 unfi 7842 . . . . 5  |-  ( ( { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  e.  Fin  /\  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )  e.  Fin )  ->  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  e.  Fin )
2216, 20, 21mp2an 677 . . . 4  |-  ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  e.  Fin
2322a1i 11 . . 3  |-  ( ph  ->  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  e.  Fin )
2415, 23syl5eqel 2515 . 2  |-  ( ph  ->  ( { ( ran 
S  i^i  dom  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  e.  Fin )
25 id 23 . . . 4  |-  ( s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
2615unieqi 4226 . . . 4  |-  U. ( { ( ran  S  i^i  dom  ( RR  _D  ( t  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  t ) )  -  C )  /  (
2  x.  ( sin `  ( t  /  2
) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  U. ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )
2725, 26syl6eleq 2521 . . 3  |-  ( s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
28 simpl 459 . . . . 5  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  ph )
29 uniun 4236 . . . . . . . . 9  |-  U. ( { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( U. {
( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
3029eleq2i 2501 . . . . . . . 8  |-  ( s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  <->  s  e.  ( U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
31 elun 3607 . . . . . . . 8  |-  ( s  e.  ( U. {
( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  <->  ( s  e.  U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  \/  s  e. 
U. ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
3230, 31sylbb 201 . . . . . . 7  |-  ( s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  (
s  e.  U. {
( ran  S  i^i  dom  ( RR  _D  O
) ) }  \/  s  e.  U. ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
3332adantl 468 . . . . . 6  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  (
s  e.  U. {
( ran  S  i^i  dom  ( RR  _D  O
) ) }  \/  s  e.  U. ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
34 fourierdlem80.sf . . . . . . . . . . . . 13  |-  ( ph  ->  S : ( 0 ... N ) --> ( A [,] B ) )
35 ovex 6331 . . . . . . . . . . . . . 14  |-  ( 0 ... N )  e. 
_V
3635a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 ... N
)  e.  _V )
37 fex 6151 . . . . . . . . . . . . 13  |-  ( ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( 0 ... N )  e.  _V )  ->  S  e.  _V )
3834, 36, 37syl2anc 666 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  _V )
39 rnexg 6737 . . . . . . . . . . . 12  |-  ( S  e.  _V  ->  ran  S  e.  _V )
4038, 39syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ran  S  e.  _V )
41 inex1g 4565 . . . . . . . . . . 11  |-  ( ran 
S  e.  _V  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V )
4240, 41syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V )
43 unisng 4233 . . . . . . . . . 10  |-  ( ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V  ->  U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
4442, 43syl 17 . . . . . . . . 9  |-  ( ph  ->  U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
4544eleq2d 2493 . . . . . . . 8  |-  ( ph  ->  ( s  e.  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  <-> 
s  e.  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) ) )
4645adantr 467 . . . . . . 7  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  (
s  e.  U. {
( ran  S  i^i  dom  ( RR  _D  O
) ) }  <->  s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) ) )
4746orbi1d 708 . . . . . 6  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  (
( s  e.  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  \/  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  <->  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) )  \/  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) ) ) )
4833, 47mpbid 214 . . . . 5  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  (
s  e.  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  \/  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
49 dvf 22854 . . . . . . . . 9  |-  ( RR 
_D  O ) : dom  ( RR  _D  O ) --> CC
5049a1i 11 . . . . . . . 8  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
( RR  _D  O
) : dom  ( RR  _D  O ) --> CC )
51 elinel2 3653 . . . . . . . 8  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
s  e.  dom  ( RR  _D  O ) )
5250, 51ffvelrnd 6036 . . . . . . 7  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
5352adantl 468 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
54 ovex 6331 . . . . . . . . . . . 12  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  e. 
_V
5554dfiun3 5106 . . . . . . . . . . 11  |-  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  =  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
5655eleq2i 2501 . . . . . . . . . 10  |-  ( s  e.  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  <->  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )
5756biimpri 210 . . . . . . . . 9  |-  ( s  e.  U. ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
5857adantl 468 . . . . . . . 8  |-  ( (
ph  /\  s  e.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  -> 
s  e.  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
59 eliun 4302 . . . . . . . 8  |-  ( s  e.  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  <->  E. j  e.  ( 0..^ N ) s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )
6058, 59sylib 200 . . . . . . 7  |-  ( (
ph  /\  s  e.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  ->  E. j  e.  (
0..^ N ) s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )
61 nfv 1752 . . . . . . . . 9  |-  F/ j
ph
62 nfmpt1 4511 . . . . . . . . . . . 12  |-  F/_ j
( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6362nfrn 5094 . . . . . . . . . . 11  |-  F/_ j ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6463nfuni 4223 . . . . . . . . . 10  |-  F/_ j U. ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
6564nfcri 2578 . . . . . . . . 9  |-  F/ j  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6661, 65nfan 1985 . . . . . . . 8  |-  F/ j ( ph  /\  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
67 nfv 1752 . . . . . . . 8  |-  F/ j ( ( RR  _D  O ) `  s
)  e.  CC
6849a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( RR  _D  O
) : dom  ( RR  _D  O ) --> CC )
691reseq1i 5118 . . . . . . . . . . . . . . . . . . . 20  |-  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )
70 ioossicc 11722 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )
71 fourierdlem80.sjss . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) [,] ( S `  (
j  +  1 ) ) )  C_  ( A [,] B ) )
7270, 71syl5ss 3476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  ( A [,] B ) )
7372resmptd 5173 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( s  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
7469, 73syl5eq 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
75 fourierdlem80.y . . . . . . . . . . . . . . . . . . 19  |-  Y  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
7674, 75syl6reqr 2483 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Y  =  ( O  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
7776oveq2d 6319 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  Y )  =  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
78 ax-resscn 9598 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  C_  CC
7978a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  RR  C_  CC )
80 fourierdlem80.f . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F : RR --> RR )
8180adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  F : RR
--> RR )
82 fourierdlem80.xre . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  e.  RR )
8382adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  X  e.  RR )
84 fourierdlem80.a . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A  e.  RR )
85 fourierdlem80.b . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  B  e.  RR )
8684, 85iccssred 37439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A [,] B
)  C_  RR )
8786sselda 3465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  RR )
8883, 87readdcld 9672 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( X  +  s )  e.  RR )
8981, 88ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
9089recnd 9671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
91 fourierdlem80.c . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  C  e.  RR )
9291recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  C  e.  CC )
9392adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  C  e.  CC )
9490, 93subcld 9988 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( ( F `  ( X  +  s ) )  -  C )  e.  CC )
95 2cnd 10684 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  2  e.  CC )
9686, 79sstrd 3475 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A [,] B
)  C_  CC )
9796sselda 3465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  CC )
9897halfcld 10859 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( s  /  2 )  e.  CC )
9998sincld 14177 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( sin `  ( s  /  2
) )  e.  CC )
10095, 99mulcld 9665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  e.  CC )
101 2ne0 10704 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  =/=  0
102101a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  2  =/=  0 )
103 fourierdlem80.ab . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
104103sselda 3465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  ( -u pi [,] pi ) )
105 eqcom 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  0  <->  0  =  s )
106105biimpi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  0  ->  0  =  s )
107106adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  0  =  s )
108 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  s  e.  ( A [,] B ) )
109107, 108eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  0  e.  ( A [,] B ) )
110109adantll 719 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  s  =  0 )  -> 
0  e.  ( A [,] B ) )
111 fourierdlem80.n0 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
112111ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  s  =  0 )  ->  -.  0  e.  ( A [,] B ) )
113110, 112pm2.65da 579 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  -.  s  =  0 )
114113neqned 2628 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  =/=  0 )
115 fourierdlem44 37841 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
116104, 114, 115syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( sin `  ( s  /  2
) )  =/=  0
)
11795, 99, 102, 116mulne0d 10266 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =/=  0
)
11894, 100, 117divcld 10385 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( (
( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  CC )
119118, 1fmptd 6059 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  O : ( A [,] B ) --> CC )
120 ioossre 11698 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR
121120a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR )
122 eqid 2423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
123122tgioo2 21813 . . . . . . . . . . . . . . . . . . . . 21  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
124122, 123dvres 22858 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( RR  C_  CC  /\  O : ( A [,] B ) --> CC )  /\  ( ( A [,] B ) 
C_  RR  /\  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
C_  RR ) )  ->  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  =  ( ( RR  _D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )
12579, 119, 86, 121, 124syl22anc 1266 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  _D  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )
126 ioontr 37448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )
127126reseq2i 5119 . . . . . . . . . . . . . . . . . . 19  |-  ( ( RR  _D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
128125, 127syl6eq 2480 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
129128adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  =  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
13077, 129eqtr2d 2465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( RR  _D  Y ) )
131130dmeqd 5054 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  dom  ( RR  _D  Y
) )
13280adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  F : RR --> RR )
13382adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  X  e.  RR )
13486adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A [,] B )  C_  RR )
13534adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> ( A [,] B
) )
136 elfzofz 11937 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
137136adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
138135, 137ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  ( A [,] B ) )
139134, 138sseldd 3466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
140 fzofzp1 12009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
141140adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
142135, 141ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )
143134, 142sseldd 3466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
144 fdv . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : I --> RR )
145 fourierdlem80.i . . . . . . . . . . . . . . . . . . . . . 22  |-  I  =  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )
146145feq2i 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( RR  _D  ( F  |`  I ) ) : I --> RR  <->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
147144, 146sylib 200 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
148145reseq2i 5119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F  |`  I )  =  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
149148oveq2i 6314 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
_D  ( F  |`  I ) )  =  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
150149feq1i 5736 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR  <->  ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
151147, 150sylib 200 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
152103adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )
15372, 152sstrd 3475 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
154111adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( A [,] B ) )
15572, 154ssneldd 3468 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
15691adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  e.  RR )
157132, 133, 139, 143, 151, 153, 155, 156, 75fourierdlem57 37853 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR  _D  Y ) : ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) --> RR  /\  ( RR  _D  Y )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( ( ( ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 ( X  +  s ) )  x.  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )  -  ( ( cos `  ( s  /  2 ) )  x.  ( ( F `
 ( X  +  s ) )  -  C ) ) )  /  ( ( 2  x.  ( sin `  (
s  /  2 ) ) ) ^ 2 ) ) ) ) )  /\  ( RR 
_D  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( cos `  (
s  /  2 ) ) ) )
158157simpli 460 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  Y ) : ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) --> RR  /\  ( RR  _D  Y )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( ( ( ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 ( X  +  s ) )  x.  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )  -  ( ( cos `  ( s  /  2 ) )  x.  ( ( F `
 ( X  +  s ) )  -  C ) ) )  /  ( ( 2  x.  ( sin `  (
s  /  2 ) ) ) ^ 2 ) ) ) ) )
159158simpld 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  Y ) : ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) --> RR )
160 fdm 5748 . . . . . . . . . . . . . . . 16  |-  ( ( RR  _D  Y ) : ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) --> RR  ->  dom  ( RR  _D  Y
)  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
161159, 160syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( RR  _D  Y )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
162131, 161eqtr2d 2465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  =  dom  ( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )
163 resss 5145 . . . . . . . . . . . . . . 15  |-  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  ( RR  _D  O )
164 dmss 5051 . . . . . . . . . . . . . . 15  |-  ( ( ( RR  _D  O
)  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  C_  ( RR  _D  O
)  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  dom  ( RR  _D  O
) )
165163, 164mp1i 13 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  dom  ( RR  _D  O
) )
166162, 165eqsstrd 3499 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  dom  ( RR  _D  O
) )
1671663adant3 1026 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  dom  ( RR 
_D  O ) )
168 simp3 1008 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
169167, 168sseldd 3466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
s  e.  dom  ( RR  _D  O ) )
17068, 169ffvelrnd 6036 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
1711703exp 1205 . . . . . . . . 9  |-  ( ph  ->  ( j  e.  ( 0..^ N )  -> 
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  ->  ( ( RR 
_D  O ) `  s )  e.  CC ) ) )
172171adantr 467 . . . . . . . 8  |-  ( (
ph  /\  s  e.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  -> 
( j  e.  ( 0..^ N )  -> 
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  ->  ( ( RR 
_D  O ) `  s )  e.  CC ) ) )
17366, 67, 172rexlimd 2910 . . . . . . 7  |-  ( (
ph  /\  s  e.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  -> 
( E. j  e.  ( 0..^ N ) s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC ) )
17460, 173mpd 15 . . . . . 6  |-  ( (
ph  /\  s  e.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
17553, 174jaodan 793 . . . . 5  |-  ( (
ph  /\  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) )  \/  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )  ->  ( ( RR  _D  O ) `  s )  e.  CC )
17628, 48, 175syl2anc 666 . . . 4  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  (
( RR  _D  O
) `  s )  e.  CC )
177176abscld 13491 . . 3  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  ( abs `  ( ( RR 
_D  O ) `  s ) )  e.  RR )
17827, 177sylan2 477 . 2  |-  ( (
ph  /\  s  e.  U. ( { ( ran 
S  i^i  dom  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  ->  ( abs `  ( ( RR 
_D  O ) `  s ) )  e.  RR )
179 id 23 . . . 4  |-  ( r  e.  ( { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  r  e.  ( { ( ran 
S  i^i  dom  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
180179, 15syl6eleq 2521 . . 3  |-  ( r  e.  ( { ( ran  S  i^i  dom  ( RR  _D  (
t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t
) )  -  C
)  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  r  e.  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
181 elsni 4022 . . . . . 6  |-  ( r  e.  { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
182 simpr 463 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
183 fzfid 12187 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
184 rnffi 37295 . . . . . . . . . . 11  |-  ( ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( 0 ... N )  e.  Fin )  ->  ran  S  e.  Fin )
18534, 183, 184syl2anc 666 . . . . . . . . . 10  |-  ( ph  ->  ran  S  e.  Fin )
186 infi 7799 . . . . . . . . . 10  |-  ( ran 
S  e.  Fin  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
187185, 186syl 17 . . . . . . . . 9  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
188187adantr 467 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
189182, 188eqeltrd 2511 . . . . . . 7  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
r  e.  Fin )
190 nfv 1752 . . . . . . . . 9  |-  F/ s
ph
191 nfcv 2585 . . . . . . . . . . 11  |-  F/_ s ran  S
192 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ s RR
193 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ s  _D
194 nfmpt1 4511 . . . . . . . . . . . . . 14  |-  F/_ s
( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
1951, 194nfcxfr 2583 . . . . . . . . . . . . 13  |-  F/_ s O
196192, 193, 195nfov 6329 . . . . . . . . . . . 12  |-  F/_ s
( RR  _D  O
)
197196nfdm 5093 . . . . . . . . . . 11  |-  F/_ s dom  ( RR  _D  O
)
198191, 197nfin 3670 . . . . . . . . . 10  |-  F/_ s
( ran  S  i^i  dom  ( RR  _D  O
) )
199198nfeq2 2602 . . . . . . . . 9  |-  F/ s  r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )
200190, 199nfan 1985 . . . . . . . 8  |-  F/ s ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )
201 simpr 463 . . . . . . . . . . . . 13  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  r )
202 simpl 459 . . . . . . . . . . . . 13  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
203201, 202eleqtrd 2513 . . . . . . . . . . . 12  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
204203, 51syl 17 . . . . . . . . . . 11  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  dom  ( RR  _D  O
) )
205204adantll 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  s  e.  dom  ( RR  _D  O
) )
20649ffvelrni 6034 . . . . . . . . . . 11  |-  ( s  e.  dom  ( RR 
_D  O )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
207206abscld 13491 . . . . . . . . . 10  |-  ( s  e.  dom  ( RR 
_D  O )  -> 
( abs `  (
( RR  _D  O
) `  s )
)  e.  RR )
208205, 207syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  ( abs `  ( ( RR  _D  O ) `  s
) )  e.  RR )
209208ex 436 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( s  e.  r  ->  ( abs `  (
( RR  _D  O
) `  s )
)  e.  RR ) )
210200, 209ralrimi 2826 . . . . . . 7  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  ->  A. s  e.  r 
( abs `  (
( RR  _D  O
) `  s )
)  e.  RR )
211 fimaxre3 10555 . . . . . . 7  |-  ( ( r  e.  Fin  /\  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  e.  RR )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
212189, 210, 211syl2anc 666 . . . . . 6  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
213181, 212sylan2 477 . . . . 5  |-  ( (
ph  /\  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O
) ) } )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
214213adantlr 720 . . . 4  |-  ( ( ( ph  /\  r  e.  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  /\  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
215 simpll 759 . . . . 5  |-  ( ( ( ph  /\  r  e.  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  /\  -.  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )  ->  ph )
216 elunnel1 3608 . . . . . 6  |-  ( ( r  e.  ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  /\  -.  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )  ->  r  e.  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
217216adantll 719 . . . . 5  |-  ( ( ( ph  /\  r  e.  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  /\  -.  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )  ->  r  e.  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
218 vex 3085 . . . . . . . . 9  |-  r  e. 
_V
21918elrnmpt 5098 . . . . . . . . 9  |-  ( r  e.  _V  ->  (
r  e.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  <->  E. j  e.  (
0..^ N ) r  =  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
220218, 219ax-mp 5 . . . . . . . 8  |-  ( r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  <->  E. j  e.  ( 0..^ N ) r  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
221220biimpi 198 . . . . . . 7  |-  ( r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  ->  E. j  e.  (
0..^ N ) r  =  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )
222221adantl 468 . . . . . 6  |-  ( (
ph  /\  r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  E. j  e.  ( 0..^ N ) r  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
22363nfcri 2578 . . . . . . . 8  |-  F/ j  r  e.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
22461, 223nfan 1985 . . . . . . 7  |-  F/ j ( ph  /\  r  e.  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
225 nfv 1752 . . . . . . 7  |-  F/ j E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y
226 fourierdlem80.fbdioo . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  I  ( abs `  ( F `
 t ) )  <_  w )
227 fourierdlem80.fdvbdioo . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z )
228 reeanv 2997 . . . . . . . . . . . . 13  |-  ( E. w  e.  RR  E. z  e.  RR  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z )  <->  ( E. w  e.  RR  A. t  e.  I  ( abs `  ( F `  t
) )  <_  w  /\  E. z  e.  RR  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )
229226, 227, 228sylanbrc 669 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. w  e.  RR  E. z  e.  RR  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )
230 simp1 1006 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  -> 
( ph  /\  j  e.  ( 0..^ N ) ) )
231 simp2l 1032 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  ->  w  e.  RR )
232 simp2r 1033 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  -> 
z  e.  RR )
233230, 231, 232jca31 537 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  -> 
( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR ) )
234 simp3l 1034 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  ->  A. t  e.  I 
( abs `  ( F `  t )
)  <_  w )
235 simp3r 1035 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  ->  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )
236233, 234, 235jca31 537 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  -> 
( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t ) )  <_  w )  /\  A. t  e.  I  ( abs `  ( ( RR 
_D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )
237 fourierdlem80.ch . . . . . . . . . . . . . . . 16  |-  ( ch  <->  ( ( ( ( (
ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t )
)  <_  w )  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z ) )
238236, 237sylibr 216 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  ->  ch )
239237biimpi 198 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t ) )  <_  w )  /\  A. t  e.  I  ( abs `  ( ( RR 
_D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )
240 simp-5l 777 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t )
)  <_  w )  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )  ->  ph )
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ph )
242241, 80syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  F : RR --> RR )
243241, 82syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  X  e.  RR )
244 simp-4l 775 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t )
)  <_  w )  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )  -> 
( ph  /\  j  e.  ( 0..^ N ) ) )
245239, 244syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ph  /\  j  e.  ( 0..^ N ) ) )
246245, 139syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  j
)  e.  RR )
247245, 143syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR )
248 fourierdlem80.slt . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
249245, 248syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  j
)  <  ( S `  ( j  +  1 ) ) )
25071, 152sstrd 3475 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) [,] ( S `  (
j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
251245, 250syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
25271, 154ssneldd 3468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) ) )
253245, 252syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  -.  0  e.  ( ( S `  j
) [,] ( S `
 ( j  +  1 ) ) ) )
254245, 151syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
255 simp-4r 776 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t )
)  <_  w )  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )  ->  w  e.  RR )
256239, 255syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  w  e.  RR )
257239simplrd 762 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  A. t  e.  I 
( abs `  ( F `  t )
)  <_  w )
258 id 23 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
259258, 145syl6eleqr 2522 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  t  e.  I )
260 rspa 2793 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  t  e.  I )  ->  ( abs `  ( F `  t )
)  <_  w )
261257, 259, 260syl2an 480 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  ( abs `  ( F `  t
) )  <_  w
)
262 simpllr 768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  j  e.  ( 0..^ N ) )  /\  w  e.  RR )  /\  z  e.  RR )  /\  A. t  e.  I  ( abs `  ( F `  t )
)  <_  w )  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )  -> 
z  e.  RR )
263239, 262syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  z  e.  RR )
264149fveq1i 5880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  ( F  |`  I ) ) `  t )  =  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t )
265264fveq2i 5882 . . . . . . . . . . . . . . . . . . . . 21  |-  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  =  ( abs `  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )
266239simprd 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )
267266r19.21bi 2795 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  I ) ) `  t ) )  <_ 
z )
268265, 267syl5eqbrr 4456 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `  t
) )  <_  z
)
269259, 268sylan2 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  ( abs `  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )  <_  z )
270241, 91syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  C  e.  RR )
271242, 243, 246, 247, 249, 251, 253, 254, 256, 261, 263, 269, 270, 75fourierdlem68 37864 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( dom  ( RR 
_D  Y )  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  /\  E. y  e.  RR  A. s  e. 
dom  ( RR  _D  Y ) ( abs `  ( ( RR  _D  Y ) `  s
) )  <_  y
) )
272271simprd 465 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  E. y  e.  RR  A. s  e.  dom  ( RR  _D  Y ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y )
273271simpld 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  dom  ( RR  _D  Y )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
274273raleqdv 3032 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( A. s  e. 
dom  ( RR  _D  Y ) ( abs `  ( ( RR  _D  Y ) `  s
) )  <_  y  <->  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y ) )
275274rexbidv 2940 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( E. y  e.  RR  A. s  e. 
dom  ( RR  _D  Y ) ( abs `  ( ( RR  _D  Y ) `  s
) )  <_  y  <->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ( abs `  ( ( RR  _D  Y ) `  s
) )  <_  y
) )
276272, 275mpbid 214 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y )
277126eqcomi 2436 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  =  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )
278277reseq2i 5119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( RR  _D  O
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
279278fveq1i 5880 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( RR  _D  O
)  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) `  s )  =  ( ( ( RR  _D  O )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s )
280 fvres 5893 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  (
( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) `  s )  =  ( ( RR 
_D  O ) `  s ) )
281280adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) `  s )  =  ( ( RR 
_D  O ) `  s ) )
282245, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( A [,] B ) )
283282resmptd 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  ( ( s  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  s ) )  -  C )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
28469, 283syl5eq 2476 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( O  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
285284, 75syl6reqr 2483 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  Y  =  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
286285oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( RR  _D  Y
)  =  ( RR 
_D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
287286fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( RR  _D  Y ) `  s
)  =  ( ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) `  s ) )
288125fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) `  s )  =  ( ( ( RR  _D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s ) )
289241, 288syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) `  s )  =  ( ( ( RR  _D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s ) )
290287, 289eqtr2d 2465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( ( RR 
_D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s )  =  ( ( RR  _D  Y ) `  s
) )
291290adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( ( RR  _D  O )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s )  =  ( ( RR  _D  Y ) `  s
) )
292279, 281, 2913eqtr3a 2488 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( RR  _D  O
) `  s )  =  ( ( RR 
_D  Y ) `  s ) )
293292fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  O ) `  s ) )  =  ( abs `  (
( RR  _D  Y
) `  s )
) )
294293breq1d 4431 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  ( abs `  ( ( RR  _D  Y ) `  s
) )  <_  y
) )
295294ralbidva 2862 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  Y
) `  s )
)  <_  y )
)
296295rexbidv 2940 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  Y
) `  s )
)  <_  y )
)
297276, 296mpbird 236 . . . . . . . . . . . . . . 15  |-  ( ch 
->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
298238, 297syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( w  e.  RR  /\  z  e.  RR )  /\  ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z ) )  ->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
2992983exp 1205 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( w  e.  RR  /\  z  e.  RR )  ->  (
( A. t  e.  I  ( abs `  ( F `  t )
)  <_  w  /\  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z )  ->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
) )
300299rexlimdvv 2924 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E. w  e.  RR  E. z  e.  RR  ( A. t  e.  I  ( abs `  ( F `  t
) )  <_  w  /\  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )  ->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y ) )
301229, 300mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
3023013adant3 1026 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  r  =  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  ->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
303 raleq 3026 . . . . . . . . . . . 12  |-  ( r  =  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  ( A. s  e.  r 
( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
)
3043033ad2ant3 1029 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  r  =  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
)
305304rexbidv 2940 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  r  =  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
)
306302, 305mpbird 236 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  r  =  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
3073063exp 1205 . . . . . . . 8  |-  ( ph  ->  ( j  e.  ( 0..^ N )  -> 
( r  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y ) ) )
308307adantr 467 . . . . . . 7  |-  ( (
ph  /\  r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  (
j  e.  ( 0..^ N )  ->  (
r  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y ) ) )
309224, 225, 308rexlimd 2910 . . . . . 6  |-  ( (
ph  /\  r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  ( E. j  e.  (
0..^ N ) r  =  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
)
310222, 309mpd 15 . . . . 5  |-  ( (
ph  /\  r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
311215, 217, 310syl2anc 666 . . . 4  |-  ( ( ( ph  /\  r  e.  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )  /\  -.  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
312214, 311pm2.61dan 799 . . 3  |-  ( (
ph  /\  r  e.  ( { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
313180, 312sylan2 477 . 2  |-  ( (
ph  /\  r  e.  ( { ( ran  S  i^i  dom  ( RR  _D  ( t  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  t ) )  -  C )  /  (
2  x.  ( sin `  ( t  /  2
) ) ) ) ) ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )  ->  E. y  e.  RR  A. s  e.  r  ( abs `  (
( RR  _D  O
) `  s )
)  <_  y )
314 pm3.22 451 . . . . . . . . . . . 12  |-  ( ( r  e.  dom  ( RR  _D  O )  /\  r  e.  ran  S )  ->  ( r  e. 
ran  S  /\  r  e.  dom  ( RR  _D  O ) ) )
315 elin 3650 . . . . . . . . . . . 12  |-  ( r  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  <->  ( r  e.  ran  S  /\  r  e.  dom  ( RR  _D  O ) ) )
316314, 315sylibr 216 . . . . . . . . . . 11  |-  ( ( r  e.  dom  ( RR  _D  O )  /\  r  e.  ran  S )  ->  r  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
317316adantll 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  r  e.  ran  S )  ->  r  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
31844eqcomd 2431 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  =  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )
319318ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  r  e.  ran  S )  ->  ( ran  S  i^i  dom  ( RR  _D  O ) )  = 
U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) } )
320317, 319eleqtrd 2513 . . . . . . . . 9  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  r  e.  ran  S )  ->  r  e.  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )
321320orcd 394 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  r  e.  ran  S )  ->  ( r  e. 
U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  \/  r  e. 
U. ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
322 simpll 759 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  -.  r  e.  ran  S )  ->  ph )
32378a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  RR  C_  CC )
324119adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  O : ( A [,] B ) --> CC )
32584adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  A  e.  RR )
32685adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  B  e.  RR )
327325, 326iccssred 37439 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  ( A [,] B )  C_  RR )
328323, 324, 327dvbss 22848 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  dom  ( RR  _D  O
)  C_  ( A [,] B ) )
329 simpr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  r  e.  dom  ( RR  _D  O ) )
330328, 329sseldd 3466 . . . . . . . . . . . 12  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  r  e.  ( A [,] B
) )
331330adantr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  -.  r  e.  ran  S )  ->  r  e.  ( A [,] B ) )
332 simpr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  -.  r  e.  ran  S )  ->  -.  r  e.  ran  S )
333 fourierdlem80.relioo . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  ( A [,] B
) )  /\  -.  r  e.  ran  S )  ->  E. k  e.  ( 0..^ N ) r  e.  ( ( S `
 k ) (,) ( S `  (
k  +  1 ) ) ) )
334 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( j  =  k  ->  ( S `  j )  =  ( S `  k ) )
335 oveq1 6310 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  k  ->  (
j  +  1 )  =  ( k  +  1 ) )
336335fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( j  =  k  ->  ( S `  ( j  +  1 ) )  =  ( S `  ( k  +  1 ) ) )
337334, 336oveq12d 6321 . . . . . . . . . . . . . . . 16  |-  ( j  =  k  ->  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  =  (