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

Theorem fourierdlem76 31806
Description: Continuity of  O and its limits with respect to the  S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem76.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem76.xre  |-  ( ph  ->  X  e.  RR )
fourierdlem76.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem76.m  |-  ( ph  ->  M  e.  NN )
fourierdlem76.v  |-  ( ph  ->  V  e.  ( P `
 M ) )
fourierdlem76.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem76.r  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
fourierdlem76.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
fourierdlem76.a  |-  ( ph  ->  A  e.  RR )
fourierdlem76.b  |-  ( ph  ->  B  e.  RR )
fourierdlem76.altb  |-  ( ph  ->  A  <  B )
fourierdlem76.ab  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
fourierdlem76.n0  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
fourierdlem76.c  |-  ( ph  ->  C  e.  RR )
fourierdlem76.o  |-  O  =  ( s  e.  ( A [,] B ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  C )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
fourierdlem76.q  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
fourierdlem76.t  |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
fourierdlem76.n  |-  N  =  ( ( # `  T
)  -  1 )
fourierdlem76.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
fourierdlem76.d  |-  D  =  ( ( ( if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  -  C )  /  ( S `  ( j  +  1 ) ) )  x.  ( ( S `  ( j  +  1 ) )  /  (
2  x.  ( sin `  ( ( S `  ( j  +  1 ) )  /  2
) ) ) ) )
fourierdlem76.e  |-  E  =  ( ( ( if ( ( S `  j )  =  ( Q `  i ) ,  R ,  ( F `  ( X  +  ( S `  j ) ) ) )  -  C )  /  ( S `  j ) )  x.  ( ( S `  j )  /  (
2  x.  ( sin `  ( ( S `  j )  /  2
) ) ) ) )
fourierdlem76.ch  |-  ( ch  <->  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
Assertion
Ref Expression
fourierdlem76  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( ( D  e.  ( ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) )  /\  E  e.  ( ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) lim CC  ( S `  j )
) )  /\  ( O  |`  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) )  e.  ( ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) ) -cn-> CC ) ) )
Distinct variable groups:    A, s    B, s    C, s    F, s    L, s    i, M, j   
m, M, p, i   
f, N    Q, s    R, s    S, f    S, s    T, f    i, V, j, s    V, p    i, X, j, s    m, X, p    ch, s    ph, f    ph, i, j, s
Allowed substitution hints:    ph( m, p)    ch( f, i, j, m, p)    A( f, i, j, m, p)    B( f,
i, j, m, p)    C( f, i, j, m, p)    D( f, i, j, m, s, p)    P( f, i, j, m, s, p)    Q( f, i, j, m, p)    R( f,
i, j, m, p)    S( i, j, m, p)    T( i, j, m, s, p)    E( f, i, j, m, s, p)    F( f, i, j, m, p)    L( f, i, j, m, p)    M( f, s)    N( i, j, m, s, p)    O( f, i, j, m, s, p)    V( f, m)    X( f)

