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

Theorem fourierdlem76 32207
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 . . 3  |-  ( ch  <->  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
2 eqid 2454 . . . . 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 ) )
3 eqid 2454 . . . . 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 ) ) ) ) )
4 eqid 2454 . . . . 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 ) ) ) ) ) )
5 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  ph )
61, 5sylbi 195 . . . . . . . . . 10  |-  ( ch 
->  ph )
76adantr 463 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ph )
8 ioossicc 11613 . . . . . . . . . 10  |-  ( A (,) B )  C_  ( A [,] B )
9 fourierdlem76.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR )
109rexrd 9632 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR* )
116, 10syl 16 . . . . . . . . . . . 12  |-  ( ch 
->  A  e.  RR* )
1211adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  e.  RR* )
13 fourierdlem76.b . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  RR )
1413rexrd 9632 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  RR* )
156, 14syl 16 . . . . . . . . . . . 12  |-  ( ch 
->  B  e.  RR* )
1615adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  B  e.  RR* )
17 elioore 11562 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  s  e.  RR )
1817adantl 464 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  RR )
196, 9syl 16 . . . . . . . . . . . . 13  |-  ( ch 
->  A  e.  RR )
2019adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  e.  RR )
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19  |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
22 prfi 7787 . . . . . . . . . . . . . . . . . . . . 21  |-  { A ,  B }  e.  Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { A ,  B }  e.  Fin )
24 fzfid 12068 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
2625rnmptfi 31690 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
27 infi 7736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
2824, 26, 273syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
29 unfi 7779 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { A ,  B }  e.  Fin  /\  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )  -> 
( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
3023, 28, 29syl2anc 659 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
3121, 30syl5eqel 2546 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  e.  Fin )
32 prssg 4171 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
339, 13, 32syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
349, 13, 33mpbi2and 919 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { A ,  B }  C_  RR )
35 inss2 3705 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A (,) B )
36 ioossre 11589 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A (,) B )  C_  RR
3735, 36sstri 3498 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  RR
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  RR )
3934, 38unssd 3666 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  RR )
4021, 39syl5eqss 3533 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  C_  RR )
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18  |-  N  =  ( ( # `  T
)  -  1 )
4331, 40, 41, 42fourierdlem36 32167 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
446, 43syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  T
) )
45 isof1o 6196 . . . . . . . . . . . . . . . 16  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  ->  S : ( 0 ... N ) -1-1-onto-> T )
46 f1of 5798 . . . . . . . . . . . . . . . 16  |-  ( S : ( 0 ... N ) -1-1-onto-> T  ->  S :
( 0 ... N
) --> T )
4744, 45, 463syl 20 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( 0 ... N ) --> T )
486, 40syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  T  C_  RR )
4947, 48fssd 5722 . . . . . . . . . . . . . 14  |-  ( ch 
->  S : ( 0 ... N ) --> RR )
5049adantr 463 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  S : ( 0 ... N ) --> RR )
51 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 ) )
521, 51sylbi 195 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  (
0..^ N ) )
53 elfzofz 11819 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
5452, 53syl 16 . . . . . . . . . . . . . 14  |-  ( ch 
->  j  e.  (
0 ... N ) )
5554adantr 463 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  j  e.  ( 0 ... N
) )
5650, 55ffvelrnd 6008 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  e.  RR )
5743, 45, 463syl 20 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  S : ( 0 ... N ) --> T )
58 frn 5719 . . . . . . . . . . . . . . . . . 18  |-  ( S : ( 0 ... N ) --> T  ->  ran  S  C_  T )
5957, 58syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  S  C_  T
)
609leidd 10115 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  <_  A )
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  <  B )
629, 13, 61ltled 9722 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  <_  B )
639, 13, 9, 60, 62eliccd 31780 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  ( A [,] B ) )
6413leidd 10115 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  <_  B )
659, 13, 13, 62, 64eliccd 31780 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  ( A [,] B ) )
66 prssg 4171 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  ( A [,] B
)  /\  B  e.  ( A [,] B ) )  <->  { A ,  B }  C_  ( A [,] B ) ) )
679, 13, 66syl2anc 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( A  e.  ( A [,] B
)  /\  B  e.  ( A [,] B ) )  <->  { A ,  B }  C_  ( A [,] B ) ) )
6863, 65, 67mpbi2and 919 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { A ,  B }  C_  ( A [,] B ) )
6935, 8sstri 3498 . . . . . . . . . . . . . . . . . . . 20  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A [,] B )
7069a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  ( A [,] B ) )
7168, 70unssd 3666 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  ( A [,] B ) )
7221, 71syl5eqss 3533 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  C_  ( A [,] B ) )
7359, 72sstrd 3499 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  S  C_  ( A [,] B ) )
746, 73syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ran  S  C_  ( A [,] B ) )
75 ffun 5715 . . . . . . . . . . . . . . . . 17  |-  ( S : ( 0 ... N ) --> RR  ->  Fun 
S )
7649, 75syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  Fun  S )
77 fdm 5717 . . . . . . . . . . . . . . . . . . 19  |-  ( S : ( 0 ... N ) --> RR  ->  dom 
S  =  ( 0 ... N ) )
7849, 77syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  dom  S  =  ( 0 ... N ) )
7978eqcomd 2462 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( 0 ... N
)  =  dom  S
)
8054, 79eleqtrd 2544 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  j  e.  dom  S )
81 fvelrn 6000 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  S  /\  j  e.  dom  S )  -> 
( S `  j
)  e.  ran  S
)
8276, 80, 81syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  j
)  e.  ran  S
)
8374, 82sseldd 3490 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  ( A [,] B ) )
84 iccgelb 11584 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( S `
 j )  e.  ( A [,] B
) )  ->  A  <_  ( S `  j
) )
8511, 15, 83, 84syl3anc 1226 . . . . . . . . . . . . 13  |-  ( ch 
->  A  <_  ( S `
 j ) )
