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

Theorem fourierdlem76 37863
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 2422 . . . . 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 2422 . . . . 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 2422 . . . . 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 766 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  ->  ph )
61, 5sylbi 198 . . . . . . . . . 10  |-  ( ch 
->  ph )
76adantr 466 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ph )
8 ioossicc 11720 . . . . . . . . . 10  |-  ( A (,) B )  C_  ( A [,] B )
9 fourierdlem76.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR )
109rexrd 9690 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR* )
116, 10syl 17 . . . . . . . . . . . 12  |-  ( ch 
->  A  e.  RR* )
1211adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  e.  RR* )
13 fourierdlem76.b . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  RR )
1413rexrd 9690 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  RR* )
156, 14syl 17 . . . . . . . . . . . 12  |-  ( ch 
->  B  e.  RR* )
1615adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  B  e.  RR* )
17 elioore 11666 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  s  e.  RR )
1817adantl 467 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  RR )
196, 9syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  A  e.  RR )
2019adantr 466 . . . . . . . . . . . 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 7848 . . . . . . . . . . . . . . . . . . . . 21  |-  { A ,  B }  e.  Fin
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { A ,  B }  e.  Fin )
24 fzfid 12185 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
2625rnmptfi 37281 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
27 infi 7797 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
29 unfi 7840 . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
3121, 30syl5eqel 2514 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  e.  Fin )
32 prssg 4152 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
339, 13, 32syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
349, 13, 33mpbi2and 929 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { A ,  B }  C_  RR )
35 inss2 3683 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A (,) B )
36 ioossre 11696 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A (,) B )  C_  RR
3735, 36sstri 3473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  RR
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  RR )
3934, 38unssd 3642 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  RR )
4021, 39syl5eqss 3508 . . . . . . . . . . . . . . . . . 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 37823 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
446, 43syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  T
) )
45 isof1o 6227 . . . . . . . . . . . . . . . 16  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  ->  S : ( 0 ... N ) -1-1-onto-> T )
46 f1of 5827 . . . . . . . . . . . . . . . 16  |-  ( S : ( 0 ... N ) -1-1-onto-> T  ->  S :
( 0 ... N
) --> T )
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( 0 ... N ) --> T )
486, 40syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  T  C_  RR )
4947, 48fssd 5751 . . . . . . . . . . . . . 14  |-  ( ch 
->  S : ( 0 ... N ) --> RR )
5049adantr 466 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  S : ( 0 ... N ) --> RR )
51 simpllr 767 . . . . . . . . . . . . . . . 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 198 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  (
0..^ N ) )
53 elfzofz 11935 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
5452, 53syl 17 . . . . . . . . . . . . . 14  |-  ( ch 
->  j  e.  (
0 ... N ) )
5554adantr 466 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  j  e.  ( 0 ... N
) )
5650, 55ffvelrnd 6034 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  e.  RR )
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  S : ( 0 ... N ) --> T )
58 frn 5748 . . . . . . . . . . . . . . . . . 18  |-  ( S : ( 0 ... N ) --> T  ->  ran  S  C_  T )
5957, 58syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  S  C_  T
)
609leidd 10180 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  <_  A )
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  <  B )
629, 13, 61ltled 9783 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  <_  B )
639, 13, 9, 60, 62eliccd 37429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  ( A [,] B ) )
6413leidd 10180 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  <_  B )
659, 13, 13, 62, 64eliccd 37429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  B  e.  ( A [,] B ) )
66 prssg 4152 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  ( A [,] B
)  /\  B  e.  ( A [,] B ) )  <->  { A ,  B }  C_  ( A [,] B ) ) )
679, 13, 66syl2anc 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( A  e.  ( A [,] B
)  /\  B  e.  ( A [,] B ) )  <->  { A ,  B }  C_  ( A [,] B ) ) )
6863, 65, 67mpbi2and 929 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { A ,  B }  C_  ( A [,] B ) )
6935, 8sstri 3473 . . . . . . . . . . . . . . . . . . . 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 3642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  ( A [,] B ) )
7221, 71syl5eqss 3508 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  C_  ( A [,] B ) )
7359, 72sstrd 3474 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  S  C_  ( A [,] B ) )
746, 73syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ran  S  C_  ( A [,] B ) )
75 ffun 5744 . . . . . . . . . . . . . . . . 17  |-  ( S : ( 0 ... N ) --> RR  ->  Fun 
S )
7649, 75syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  Fun  S )
77 fdm 5746 . . . . . . . . . . . . . . . . . . 19  |-  ( S : ( 0 ... N ) --> RR  ->  dom 
S  =  ( 0 ... N ) )
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  dom  S  =  ( 0 ... N ) )
7978eqcomd 2430 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( 0 ... N
)  =  dom  S
)
8054, 79eleqtrd 2512 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  j  e.  dom  S )
81 fvelrn 6026 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  S  /\  j  e.  dom  S )  -> 
( S `  j
)  e.  ran  S
)
8276, 80, 81syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  j
)  e.  ran  S
)
8374, 82sseldd 3465 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  ( A [,] B ) )
84 iccgelb 11691 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( S `
 j )  e.  ( A [,] B
) )  ->  A  <_  ( S `  j
) )
8511, 15, 83, 84syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ch 
->  A  <_  ( S `
 j ) )
