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

Theorem fourierdlem80 32172
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 6304 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  ( X  +  s )  =  ( X  +  t ) )
32fveq2d 5876 . . . . . . . . . . . 12  |-  ( s  =  t  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  t
) ) )
43oveq1d 6311 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
( F `  ( X  +  s )
)  -  C )  =  ( ( F `
 ( X  +  t ) )  -  C ) )
5 oveq1 6303 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
s  /  2 )  =  ( t  / 
2 ) )
65fveq2d 5876 . . . . . . . . . . . 12  |-  ( s  =  t  ->  ( sin `  ( s  / 
2 ) )  =  ( sin `  (
t  /  2 ) ) )
76oveq2d 6312 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =  ( 2  x.  ( sin `  ( t  / 
2 ) ) ) )
84, 7oveq12d 6314 . . . . . . . . . 10  |-  ( s  =  t  ->  (
( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  =  ( ( ( F `
 ( X  +  t ) )  -  C )  /  (
2  x.  ( sin `  ( t  /  2
) ) ) ) )
98cbvmptv 4548 . . . . . . . . 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 2487 . . . . . . . 8  |-  ( t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t )
)  -  C )  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) )  =  O
1110oveq2i 6307 . . . . . . 7  |-  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )  =  ( RR  _D  O
)
1211dmeqi 5214 . . . . . 6  |-  dom  ( RR  _D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )  =  dom  ( RR  _D  O )
1312ineq2i 3693 . . . . 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 4043 . . . 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 3650 . . 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 7615 . . . . 5  |-  { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  e.  Fin
17 fzofi 12087 . . . . . 6  |-  ( 0..^ N )  e.  Fin
18 eqid 2457 . . . . . . 7  |-  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  =  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
1918rnmptfi 31650 . . . . . 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 7805 . . . . 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 672 . . . 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 2549 . 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 22 . . . 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 4260 . . . 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 2555 . . 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 457 . . . . 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 4270 . . . . . . . . 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 2535 . . . . . . . 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 3641 . . . . . . . 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 197 . . . . . . 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 466 . . . . . 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 6324 . . . . . . . . . . . . . 14  |-  ( 0 ... N )  e. 
_V
3635a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 ... N
)  e.  _V )
37 fex 6146 . . . . . . . . . . . . 13  |-  ( ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( 0 ... N )  e.  _V )  ->  S  e.  _V )
3834, 36, 37syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  _V )
39 rnexg 6731 . . . . . . . . . . . 12  |-  ( S  e.  _V  ->  ran  S  e.  _V )
4038, 39syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ran  S  e.  _V )
41 inex1g 4599 . . . . . . . . . . 11  |-  ( ran 
S  e.  _V  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V )
4240, 41syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V )
43 unisng 4267 . . . . . . . . . 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 16 . . . . . . . . 9  |-  ( ph  ->  U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
4544eleq2d 2527 . . . . . . . 8  |-  ( ph  ->  ( s  e.  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  <-> 
s  e.  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) ) )
4645adantr 465 . . . . . . 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 702 . . . . . 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 210 . . . . 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 22437 . . . . . . . . 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 31626 . . . . . . . 8  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
s  e.  dom  ( RR  _D  O ) )
5250, 51ffvelrnd 6033 . . . . . . 7  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
5352adantl 466 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
54 ovex 6324 . . . . . . . . . . . 12  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  e. 
_V
5554dfiun3 5267 . . . . . . . . . . 11  |-  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  =  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
5655eleq2i 2535 . . . . . . . . . 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 206 . . . . . . . . 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 466 . . . . . . . 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 4337 . . . . . . . 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 196 . . . . . . 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 1708 . . . . . . . . 9  |-  F/ j
ph
62 nfmpt1 4546 . . . . . . . . . . . 12  |-  F/_ j
( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6362nfrn 5255 . . . . . . . . . . 11  |-  F/_ j ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6463nfuni 4257 . . . . . . . . . 10  |-  F/_ j U. ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
6564nfcri 2612 . . . . . . . . 9  |-  F/ j  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6661, 65nfan 1929 . . . . . . . 8  |-  F/ j ( ph  /\  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
67 nfv 1708 . . . . . . . 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 5279 . . . . . . . . . . . . . . . . . . . 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 11635 . . . . . . . . . . . . . . . . . . . . . 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 3510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  ( A [,] B ) )
7372resmptd 5335 . . . . . . . . . . . . . . . . . . . 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 2510 . . . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Y  =  ( O  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
7776oveq2d 6312 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  Y )  =  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
78 ax-resscn 9566 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  C_  CC
7978a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  RR  C_  CC )
80 fourierdlem80.f . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F : RR --> RR )
8180adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  F : RR
--> RR )
82 fourierdlem80.xre . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  e.  RR )
8382adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 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 31742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A [,] B
)  C_  RR )
8786sselda 3499 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  RR )
8883, 87readdcld 9640 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( X  +  s )  e.  RR )
8981, 88ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
9089recnd 9639 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
91 fourierdlem80.c . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  C  e.  RR )
9291recnd 9639 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  C  e.  CC )
9392adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  C  e.  CC )
9490, 93subcld 9950 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( ( F `  ( X  +  s ) )  -  C )  e.  CC )
95 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  2  e.  CC )
9686, 79sstrd 3509 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A [,] B
)  C_  CC )
9796sselda 3499 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  CC )
9897halfcld 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( s  /  2 )  e.  CC )
9998sincld 13877 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( sin `  ( s  /  2
) )  e.  CC )
10095, 99mulcld 9633 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  e.  CC )
101 2ne0 10649 . . . . . . . . . . . . . . . . . . . . . . . 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 3499 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  ( -u pi [,] pi ) )
105 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  0  <->  0  =  s )
106105biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  0  ->  0  =  s )
107106adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  0  =  s )
108 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  s  e.  ( A [,] B ) )
109107, 108eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  0  e.  ( A [,] B ) )
110109adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  s  =  0 )  -> 
0  e.  ( A [,] B ) )
111 fourierdlem80.n0 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
112111ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  s  =  0 )  ->  -.  0  e.  ( A [,] B ) )
113110, 112pm2.65da 576 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  -.  s  =  0 )
114113neqned 2660 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  =/=  0 )
115 fourierdlem44 32136 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
116104, 114, 115syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( sin `  ( s  /  2
) )  =/=  0
)
11795, 99, 102, 116mulne0d 10222 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =/=  0
)
11894, 100, 117divcld 10341 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( (
( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  CC )
119118, 1fmptd 6056 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  O : ( A [,] B ) --> CC )
120 ioossre 11611 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR
121120a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR )
122 eqid 2457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
123122tgioo2 21434 . . . . . . . . . . . . . . . . . . . . 21  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
124122, 123dvres 22441 . . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  _D  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )
126 ioontr 31752 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )
127126reseq2i 5280 . . . . . . . . . . . . . . . . . . 19  |-  ( ( RR  _D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
128125, 127syl6eq 2514 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
129128adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  =  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
13077, 129eqtr2d 2499 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( RR  _D  Y ) )
131130dmeqd 5215 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  dom  ( RR  _D  Y
) )
13280adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  F : RR --> RR )
13382adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  X  e.  RR )
13486adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A [,] B )  C_  RR )
13534adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> ( A [,] B
) )
136 elfzofz 11841 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
137136adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
138135, 137ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  ( A [,] B ) )
139134, 138sseldd 3500 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
140 fzofzp1 11912 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
141140adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
142135, 141ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )
143134, 142sseldd 3500 . . . . . . . . . . . . . . . . . . 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 5730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( RR  _D  ( F  |`  I ) ) : I --> RR  <->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
147144, 146sylib 196 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
148145reseq2i 5280 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F  |`  I )  =  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
149148oveq2i 6307 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
_D  ( F  |`  I ) )  =  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
150149feq1i 5729 . . . . . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )
15372, 152sstrd 3509 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
154111adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( A [,] B ) )
15572, 154ssneldd 3502 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
15691adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  e.  RR )
157132, 133, 139, 143, 151, 153, 155, 156, 75fourierdlem57 32149 . . . . . . . . . . . . . . . . . 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 458 . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  Y ) : ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) --> RR )
160 fdm 5741 . . . . . . . . . . . . . . . 16  |-  ( ( RR  _D  Y ) : ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) --> RR  ->  dom  ( RR  _D  Y
)  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
161159, 160syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( RR  _D  Y )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
162131, 161eqtr2d 2499 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  =  dom  ( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )
163 resss 5307 . . . . . . . . . . . . . . 15  |-  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  ( RR  _D  O )
164 dmss 5212 . . . . . . . . . . . . . . 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 12 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  dom  ( RR  _D  O
) )
166162, 165eqsstrd 3533 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  dom  ( RR  _D  O
) )
1671663adant3 1016 . . . . . . . . . . . 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 998 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
169167, 168sseldd 3500 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
s  e.  dom  ( RR  _D  O ) )
17068, 169ffvelrnd 6033 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
1711703exp 1195 . . . . . . . . 9  |-  ( ph  ->  ( j  e.  ( 0..^ N )  -> 
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  ->  ( ( RR 
_D  O ) `  s )  e.  CC ) ) )
172171adantr 465 . . . . . . . 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 2941 . . . . . . 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 785 . . . . 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 661 . . . 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 13279 . . 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 474 . 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 22 . . . 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 2555 . . 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 4057 . . . . . 6  |-  ( r  e.  { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
182 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
183 fzfid 12086 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
184 rnffi 31655 . . . . . . . . . . 11  |-  ( ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( 0 ... N )  e.  Fin )  ->  ran  S  e.  Fin )
18534, 183, 184syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ran  S  e.  Fin )
186 infi 7762 . . . . . . . . . 10  |-  ( ran 
S  e.  Fin  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
187185, 186syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
188187adantr 465 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
189182, 188eqeltrd 2545 . . . . . . 7  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
r  e.  Fin )
190 nfv 1708 . . . . . . . . 9  |-  F/ s
ph
191 nfcv 2619 . . . . . . . . . . 11  |-  F/_ s ran  S
192 nfcv 2619 . . . . . . . . . . . . 13  |-  F/_ s RR
193 nfcv 2619 . . . . . . . . . . . . 13  |-  F/_ s  _D
194 nfmpt1 4546 . . . . . . . . . . . . . 14  |-  F/_ s
( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
1951, 194nfcxfr 2617 . . . . . . . . . . . . 13  |-  F/_ s O
196192, 193, 195nfov 6322 . . . . . . . . . . . 12  |-  F/_ s
( RR  _D  O
)
197196nfdm 5254 . . . . . . . . . . 11  |-  F/_ s dom  ( RR  _D  O
)
198191, 197nfin 3701 . . . . . . . . . 10  |-  F/_ s
( ran  S  i^i  dom  ( RR  _D  O
) )
199198nfeq2 2636 . . . . . . . . 9  |-  F/ s  r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )
200190, 199nfan 1929 . . . . . . . 8  |-  F/ s ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )
201 simpr 461 . . . . . . . . . . . . 13  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  r )
202 simpl 457 . . . . . . . . . . . . 13  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
203201, 202eleqtrd 2547 . . . . . . . . . . . 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 16 . . . . . . . . . . 11  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  dom  ( RR  _D  O
) )
205204adantll 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  s  e.  dom  ( RR  _D  O
) )
20649ffvelrni 6031 . . . . . . . . . . 11  |-  ( s  e.  dom  ( RR 
_D  O )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
207206abscld 13279 . . . . . . . . . 10  |-  ( s  e.  dom  ( RR 
_D  O )  -> 
( abs `  (
( RR  _D  O
) `  s )
)  e.  RR )
208205, 207syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  ( abs `  ( ( RR  _D  O ) `  s
) )  e.  RR )
209208ex 434 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( s  e.  r  ->  ( abs `  (
( RR  _D  O
) `  s )
)  e.  RR ) )
210200, 209ralrimi 2857 . . . . . . 7  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  ->  A. s  e.  r 
( abs `  (
( RR  _D  O
) `  s )
)  e.  RR )
211 fimaxre3 10512 . . . . . . 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 661 . . . . . 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 474 . . . . 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 714 . . . 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 753 . . . . 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 31617 . . . . . 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 713 . . . . 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 3112 . . . . . . . . 9  |-  r  e. 
_V
21918elrnmpt 5259 . . . . . . . . 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 194 . . . . . . 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 466 . . . . . 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 2612 . . . . . . . 8  |-  F/ j  r  e.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
22461, 223nfan 1929 . . . . . . 7  |-  F/ j ( ph  /\  r  e.  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
225 nfv 1708 . . . . . . 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 3025 . . . . . . . . . . . . 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 664 . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . . 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 1022 . . . . . . . . . . . . . . . . . 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 1023 . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . 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 1024 . . . . . . . . . . . . . . . . 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 1025 . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . 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 194 . . . . . . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ph )
242241, 80syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  F : RR --> RR )
243241, 82syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  X  e.  RR )
244 simp-4l 767 . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ph  /\  j  e.  ( 0..^ N ) ) )
246245, 139syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  j
)  e.  RR )
247245, 143syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR )
248 fourierdlem80.slt . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
249245, 248syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  j
)  <  ( S `  ( j  +  1 ) ) )
25071, 152sstrd 3509 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) [,] ( S `  (
j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
251245, 250syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
25271, 154ssneldd 3502 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) ) )
253245, 252syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  -.  0  e.  ( ( S `  j
) [,] ( S `
 ( j  +  1 ) ) ) )