Proof of Theorem fourierdlem76
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 fourierdlem76.ch . . . 4  |-  ( ch  <->  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
21biimpri 206 . . 3  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  ch )
3 eqid 2467 . . . . 5  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s )
)  -  C )  /  s ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s ) )  -  C )  / 
s ) )
4 eqid 2467 . . . . 5  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) )
5 eqid 2467 . . . . 5  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( ( F `  ( X  +  s
) )  -  C
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  C )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
61biimpi 194 . . . . . . . . . . 11  |-  ( ch 
->  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
7 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  ph )
86, 7syl 16 . . . . . . . . . 10  |-  ( ch 
->  ph )
98adantr 465 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ph )
10 ioossicc 11622 . . . . . . . . . . 11  |-  ( A (,) B )  C_  ( A [,] B )
1110a1i 11 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( A (,) B )  C_  ( A [,] B ) )
12 fourierdlem76.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR )
1312rexrd 9655 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR* )
148, 13syl 16 . . . . . . . . . . . 12  |-  ( ch 
->  A  e.  RR* )
1514adantr 465 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  e.  RR* )
16 fourierdlem76.b . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  RR )
1716rexrd 9655 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  RR* )
188, 17syl 16 . . . . . . . . . . . 12  |-  ( ch 
->  B  e.  RR* )
1918adantr 465 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  B  e.  RR* )
20 ioossre 11598 . . . . . . . . . . . . 13  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR
2120sseli 3505 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  s  e.  RR )
2221adantl 466 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  RR )
238, 12syl 16 . . . . . . . . . . . . 13  |-  ( ch 
->  A  e.  RR )
2423adantr 465 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  e.  RR )
25 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19  |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
26 prfi 7807 . . . . . . . . . . . . . . . . . . . . 21  |-  { A ,  B }  e.  Fin
2726a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { A ,  B }  e.  Fin )
28 fzfid 12063 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
29 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . . 23  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
3029rnmptfi 31348 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
3128, 30syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ran  Q  e.  Fin )
32 infi 7755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
3331, 32syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
34 unfi 7799 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  Fin  /\  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )  -> 
( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
3527, 33, 34syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
3625, 35syl5eqel 2559 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  e.  Fin )
3712, 16jca 532 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
38 prssg 4188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
3912, 16, 38syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
4037, 39mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { A ,  B }  C_  RR )
41 inss2 3724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A (,) B )
42 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A (,) B )  C_  RR
4341, 42sstri 3518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  RR
4443a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  RR )
4540, 44unssd 3685 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  RR )
4625, 45syl5eqss 3553 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  C_  RR )
47 fourierdlem76.s . . . . . . . . . . . . . . . . . 18  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
48 fourierdlem76.n . . . . . . . . . . . . . . . . . 18  |-  N  =  ( ( # `  T
)  -  1 )
4936, 46, 47, 48fourierdlem36 31766 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
508, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  T
) )
51 isof1o 6220 . . . . . . . . . . . . . . . 16  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  ->  S : ( 0 ... N ) -1-1-onto-> T )
52 f1of 5822 . . . . . . . . . . . . . . . 16  |-  ( S : ( 0 ... N ) -1-1-onto-> T  ->  S :
( 0 ... N
) --> T )
5350, 51, 523syl 20 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( 0 ... N ) --> T )
548, 46syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  T  C_  RR )
5553, 54fssd 5746 . . . . . . . . . . . . . 14  |-  ( ch 
->  S : ( 0 ... N ) --> RR )
5655adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  S : ( 0 ... N ) --> RR )
57 simpllr 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
j  e.  ( 0..^ N ) )
586, 57syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  (
0..^ N ) )
59 elfzofz 11823 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
6058, 59syl 16 . . . . . . . . . . . . . 14  |-  ( ch 
->  j  e.  (
0 ... N ) )
6160adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  j  e.  ( 0 ... N
) )
6256, 61ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  e.  RR )
6349, 51, 523syl 20 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  S : ( 0 ... N ) --> T )
64 frn 5743 . . . . . . . . . . . . . . . . . 18  |-  ( S : ( 0 ... N ) --> T  ->  ran  S  C_  T )
6563, 64syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  S  C_  T
)
66 leid 9692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A  e.  RR  ->  A  <_  A )
6712, 66syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  <_  A )
68 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  <  B )
6912, 16, 68ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  <_  B )
7012, 16, 12, 67, 69eliccd 31425 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  ( A [,] B ) )
7116leidd 10131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  <_  B )
7212, 16, 16, 69, 71eliccd 31425 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  ( A [,] B ) )
7370, 72jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  ( A [,] B )  /\  B  e.  ( A [,] B ) ) )
74 prssg 4188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  ( A [,] B
)  /\  B  e.  ( A [,] B ) )  <->  { A ,  B }  C_  ( A [,] B ) ) )
7512, 16, 74syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( A  e.  ( A [,] B
)  /\  B  e.  ( A [,] B ) )  <->  { A ,  B }  C_  ( A [,] B ) ) )
7673, 75mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { A ,  B }  C_  ( A [,] B ) )
7741, 10sstri 3518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A [,] B )
7877a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  ( A [,] B ) )
7976, 78unssd 3685 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  ( A [,] B ) )
8025, 79syl5eqss 3553 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  C_  ( A [,] B ) )
8165, 80sstrd 3519 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  S  C_  ( A [,] B ) )
828, 81syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ran  S  C_  ( A [,] B ) )
83 ffun 5739 . . . . . . . . . . . . . . . . 17  |-  ( S : ( 0 ... N ) --> RR  ->  Fun 
S )
8455, 83syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  Fun  S )
85 fdm 5741 . . . . . . . . . . . . . . . . . . 19  |-  ( S : ( 0 ... N ) --> RR  ->  dom 
S  =  ( 0 ... N ) )
8655, 85syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  dom  S  =  ( 0 ... N ) )
8786eqcomd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( 0 ... N
)  =  dom  S
)
8860, 87eleqtrd 2557 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  j  e.  dom  S )
89 fvelrn 6025 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  S  /\  j  e.  dom  S )  -> 
( S `  j
)  e.  ran  S
)
9084, 88, 89syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  j
)  e.  ran  S
)
9182, 90sseldd 3510 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  ( A [,] B ) )
92 iccgelb 11593 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( S `
 j )  e.  ( A [,] B
) )  ->  A  <_  ( S `  j
) )
9314, 18, 91, 92syl3anc 1228 . . . . . . . . . . . . 13  |-  ( ch 
->  A  <_  ( S `
 j ) )