8685adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  <_  ( S `  j
) )
8756rexrd 9690 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  e.  RR* )
88 fzofzp1 12007 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
8952, 88syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( j  +  1 )  e.  ( 0 ... N ) )
9049, 89ffvelrnd 6034 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR )
9190rexrd 9690 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  RR* )
9291adantr 466 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  e.  RR* )
93 simpr 462 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )
94 ioogtlb 37420 . . . . . . . . . . . . 13  |-  ( ( ( S `  j
)  e.  RR*  /\  ( S `  ( j  +  1 ) )  e.  RR*  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  <  s )
9587, 92, 93, 94syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  j )  <  s )
9620, 56, 18, 86, 95lelttrd 9793 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  A  <  s )
9790adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
986, 13syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  B  e.  RR )
9998adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  B  e.  RR )
100 iooltub 37438 . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  ( S `  (
j  +  1 ) ) )
10289, 79eleqtrd 2512 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( j  +  1 )  e.  dom  S
)
103 fvelrn 6026 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  S  /\  (
j  +  1 )  e.  dom  S )  ->  ( S `  ( j  +  1 ) )  e.  ran  S )
10476, 102, 103syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ran  S
)
10574, 104sseldd 3465 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( A [,] B ) )
106 iccleub 11690 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( S `
 ( j  +  1 ) )  e.  ( A [,] B
) )  ->  ( S `  ( j  +  1 ) )  <_  B )
10711, 15, 105, 106syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  (
j  +  1 ) )  <_  B )
108107adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( S `  ( j  +  1 ) )  <_  B )
10918, 97, 99, 101, 108ltletrd 9795 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  <  B )
11012, 16, 18, 96, 109eliood 37423 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( A (,) B
) )
1118, 110sseldi 3462 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( A [,] B
) )
112 fourierdlem76.f . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> RR )
113112adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  F : RR
--> RR )
114 fourierdlem76.xre . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  RR )
115114adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  X  e.  RR )
1169, 13iccssred 37430 . . . . . . . . . . . 12  |-  ( ph  ->  ( A [,] B
)  C_  RR )
117116sselda 3464 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  RR )
118115, 117readdcld 9670 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( X  +  s )  e.  RR )
119113, 118ffvelrnd 6034 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
1207, 111, 119syl2anc 665 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  RR )
121120recnd 9669 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  e.  CC )
122 fourierdlem76.c . . . . . . . . . 10  |-  ( ph  ->  C  e.  RR )
123122recnd 9669 . . . . . . . . 9  |-  ( ph  ->  C  e.  CC )
1246, 123syl 17 . . . . . . . 8  |-  ( ch 
->  C  e.  CC )
125124adantr 466 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  C  e.  CC )
126121, 125subcld 9986 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( F `  ( X  +  s )
)  -  C )  e.  CC )
127 ioossre 11696 . . . . . . . . 9  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR
128127a1i 11 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  RR )
129128sselda 3464 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  RR )
130129recnd 9669 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  CC )
131 nne 2624 . . . . . . . . . . . 12  |-  ( -.  s  =/=  0  <->  s  =  0 )
132131biimpi 197 . . . . . . . . . . 11  |-  ( -.  s  =/=  0  -> 
s  =  0 )
133132eqcomd 2430 . . . . . . . . . 10  |-  ( -.  s  =/=  0  -> 
0  =  s )
134133adantl 467 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
0  =  s )
135 simpr 462 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  e.  ( A [,] B ) )
136135adantr 466 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
s  e.  ( A [,] B ) )
137134, 136eqeltrd 2510 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  -> 
0  e.  ( A [,] B ) )
138 fourierdlem76.n0 . . . . . . . . 9  |-  ( ph  ->  -.  0  e.  ( A [,] B ) )
139138ad2antrr 730 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  ( A [,] B
) )  /\  -.  s  =/=  0 )  ->  -.  0  e.  ( A [,] B ) )
140137, 139condan 801 . . . . . . 7  |-  ( (
ph  /\  s  e.  ( A [,] B ) )  ->  s  =/=  0 )
1417, 111, 140syl2anc 665 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  =/=  0 )
142126, 130, 141divcld 10383 . . . . 5  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( ( F `  ( X  +  s
) )  -  C
)  /  s )  e.  CC )
143 2cnd 10682 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  CC )
144130halfcld 10857 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  2 )  e.  CC )
145144sincld 14169 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
146143, 145mulcld 9663 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
14717recnd 9669 . . . . . . . . . 10  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  s  e.  CC )
148147adantl 467 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  CC )
149148halfcld 10857 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  2 )  e.  CC )
150149sincld 14169 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  CC )
151 2ne0 10702 . . . . . . . 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 17 . . . . . . . . . 10  |-  ( ch 
->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
155154adantr 466 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( A [,] B )  C_  ( -u pi [,] pi ) )
156155, 111sseldd 3465 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( -u pi [,] pi ) )
157 fourierdlem44 37832 . . . . . . . 8  |-  ( ( s  e.  ( -u pi [,] pi )  /\  s  =/=  0 )  -> 
( sin `  (
s  /  2 ) )  =/=  0 )
158156, 141, 157syl2anc 665 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  =/=  0 )
159143, 150, 152, 158mulne0d 10264 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  =/=  0 )
160130, 146, 159divcld 10383 . . . . 5  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) )  e.  CC )
161 eqid 2422 . . . . . 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 2422 . . . . . 6  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  s )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  s )
163141neneqd 2625 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  s  =  0 )
164 elsn 4010 . . . . . . . 8  |-  ( s  e.  { 0 }  <-> 
s  =  0 )
165163, 164sylnibr 306 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  s  e.  { 0 } )
166130, 165eldifd 3447 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  s  e.  ( CC  \  {
0 } ) )
167 eqid 2422 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
168 eqid 2422 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  C )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  C )
169 elfzofz 11935 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
170169adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
171 pire 23397 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  e.  RR
172171renegcli 9935 . . . . . . . . . . . . . . . . . . . 20  |-  -u pi  e.  RR
173172a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
-u pi  e.  RR )
174173, 114readdcld 9670 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
175171a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  pi  e.  RR )
176175, 114readdcld 9670 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
177174, 176iccssred 37430 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
178177adantr 466 . . . . . . . . . . . . . . . 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 37801 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
183182adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
184183, 170ffvelrnd 6034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
185178, 184sseldd 3465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
186114adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  X  e.  RR )
187185, 186resubcld 10047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  e.  RR )
18825fvmpt2 5969 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
189170, 187, 188syl2anc 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
190189, 187eqeltrd 2510 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
191190adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
192191adantr 466 . . . . . . . . . 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 198 . . . . . . . . 9  |-  ( ch 
->  ( Q `  i
)  e.  RR )
194 fveq2 5877 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  ( V `  i )  =  ( V `  j ) )
195194oveq1d 6316 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
( V `  i
)  -  X )  =  ( ( V `
 j )  -  X ) )