8685adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  <_  ( S `  j
) )
8756rexrd 9632 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  e.  RR* )
88 fzofzp1 11890 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
8952, 88syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( j  +  1 )  e.  ( 0 ... N ) )
9049, 89ffvelrnd 6008 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR )
9190rexrd 9632 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR* )
9291adantr 463 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  e.  RR* )
93 simpr 459 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
94 ioogtlb 31770 . . . . . . . . . . . . 13  |-  ( ( ( S `  j
)  e.  RR*  /\  ( S `  ( j  +  1 ) )  e.  RR*  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  <  s )
9587, 92, 93, 94syl3anc 1226 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  <  s )
9620, 56, 18, 86, 95lelttrd 9729 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  <  s )
9790adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
986, 13syl 16 . . . . . . . . . . . . 13  |-  ( ch 
->  B  e.  RR )
9998adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  B  e.  RR )
100 iooltub 31790 . . . . . . . . . . . . 13  |-  ( ( ( S `  j
)  e.  RR*  /\  ( S `  ( j  +  1 ) )  e.  RR*  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  ( S `  (
j  +  1 ) ) )
10187, 92, 93, 100syl3anc 1226 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  ( S `  (
j  +  1 ) ) )
10289, 79eleqtrd 2544 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( j  +  1 )  e.  dom  S
)
103 fvelrn 6000 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  S  /\  (
j  +  1 )  e.  dom  S )  ->  ( S `  ( j  +  1 ) )  e.  ran  S )
10476, 102, 103syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ran  S
)
10574, 104sseldd 3490 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( A [,] B ) )
106 iccleub 11583 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( S `
 ( j  +  1 ) )  e.  ( A [,] B
) )  ->  ( S `  ( j  +  1 ) )  <_  B )
10711, 15, 105, 106syl3anc 1226 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  (
j  +  1 ) )  <_  B )
108107adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  <_  B )
10918, 97, 99, 101, 108ltletrd 9731 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  B )
11012, 16, 18, 96, 109eliood 31773 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( A (,) B
) )
1118, 110sseldi 3487 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( A [,] B
) )
112 fourierdlem76.f . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> RR )
113112adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  F : RR
--> RR )
114 fourierdlem76.xre . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  RR )
115114adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  X  e.  RR )
1169, 13iccssred 31781 . . . . . . . . . . . 12  |-  ( ph  ->  ( A [,] B
)  C_  RR )
117116sselda 3489 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  RR )
118115, 117readdcld 9612 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( X  +  s )  e.  RR )
119113, 118ffvelrnd 6008 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
1207, 111, 119syl2anc 659 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
121120recnd 9611 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
122 fourierdlem76.c . . . . . . . . . 10  |-  ( ph  ->  C  e.  RR )
123122recnd 9611 . . . . . . . . 9  |-  ( ph  ->  C  e.  CC )
1246, 123syl 16 . . . . . . . 8  |-  ( ch 
->  C  e.  CC )
125124adantr 463 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  C  e.  CC )
126121, 125subcld 9922 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( F `  ( X  +  s )
)  -  C )  e.  CC )
127 ioossre 11589 . . . . . . . . 9  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR
128127a1i 11 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR )
129128sselda 3489 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  RR )
130129recnd 9611 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  CC )
131 nne 2655 . . . . . . . . . . . 12  |-  ( -.  s  =/=  0  <->  s  =  0 )
132131biimpi 194 . . . . . . . . . . 11  |-  ( -.  s  =/=  0  -> 
s  =  0 )
133132eqcomd 2462 . . . . . . . . . 10  |-  ( -.  s  =/=  0  -> 
0  =  s )
134133adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
0  =  s )
135 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  ( A [,] B ) )
136135adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
s  e.  ( A [,] B ) )
137134, 136eqeltrd 2542 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
0  e.  ( A [,] B ) )
138 fourierdlem76.n0 . . . . . . . . 9  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
139138ad2antrr 723 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  ->  -.  0  e.  ( A [,] B ) )
140137, 139condan 792 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  =/=  0 )
1417, 111, 140syl2anc 659 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  =/=  0 )
142126, 130, 141divcld 10316 . . . . 5  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( ( F `  ( X  +  s
) )  -  C
)  /  s )  e.  CC )
143 2cnd 10604 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  CC )
144130halfcld 10779 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  2 )  e.  CC )
145144sincld 13950 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
146143, 145mulcld 9605 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
14717recnd 9611 . . . . . . . . . 10  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  s  e.  CC )
148147adantl 464 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  CC )
149148halfcld 10779 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  2 )  e.  CC )
150149sincld 13950 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
151 2ne0 10624 . . . . . . . 8  |-  2  =/=  0
152151a1i 11 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  =/=  0 )
153 fourierdlem76.ab . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
1546, 153syl 16 . . . . . . . . . 10  |-  ( ch 
->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
155154adantr 463 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )
156155, 111sseldd 3490 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( -u pi [,] pi ) )
157 fourierdlem44 32175 . . . . . . . 8  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
158156, 141, 157syl2anc 659 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  =/=  0 )
159143, 150, 152, 158mulne0d 10197 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =/=  0 )
160130, 146, 159divcld 10316 . . . . 5  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  CC )
161 eqid 2454 . . . . . 6  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( F `  ( X  +  s ) )  -  C ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( F `
 ( X  +  s ) )  -  C ) )