9493adantr 465 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  <_  ( S `  j
) )
9562rexrd 9655 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  e.  RR* )
96 fzofzp1 11889 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
9758, 96syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( j  +  1 )  e.  ( 0 ... N ) )
9855, 97ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR )
9998rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR* )
10099adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  e.  RR* )
101 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
102 ioogtlb 31415 . . . . . . . . . . . . 13  |-  ( ( ( S `  j
)  e.  RR*  /\  ( S `  ( j  +  1 ) )  e.  RR*  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  <  s )
10395, 100, 101, 102syl3anc 1228 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  <  s )
10424, 62, 22, 94, 103lelttrd 9751 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  <  s )
10598adantr 465 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
1068, 16syl 16 . . . . . . . . . . . . 13  |-  ( ch 
->  B  e.  RR )
107106adantr 465 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  B  e.  RR )
108 iooltub 31435 . . . . . . . . . . . . 13  |-  ( ( ( S `  j
)  e.  RR*  /\  ( S `  ( j  +  1 ) )  e.  RR*  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  ( S `  (
j  +  1 ) ) )
10995, 100, 101, 108syl3anc 1228 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  ( S `  (
j  +  1 ) ) )
11097, 87eleqtrd 2557 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( j  +  1 )  e.  dom  S
)
111 fvelrn 6025 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  S  /\  (
j  +  1 )  e.  dom  S )  ->  ( S `  ( j  +  1 ) )  e.  ran  S )
11284, 110, 111syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ran  S
)
11382, 112sseldd 3510 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( A [,] B ) )
114 iccleub 11592 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( S `
 ( j  +  1 ) )  e.  ( A [,] B
) )  ->  ( S `  ( j  +  1 ) )  <_  B )
11514, 18, 113, 114syl3anc 1228 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  (
j  +  1 ) )  <_  B )
116115adantr 465 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  <_  B )
11722, 105, 107, 109, 116ltletrd 9753 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  B )
11815, 19, 22, 104, 117eliood 31418 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( A (,) B
) )
11911, 118sseldd 3510 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( A [,] B
) )
120 fourierdlem76.f . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> RR )
121120adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  F : RR
--> RR )
122 fourierdlem76.xre . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  RR )
123122adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  X  e.  RR )
12412, 16iccssred 31426 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A [,] B
)  C_  RR )
125124adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( A [,] B )  C_  RR )
126 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  ( A [,] B ) )
127125, 126sseldd 3510 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  RR )
128123, 127readdcld 9635 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( X  +  s )  e.  RR )
129121, 128ffvelrnd 6033 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
1309, 119, 129syl2anc 661 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
131130recnd 9634 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
132 ax-resscn 9561 . . . . . . . . . 10  |-  RR  C_  CC
133 fourierdlem76.c . . . . . . . . . 10  |-  ( ph  ->  C  e.  RR )
134132, 133sseldi 3507 . . . . . . . . 9  |-  ( ph  ->  C  e.  CC )
1358, 134syl 16 . . . . . . . 8  |-  ( ch 
->  C  e.  CC )
136135adantr 465 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  C  e.  CC )
137131, 136subcld 9942 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( F `  ( X  +  s )
)  -  C )  e.  CC )
13820a1i 11 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR )
139138sselda 3509 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  RR )
140132, 139sseldi 3507 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  CC )
141 nne 2668 . . . . . . . . . . . 12  |-  ( -.  s  =/=  0  <->  s  =  0 )
142141biimpi 194 . . . . . . . . . . 11  |-  ( -.  s  =/=  0  -> 
s  =  0 )
143142eqcomd 2475 . . . . . . . . . 10  |-  ( -.  s  =/=  0  -> 
0  =  s )
144143adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
0  =  s )
145126adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
s  e.  ( A [,] B ) )
146144, 145eqeltrd 2555 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
0  e.  ( A [,] B ) )
147 fourierdlem76.n0 . . . . . . . . 9  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
148147ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  ->  -.  0  e.  ( A [,] B ) )
149146, 148condan 792 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  =/=  0 )
1509, 119, 149syl2anc 661 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  =/=  0 )
151137, 140, 150divcld 10332 . . . . 5  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( ( F `  ( X  +  s
) )  -  C
)  /  s )  e.  CC )
152 2cn 10618 . . . . . . . 8  |-  2  e.  CC
153152a1i 11 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  CC )
154140halfcld 10795 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  2 )  e.  CC )
155154sincld 13743 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
156153, 155mulcld 9628 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
157 2ne0 10640 . . . . . . . 8  |-  2  =/=  0
158157a1i 11 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  =/=  0 )
159132, 21sseldi 3507 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  s  e.  CC )
160159adantl 466 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  CC )
161 halfcl 10776 . . . . . . . . . . 11  |-  ( s  e.  CC  ->  (
s  /  2 )  e.  CC )
162160, 161syl 16 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  2 )  e.  CC )
163 sincl 13739 . . . . . . . . . 10  |-  ( ( s  /  2 )  e.  CC  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
164162, 163syl 16 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
165 fourierdlem76.ab . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
1668, 165syl 16 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
167166adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )
168167, 119sseldd 3510 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( -u pi [,] pi ) )
169 fourierdlem44 31774 . . . . . . . . . . . 12  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
170168, 150, 169syl2anc 661 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  =/=  0 )
171153, 164, 158, 170mulne0d 10213 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =/=  0 )
172153, 164, 171mulne0bbd 10217 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  =/=  0 )
173153, 164, 158, 172mulne0d 10213 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =/=  0 )
174153, 155, 173mulne0bbd 10217 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  =/=  0 )
175153, 155, 158, 174mulne0d 10213 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =/=  0 )
176140, 156, 175divcld 10332 . . . . 5  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  CC )
177 eqid 2467 . . . . . 6  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  C ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  C ) )
178 eqid 2467 . . . . . 6  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  s )
179150neneqd 2669 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  s  =  0 )
180 elsn 4047 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
181179, 180sylnibr 305 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
182140, 181eldifd 3492 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
183 eqid 2467 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
184 eqid 2467 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  C )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  C )
185 elfzofz 11823 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
186185adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
187 pire 22718 . . . . . . . . . . . . . . . . . . . . . 22  |-  pi  e.  RR
188187renegcli 9892 . . . . . . . . . . . . . . . . . . . . 21  |-  -u pi  e.  RR
189188a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u pi  e.  RR )
190189, 122jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( -u pi  e.  RR  /\  X  e.  RR ) )
191 readdcl 9587 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-u pi  e.  RR  /\  X  e.  RR )  ->  ( -u pi  +  X )  e.  RR )
192190, 191syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
193187a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  pi  e.  RR )
194193, 122jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( pi  e.  RR  /\  X  e.  RR ) )
195 readdcl 9587 . . . . . . . . . . . . . . . . . . 19  |-  ( ( pi  e.  RR  /\  X  e.  RR )  ->  ( pi  +  X
)  e.  RR )
196194, 195syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
197 iccssre 11618 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -u pi  +  X )  e.  RR  /\  ( pi  +  X
)  e.  RR )  ->  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  C_  RR )
198192, 196, 197syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
199198adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  C_  RR )
200 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
201 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  NN )
202 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  V  e.  ( P `
 M ) )
203200, 201, 202fourierdlem15 31745 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
204203adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
205204, 186ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
206199, 205sseldd 3510 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
207122adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
208206, 207resubcld 9999 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
20929fvmpt2 5964 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
210186, 208, 209syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
211210, 208eqeltrd 2555 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
212211adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
213212adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  e.  RR )
2141, 213sylbi 195 . . . . . . . . 9  |-  ( ch 
->  ( Q `  i
)  e.  RR )
215 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
216215oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
217216cbvmptv 4544 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
21829, 217eqtri 2496 . . . . . . . . . . . . . . 15  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
219218a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
220 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
221220oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
222221adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
223 fzofzp1 11889 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
224223adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
225204, 224ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
226199, 225sseldd 3510 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
227226, 207resubcld 9999 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
228219, 222, 224, 227fvmptd 5962 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
229228, 227eqeltrd 2555 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
230229adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
231230adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
2321, 231sylbi 195 . . . . . . . . 9  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
233200fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  NN  ->  ( V  e.  ( P `  M )  <->  ( V  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
234201, 233syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( V  e.  ( P `  M )  <-> 
( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
235202, 234mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) )
236235simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
237236simprd 463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
238237adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
239 simpr 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0..^ M ) )
240 rspa 2834 . . . . . . . . . . . . . . 15  |-  ( ( A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) )  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
241238, 239, 240syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
242206, 226, 207, 241ltsub1dd 10176 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  <  (
( V `  (
i  +  1 ) )  -  X ) )
243210, 228breq12d 4466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i )  < 
( Q `  (
i  +  1 ) )  <->  ( ( V `
 i )  -  X )  <  (
( V `  (
i  +  1 ) )  -  X ) ) )
244242, 243mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
245244adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
246245adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )
2471, 246sylbi 195 . . . . . . . . 9  |-  ( ch 
->  ( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )
248 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  -> 
i  e.  ( 0..^ M ) )
2496, 248syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  i  e.  (
0..^ M ) )
2508, 249, 206syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  e.  RR )
251250rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  i
)  e.  RR* )
252251adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
2538, 249, 226syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR )
254253rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR* )
255254adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
2568, 122syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  X  e.  RR )
257256adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
258 elioore 11571 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
259258adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
260257, 259readdcld 9635 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
2618, 249, 210syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  =  ( ( V `  i )  -  X ) )
262261oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  i ) )  =  ( X  +  ( ( V `
 i )  -  X ) ) )