196195cbvmptv 4513 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) )  =  ( j  e.  ( 0 ... M
)  |->  ( ( V `
 j )  -  X ) )
19725, 196eqtri 2451 . . . . . . . . . . . . . . 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 5877 . . . . . . . . . . . . . . . 16  |-  ( j  =  ( i  +  1 )  ->  ( V `  j )  =  ( V `  ( i  +  1 ) ) )
200199oveq1d 6316 . . . . . . . . . . . . . . 15  |-  ( j  =  ( i  +  1 )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
201200adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  j  =  ( i  +  1 ) )  ->  (
( V `  j
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
202 fzofzp1 12007 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
203202adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
204183, 203ffvelrnd 6034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
205178, 204sseldd 3465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
206205, 186resubcld 10047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )
207198, 201, 203, 206fvmptd 5966 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) )
208207, 206eqeltrd 2510 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
209208adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
210209adantr 466 . . . . . . . . . 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 198 . . . . . . . . 9  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
212179fourierdlem2 37788 . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
216215r19.21bi 2794 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
217185, 205, 186, 216ltsub1dd 10225 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( V `
 i )  -  X )  <  (
( V `  (
i  +  1 ) )  -  X ) )
218217, 189, 2073brtr4d 4451 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
219218adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
220219adantr 466 . . . . . . . . . 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 198 . . . . . . . . 9  |-  ( ch 
->  ( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )
2221biimpi 197 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
223222simplrd 761 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  i  e.  (
0..^ M ) )
2246, 223, 185syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  e.  RR )
225224rexrd 9690 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  i
)  e.  RR* )
226225adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  e.  RR* )
2276, 223, 205syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR )
228227rexrd 9690 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR* )
229228adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  ( i  +  1 ) )  e.  RR* )
2306, 114syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  X  e.  RR )
231230adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  X  e.  RR )
232 elioore 11666 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
233232adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
234231, 233readdcld 9670 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  RR )
2356, 223, 189syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  =  ( ( V `  i )  -  X ) )
236235oveq2d 6317 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  i ) )  =  ( X  +  ( ( V `
 i )  -  X ) ) )
