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

Theorem fourierdlem80 31810
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 . . . . . . . . . 10  |-  O  =  ( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
2 oveq2 6303 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  ( X  +  s )  =  ( X  +  t ) )
32fveq2d 5876 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  t
) ) )
43oveq1d 6310 . . . . . . . . . . . 12  |-  ( s  =  t  ->  (
( F `  ( X  +  s )
)  -  C )  =  ( ( F `
 ( X  +  t ) )  -  C ) )
5 oveq1 6302 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
s  /  2 )  =  ( t  / 
2 ) )
65fveq2d 5876 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  ( sin `  ( s  / 
2 ) )  =  ( sin `  (
t  /  2 ) ) )
76oveq2d 6311 . . . . . . . . . . . 12  |-  ( s  =  t  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =  ( 2  x.  ( sin `  ( t  / 
2 ) ) ) )
84, 7oveq12d 6313 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  =  ( ( ( F `
 ( X  +  t ) )  -  C )  /  (
2  x.  ( sin `  ( t  /  2
) ) ) ) )
98cbvmptv 4544 . . . . . . . . . 10  |-  ( 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 2497 . . . . . . . . 9  |-  ( t  e.  ( A [,] B )  |->  ( ( ( F `  ( X  +  t )
)  -  C )  /  ( 2  x.  ( sin `  (
t  /  2 ) ) ) ) )  =  O
1110oveq2i 6306 . . . . . . . 8  |-  ( RR 
_D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )  =  ( RR  _D  O
)
1211dmeqi 5210 . . . . . . 7  |-  dom  ( RR  _D  ( t  e.  ( A [,] B
)  |->  ( ( ( F `  ( X  +  t ) )  -  C )  / 
( 2  x.  ( sin `  ( t  / 
2 ) ) ) ) ) )  =  dom  ( RR  _D  O )
1312ineq2i 3702 . . . . . 6  |-  ( 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 4044 . . . . 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 ) ) }
1514uneq1i 3659 . . . 4  |-  ( { ( 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 ) ) ) ) )
1615a1i 11 . . 3  |-  ( 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 ) ) ) ) )  =  ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
17 snfi 7608 . . . . 5  |-  { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  e.  Fin
18 fzofi 12064 . . . . . 6  |-  ( 0..^ N )  e.  Fin
19 eqid 2467 . . . . . . 7  |-  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  =  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
2019rnmptfi 31348 . . . . . 6  |-  ( ( 0..^ N )  e. 
Fin  ->  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  e.  Fin )
2118, 20ax-mp 5 . . . . 5  |-  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  e.  Fin
22 unfi 7799 . . . . 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 )
2317, 21, 22mp2an 672 . . . 4  |-  ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )  e.  Fin
2423a1i 11 . . 3  |-  ( ph  ->  ( { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  e.  Fin )
2516, 24eqeltrd 2555 . 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 )
26 simpl 457 . . 3  |-  ( (
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 ) ) ) ) ) )  ->  ph )
27 id 22 . . . . 5  |-  ( 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 ) ) ) ) ) )
2815unieqi 4260 . . . . 5  |-  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 ) ) ) ) )
2927, 28syl6eleq 2565 . . . 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  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
3029adantl 466 . . 3  |-  ( (
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 ) ) ) ) ) )  ->  s  e.  U. ( { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) ) )
31 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 )
32 uniun 4270 . . . . . . . . . 10  |-  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 ) ) ) ) )
3332eleq2i 2545 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
3433biimpi 194 . . . . . . . 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 ) ) ) ) ) )
35 elun 3650 . . . . . . . 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 ) ) ) ) ) )
3634, 35sylib 196 . . . . . . 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 ) ) ) ) ) )
3736adantl 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 ) ) ) ) ) )
38 fourierdlem80.sf . . . . . . . . . . . . 13  |-  ( ph  ->  S : ( 0 ... N ) --> ( A [,] B ) )
39 ovex 6320 . . . . . . . . . . . . . 14  |-  ( 0 ... N )  e. 
_V
4039a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 ... N
)  e.  _V )
41 fex 6144 . . . . . . . . . . . . 13  |-  ( ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( 0 ... N )  e.  _V )  ->  S  e.  _V )
4238, 40, 41syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  _V )
43 rnexg 6727 . . . . . . . . . . . 12  |-  ( S  e.  _V  ->  ran  S  e.  _V )
4442, 43syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ran  S  e.  _V )
45 inex1g 4596 . . . . . . . . . . 11  |-  ( ran 
S  e.  _V  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V )
4644, 45syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  _V )
47 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 ) ) )
4846, 47syl 16 . . . . . . . . 9  |-  ( ph  ->  U. { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
4948eleq2d 2537 . . . . . . . 8  |-  ( ph  ->  ( s  e.  U. { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  <-> 
s  e.  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) ) )
5049adantr 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
) ) ) )
5150orbi1d 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 ) ) ) ) ) ) )
5237, 51mpbid 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 ) ) ) ) ) )
53 dvf 22179 . . . . . . . . 9  |-  ( RR 
_D  O ) : dom  ( RR  _D  O ) --> CC
5453a1i 11 . . . . . . . 8  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
( RR  _D  O
) : dom  ( RR  _D  O ) --> CC )
55 elin 3692 . . . . . . . . . 10  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  <->  ( s  e.  ran  S  /\  s  e.  dom  ( RR  _D  O ) ) )
5655biimpi 194 . . . . . . . . 9  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
( s  e.  ran  S  /\  s  e.  dom  ( RR  _D  O
) ) )
5756simprd 463 . . . . . . . 8  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
s  e.  dom  ( RR  _D  O ) )
5854, 57ffvelrnd 6033 . . . . . . 7  |-  ( s  e.  ( ran  S  i^i  dom  ( RR  _D  O ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
5958adantl 466 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
60 ovex 6320 . . . . . . . . . . . . . 14  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  e. 
_V
6160rgenw 2828 . . . . . . . . . . . . 13  |-  A. j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  e.  _V
62 dfiun3g 5261 . . . . . . . . . . . . 13  |-  ( A. j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  e. 
_V  ->  U_ j  e.  ( 0..^ N ) ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  =  U. ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
6361, 62ax-mp 5 . . . . . . . . . . . 12  |-  U_ j  e.  ( 0..^ N ) ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  =  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
6463eleq2i 2545 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
6564bicomi 202 . . . . . . . . . 10  |-  ( 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 ) ) ) )
6665biimpi 194 . . . . . . . . 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 ) ) ) )
6766adantl 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 ) ) ) )
68 eliun 4336 . . . . . . . 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 ) ) ) )
6967, 68sylib 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 ) ) ) )
70 nfv 1683 . . . . . . . . 9  |-  F/ j
ph
71 nfcv 2629 . . . . . . . . . 10  |-  F/_ j
s
72 nfmpt1 4542 . . . . . . . . . . . 12  |-  F/_ j
( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
7372nfrn 5251 . . . . . . . . . . 11  |-  F/_ j ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
7473nfuni 4257 . . . . . . . . . 10  |-  F/_ j U. ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
7571, 74nfel 2642 . . . . . . . . 9  |-  F/ j  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
7670, 75nfan 1875 . . . . . . . 8  |-  F/ j ( ph  /\  s  e.  U. ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )
77 nfv 1683 . . . . . . . 8  |-  F/ j ( ( RR  _D  O ) `  s
)  e.  CC
7853a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( RR  _D  O
) : dom  ( RR  _D  O ) --> CC )
79 fourierdlem80.y . . . . . . . . . . . . . . . . . . . 20  |-  Y  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
8079a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Y  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
81 eqid 2467 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s ) )  -  C )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
8281a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s ) )  -  C )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s
) )  -  C
)  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
831reseq1i 5275 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )
8483a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
85 ioossicc 11622 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  (
( S `  j
) [,] ( S `
 ( j  +  1 ) ) ) )