263256recnd 9634 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  X  e.  CC )
264132, 250sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( V `  i
)  e.  CC )
265263, 264pncan3d 9945 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( ( V `  i
)  -  X ) )  =  ( V `
 i ) )
266262, 265eqtr2d 2509 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  =  ( X  +  ( Q `  i ) ) )
267266adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
2686, 213syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( Q `  i
)  e.  RR )
269268adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
270268rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
271270adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
2726, 231syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
273272rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
274273adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
275 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
276 ioogtlb 31415 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
277271, 274, 275, 276syl3anc 1228 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
278269, 259, 257, 277ltadd2dd 9752 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
279267, 278eqbrtrd 4473 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
280272adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
281 iooltub 31435 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
282271, 274, 275, 281syl3anc 1228 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
283259, 280, 257, 282ltadd2dd 9752 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
2848, 249, 228syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) )
285284oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
286132, 253sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  CC )
287263, 286pncan3d 9945 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( ( V `  (
i  +  1 ) )  -  X ) )  =  ( V `
 ( i  +  1 ) ) )
288285, 287eqtrd 2508 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
289288adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
290283, 289breqtrd 4477 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
291252, 255, 260, 279, 290eliood 31418 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
292 fvres 5886 . . . . . . . . . . . . 13  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
293291, 292syl 16 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
294293eqcomd 2475 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
) )
295294mpteq2dva 4539 . . . . . . . . . 10  |-  ( ch 
->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) ) ) )
296 ioossre 11598 . . . . . . . . . . . . 13  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
297296, 132sstri 3518 . . . . . . . . . . . 12  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  CC
298297a1i 11 . . . . . . . . . . 11  |-  ( ch 
->  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  CC )
299 fourierdlem76.fcn . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
3008, 249, 299syl2anc 661 . . . . . . . . . . 11  |-  ( ch 
->  ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) )
-cn-> CC ) )
301 ioosscn 31414 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
302301a1i 11 . . . . . . . . . . 11  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC )
303298, 300, 302, 263, 291fourierdlem23 31753 . . . . . . . . . 10  |-  ( ch 
->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
304295, 303eqeltrd 2555 . . . . . . . . 9  |-  ( ch 
->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
3058, 120syl 16 . . . . . . . . . 10  |-  ( ch 
->  F : RR --> RR )
306 ioossre 11598 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
307306a1i 11 . . . . . . . . . 10  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR )
308 eqid 2467 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
309296a1i 11 . . . . . . . . . 10  |-  ( ch 
->  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR )
310259, 282ltned 9732 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  (
i  +  1 ) ) )
311 fourierdlem76.l . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
3128, 249, 311syl2anc 661 . . . . . . . . . . 11  |-  ( ch 
->  L  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
313288eqcomd 2475 . . . . . . . . . . . 12  |-  ( ch 
->  ( V `  (
i  +  1 ) )  =  ( X  +  ( Q `  ( i  +  1 ) ) ) )
314313oveq2d 6311 . . . . . . . . . . 11  |-  ( ch 
->  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
315312, 314eleqtrd 2557 . . . . . . . . . 10  |-  ( ch 
->  L  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
316132, 272sseldi 3507 . . . . . . . . . 10  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  CC )
317305, 256, 307, 308, 291, 309, 310, 315, 316fourierdlem53 31783 . . . . . . . . 9  |-  ( ch 
->  L  e.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
31855, 60ffvelrnd 6033 . . . . . . . . 9  |-  ( ch 
->  ( S `  j
)  e.  RR )
319 elfzoelz 11809 . . . . . . . . . . . 12  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
320 zre 10880 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  j  e.  RR )
32158, 319, 3203syl 20 . . . . . . . . . . 11  |-  ( ch 
->  j  e.  RR )
322321ltp1d 10488 . . . . . . . . . 10  |-  ( ch 
->  j  <  ( j  +  1 ) )
323 isorel 6221 . . . . . . . . . . 11  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  T )  /\  ( j  e.  ( 0 ... N
)  /\  ( j  +  1 )  e.  ( 0 ... N
) ) )  -> 
( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
32450, 60, 97, 323syl12anc 1226 . . . . . . . . . 10  |-  ( ch 
->  ( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
325322, 324mpbid 210 . . . . . . . . 9  |-  ( ch 
->  ( S `  j
)  <  ( S `  ( j  +  1 ) ) )
3261simprbi 464 . . . . . . . . 9  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
327 eqid 2467 . . . . . . . . 9  |-  if ( ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) `  ( S `
 ( j  +  1 ) ) ) )  =  if ( ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) `  ( S `
 ( j  +  1 ) ) ) )