237230recnd 9669 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  X  e.  CC )
238224recnd 9669 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( V `  i
)  e.  CC )
239237, 238pncan3d 9989 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( ( V `  i
)  -  X ) )  =  ( V `
 i ) )
240236, 239eqtr2d 2464 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  =  ( X  +  ( Q `  i ) ) )
241240adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  =  ( X  +  ( Q `  i ) ) )
242193adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR )
243193rexrd 9690 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
244243adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  e.  RR* )
245211rexrd 9690 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
246245adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR* )
247 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
248 ioogtlb 37420 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  i
)  e.  RR*  /\  ( Q `  ( i  +  1 ) )  e.  RR*  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
249244, 246, 247, 248syl3anc 1264 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  i )  <  s )
250242, 233, 231, 249ltadd2dd 9794 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  i ) )  < 
( X  +  s ) )
251241, 250eqbrtrd 4441 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( V `  i )  <  ( X  +  s ) )
252211adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
253 iooltub 37438 . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . 16  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  <  ( Q `  (
i  +  1 ) ) )
255233, 252, 231, 254ltadd2dd 9794 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
2566, 223, 207syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) )
257256oveq2d 6317 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
258227recnd 9669 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  CC )
259237, 258pncan3d 9989 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( ( V `  (
i  +  1 ) )  -  X ) )  =  ( V `
 ( i  +  1 ) ) )