162 eqid 2454 . . . . . 6  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  s )
163141neneqd 2656 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  s  =  0 )
164 elsn 4030 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
165163, 164sylnibr 303 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
166130, 165eldifd 3472 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
167 eqid 2454 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
168 eqid 2454 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  C )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  C )
169 elfzofz 11819 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
170169adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
171 pire 23020 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  e.  RR
172171renegcli 9871 . . . . . . . . . . . . . . . . . . . 20  |-  -u pi  e.  RR
173172a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
-u pi  e.  RR )
174173, 114readdcld 9612 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
175171a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  pi  e.  RR )
176175, 114readdcld 9612 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
177174, 176iccssred 31781 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
178177adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  C_  RR )
179 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 ) ) ) } )
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  NN )
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  V  e.  ( P `
 M ) )
182179, 180, 181fourierdlem15 32146 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
183182adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
184183, 170ffvelrnd 6008 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
185178, 184sseldd 3490 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
186114adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
187185, 186resubcld 9983 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
18825fvmpt2 5939 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
189170, 187, 188syl2anc 659 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
190189, 187eqeltrd 2542 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
191190adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
192191adantr 463 . . . . . . . . . 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 )
1931, 192sylbi 195 . . . . . . . . 9  |-  ( ch 
->  ( Q `  i
)  e.  RR )
194 fveq2 5848 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
195194oveq1d 6285 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
196195cbvmptv 4530 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
19725, 196eqtri 2483 . . . . . . . . . . . . . . 15  |-  Q  =  ( j  e.  ( 0 ... M ) 
|->  ( ( V `  j )  -  X
) )
198197a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q  =  ( j  e.  ( 0 ... M )  |->  ( ( V `  j
)  -  X ) ) )
199 fveq2 5848 . . . . . . . . . . . . . . . 16  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
200199oveq1d 6285 . . . . . . . . . . . . . . 15  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
201200adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
202 fzofzp1 11890 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
203202adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
204183, 203ffvelrnd 6008 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
205178, 204sseldd 3490 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
206205, 186resubcld 9983 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
207198, 201, 203, 206fvmptd 5936 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
208207, 206eqeltrd 2542 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
209208adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
210209adantr 463 . . . . . . . . . 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 )
2111, 210sylbi 195 . . . . . . . . 9  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
212179fourierdlem2 32133 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) ) )
213180, 212syl 16 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) ) )
214181, 213mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) ) )
215214simprrd 756 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
216215r19.21bi 2823 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
217185, 205, 186, 216ltsub1dd 10160 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  <  (
( V `  (
i  +  1 ) )  -  X ) )
218217, 189, 2073brtr4d 4469 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
219218adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
220219adantr 463 . . . . . . . . . 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 ) ) )
2211, 220sylbi 195 . . . . . . . . 9  |-  ( ch 
->  ( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )
2221biimpi 194 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
223222simplrd 31669 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  i  e.  (
0..^ M ) )
2246, 223, 185syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  e.  RR )
225224rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  i
)  e.  RR* )
226225adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
2276, 223, 205syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR )
228227rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR* )
229228adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
2306, 114syl 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  X  e.  RR )
231230adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
232 elioore 11562 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
233232adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
234231, 233readdcld 9612 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
2356, 223, 189syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  =  ( ( V `  i )  -  X ) )
236235oveq2d 6286 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  i ) )  =  ( X  +  ( ( V `
 i )  -  X ) ) )
237230recnd 9611 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  X  e.  CC )
238224recnd 9611 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( V `  i
)  e.  CC )
239237, 238pncan3d 9925 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( ( V `  i
)  -  X ) )  =  ( V `
 i ) )
240236, 239eqtr2d 2496 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  =  ( X  +  ( Q `  i ) ) )
241240adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
242193adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
243193rexrd 9632 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
244243adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
245211rexrd 9632 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
246245adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
247 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
248 ioogtlb 31770 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
249244, 246, 247, 248syl3anc 1226 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
250242, 233, 231, 249ltadd2dd 9730 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
251241, 250eqbrtrd 4459 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
252211adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
253 iooltub 31790 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
254244, 246, 247, 253syl3anc 1226 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
255233, 252, 231, 254ltadd2dd 9730 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
2566, 223, 207syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) )
257256oveq2d 6286 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
258227recnd 9611 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  CC )
259237, 258pncan3d 9925 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( ( V `  (
i  +  1 ) )  -  X ) )  =  ( V `
 ( i  +  1 ) ) )
260257, 259eqtrd 2495 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
261260adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
262255, 261breqtrd 4463 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
263226, 229, 234, 251, 262eliood 31773 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
264 fvres 5862 . . . . . . . . . . . . 13  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
265263, 264syl 16 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
266265eqcomd 2462 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
) )
267266mpteq2dva 4525 . . . . . . . . . 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 ) ) ) )
268 ioosscn 31769 . . . . . . . . . . . 12  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  CC
269268a1i 11 . . . . . . . . . . 11  |-  ( ch 
->  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  CC )
270 fourierdlem76.fcn . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
2716, 223, 270syl2anc 659 . . . . . . . . . . 11  |-  ( ch 
->  ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) )
-cn-> CC ) )
272 ioosscn 31769 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
273272a1i 11 . . . . . . . . . . 11  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC )
274269, 271, 273, 237, 263fourierdlem23 32154 . . . . . . . . . 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 ) )
275267, 274eqeltrd 2542 . . . . . . . . 9  |-  ( ch 
->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
2766, 112syl 16 . . . . . . . . . 10  |-  ( ch 
->  F : RR --> RR )
277 ioossre 11589 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
278277a1i 11 . . . . . . . . . 10  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR )
279 eqid 2454 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
280 ioossre 11589 . . . . . . . . . . 11  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
281280a1i 11 . . . . . . . . . 10  |-  ( ch 
->  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR )
282233, 254ltned 9710 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  (
i  +  1 ) ) )
283 fourierdlem76.l . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
2846, 223, 283syl2anc 659 . . . . . . . . . . 11  |-  ( ch 
->  L  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
285260eqcomd 2462 . . . . . . . . . . . 12  |-  ( ch 
->  ( V `  (
i  +  1 ) )  =  ( X  +  ( Q `  ( i  +  1 ) ) ) )
286285oveq2d 6286 . . . . . . . . . . 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 ) ) ) ) )
287284, 286eleqtrd 2544 . . . . . . . . . 10  |-  ( ch 
->  L  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
288211recnd 9611 . . . . . . . . . 10  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  CC )
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 32184 . . . . . . . . 9  |-  ( ch 
->  L  e.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
29049, 54ffvelrnd 6008 . . . . . . . . 9  |-  ( ch 
->  ( S `  j
)  e.  RR )
291 elfzoelz 11804 . . . . . . . . . . . 12  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
292 zre 10864 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  j  e.  RR )
29352, 291, 2923syl 20 . . . . . . . . . . 11  |-  ( ch 
->  j  e.  RR )
294293ltp1d 10471 . . . . . . . . . 10  |-  ( ch 
->  j  <  ( j  +  1 ) )
295 isorel 6197 . . . . . . . . . . 11  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  T )  /\  ( j  e.  ( 0 ... N
)  /\  ( j  +  1 )  e.  ( 0 ... N
) ) )  -> 
( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
29644, 54, 89, 295syl12anc 1224 . . . . . . . . . 10  |-  ( ch 
->  ( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
297294, 296mpbid 210 . . . . . . . . 9  |-  ( ch 
->  ( S `  j
)  <  ( S `  ( j  +  1 ) ) )
2981simprbi 462 . . . . . . . . 9  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
299 eqid 2454 . . . . . . . . 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 ) ) ) )
300 eqid 2454 . . . . . . . . 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 ) ) } ) )
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 32164 . . . . . . . 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 ) ) ) )
302 eqidd 2455 . . . . . . . . . 10  |-  ( ( 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 ) ) ) )
303 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
s  =  ( S `
 ( j  +  1 ) ) )
304303oveq2d 6286 . . . . . . . . . . 11  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
( X  +  s )  =  ( X  +  ( S `  ( j  +  1 ) ) ) )
305304fveq2d 5852 . . . . . . . . . 10  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
( F `  ( X  +  s )
)  =  ( F `
 ( X  +  ( S `  ( j  +  1 ) ) ) ) )
306243adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  e.  RR* )
307245adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
30890adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  e.  RR )
309193, 211, 290, 90, 297, 298fourierdlem10 32141 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( Q `  i )  <_  ( S `  j )  /\  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) )
310309simpld 457 . . . . . . . . . . . . 13  |-  ( ch 
->  ( Q `  i
)  <_  ( S `  j ) )
311193, 290, 90, 310, 297lelttrd 9729 . . . . . . . . . . . 12  |-  ( ch 
->  ( Q `  i
)  <  ( S `  ( j  +  1 ) ) )
312311adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  <  ( S `  ( j  +  1 ) ) )
313211adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
314309simprd 461 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
315314adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
316 neqne 31677 . . . . . . . . . . . . . 14  |-  ( -.  ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) )  -> 
( S `  (
j  +  1 ) )  =/=  ( Q `
 ( i  +  1 ) ) )