87 fourierdlem80.sjss . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) [,] ( S `  (
j  +  1 ) ) )  C_  ( A [,] B ) )
8886, 87sstrd 3519 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  ( A [,] B ) )
8988resmptd 5331 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
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 ) ) ) ) ) )
9084, 89eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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 ) ) ) ) ) )
9190eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s ) )  -  C )  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )  =  ( O  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
9280, 82, 913eqtrd 2512 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Y  =  ( O  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )
9392oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  Y )  =  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
94 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  C_  CC
9594a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  RR  C_  CC )
9694a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  RR  C_  CC )
97 fourierdlem80.f . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F : RR --> RR )
9897adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  F : RR
--> RR )
99 fourierdlem80.xre . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  e.  RR )
10099adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  X  e.  RR )
101 fourierdlem80.a . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A  e.  RR )
102 fourierdlem80.b . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  B  e.  RR )
103101, 102iccssred 31426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A [,] B
)  C_  RR )
104103sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  RR )
105100, 104readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( X  +  s )  e.  RR )
10698, 105ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
10796, 106sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
108 fourierdlem80.c . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  C  e.  RR )
10994, 108sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  C  e.  CC )
110109adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  C  e.  CC )
111107, 110subcld 9942 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( ( F `  ( X  +  s ) )  -  C )  e.  CC )
112 2cn 10618 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  CC
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  2  e.  CC )
114103, 95sstrd 3519 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A [,] B
)  C_  CC )
115114sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  CC )
116115halfcld 10795 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( s  /  2 )  e.  CC )
117116sincld 13743 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( sin `  ( s  /  2
) )  e.  CC )
118113, 117mulcld 9628 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  e.  CC )
119 2ne0 10640 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  =/=  0
120119a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  2  =/=  0 )
121 fourierdlem80.ab . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
122121sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  ( -u pi [,] pi ) )
123 eqcom 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  0  <->  0  =  s )
124123biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  0  ->  0  =  s )
125124adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  0  =  s )
126 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  s  e.  ( A [,] B ) )
127125, 126eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  ( A [,] B )  /\  s  =  0 )  ->  0  e.  ( A [,] B ) )
128127adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  s  =  0 )  -> 
0  e.  ( A [,] B ) )
129 fourierdlem80.n0 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
130129ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  s  =  0 )  ->  -.  0  e.  ( A [,] B ) )
131128, 130pm2.65da 576 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  -.  s  =  0 )
132131neqned 2670 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  =/=  0 )
133 fourierdlem44 31774 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
134122, 132, 133syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( sin `  ( s  /  2
) )  =/=  0
)
135113, 117, 120, 134mulne0d 10213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =/=  0
)
136111, 118, 135divcld 10332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( (
( F `  ( X  +  s )
)  -  C )  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  CC )
137136, 1fmptd 6056 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  O : ( A [,] B ) --> CC )
138 ioossre 11598 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR
139138a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR )
140 eqid 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
141140tgioo2 21176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
142140, 141dvres 22183 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
14395, 137, 103, 139, 142syl22anc 1229 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  _D  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )
144 ioontr 31436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )
145144reseq2i 5276 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( RR  _D  O )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
146145a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( RR  _D  O )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
147143, 146eqtrd 2508 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( RR  _D  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) )  =  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
148147adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  =  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
14993, 148eqtr2d 2509 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( RR  _D  Y ) )
150149dmeqd 5211 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  dom  ( RR  _D  Y
) )
15197adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  F : RR --> RR )
15299adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  X  e.  RR )
153103adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A [,] B )  C_  RR )
15438adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> ( A [,] B
) )
155 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
156155adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
157154, 156ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  ( A [,] B ) )
158153, 157sseldd 3510 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
159 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
160159adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
161154, 160ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )
162153, 161sseldd 3510 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
163 fdv . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : I --> RR )
164 fourierdlem80.i . . . . . . . . . . . . . . . . . . . . . . 23  |-  I  =  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )
165164feq2i 5730 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  ( F  |`  I ) ) : I --> RR  <->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
166165a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  ( F  |`  I ) ) : I --> RR  <->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR ) )
167163, 166mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  I ) ) : ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
168164reseq2i 5276 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F  |`  I )  =  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
169168oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
_D  ( F  |`  I ) )  =  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
170 feq1 5719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( RR  _D  ( F  |`  I ) )  =  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )  ->  ( ( 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 ) )
171169, 170ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 )
172171a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( 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 ) )
173167, 172mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
174121adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )
17588, 174sstrd 3519 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
176129adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( A [,] B ) )
17788, 176ssneldd 3512 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
178108adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  e.  RR )
179151, 152, 158, 162, 173, 175, 177, 178, 79fourierdlem57 31787 . . . . . . . . . . . . . . . . . 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 ) ) ) )
180179simpli 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 ) ) ) ) )
181180simpld 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( RR  _D  Y ) : ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) --> RR )
182 fdm 5741 . . . . . . . . . . . . . . . 16  |-  ( ( RR  _D  Y ) : ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) --> RR  ->  dom  ( RR  _D  Y
)  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
183181, 182syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( RR  _D  Y )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
184150, 183eqtr2d 2509 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  =  dom  ( ( RR  _D  O )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) )
185 resss 5303 . . . . . . . . . . . . . . . 16  |-  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  ( RR  _D  O )
186185a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  ( RR  _D  O ) )
187 dmss 5208 . . . . . . . . . . . . . . 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
) )
188186, 187syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  O )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  C_  dom  ( RR  _D  O
) )
189184, 188eqsstrd 3543 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  dom  ( RR  _D  O
) )
1901893adant3 1016 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  dom  ( RR 
_D  O ) )
191 simp3 998 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
192190, 191sseldd 3510 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
s  e.  dom  ( RR  _D  O ) )
19378, 192ffvelrnd 6033 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N )  /\  s  e.  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
1941933exp 1195 . . . . . . . . 9  |-  ( ph  ->  ( j  e.  ( 0..^ N )  -> 
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) )  ->  ( ( RR 
_D  O ) `  s )  e.  CC ) ) )
195194adantr 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 ) ) )
19676, 77, 195rexlimd 2951 . . . . . . 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 ) )
19769, 196mpd 15 . . . . . 6  |-  ( (
ph  /\  s  e.  U.
ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
19859, 197jaodan 783 . . . . 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 )
19931, 52, 198syl2anc 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 )
200199abscld 13247 . . 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 )
20126, 30, 200syl2anc 661 . 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 )
202 simpl 457 . . 3  |-  ( (
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 ) ) ) ) ) )  ->  ph )
203 id 22 . . . . 5  |-  ( 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 ) ) ) ) ) )
204203, 15syl6eleq 2565 . . . 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  O ) ) }  u.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) ) )
205204adantl 466 . . 3  |-  ( (
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 ) ) ) ) ) )  ->  r  e.  ( { ( ran  S  i^i  dom  ( RR  _D  O ) ) }  u.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )
206 simpl 457 . . . . . 6  |-  ( (
ph  /\  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O
) ) } )  ->  ph )
207 elsni 4058 . . . . . . 7  |-  ( r  e.  { ( ran 
S  i^i  dom  ( RR 
_D  O ) ) }  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
208207adantl 466 . . . . . 6  |-  ( (
ph  /\  r  e.  { ( ran  S  i^i  dom  ( RR  _D  O
) ) } )  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
209 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) ) )
210 fzfid 12063 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
211 rnffi 31353 . . . . . . . . . . 11  |-  ( ( S : ( 0 ... N ) --> ( A [,] B )  /\  ( 0 ... N )  e.  Fin )  ->  ran  S  e.  Fin )
21238, 210, 211syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ran  S  e.  Fin )
213 infi 7755 . . . . . . . . . 10  |-  ( ran 
S  e.  Fin  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
214212, 213syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
215214adantr 465 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( ran  S  i^i  dom  ( RR  _D  O
) )  e.  Fin )
216209, 215eqeltrd 2555 . . . . . . 7  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
r  e.  Fin )
217 nfv 1683 . . . . . . . . 9  |-  F/ s
ph
218 nfcv 2629 . . . . . . . . . 10  |-  F/_ s
r
219 nfcv 2629 . . . . . . . . . . 11  |-  F/_ s ran  S
220 nfcv 2629 . . . . . . . . . . . . 13  |-  F/_ s RR
221 nfcv 2629 . . . . . . . . . . . . 13  |-  F/_ s  _D
222 nfmpt1 4542 . . . . . . . . . . . . . 14  |-  F/_ s
( s  e.  ( A [,] B ) 
|->  ( ( ( F `
 ( X  +  s ) )  -  C )  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