328 eqid 2467 . . . . . . . . 9  |-  ( (
TopOpen ` fld )t  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  u.  {
( Q `  (
i  +  1 ) ) } ) )  =  ( ( TopOpen ` fld )t  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  u.  { ( Q `  ( i  +  1 ) ) } ) )
329214, 232, 247, 304, 317, 318, 98, 325, 326, 327, 328fourierdlem33 31763 . . . . . . . 8  |-  ( ch 
->  if ( ( S `
 ( j  +  1 ) )  =  ( Q `  (
i  +  1 ) ) ,  L , 
( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) ) `  ( S `  ( j  +  1 ) ) ) )  e.  ( ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) ) )
330 iftrue 3951 . . . . . . . . . . . 12  |-  ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) )  ->  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) `  ( S `  ( j  +  1 ) ) ) )  =  L )
331 iftrue 3951 . . . . . . . . . . . 12  |-  ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) )  ->  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  =  L )
332330, 331eqtr4d 2511 . . . . . . . . . . 11  |-  ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) )  ->  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) `  ( S `  ( j  +  1 ) ) ) )  =  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
333332adantl 466 . . . . . . . . . 10  |-  ( ( ch  /\  ( S `
 ( j  +  1 ) )  =  ( Q `  (
i  +  1 ) ) )  ->  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) `  ( S `  ( j  +  1 ) ) ) )  =  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
334 eqidd 2468 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) )
335 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
s  =  ( S `
 ( j  +  1 ) ) )
336335oveq2d 6311 . . . . . . . . . . . . 13  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
( X  +  s )  =  ( X  +  ( S `  ( j  +  1 ) ) ) )
337336fveq2d 5876 . . . . . . . . . . . 12  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
( F `  ( X  +  s )
)  =  ( F `
 ( X  +  ( S `  ( j  +  1 ) ) ) ) )
338214rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
339338adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  e.  RR* )
340232rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
341340adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
34298adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  e.  RR )
3436simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
344318rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( S `  j
)  e.  RR* )
345270, 273, 344, 99, 325ioossioobi 31444 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  C_  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  <-> 
( ( Q `  i )  <_  ( S `  j )  /\  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) ) )
346343, 345mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( Q `  i )  <_  ( S `  j )  /\  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) )
347346simpld 459 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( Q `  i
)  <_  ( S `  j ) )
348268, 318, 98, 347, 325lelttrd 9751 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( Q `  i
)  <  ( S `  ( j  +  1 ) ) )
349348adantr 465 . . . . . . . . . . . . 13  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  <  ( S `  ( j  +  1 ) ) )
350272adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
351346simprd 463 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
352351adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
353 neqne 31339 . . . . . . . . . . . . . . . 16  |-  ( -.  ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) )  -> 
( S `  (
j  +  1 ) )  =/=  ( Q `
 ( i  +  1 ) ) )
354353necomd 2738 . . . . . . . . . . . . . . 15  |-  ( -.  ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) )  -> 
( Q `  (
i  +  1 ) )  =/=  ( S `
 ( j  +  1 ) ) )
355354adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  =/=  ( S `
 ( j  +  1 ) ) )