317316necomd 2725 . . . . . . . . . . . . 13  |-  ( -.  ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) )  -> 
( Q `  (
i  +  1 ) )  =/=  ( S `
 ( j  +  1 ) ) )
318317adantl 464 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  =/=  ( S `
 ( j  +  1 ) ) )
319308, 313, 315, 318leneltd 31736 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  <  ( Q `
 ( i  +  1 ) ) )
320306, 307, 308, 312, 319eliood 31773 . . . . . . . . . 10  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
321230, 90readdcld 9612 . . . . . . . . . . . 12  |-  ( ch 
->  ( X  +  ( S `  ( j  +  1 ) ) )  e.  RR )
322276, 321ffvelrnd 6008 . . . . . . . . . . 11  |-  ( ch 
->  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) )  e.  RR )
323322adantr 463 . . . . . . . . . 10  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( F `  ( X  +  ( S `  ( j  +  1 ) ) ) )  e.  RR )
324302, 305, 320, 323fvmptd 5936 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) )
325324ifeq2da 3960 . . . . . . . 8  |-  ( 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 ) ) ) ) ) )
326298resmptd 5313 . . . . . . . . 9  |-  ( 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 ) ) ) )
327326oveq1d 6285 . . . . . . . 8  |-  ( 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 ) ) ) )
328301, 325, 3273eltr3d 2556 . . . . . . 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 ) ) ) )
329 ax-resscn 9538 . . . . . . . . 9  |-  RR  C_  CC
330128, 329syl6ss 3501 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  CC )
33190recnd 9611 . . . . . . . 8  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  CC )
332168, 330, 124, 331constlimc 31872 . . . . . . 7  |-  ( ch 
->  C  e.  (
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  C ) lim CC  ( S `  ( j  +  1 ) ) ) )
333167, 168, 161, 121, 125, 328, 332sublimc 31900 . . . . . 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 ) ) ) )
334330, 162, 331idlimc 31874 . . . . . 6  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  s ) lim CC  ( S `
 ( j  +  1 ) ) ) )
3356, 105jca 530 . . . . . . 7  |-  ( ch 
->  ( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) ) )
336 eleq1 2526 . . . . . . . . . 10  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
s  e.  ( A [,] B )  <->  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) ) )
337336anbi2d 701 . . . . . . . . 9  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
( ph  /\  s  e.  ( A [,] B
) )  <->  ( ph  /\  ( S `  (
j  +  1 ) )  e.  ( A [,] B ) ) ) )
338 neeq1 2735 . . . . . . . . 9  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
s  =/=  0  <->  ( S `  ( j  +  1 ) )  =/=  0 ) )
339337, 338imbi12d 318 . . . . . . . 8  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
( ( ph  /\  s  e.  ( A [,] B ) )  -> 
s  =/=  0 )  <-> 
( ( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )  -> 
( S `  (
j  +  1 ) )  =/=  0 ) ) )
340339, 140vtoclg 3164 . . . . . . 7  |-  ( ( S `  ( j  +  1 ) )  e.  RR  ->  (
( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )  -> 
( S `  (
j  +  1 ) )  =/=  0 ) )
34190, 335, 340sylc 60 . . . . . 6  |-  ( ch 
->  ( S `  (
j  +  1 ) )  =/=  0 )
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 31904 . . . . 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 ) ) ) )
343 eqid 2454 . . . . . 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 ) ) ) )
344143, 150mulcld 9605 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
345159neneqd 2656 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  ( 2  x.  ( sin `  ( s  / 
2 ) ) )  =  0 )
346 2re 10601 . . . . . . . . . . 11  |-  2  e.  RR
347346a1i 11 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  RR )
34817rehalfcld 10781 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  (
s  /  2 )  e.  RR )
349348resincld 13963 . . . . . . . . . . 11  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
350349adantl 464 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
351347, 350remulcld 9613 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  RR )
352 elsncg 4039 . . . . . . . . 9  |-  ( ( 2  x.  ( sin `  ( s  /  2
) ) )  e.  RR  ->  ( (
2  x.  ( sin `  ( s  /  2
) ) )  e. 
{ 0 }  <->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =  0 ) )
353351, 352syl 16 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  { 0 }  <-> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  =  0 ) )
354345, 353mtbird 299 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  ( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  { 0 } )
355344, 354eldifd 3472 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  ( CC  \  {
0 } ) )
356 eqid 2454 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  2 )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  2 )
357 eqid 2454 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( sin `  ( s  /  2
) ) )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( sin `  (
s  /  2 ) ) )
358 2cnd 10604 . . . . . . . 8  |-  ( ch 
->  2  e.  CC )
359356, 330, 358, 331constlimc 31872 . . . . . . 7  |-  ( ch 
->  2  e.  (
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  2 ) lim CC  ( S `  ( j  +  1 ) ) ) )
360348ad2antrl 725 . . . . . . . 8  |-  ( ( ch  /\  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  /\  (
s  /  2 )  =/=  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  ->  ( s  / 
2 )  e.  RR )
361 recn 9571 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  CC )
362361sincld 13950 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( sin `  x )  e.  CC )
363362adantl 464 . . . . . . . 8  |-  ( ( ch  /\  x  e.  RR )  ->  ( sin `  x )  e.  CC )
364 eqid 2454 . . . . . . . . 9  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( s  /  2 ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  / 
2 ) )
365 2cn 10602 . . . . . . . . . . 11  |-  2  e.  CC
366 eldifsn 4141 . . . . . . . . . . 11  |-  ( 2  e.  ( CC  \  { 0 } )  <-> 
( 2  e.  CC  /\  2  =/=  0 ) )
367365, 151, 366mpbir2an 918 . . . . . . . . . 10  |-  2  e.  ( CC  \  {
0 } )
368367a1i 11 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  ( CC  \  {
0 } ) )
369151a1i 11 . . . . . . . . 9  |-  ( ch 
->  2  =/=  0
)
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 31904 . . . . . . . 8  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  /  2 ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
371 sinf 13944 . . . . . . . . . . . . . 14  |-  sin : CC
--> CC
372371a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  sin : CC --> CC )
373329a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  RR  C_  CC )
374372, 373feqresmpt 5902 . . . . . . . . . . . 12  |-  ( T. 
->  ( sin  |`  RR )  =  ( x  e.  RR  |->  ( sin `  x
) ) )
375374trud 1407 . . . . . . . . . . 11  |-  ( sin  |`  RR )  =  ( x  e.  RR  |->  ( sin `  x ) )
376 resincncf 31919 . . . . . . . . . . 11  |-  ( sin  |`  RR )  e.  ( RR -cn-> RR )
377375, 376eqeltrri 2539 . . . . . . . . . 10  |-  ( x  e.  RR  |->  ( sin `  x ) )  e.  ( RR -cn-> RR )
378377a1i 11 . . . . . . . . 9  |-  ( ch 
->  ( x  e.  RR  |->  ( sin `  x ) )  e.  ( RR
-cn-> RR ) )
37990rehalfcld 10781 . . . . . . . . 9  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  RR )
380 fveq2 5848 . . . . . . . . 9  |-  ( x  =  ( ( S `
 ( j  +  1 ) )  / 
2 )  ->  ( sin `  x )  =  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) ) )
381378, 379, 380cnmptlimc 22463 . . . . . . . 8  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  ( ( x  e.  RR  |->  ( sin `  x ) ) lim CC  ( ( S `  ( j  +  1 ) )  /  2 ) ) )
382 fveq2 5848 . . . . . . . 8  |-  ( x  =  ( s  / 
2 )  ->  ( sin `  x )  =  ( sin `  (
s  /  2 ) ) )
383 fveq2 5848 . . . . . . . . 9  |-  ( ( s  /  2 )  =  ( ( S `
 ( j  +  1 ) )  / 
2 )  ->  ( sin `  ( s  / 
2 ) )  =  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) ) )
384383ad2antll 726 . . . . . . . 8  |-  ( ( ch  /\  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  /\  (
s  /  2 )  =  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  ->  ( sin `  (
s  /  2 ) )  =  ( sin `  ( ( S `  ( j  +  1 ) )  /  2
) ) )
385360, 363, 370, 381, 382, 384limcco 22466 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( sin `  ( s  /  2 ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
386356, 357, 343, 143, 150, 359, 385mullimc 31864 . . . . . 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 ) ) ) )
387331halfcld 10779 . . . . . . . 8  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  CC )
388387sincld 13950 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  CC )
389154, 105sseldd 3490 . . . . . . . 8  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( -u pi [,] pi ) )
390 fourierdlem44 32175 . . . . . . . 8  |-  ( ( ( S `  (
j  +  1 ) )  e.  ( -u pi [,] pi )  /\  ( S `  ( j  +  1 ) )  =/=  0 )  -> 
( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  =/=  0 )
391389, 341, 390syl2anc 659 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  =/=  0 )
392358, 388, 369, 391mulne0d 10197 . . . . . 6  |-  ( ch 
->  ( 2  x.  ( sin `  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  =/=  0 )
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 31904 . . . . 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 ) ) ) )
3942, 3, 4, 142, 160, 342, 393mullimc 31864 . . . 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 `  ( ( S `  ( j  +  1 ) )  /  2
) ) ) ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  C )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
395 fourierdlem76.d . . . . 5  |-  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
) ) ) ) )
396395a1i 11 . . . 4  |-  ( ch 
->  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 ) ) ) ) ) )
397 fourierdlem76.o . . . . . . 7  |-  O  =  ( s  e.  ( A [,] B ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  C )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
398397reseq1i 5258 . . . . . 6  |-  ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  =  ( ( s  e.  ( A [,] B ) 
|->  ( ( ( ( F `  ( X  +  s ) )  -  C )  / 
s )  x.  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )  |`  ( ( S `  j ) (,) ( S `  (
j  +  1 ) ) ) )
399 ioossicc 11613 . . . . . . . 8  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )
400 iccss 11595 . . . . . . . . 9  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( A  <_ 
( S `  j
)  /\  ( S `  ( j  +  1 ) )  <_  B
) )  ->  (
( S `  j
) [,] ( S `
 ( j  +  1 ) ) ) 
C_  ( A [,] B ) )
40119, 98, 85, 107, 400syl22anc 1227 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )  C_  ( A [,] B ) )
402399, 401syl5ss 3500 . . . . . . 7  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( A [,] B ) )
403402resmptd 5313 . . . . . 6  |-  ( ch 
->  ( ( s  e.  ( A [,] B
)  |->  ( ( ( ( F `  ( X  +  s )
)  -  C )  /  s )  x.  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) ) )  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( ( F `  ( X  +  s
) )  -  C
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
404398, 403syl5eq 2507 . . . . 5  |-  ( ch 
->  ( O  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) )  =  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( ( ( ( F `  ( X  +  s
) )  -  C
)  /  s )  x.  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) ) )
405404oveq1d 6285 . . . 4  |-  ( ch 
->  ( ( O  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) lim CC  ( S `  ( j  +  1 ) ) )  =  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( ( ( ( F `
 ( X  +  s ) )  -  C )  /  s
)  x.  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
406394, 396, 4053eltr4d 2557 . . 3  |-  ( ch 
->  D  e.  (
( O  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
4071, 406sylbir 213 . 2  |-  ( ( ( ( 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 ) ) ) )
408242, 249gtned 9709 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  =/=  ( Q `  i
) )
409 fourierdlem76.r . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
4106, 223, 409syl2anc 659 . . . . . . . . . . 11  |-  ( ch 
->  R  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
411240oveq2d 6286 . . . . . . . . . . 11  |-  ( ch 
->  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  i )
)  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  i )
) ) )
412410, 411eleqtrd 2544 . . . . . . . . . 10  |-  ( ch 
->  R  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  i ) ) ) )
413193recnd 9611 . . . . . . . . . 10  |-  ( ch 
->  ( Q `  i
)  e.  CC )
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 32184 . . . . . . . . 9  |-  ( ch 
->  R  e.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  i )
) )
415 eqid 2454 . . . . . . . . 9  |-  if ( ( S `  j
)  =  ( Q `
 i ) ,  R ,  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) `  ( S `
 j ) ) )  =  if ( ( S `  j
)  =  ( Q `
 i ) ,  R ,  ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) `  ( S `
 j ) ) )