2231, 222nfcxfr 2627 . . . . . . . . . . . . 13  |-  F/_ s O
224220, 221, 223nfov 6318 . . . . . . . . . . . 12  |-  F/_ s
( RR  _D  O
)
225224nfdm 5250 . . . . . . . . . . 11  |-  F/_ s dom  ( RR  _D  O
)
226219, 225nfin 3710 . . . . . . . . . 10  |-  F/_ s
( ran  S  i^i  dom  ( RR  _D  O
) )
227218, 226nfeq 2640 . . . . . . . . 9  |-  F/ s  r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )
228217, 227nfan 1875 . . . . . . . 8  |-  F/ s ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )
229 simpll 753 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  ph )
230 simpr 461 . . . . . . . . . . . . 13  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  r )
231 simpl 457 . . . . . . . . . . . . 13  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
232230, 231eleqtrd 2557 . . . . . . . . . . . 12  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  ( ran  S  i^i  dom  ( RR  _D  O
) ) )
233232, 57syl 16 . . . . . . . . . . 11  |-  ( ( r  =  ( ran 
S  i^i  dom  ( RR 
_D  O ) )  /\  s  e.  r )  ->  s  e.  dom  ( RR  _D  O
) )
234233adantll 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  s  e.  dom  ( RR  _D  O
) )
23553ffvelrni 6031 . . . . . . . . . . . 12  |-  ( s  e.  dom  ( RR 
_D  O )  -> 
( ( RR  _D  O ) `  s
)  e.  CC )
236235abscld 13247 . . . . . . . . . . 11  |-  ( s  e.  dom  ( RR 
_D  O )  -> 
( abs `  (
( RR  _D  O
) `  s )
)  e.  RR )
237236adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  dom  ( RR  _D  O
) )  ->  ( abs `  ( ( RR 
_D  O ) `  s ) )  e.  RR )
238229, 234, 237syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O ) ) )  /\  s  e.  r )  ->  ( abs `  ( ( RR  _D  O ) `  s
) )  e.  RR )
239238ex 434 . . . . . . . 8  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  -> 
( s  e.  r  ->  ( abs `  (
( RR  _D  O
) `  s )
)  e.  RR ) )
240228, 239ralrimi 2867 . . . . . . 7  |-  ( (
ph  /\  r  =  ( ran  S  i^i  dom  ( RR  _D  O
) ) )  ->  A. s  e.  r 
( abs `  (
( RR  _D  O
) `  s )
)  e.  RR )
241 fimaxre3 10504 . . . . . . 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 )
242216, 240, 241syl2anc 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 )
243206, 208, 242syl2anc 661 . . . . 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 )
244243adantlr 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 )
245 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 )
246 elun 3650 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
247246biimpi 194 . . . . . . . 8  |-  ( 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 ) ) ) ) ) )
248247adantr 465 . . . . . . 7  |-  ( ( 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  S  i^i  dom  ( RR  _D  O
) ) }  \/  r  e.  ran  ( j  e.  ( 0..^ N )  |->  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) ) ) )
249 simpr 461 . . . . . . 7  |-  ( ( 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  S  i^i  dom  ( RR  _D  O ) ) } )
250 df-or 370 . . . . . . . 8  |-  ( ( r  e.  { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  \/  r  e.  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 ) ) ) ) ) )
251250biimpi 194 . . . . . . 7  |-  ( ( r  e.  { ( ran  S  i^i  dom  ( RR  _D  O
) ) }  \/  r  e.  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 ) ) ) ) ) )
252248, 249, 251sylc 60 . . . . . 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 ) ) ) ) )
253252adantll 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 ) ) ) ) )
254 vex 3121 . . . . . . . . 9  |-  r  e. 
_V
25519elrnmpt 5255 . . . . . . . . 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 ) ) ) ) )
256254, 255ax-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 ) ) ) )
257256biimpi 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 ) ) ) )
258257adantl 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 ) ) ) )
259 nfcv 2629 . . . . . . . . 9  |-  F/_ j
r
260259, 73nfel 2642 . . . . . . . 8  |-  F/ j  r  e.  ran  (
j  e.  ( 0..^ N )  |->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
26170, 260nfan 1875 . . . . . . 7  |-  F/ j ( ph  /\  r  e.  ran  ( j  e.  ( 0..^ N ) 
|->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) )
262 nfv 1683 . . . . . . 7  |-  F/ j E. y  e.  RR  A. s  e.  r  ( abs `  ( ( RR  _D  O ) `
 s ) )  <_  y
263 fourierdlem80.fbdioo . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  I  ( abs `  ( F `
 t ) )  <_  w )
264 fourierdlem80.fdvbdioo . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z )
265263, 264jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( 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 ) )
266 reeanv 3034 . . . . . . . . . . . . 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 ) )
267265, 266sylibr 212 . . . . . . . . . . . 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 ) )
268 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 ) ) )
269 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 )
270 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 )
271268, 269, 270jca31 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 ) )
272 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 )
273 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 )
274271, 272, 273jca31 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 ) )
275 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 ) )
276274, 275sylibr 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 )
277275biimpi 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 ) )
278 simp-5l 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 )
279277, 278syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ph )
280279, 97syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  F : RR --> RR )
281279, 99syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  X  e.  RR )
282 simp-4l 765 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
283277, 282syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ph  /\  j  e.  ( 0..^ N ) ) )
284283, 158syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  j
)  e.  RR )
285283, 162syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR )
286 fourierdlem80.slt . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
287283, 286syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  j
)  <  ( S `  ( j  +  1 ) ) )
28887, 174sstrd 3519 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j ) [,] ( S `  (
j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
289283, 288syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )  C_  ( -u pi [,] pi ) )
290 ssnel 31325 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )  C_  ( A [,] B )  /\  -.  0  e.  ( A [,] B ) )  ->  -.  0  e.  (
( S `  j
) [,] ( S `
 ( j  +  1 ) ) ) )
29187, 176, 290syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  -.  0  e.  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) ) )
292283, 291syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  -.  0  e.  ( ( S `  j
) [,] ( S `
 ( j  +  1 ) ) ) )
293283, 173syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) : ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) --> RR )
294 simp-4r 766 . . . . . . . . . . . . . . . . . . . 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 )
295277, 294syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  w  e.  RR )
296 simplr 754 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
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 )
297277, 296syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  A. t  e.  I 
( abs `  ( F `  t )
)  <_  w )
298297adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  A. t  e.  I  ( abs `  ( F `  t
) )  <_  w
)
299 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
300164eleq2i 2545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  I  <->  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  (
t  e.  I  <->  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
302299, 301mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) )  ->  t  e.  I )
303302adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  t  e.  I )
304 rspa 2834 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. t  e.  I 
( abs `  ( F `  t )
)  <_  w  /\  t  e.  I )  ->  ( abs `  ( F `  t )
)  <_  w )
305298, 303, 304syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  ( abs `  ( F `  t
) )  <_  w
)
306 simpllr 758 . . . . . . . . . . . . . . . . . . . 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 )
307277, 306syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  z  e.  RR )
308 simpl 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  ch )
309277simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z )
310309adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  t  e.  I )  ->  A. t  e.  I  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_  z )
311 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  t  e.  I )  ->  t  e.  I )
312 rspa 2834 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A. t  e.  I 
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  I ) ) `  t ) )  <_ 
z )
313310, 311, 312syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  I ) ) `  t ) )  <_ 
z )
314169fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( RR  _D  ( F  |`  I ) ) `  t )  =  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t )
315314fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  =  ( abs `  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )
316315breq1i 4460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( abs `  ( ( RR  _D  ( F  |`  I ) ) `  t ) )  <_ 
z  <->  ( abs `  (
( RR  _D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )  <_  z )
317316a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  t  e.  I )  ->  (
( abs `  (
( RR  _D  ( F  |`  I ) ) `
 t ) )  <_  z  <->  ( abs `  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )  <_  z ) )