356342, 350, 352, 355leneltd 31394 . . . . . . . . . . . . 13  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  <  ( Q `
 ( i  +  1 ) ) )
357339, 341, 342, 349, 356eliood 31418 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
358256, 98readdcld 9635 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( X  +  ( S `  ( j  +  1 ) ) )  e.  RR )
359305, 358ffvelrnd 6033 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) )  e.  RR )
360359adantr 465 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( F `  ( X  +  ( S `  ( j  +  1 ) ) ) )  e.  RR )
361334, 337, 357, 360fvmptd 5962 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) ) `  ( S `  ( j  +  1 ) ) )  =  ( F `
 ( X  +  ( S `  ( j  +  1 ) ) ) ) )
362361ifeq2d 3964 . . . . . . . . . 10  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  ->  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) `  ( S `  ( j  +  1 ) ) ) )  =  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
363333, 362pm2.61dan 789 . . . . . . . . 9  |-  ( ch 
->  if ( ( S `
 ( j  +  1 ) )  =  ( Q `  (
i  +  1 ) ) ,  L , 
( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) ) `  ( S `  ( j  +  1 ) ) ) )  =  if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) ) )
364326resmptd 5331 . . . . . . . . . 10  |-  ( ch 
->  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) )
365364oveq1d 6310 . . . . . . . . 9  |-  ( ch 
->  ( ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) )  =  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
366363, 365eleq12d 2549 . . . . . . . 8  |-  ( ch 
->  ( if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) ) `
 ( S `  ( j  +  1 ) ) ) )  e.  ( ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) )  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) )  <->  if ( ( S `
 ( j  +  1 ) )  =  ( Q `  (
i  +  1 ) ) ,  L , 
( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) ) )
367329, 366mpbid 210 . . . . . . 7  |-  ( ch 
->  if ( ( S `
 ( j  +  1 ) )  =  ( Q `  (
i  +  1 ) ) ,  L , 
( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
368138, 132syl6ss 3521 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  CC )
369132, 98sseldi 3507 . . . . . . . 8  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  CC )
370184, 368, 135, 369constlimc 31489 . . . . . . 7  |-  ( ch 
->  C  e.  (
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  C ) lim CC  ( S `  ( j  +  1 ) ) ) )
371183, 184, 177, 131, 136, 367, 370sublimc 31517 . . . . . 6  |-  ( ch 
->  ( if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  -  C )  e.  ( ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( ( F `  ( X  +  s
) )  -  C
) ) lim CC  ( S `  ( j  +  1 ) ) ) )
372368, 178, 369idlimc 31491 . . . . . 6  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  s ) lim CC  ( S `
 ( j  +  1 ) ) ) )