260257, 259eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `
 ( i  +  1 ) ) )
261260adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( V `  (
i  +  1 ) ) )
262255, 261breqtrd 4445 . . . . . . . . . . . . . 14  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  <  ( V `  (
i  +  1 ) ) )
263226, 229, 234, 251, 262eliood 37423 . . . . . . . . . . . . 13  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( X  +  s )  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
264 fvres 5891 . . . . . . . . . . . . 13  |-  ( ( X  +  s )  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
265263, 264syl 17 . . . . . . . . . . . 12  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  ( X  +  s ) )  =  ( F `  ( X  +  s
) ) )
266265eqcomd 2430 . . . . . . . . . . 11  |-  ( ( ch  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( F `  ( X  +  s ) )  =  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  ( X  +  s )
) )
267266mpteq2dva 4507 . . . . . . . . . 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 37419 . . . . . . . . . . . 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 665 . . . . . . . . . . 11  |-  ( ch 
->  ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  e.  ( ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) )
-cn-> CC ) )
272 ioosscn 37419 . . . . . . . . . . . 12  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC
273272a1i 11 . . . . . . . . . . 11  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  CC )
274269, 271, 273, 237, 263fourierdlem23 37809 . . . . . . . . . 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 2510 . . . . . . . . 9  |-  ( ch 
->  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
2766, 112syl 17 . . . . . . . . . 10  |-  ( ch 
->  F : RR --> RR )
277 ioossre 11696 . . . . . . . . . . 11  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
278277a1i 11 . . . . . . . . . 10  |-  ( ch 
->  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR )
279 eqid 2422 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  |->  ( F `
 ( X  +  s ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( F `  ( X  +  s
) ) )
280 ioossre 11696 . . . . . . . . . . 11  |-  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR
281280a1i 11 . . . . . . . . . 10  |-  ( ch 
->  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  C_  RR )
282233, 254ltned 9771 . . . . . . . . . 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 665 . . . . . . . . . . 11  |-  ( ch 
->  L  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
285260eqcomd 2430 . . . . . . . . . . . 12  |-  ( ch 
->  ( V `  (
i  +  1 ) )  =  ( X  +  ( Q `  ( i  +  1 ) ) ) )
286285oveq2d 6317 . . . . . . . . . . 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 2512 . . . . . . . . . 10  |-  ( ch 
->  L  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
288211recnd 9669 . . . . . . . . . 10  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  CC )
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 37840 . . . . . . . . 9  |-  ( ch 
->  L  e.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
29049, 54ffvelrnd 6034 . . . . . . . . 9  |-  ( ch 
->  ( S `  j
)  e.  RR )
291 elfzoelz 11920 . . . . . . . . . . . 12  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
292 zre 10941 . . . . . . . . . . . 12  |-  ( j  e.  ZZ  ->  j  e.  RR )
29352, 291, 2923syl 18 . . . . . . . . . . 11  |-  ( ch 
->  j  e.  RR )
294293ltp1d 10537 . . . . . . . . . 10  |-  ( ch 
->  j  <  ( j  +  1 ) )
295 isorel 6228 . . . . . . . . . . 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 1262 . . . . . . . . . 10  |-  ( ch 
->  ( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
297294, 296mpbid 213 . . . . . . . . 9  |-  ( ch 
->  ( S `  j
)  <  ( S `  ( j  +  1 ) ) )
2981simprbi 465 . . . . . . . . 9  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
299 eqid 2422 . . . . . . . . 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 2422 . . . . . . . . 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 37820 . . . . . . . 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 2423 . . . . . . . . . 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 462 . . . . . . . . . . . 12  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
s  =  ( S `
 ( j  +  1 ) ) )
304303oveq2d 6317 . . . . . . . . . . 11  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
( X  +  s )  =  ( X  +  ( S `  ( j  +  1 ) ) ) )
305304fveq2d 5881 . . . . . . . . . 10  |-  ( ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  /\  s  =  ( S `  ( j  +  1 ) ) )  -> 
( F `  ( X  +  s )
)  =  ( F `
 ( X  +  ( S `  ( j  +  1 ) ) ) ) )
306243adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  e.  RR* )
307245adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
30890adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  e.  RR )
309193, 211, 290, 90, 297, 298fourierdlem10 37796 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( Q `  i )  <_  ( S `  j )  /\  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) )
310309simpld 460 . . . . . . . . . . . . 13  |-  ( ch 
->  ( Q `  i
)  <_  ( S `  j ) )
311193, 290, 90, 310, 297lelttrd 9793 . . . . . . . . . . . 12  |-  ( ch 
->  ( Q `  i
)  <  ( S `  ( j  +  1 ) ) )
312311adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  i
)  <  ( S `  ( j  +  1 ) ) )
313211adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR )
314309simprd 464 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
315314adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
316 neqne 37232 . . . . . . . . . . . . . 14  |-  ( -.  ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) )  -> 
( S `  (
j  +  1 ) )  =/=  ( Q `
 ( i  +  1 ) ) )
317316necomd 2695 . . . . . . . . . . . . 13  |-  ( -.  ( S `  (
j  +  1 ) )  =  ( Q `
 ( i  +  1 ) )  -> 
( Q `  (
i  +  1 ) )  =/=  ( S `
 ( j  +  1 ) ) )
318317adantl 467 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( Q `  (
i  +  1 ) )  =/=  ( S `
 ( j  +  1 ) ) )
319308, 313, 315, 318leneltd 9789 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  <  ( Q `
 ( i  +  1 ) ) )