254245, 151syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
255 simp-4r 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 )  ->  w  e.  RR )
256239, 255syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  w  e.  RR )
257239simplrd 31629 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  A. t  e.  I 
( abs `  ( F `  t )
)  <_  w )
258 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
259258, 145syl6eleqr 2556 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  t  e.  I )
260 rspa 2824 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  t  e.  I )  ->  ( abs `  ( F `  t )
)  <_  w )
261257, 259, 260syl2an 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  ( abs `  ( F `  t
) )  <_  w
)
262 simpllr 760 . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  z  e.  RR )
264149fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  ( F  |`  I ) ) `  t )  =  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t )
265264fveq2i 5875 . . . . . . . . . . . . . . . . . . . . 21  |-  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  =  ( abs `  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )
266239simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )
267266r19.21bi 2826 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  I ) ) `  t ) )  <_ 
z )
268265, 267syl5eqbrr 4490 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `  t
) )  <_  z
)
269259, 268sylan2 474 . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  C  e.  RR )
271242, 243, 246, 247, 249, 251, 253, 254, 256, 261, 263, 269, 270, 75fourierdlem68 32160 . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  E. y  e.  RR  A. s  e.  dom  ( RR  _D  Y ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y )
273271simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  dom  ( RR  _D  Y )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
274273raleqdv 3060 . . . . . . . . . . . . . . . . . 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 2968 . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y )
277126eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  =  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )
278277reseq2i 5280 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( RR  _D  O
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
279278fveq1i 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( RR  _D  O
)  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) `  s )  =  ( ( ( RR  _D  O )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s )
280 fvres 5886 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  (
( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) `  s )  =  ( ( RR 
_D  O ) `  s ) )
281280adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) `  s )  =  ( ( RR 
_D  O ) `  s ) )
282245, 72syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( A [,] B ) )
283282resmptd 5335 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2510 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  Y  =  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
286285oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( RR  _D  Y
)  =  ( RR 
_D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
287286fveq1d 5874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( RR  _D  Y ) `  s
)  =  ( ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) `  s ) )
288125fveq1d 5874 . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( ( RR 
_D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) `
 s )  =  ( ( RR  _D  Y ) `  s
) )
291290adantr 465 . . . . . . . . . . . . . . . . . . . . 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 2522 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( RR  _D  O
) `  s )  =  ( ( RR 
_D  Y ) `  s ) )
293292fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( abs `  ( ( RR 
_D  O ) `  s ) )  =  ( abs `  (
( RR  _D  Y
) `  s )
) )
294293breq1d 4466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( abs `  (
( RR  _D  O
) `  s )
)  <_  y  <->  ( abs `  ( ( RR  _D  Y ) `  s
) )  <_  y
) )
295294ralbidva 2893 . . . . . . . . . . . . . . . . 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 2968 . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . 15  |-  ( ch 
->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y )
298238, 297syl 16 . . . . . . . . . . . . . 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 1195 . . . . . . . . . . . . 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 2955 . . . . . . . . . . . 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 1016 . . . . . . . . . 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 3054 . . . . . . . . . . . 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 1019 . . . . . . . . . . 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 2968 . . . . . . . . . 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 232 . . . . . . . . 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 1195 . . . . . . . 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 465 . . . . . . 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 2941 . . . . . 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 661 . . . 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 791 . . 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 474 . 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 449 . . . . . . . . . . . 12  |-  ( ( r  e.  dom  ( RR  _D  O )  /\  r  e.  ran  S )  ->  ( r  e. 
ran  S  /\  r  e.  dom  ( RR  _D  O ) ) )
315 elin 3683 . . . . . . . . . . . 12  |-  ( r  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  <->  ( r  e.  ran  S  /\  r  e.  dom  ( RR  _D  O ) ) )
316314, 315sylibr 212 . . . . . . . . . . 11  |-  ( ( r  e.  dom  ( RR  _D  O )  /\  r  e.  ran  S )  ->  r  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
317316adantll 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  r  e.  ran  S )  ->  r  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
31844eqcomd 2465 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  =  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )
319318ad2antrr 725 . . . . . . . . . 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 2547 . . . . . . . . 9  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  r  e.  ran  S )  ->  r  e.  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) } )
321320orcd 392 . . . . . . . 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 753 . . . . . . . . . . 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 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  O : ( A [,] B ) --> CC )
32584adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  A  e.  RR )
32685adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  B  e.  RR )
327325, 326iccssred 31742 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  ( A [,] B )  C_  RR )
328323, 324, 327dvbss 22431 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  dom  ( RR  _D  O
)  C_  ( A [,] B ) )
329 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  r  e.  dom  ( RR  _D  O ) )
330328, 329sseldd 3500 . . . . . . . . . . . 12  |-  ( (
ph  /\  r  e.  dom  ( RR  _D  O
) )  ->  r  e.  ( A [,] B
) )
331330adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  dom  ( RR  _D  O ) )  /\  -.  r  e.  ran  S )  ->  r  e.  ( A [,] B ) )
332 simpr 461 . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . 17  |-  ( j  =  k  ->  ( S `  j )  =  ( S `  k ) )
335 oveq1 6303 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  k  ->  (
j  +  1 )  =  ( k  +  1 ) )
336335fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( j  =  k  ->  ( S `  ( j  +  1 ) )  =  ( S `  ( k  +  1 ) ) )
337334, 336oveq12d 6314 . . . . . . . . . . . . . . . 16  |-  ( j  =  k  ->  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  =  (