3738, 113jca 532 . . . . . . 7  |-  ( ch 
->  ( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) ) )
374 eleq1 2539 . . . . . . . . . 10  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
s  e.  ( A [,] B )  <->  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) ) )
375374anbi2d 703 . . . . . . . . 9  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
( ph  /\  s  e.  ( A [,] B
) )  <->  ( ph  /\  ( S `  (
j  +  1 ) )  e.  ( A [,] B ) ) ) )
376 neeq1 2748 . . . . . . . . 9  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
s  =/=  0  <->  ( S `  ( j  +  1 ) )  =/=  0 ) )
377375, 376imbi12d 320 . . . . . . . 8  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
( ( ph  /\  s  e.  ( A [,] B ) )  -> 
s  =/=  0 )  <-> 
( ( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )  -> 
( S `  (
j  +  1 ) )  =/=  0 ) ) )
378377, 149vtoclg 3176 . . . . . . 7  |-  ( ( S `  ( j  +  1 ) )  e.  RR  ->  (
( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )  -> 
( S `  (
j  +  1 ) )  =/=  0 ) )
37998, 373, 378sylc 60 . . . . . 6  |-  ( ch 
->  ( S `  (
j  +  1 ) )  =/=  0 )
380177, 178, 3, 137, 182, 371, 372, 379, 150divlimc 31521 . . . . 5  |-  ( ch 
->  ( ( if ( ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) ) ,  L ,  ( F `
 ( X  +  ( S `  ( j  +  1 ) ) ) ) )  -  C )  /  ( S `  ( j  +  1 ) ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( F `  ( X  +  s
) )  -  C
)  /  s ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
381 eqid 2467 . . . . . 6  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
382153, 164mulcld 9628 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
383171neneqd 2669 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  ( 2  x.  ( sin `  ( s  / 
2 ) ) )  =  0 )
384 2re 10617 . . . . . . . . . . 11  |-  2  e.  RR
385384a1i 11 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  RR )
386 rehalfcl 10777 . . . . . . . . . . . . 13  |-  ( s  e.  RR  ->  (
s  /  2 )  e.  RR )
38721, 386syl 16 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  (
s  /  2 )  e.  RR )
388 resincl 13753 . . . . . . . . . . . 12  |-  ( ( s  /  2 )  e.  RR  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
389387, 388syl 16 . . . . . . . . . . 11  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
390389adantl 466 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
391385, 390remulcld 9636 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  RR )
392 elsncg 4056 . . . . . . . . 9  |-  ( ( 2  x.  ( sin `  ( s  /  2
) ) )  e.  RR  ->  ( (
2  x.  ( sin `  ( s  /  2
) ) )  e. 
{ 0 }  <->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =  0 ) )
393391, 392syl 16 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  { 0 }  <-> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  =  0 ) )
394383, 393mtbird 301 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  ( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  { 0 } )
395382, 394eldifd 3492 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  ( CC  \  {
0 } ) )
396 eqid 2467 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  2 )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  2 )
397 eqid 2467 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( sin `  ( s  /  2
) ) )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( sin `  (
s  /  2 ) ) )
398152a1i 11 . . . . . . . 8  |-  ( ch 
->  2  e.  CC )
399396, 368, 398, 369constlimc 31489 . . . . . . 7  |-  ( ch 
->  2  e.  (
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  2 ) lim CC  ( S `  ( j  +  1 ) ) ) )
400387ad2antrl 727 . . . . . . . 8  |-  ( ( ch  /\  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  /\  (
s  /  2 )  =/=  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  ->  ( s  / 
2 )  e.  RR )
401 sinf 13737 . . . . . . . . . . 11  |-  sin : CC
--> CC
402401a1i 11 . . . . . . . . . 10  |-  ( x  e.  RR  ->  sin : CC --> CC )
403132sseli 3505 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  CC )
404402, 403ffvelrnd 6033 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( sin `  x )  e.  CC )
405404adantl 466 . . . . . . . 8  |-  ( ( ch  /\  x  e.  RR )  ->  ( sin `  x )  e.  CC )
406 eqid 2467 . . . . . . . . 9  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( s  /  2 ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  / 
2 ) )
407 eldifsn 4158 . . . . . . . . . . 11  |-  ( 2  e.  ( CC  \  { 0 } )  <-> 
( 2  e.  CC  /\  2  =/=  0 ) )
408152, 157, 407mpbir2an 918 . . . . . . . . . 10  |-  2  e.  ( CC  \  {
0 } )
409408a1i 11 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  ( CC  \  {
0 } ) )
410157a1i 11 . . . . . . . . 9  |-  ( ch 
->  2  =/=  0
)
411178, 396, 406, 160, 409, 372, 399, 410, 158divlimc 31521 . . . . . . . 8  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  /  2 ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
412401a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  sin : CC --> CC )
413132a1i 11 . . . . . . . . . . . . . 14  |-  ( T. 
->  RR  C_  CC )
414412, 413feqresmpt 5928 . . . . . . . . . . . . 13  |-  ( T. 
->  ( sin  |`  RR )  =  ( x  e.  RR  |->  ( sin `  x
) ) )
415414trud 1388 . . . . . . . . . . . 12  |-  ( sin  |`  RR )  =  ( x  e.  RR  |->  ( sin `  x ) )
416415eqcomi 2480 . . . . . . . . . . 11  |-  ( x  e.  RR  |->  ( sin `  x ) )  =  ( sin  |`  RR )
417 resincncf 31536 . . . . . . . . . . 11  |-  ( sin  |`  RR )  e.  ( RR -cn-> RR )
418416, 417eqeltri 2551 . . . . . . . . . 10  |-  ( x  e.  RR  |->  ( sin `  x ) )  e.  ( RR -cn-> RR )
419418a1i 11 . . . . . . . . 9  |-  ( ch 
->  ( x  e.  RR  |->  ( sin `  x ) )  e.  ( RR
-cn-> RR ) )
42098rehalfcld 10797 . . . . . . . . 9  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  RR )
421 fveq2 5872 . . . . . . . . 9  |-  ( x  =  ( ( S `
 ( j  +  1 ) )  / 
2 )  ->  ( sin `  x )  =  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) ) )
422419, 420, 421cnmptlimc 22162 . . . . . . . 8  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  ( ( x  e.  RR  |->  ( sin `  x ) ) lim CC  ( ( S `  ( j  +  1 ) )  /  2 ) ) )
423 fveq2 5872 . . . . . . . 8  |-  ( x  =  ( s  / 
2 )  ->  ( sin `  x )  =  ( sin `  (
s  /  2 ) ) )
424 fveq2 5872 . . . . . . . . 9  |-  ( ( s  /  2 )  =  ( ( S `
 ( j  +  1 ) )  / 
2 )  ->  ( sin `  ( s  / 
2 ) )  =  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) ) )
425424ad2antll 728 . . . . . . . 8  |-  ( ( ch  /\  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  /\  (
s  /  2 )  =  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  ->  ( sin `  (
s  /  2 ) )  =  ( sin `  ( ( S `  ( j  +  1 ) )  /  2
) ) )
426400, 405, 411, 422, 423, 425limcco 22165 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( sin `  ( s  /  2 ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
427396, 397, 381, 153, 164, 399, 426mullimc 31481 . . . . . 6  |-  ( ch 
->  ( 2  x.  ( sin `  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  e.  ( ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) ) )
428369halfcld 10795 . . . . . . . 8  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  CC )
429428sincld 13743 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  CC )
430166, 113sseldd 3510 . . . . . . . 8  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( -u pi [,] pi ) )
431 fourierdlem44 31774 . . . . . . . 8  |-  ( ( ( S `  (
j  +  1 ) )  e.  ( -u pi [,] pi )  /\  ( S `  ( j  +  1 ) )  =/=  0 )  -> 
( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  =/=  0 )
432430, 379, 431syl2anc 661 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  =/=  0 )
433398, 429, 410, 432mulne0d 10213 . . . . . 6  |-  ( ch 
->  ( 2  x.  ( sin `  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  =/=  0 )
434178, 381, 4, 160, 395, 372, 427, 433, 173divlimc 31521 . . . . 5  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  (
2  x.  ( sin `  ( ( S `  ( j  +  1 ) )  /  2
) ) ) )  e.  ( ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) lim
CC  ( S `  ( j  +  1 ) ) ) )
4353, 4, 5, 151, 176, 380, 434mullimc 31481 . . . 4  |-  ( ch 
->  ( ( ( if ( ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) ,  L ,  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) ) )  -  C )  /  ( S `  ( j  +  1 ) ) )  x.  ( ( S `  ( j  +  1 ) )  /  (
2  x.  ( sin `  ( (