320306, 307, 308, 312, 319eliood 37423 . . . . . . . . . 10  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( S `  (
j  +  1 ) )  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
321230, 90readdcld 9670 . . . . . . . . . . . 12  |-  ( ch 
->  ( X  +  ( S `  ( j  +  1 ) ) )  e.  RR )
322276, 321ffvelrnd 6034 . . . . . . . . . . 11  |-  ( ch 
->  ( F `  ( X  +  ( S `  ( j  +  1 ) ) ) )  e.  RR )
323322adantr 466 . . . . . . . . . 10  |-  ( ( ch  /\  -.  ( S `  ( j  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )  -> 
( F `  ( X  +  ( S `  ( j  +  1 ) ) ) )  e.  RR )
324302, 305, 320, 323fvmptd 5966 . . . . . . . . 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 3940 . . . . . . . 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 5171 . . . . . . . . 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 6316 . . . . . . . 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 2524 . . . . . . 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 9596 . . . . . . . . 9  |-  RR  C_  CC
330128, 329syl6ss 3476 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  CC )
33190recnd 9669 . . . . . . . 8  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  CC )
332168, 330, 124, 331constlimc 37521 . . . . . . 7  |-  ( ch 
->  C  e.  (
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  C ) lim CC  ( S `  ( j  +  1 ) ) ) )
333167, 168, 161, 121, 125, 328, 332sublimc 37550 . . . . . 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 37523 . . . . . 6  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  s ) lim CC  ( S `
 ( j  +  1 ) ) ) )
3356, 105jca 534 . . . . . . 7  |-  ( ch 
->  ( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) ) )
336 eleq1 2494 . . . . . . . . . 10  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
s  e.  ( A [,] B )  <->  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) ) )
337336anbi2d 708 . . . . . . . . 9  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
( ph  /\  s  e.  ( A [,] B
) )  <->  ( ph  /\  ( S `  (
j  +  1 ) )  e.  ( A [,] B ) ) ) )
338 neeq1 2705 . . . . . . . . 9  |-  ( s  =  ( S `  ( j  +  1 ) )  ->  (
s  =/=  0  <->  ( S `  ( j  +  1 ) )  =/=  0 ) )
339337, 338imbi12d 321 . . . . . . . 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 3139 . . . . . . 7  |-  ( ( S `  ( j  +  1 ) )  e.  RR  ->  (
( ph  /\  ( S `  ( j  +  1 ) )  e.  ( A [,] B ) )  -> 
( S `  (
j  +  1 ) )  =/=  0 ) )
34190, 335, 340sylc 62 . . . . . 6  |-  ( ch 
->  ( S `  (
j  +  1 ) )  =/=  0 )
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 37554 . . . . 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 2422 . . . . . 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 9663 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  CC )
345159neneqd 2625 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  ( 2  x.  ( sin `  ( s  / 
2 ) ) )  =  0 )
346 2re 10679 . . . . . . . . . . 11  |-  2  e.  RR
347346a1i 11 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  2  e.  RR )
34817rehalfcld 10859 . . . . . . . . . . . 12  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  (
s  /  2 )  e.  RR )
349348resincld 14182 . . . . . . . . . . 11  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
350349adantl 467 . . . . . . . . . 10  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  ( sin `  ( s  / 
2 ) )  e.  RR )
351347, 350remulcld 9671 . . . . . . . . 9  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  RR )
352 elsncg 4019 . . . . . . . . 9  |-  ( ( 2  x.  ( sin `  ( s  /  2
) ) )  e.  RR  ->  ( (
2  x.  ( sin `  ( s  /  2
) ) )  e. 
{ 0 }  <->  ( 2  x.  ( sin `  (
s  /  2 ) ) )  =  0 ) )
353351, 352syl 17 . . . . . . . 8  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  { 0 }  <-> 
( 2  x.  ( sin `  ( s  / 
2 ) ) )  =  0 ) )
354345, 353mtbird 302 . . . . . . 7  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  -.  ( 2  x.  ( sin `  ( s  / 
2 ) ) )  e.  { 0 } )
355344, 354eldifd 3447 . . . . . 6  |-  ( ( ch  /\  s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) ) )  ->  (
2  x.  ( sin `  ( s  /  2
) ) )  e.  ( CC  \  {
0 } ) )
356 eqid 2422 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  2 )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  2 )
357 eqid 2422 . . . . . . 7  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( sin `  ( s  /  2
) ) )  =  ( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  ( sin `  (
s  /  2 ) ) )
358 2cnd 10682 . . . . . . . 8  |-  ( ch 
->  2  e.  CC )
359356, 330, 358, 331constlimc 37521 . . . . . . 7  |-  ( ch 
->  2  e.  (
( s  e.  ( ( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) 
|->  2 ) lim CC  ( S `  ( j  +  1 ) ) ) )
360348ad2antrl 732 . . . . . . . 8  |-  ( ( ch  /\  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  /\  (
s  /  2 )  =/=  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  ->  ( s  / 
2 )  e.  RR )
361 recn 9629 . . . . . . . . . 10  |-  ( x  e.  RR  ->  x  e.  CC )
362361sincld 14169 . . . . . . . . 9  |-  ( x  e.  RR  ->  ( sin `  x )  e.  CC )
363362adantl 467 . . . . . . . 8  |-  ( ( ch  /\  x  e.  RR )  ->  ( sin `  x )  e.  CC )
364 eqid 2422 . . . . . . . . 9  |-  ( s  e.  ( ( S `
 j ) (,) ( S `  (
j  +  1 ) ) )  |->  ( s  /  2 ) )  =  ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  / 
2 ) )
365 2cn 10680 . . . . . . . . . . 11  |-  2  e.  CC
366 eldifsn 4122 . . . . . . . . . . 11  |-  ( 2  e.  ( CC  \  { 0 } )  <-> 
( 2  e.  CC  /\  2  =/=  0 ) )
367365, 151, 366mpbir2an 928 . . . . . . . . . 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 37554 . . . . . . . 8  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  ( ( s  e.  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  |->  ( s  /  2 ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
371 sinf 14163 . . . . . . . . . . . . . 14  |-  sin : CC
--> CC
372371a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  sin : CC --> CC )
373329a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  RR  C_  CC )
374372, 373feqresmpt 5931 . . . . . . . . . . . 12  |-  ( T. 
->  ( sin  |`  RR )  =  ( x  e.  RR  |->  ( sin `  x
) ) )
375374trud 1446 . . . . . . . . . . 11  |-  ( sin  |`  RR )  =  ( x  e.  RR  |->  ( sin `  x ) )
376 resincncf 37569 . . . . . . . . . . 11  |-  ( sin  |`  RR )  e.  ( RR -cn-> RR )
377375, 376eqeltrri 2507 . . . . . . . . . 10  |-  ( x  e.  RR  |->  ( sin `  x ) )  e.  ( RR -cn-> RR )
378377a1i 11 . . . . . . . . 9  |-  ( ch 
->  ( x  e.  RR  |->  ( sin `  x ) )  e.  ( RR
-cn-> RR ) )
37990rehalfcld 10859 . . . . . . . . 9  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  RR )
380 fveq2 5877 . . . . . . . . 9  |-  ( x  =  ( ( S `
 ( j  +  1 ) )  / 
2 )  ->  ( sin `  x )  =  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) ) )
381378, 379, 380cnmptlimc 22829 . . . . . . . 8  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  ( ( x  e.  RR  |->  ( sin `  x ) ) lim CC  ( ( S `  ( j  +  1 ) )  /  2 ) ) )
382 fveq2 5877 . . . . . . . 8  |-  ( x  =  ( s  / 
2 )  ->  ( sin `  x )  =  ( sin `  (
s  /  2 ) ) )
383 fveq2 5877 . . . . . . . . 9  |-  ( ( s  /  2 )  =  ( ( S `
 ( j  +  1 ) )  / 
2 )  ->  ( sin `  ( s  / 
2 ) )  =  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) ) )
384383ad2antll 733 . . . . . . . 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 22832 . . . . . . 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 37513 . . . . . 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 10857 . . . . . . . 8  |-  ( ch 
->  ( ( S `  ( j  +  1 ) )  /  2
)  e.  CC )
388387sincld 14169 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  e.  CC )
389154, 105sseldd 3465 . . . . . . . 8  |-  ( ch 
->  ( S `  (
j  +  1 ) )  e.  ( -u pi [,] pi ) )
390 fourierdlem44 37832 . . . . . . . 8  |-  ( ( ( S `  (
j  +  1 ) )  e.  ( -u pi [,] pi )  /\  ( S `  ( j  +  1 ) )  =/=  0 )  -> 
( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  =/=  0 )
391389, 341, 390syl2anc 665 . . . . . . 7  |-  ( ch 
->  ( sin `  (
( S `  (
j  +  1 ) )  /  2 ) )  =/=  0 )
392358, 388, 369, 391mulne0d 10264 . . . . . 6  |-  ( ch 
->  ( 2  x.  ( sin `  ( ( S `
 ( j  +  1 ) )  / 
2 ) ) )  =/=  0 )
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 37554 . . . . 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 37513 . . . 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 5116 . . . . . 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 11720 . . . . . . . 8  |-  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )
400 iccss 11702 . . . . . . . . 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 1265 . . . . . . . 8  |-  ( ch 
->  ( ( S `  j ) [,] ( S `  ( j  +  1 ) ) )  C_  ( A [,] B ) )
402399, 401syl5ss 3475 . . . . . . 7  |-  ( ch 
->  ( ( S `  j ) (,) ( S `  ( j  +  1 ) ) )  C_  ( A [,] B ) )
403402resmptd 5171 . . . . . 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 2475 . . . . 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 6316 . . . 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 2525 . . 3  |-  ( ch 
->  D  e.  (
( O  |`  (
( S `  j
) (,) ( S `
 ( j  +  1 ) ) ) ) lim CC  ( S `
 ( j  +  1 ) ) ) )