318313, 317mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  t  e.  I )  ->  ( abs `  ( ( RR 
_D  ( F  |`  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `  t
) )  <_  z
)
319308, 303, 318syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  t  e.  ( ( X  +  ( S `  j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) )  ->  ( abs `  ( ( RR  _D  ( F  |`  ( ( X  +  ( S `
 j ) ) (,) ( X  +  ( S `  ( j  +  1 ) ) ) ) ) ) `
 t ) )  <_  z )
320279, 108syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  C  e.  RR )
321280, 281, 284, 285, 287, 289, 292, 293, 295, 305, 307, 319, 320, 79fourierdlem68 31798 . . . . . . . . . . . . . . . . . 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
) )
322321simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  E. y  e.  RR  A. s  e.  dom  ( RR  _D  Y ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y )
323321simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  dom  ( RR  _D  Y )  =  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )
324 raleq 3063 . . . . . . . . . . . . . . . . . . 19  |-  ( dom  ( RR  _D  Y
)  =  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  -> 
( 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 ) )
325323, 324syl 16 . . . . . . . . . . . . . . . . . 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 ) )
326325rexbidv 2978 . . . . . . . . . . . . . . . . 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
) )
327322, 326mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  E. y  e.  RR  A. s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ( abs `  ( ( RR  _D  Y ) `
 s ) )  <_  y )
328 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
329 fvres 5886 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( ( S `
 j