416 eqid 2454 . . . . . . . . 9  |-  ( (
TopOpen ` fld )t  ( ( Q `  i ) [,) ( Q `  ( i  +  1 ) ) ) )  =  ( ( TopOpen ` fld )t  ( ( Q `
 i ) [,) ( Q `  (
i  +  1 ) ) ) )
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 32163 . . . . . . . 8  |-  ( ch 
->  if ( ( S `
 j )  =  ( Q `  i
) ,  R , 
( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) ) `  ( S `  j ) ) )  e.  ( ( ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )  |`  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) ) lim CC  ( S `  j )
) )
418 eqidd 2455 . . . . . . . . . 10  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s ) ) ) )
419 oveq2 6278 . . . . . . . . . . . 12  |-  ( s  =  ( S `  j )  ->  ( X  +  s )  =  ( X  +  ( S `  j ) ) )
420419fveq2d 5852 . . . . . . . . . . 11  |-  ( s  =  ( S `  j )  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  ( S `  j )
) ) )
421420adantl 464 . . . . . . . . . 10  |-  ( ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  /\  s  =  ( S `  j ) )  -> 
( F `  ( X  +  s )
)  =  ( F `
 ( X  +  ( S `  j ) ) ) )
422243adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( Q `  i
)  e.  RR* )
423245adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
424290adantr 463 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( S `  j
)  e.  RR )
425193adantr 463 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.