4071, 406sylbir 216 . 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 9770 . . . . . . . . . 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 665 . . . . . . . . . . 11  |-  ( ch 
->  R  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 i ) ) )
411240oveq2d 6317 . . . . . . . . . . 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 2512 . . . . . . . . . 10  |-  ( ch 
->  R  e.  (
( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( X  +  ( Q `  i ) ) ) )
413193recnd 9669 . . . . . . . . . 10  |-  ( ch 
->  ( Q `  i
)  e.  CC )
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 37840 . . . . . . . . 9  |-  ( ch 
->  R  e.  (
( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( F `  ( X  +  s )
) ) lim CC  ( Q `  i )
) )
415 eqid 2422 . . . . . . . . 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 2422 . . . . . . . . 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 37819 . . . . . . . 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 2423 . . . . . . . . . 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 6309 . . . . . . . . . . . 12  |-  ( s  =  ( S `  j )  ->  ( X  +  s )  =  ( X  +  ( S `  j ) ) )
420419fveq2d 5881 . . . . . . . . . . 11  |-  ( s  =  ( S `  j )  ->  ( F `  ( X  +  s ) )  =  ( F `  ( X  +  ( S `  j )
) ) )
421420adantl 467 . . . . . . . . . 10  |-  ( ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  /\  s  =  ( S `  j ) )  -> 
( F `  ( X  +  s )
)  =  ( F `
 ( X  +  ( S `  j ) ) ) )
422243adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( Q `  i
)  e.  RR* )
423245adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( Q `  (
i  +  1 ) )  e.  RR* )
424290adantr 466 . . . . . . . . . . 11  |-  ( ( ch  /\  -.  ( S `  j )  =  ( Q `  i ) )  -> 
( S `  j
)  e.  RR )
425193adantr 466 . . . . . . . . . . . 12  |-  ( ( ch  /\  -.  ( S