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

Theorem fourierdlem89 31819
Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem89.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem89.t  |-  T  =  ( B  -  A
)
fourierdlem89.m  |-  ( ph  ->  M  e.  NN )
fourierdlem89.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem89.f  |-  ( ph  ->  F : RR --> CC )
fourierdlem89.per  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fourierdlem89.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem89.limc  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem89.c  |-  ( ph  ->  C  e.  RR )
fourierdlem89.d  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
fourierdlem89.o  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  C  /\  ( p `
 m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem89.12  |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
fourierdlem89.n  |-  N  =  ( ( # `  H
)  -  1 )
fourierdlem89.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
fourierdlem89.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem89.z  |-  Z  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
fourierdlem89.j  |-  ( ph  ->  J  e.  ( 0..^ N ) )
fourierdlem89.u  |-  U  =  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) )
fourierdlem89.20  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ,  RR ,  <  ) )
fourierdlem89.21  |-  V  =  ( i  e.  ( 0..^ M )  |->  R )
Assertion
Ref Expression
fourierdlem89  |-  ( ph  ->  if ( ( Z `
 ( E `  ( S `  J ) ) )  =  ( Q `  ( I `
 ( S `  J ) ) ) ,  ( V `  ( I `  ( S `  J )
) ) ,  ( F `  ( Z `
 ( E `  ( S `  J ) ) ) ) )  e.  ( ( F  |`  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) ) ) lim CC  ( S `  J )
) )
Distinct variable groups:    A, f,
k, y    A, i, x, k, y    A, m, p, i    B, f, k, y    B, i, x    B, m, p    C, f, y    C, i, m, p    x, C    D, f, y    D, i, m, p    x, D    f, E, k, y    i, E, x    i, F, x, y    f, I, k, y    i, I, x   
i, J, x, y   
i, M, x    m, M, p    f, N, k, y    i, N, x   
m, N, p    Q, f, k, y    Q, i, x    Q, p    S, f, k, y    S, i, x    S, p    T, f, k, y    T, i, x    x, U, y   
x, V, y    i, Z, x, y    ph, f,
k, y    ph, i, x
Allowed substitution hints:    ph( m, p)    C( k)    D( k)    P( x, y, f, i, k, m, p)    Q( m)    R( x, y, f, i, k, m, p)    S( m)    T( m, p)    U( f, i, k, m, p)    E( m, p)    F( f,
k, m, p)    H( x, y, f, i, k, m, p)    I( m, p)    J( f, k, m, p)    M( y, f, k)    O( x, y, f, i, k, m, p)    V( f, i, k, m, p)    Z( f, k, m, p)

Proof of Theorem fourierdlem89
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 fourierdlem89.f . . . . . 6  |-  ( ph  ->  F : RR --> CC )
2 fdm 5741 . . . . . . . 8  |-  ( F : RR --> CC  ->  dom 
F  =  RR )
31, 2syl 16 . . . . . . 7  |-  ( ph  ->  dom  F  =  RR )
43feq2d 5724 . . . . . 6  |-  ( ph  ->  ( F : dom  F --> CC  <->  F : RR --> CC ) )
51, 4mpbird 232 . . . . 5  |-  ( ph  ->  F : dom  F --> CC )
6 ioosscn 31414 . . . . . 6  |-  ( ( Z `  ( E `
 ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) )  C_  CC
76a1i 11 . . . . 5  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  CC )
8 ioossre 11598 . . . . . . 7  |-  ( ( Z `  ( E `
 ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) )  C_  RR
98a1i 11 . . . . . 6  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  RR )
103sseq2d 3537 . . . . . 6  |-  ( ph  ->  ( ( ( Z `
 ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) 
C_  dom  F  <->  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) )  C_  RR ) )
119, 10mpbird 232 . . . . 5  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  dom  F )
12 ax-resscn 9561 . . . . . 6  |-  RR  C_  CC
13 fourierdlem89.u . . . . . . 7  |-  U  =  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) )
14 fourierdlem89.t . . . . . . . . . . . . . . 15  |-  T  =  ( B  -  A
)
15 fourierdlem89.p . . . . . . . . . . . . . . 15  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  A  /\  ( p `
 m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
16 fourierdlem89.m . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
17 fourierdlem89.q . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( P `
 M ) )
18 fourierdlem89.c . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR )
19 fourierdlem89.d . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
20 elioore 11571 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( C (,) +oo )  ->  D  e.  RR )
2119, 20syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  D  e.  RR )
22 elioo4g 11597 . . . . . . . . . . . . . . . . . 18  |-  ( D  e.  ( C (,) +oo )  <->  ( ( C  e.  RR*  /\ +oo  e.  RR* 
/\  D  e.  RR )  /\  ( C  < 
D  /\  D  < +oo ) ) )
2319, 22sylib 196 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( C  e. 
RR*  /\ +oo  e.  RR*  /\  D  e.  RR )  /\  ( C  < 
D  /\  D  < +oo ) ) )
2423simprd 463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  <  D  /\  D  < +oo )
)
2524simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  <  D )
26 fourierdlem89.o . . . . . . . . . . . . . . 15  |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  C  /\  ( p `
 m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
27 oveq1 6302 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  (
y  +  ( k  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
2827eleq1d 2536 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( x  +  ( k  x.  T ) )  e.  ran  Q ) )
2928rexbidv 2978 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  (
x  +  ( k  x.  T ) )  e.  ran  Q ) )
3029cbvrabv 3117 . . . . . . . . . . . . . . . 16  |-  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  =  { x  e.  ( C [,] D )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q }
3130uneq2i 3660 . . . . . . . . . . . . . . 15  |-  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } )  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
32 fourierdlem89.n . . . . . . . . . . . . . . . 16  |-  N  =  ( ( # `  H
)  -  1 )
33 fourierdlem89.12 . . . . . . . . . . . . . . . . . 18  |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
3433fveq2i 5875 . . . . . . . . . . . . . . . . 17  |-  ( # `  H )  =  (
# `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )
3534oveq1i 6305 . . . . . . . . . . . . . . . 16  |-  ( (
# `  H )  -  1 )  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 )
3632, 35eqtri 2496 . . . . . . . . . . . . . . 15  |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 )
37 fourierdlem89.s . . . . . . . . . . . . . . . 16  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
38 isoeq5 6218 . . . . . . . . . . . . . . . . . . 19  |-  ( H  =  ( { C ,  D }  u.  {
y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )  ->  (
f  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  <-> 
f  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
3933, 38ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( f 
Isom  <  ,  <  (
( 0 ... N
) ,  H )  <-> 
f  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
4039ax-gen 1601 . . . . . . . . . . . . . . . . 17  |-  A. f
( f  Isom  <  ,  <  ( ( 0 ... N ) ,  H )  <->  f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) ) )
41 iotabi 5566 . . . . . . . . . . . . . . . . 17  |-  ( A. f ( f  Isom  <  ,  <  ( ( 0 ... N ) ,  H )  <->  f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) ) )  -> 
( iota f f  Isom  <  ,  <  ( ( 0 ... N ) ,  H ) )  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
4240, 41ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( iota f f  Isom  <  ,  <  ( ( 0 ... N ) ,  H ) )  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
4337, 42eqtri 2496 . . . . . . . . . . . . . . 15  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
4414, 15, 16, 17, 18, 21, 25, 26, 31, 36, 43fourierdlem54 31784 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  e.  NN  /\  S  e.  ( O `  N
) )  /\  S  Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
4544simpld 459 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
4645simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  ( O `
 N ) )
4745simpld 459 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
4826fourierdlem2 31732 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  ( S  e.  ( O `  N )  <->  ( S  e.  ( RR  ^m  (
0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) ) )
4947, 48syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  e.  ( O `  N )  <-> 
( S  e.  ( RR  ^m  ( 0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) ) )
5046, 49mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) )
5150simpld 459 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... N ) ) )
52 elmapi 7452 . . . . . . . . . 10  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
5351, 52syl 16 . . . . . . . . 9  |-  ( ph  ->  S : ( 0 ... N ) --> RR )
54 fourierdlem89.j . . . . . . . . . 10  |-  ( ph  ->  J  e.  ( 0..^ N ) )
55 fzofzp1 11889 . . . . . . . . . 10  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
5654, 55syl 16 . . . . . . . . 9  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
5753, 56ffvelrnd 6033 . . . . . . . 8  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR )
5815, 16, 17fourierdlem11 31741 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
5958simp1d 1008 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
6059rexrd 9655 . . . . . . . . . 10  |-  ( ph  ->  A  e.  RR* )
6158simp2d 1009 . . . . . . . . . 10  |-  ( ph  ->  B  e.  RR )
62 iocssre 11616 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
6360, 61, 62syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( A (,] B
)  C_  RR )
6458simp3d 1010 . . . . . . . . . . 11  |-  ( ph  ->  A  <  B )
65 fourierdlem89.e . . . . . . . . . . 11  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
6659, 61, 64, 14, 65fourierdlem4 31734 . . . . . . . . . 10  |-  ( ph  ->  E : RR --> ( A (,] B ) )
6766, 57ffvelrnd 6033 . . . . . . . . 9  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  ( A (,] B ) )
6863, 67sseldd 3510 . . . . . . . 8  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  RR )
6957, 68resubcld 9999 . . . . . . 7  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  e.  RR )
7013, 69syl5eqel 2559 . . . . . 6  |-  ( ph  ->  U  e.  RR )
7112, 70sseldi 3507 . . . . 5  |-  ( ph  ->  U  e.  CC )
72 eqid 2467 . . . . 5  |-  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) }  =  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) }
73 ioossre 11598 . . . . . . . 8  |-  ( ( ( Z `  ( E `  ( S `  J ) ) )  +  U ) (,) ( ( E `  ( S `  ( J  +  1 ) ) )  +  U ) )  C_  RR
7473a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( ( Z `
 ( E `  ( S `  J ) ) )  +  U
) (,) ( ( E `  ( S `
 ( J  + 
1 ) ) )  +  U ) ) 
C_  RR )
753sseq2d 3537 . . . . . . 7  |-  ( ph  ->  ( ( ( ( Z `  ( E `
 ( S `  J ) ) )  +  U ) (,) ( ( E `  ( S `  ( J  +  1 ) ) )  +  U ) )  C_  dom  F  <->  ( (
( Z `  ( E `  ( S `  J ) ) )  +  U ) (,) ( ( E `  ( S `  ( J  +  1 ) ) )  +  U ) )  C_  RR )
)
7674, 75mpbird 232 . . . . . 6  |-  ( ph  ->  ( ( ( Z `
 ( E `  ( S `  J ) ) )  +  U
) (,) ( ( E `  ( S `
 ( J  + 
1 ) ) )  +  U ) ) 
C_  dom  F )
7759, 61iccssred 31426 . . . . . . . . 9  |-  ( ph  ->  ( A [,] B
)  C_  RR )
78 fourierdlem89.z . . . . . . . . . . 11  |-  Z  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
7959, 61, 64, 78fourierdlem17 31747 . . . . . . . . . 10  |-  ( ph  ->  Z : ( A (,] B ) --> ( A [,] B ) )
80 ssid 3528 . . . . . . . . . . . . 13  |-  RR  C_  RR
8180a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  RR )
82 elfzofz 11823 . . . . . . . . . . . . . 14  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
8354, 82syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  J  e.  ( 0 ... N ) )
8453, 83ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  J
)  e.  RR )
8581, 84sseldd 3510 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  J
)  e.  RR )
8666, 85ffvelrnd 6033 . . . . . . . . . 10  |-  ( ph  ->  ( E `  ( S `  J )
)  e.  ( A (,] B ) )
8779, 86ffvelrnd 6033 . . . . . . . . 9  |-  ( ph  ->  ( Z `  ( E `  ( S `  J ) ) )  e.  ( A [,] B ) )
8877, 87sseldd 3510 . . . . . . . 8  |-  ( ph  ->  ( Z `  ( E `  ( S `  J ) ) )  e.  RR )
8988, 68, 70iooshift 31449 . . . . . . 7  |-  ( ph  ->  ( ( ( Z `
 ( E `  ( S `  J ) ) )  +  U
) (,) ( ( E `  ( S `
 ( J  + 
1 ) ) )  +  U ) )  =  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) } )
9089sseq1d 3536 . . . . . 6  |-  ( ph  ->  ( ( ( ( Z `  ( E `
 ( S `  J ) ) )  +  U ) (,) ( ( E `  ( S `  ( J  +  1 ) ) )  +  U ) )  C_  dom  F  <->  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) } 
C_  dom  F )
)
9176, 90mpbid 210 . . . . 5  |-  ( ph  ->  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) x  =  ( y  +  U
) }  C_  dom  F )
92 simpl 457 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) )  ->  ph )
938sseli 3505 . . . . . . 7  |-  ( y  e.  ( ( Z `
 ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) )  ->  y  e.  RR )
9493adantl 466 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) )  ->  y  e.  RR )
95 id 22 . . . . . . . . . . . . 13  |-  ( ph  ->  ph )
9661, 59resubcld 9999 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  -  A
)  e.  RR )
9714, 96syl5eqel 2559 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T  e.  RR )
9859, 61posdifd 10151 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
9964, 98mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( B  -  A ) )
10014eqcomi 2480 . . . . . . . . . . . . . . . . 17  |-  ( B  -  A )  =  T
101100a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  -  A
)  =  T )
10299, 101breqtrd 4477 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  T )
10397, 102elrpd 11266 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  e.  RR+ )
104103rpcnd 11270 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e.  CC )
10595, 104syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  CC )
106102gt0ne0d 10129 . . . . . . . . . . . . 13  |-  ( ph  ->  T  =/=  0 )
10795, 106syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  T  =/=  0 )
10871, 105, 107divcan1d 10333 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U  /  T )  x.  T
)  =  U )
109108eqcomd 2475 . . . . . . . . . 10  |-  ( ph  ->  U  =  ( ( U  /  T )  x.  T ) )
110109oveq2d 6311 . . . . . . . . 9  |-  ( ph  ->  ( y  +  U
)  =  ( y  +  ( ( U  /  T )  x.  T ) ) )
111110adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  U )  =  ( y  +  ( ( U  /  T
)  x.  T ) ) )
112111fveq2d 5876 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  U ) )  =  ( F `  (
y  +  ( ( U  /  T )  x.  T ) ) ) )
113 eqidd 2468 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  ( ( U  /  T )  x.  T
) ) )  =  ( F `  (
y  +  ( ( U  /  T )  x.  T ) ) ) )
1141adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  F : RR
--> CC )
11595, 97syl 16 . . . . . . . . 9  |-  ( ph  ->  T  e.  RR )
116115adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  T  e.  RR )
11713oveq1i 6305 . . . . . . . . . . . 12  |-  ( U  /  T )  =  ( ( ( S `
 ( J  + 
1 ) )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  /  T )
118117a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( U  /  T
)  =  ( ( ( S `  ( J  +  1 ) )  -  ( E `
 ( S `  ( J  +  1
) ) ) )  /  T ) )
11968recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  e.  CC )
12057recnd 9634 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  CC )
121119, 120negsubdi2d 9958 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  =  ( ( S `  ( J  +  1 ) )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )
122121eqcomd 2475 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) )  =  -u ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) ) )
123122oveq1d 6310 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( S `
 ( J  + 
1 ) )  -  ( E `  ( S `
 ( J  + 
1 ) ) ) )  /  T )  =  ( -u (
( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  /  T ) )
12465a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
125 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( S `  ( J  +  1
) )  ->  x  =  ( S `  ( J  +  1
) ) )
126 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( S `  ( J  +  1
) )  ->  ( B  -  x )  =  ( B  -  ( S `  ( J  +  1 ) ) ) )
127126oveq1d 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )
128127fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( S `  ( J  +  1
) )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) ) )
129128oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) )
130125, 129oveq12d 6313 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( S `  ( J  +  1
) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 ( J  + 
1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) ) )
131130adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  =  ( S `  ( J  +  1 ) ) )  ->  ( x  +  ( ( |_
`  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `  ( J  +  1
) )  +  ( ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) ) )
13261, 57resubcld 9999 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B  -  ( S `  ( J  +  1 ) ) )  e.  RR )
133132, 115, 107redivcld 10384 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T )  e.  RR )
134133flcld 11915 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  ZZ )
135134zred 10978 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  RR )
136135, 115remulcld 9636 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T )  e.  RR )
13757, 136readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  +  ( ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) )  e.  RR )
138124, 131, 57, 137fvmptd 5962 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E `  ( S `  ( J  +  1 ) ) )  =  ( ( S `  ( J  +  1 ) )  +  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) ) )
139138oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  =  ( ( ( S `  ( J  +  1 ) )  +  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) )  -  ( S `  ( J  +  1 ) ) ) )
14012, 135sseldi 3507 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  e.  CC )
141140, 105mulcld 9628 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T )  e.  CC )
142120, 141pncan2d 9944 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( S `
 ( J  + 
1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  x.  T ) )  -  ( S `
 ( J  + 
1 ) ) )  =  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) )
143139, 142eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  =  ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T ) )
144143, 141eqeltrd 2555 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  e.  CC )
145144, 105, 107divnegd 10345 . . . . . . . . . . . 12  |-  ( ph  -> 
-u ( ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( S `  ( J  +  1
) ) )  /  T )  =  (
-u ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  /  T ) )
146145eqcomd 2475 . . . . . . . . . . 11  |-  ( ph  ->  ( -u ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( S `  ( J  +  1
) ) )  /  T )  =  -u ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  /  T ) )
147118, 123, 1463eqtrd 2512 . . . . . . . . . 10  |-  ( ph  ->  ( U  /  T
)  =  -u (
( ( E `  ( S `  ( J  +  1 ) ) )  -  ( S `
 ( J  + 
1 ) ) )  /  T ) )
148143oveq1d 6310 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  /  T )  =  ( ( ( |_ `  ( ( B  -  ( S `
 ( J  + 
1 ) ) )  /  T ) )  x.  T )  /  T ) )
149140, 105, 107divcan4d 10338 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) )  x.  T )  /  T
)  =  ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) ) )
150 eqidd 2468 . . . . . . . . . . . . 13  |-  ( ph  ->  ( |_ `  (
( B  -  ( S `  ( J  +  1 ) ) )  /  T ) )  =  ( |_
`  ( ( B  -  ( S `  ( J  +  1
) ) )  /  T ) ) )
151148, 149, 1503eqtrd 2512 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  /  T )  =  ( |_ `  ( ( B  -  ( S `  ( J  +  1 ) ) )  /  T ) ) )
152151, 134eqeltrd 2555 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( S `  ( J  +  1 ) ) )  /  T )  e.  ZZ )
153152znegcld 10980 . . . . . . . . . 10  |-  ( ph  -> 
-u ( ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( S `  ( J  +  1
) ) )  /  T )  e.  ZZ )
154147, 153eqeltrd 2555 . . . . . . . . 9  |-  ( ph  ->  ( U  /  T
)  e.  ZZ )
155154adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( U  /  T )  e.  ZZ )
156 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
157 fourierdlem89.per . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
158157adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
159114, 116, 155, 156, 158fperiodmul 31404 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  ( ( U  /  T )  x.  T
) ) )  =  ( F `  y
) )
160112, 113, 1593eqtrd 2512 . . . . . 6  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  U ) )  =  ( F `  y
) )
16192, 94, 160syl2anc 661 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) )  ->  ( F `  ( y  +  U
) )  =  ( F `  y ) )
16215fourierdlem2 31732 . . . . . . . . . . . . 13  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
16316, 162syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
16417, 163mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
165164simpld 459 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
166 elmapi 7452 . . . . . . . . . 10  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
167165, 166syl 16 . . . . . . . . 9  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
16895, 167syl 16 . . . . . . . 8  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
169 elfzofz 11823 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
170169ssriv 3513 . . . . . . . . . 10  |-  ( 0..^ M )  C_  (
0 ... M )
171170a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ M ) 
C_  ( 0 ... M ) )
17295, 16syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
17395, 17syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( P `
 M ) )
174 fourierdlem89.20 . . . . . . . . . . . 12  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ,  RR ,  <  ) )
17515, 172, 173, 14, 65, 78, 174fourierdlem37 31767 . . . . . . . . . . 11  |-  ( ph  ->  ( I : RR --> ( 0..^ M )  /\  ( x  e.  RR  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( Z `  ( E `  x )
) } ,  RR ,  <  )  e.  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ) ) )
176175simpld 459 . . . . . . . . . 10  |-  ( ph  ->  I : RR --> ( 0..^ M ) )
177176, 84ffvelrnd 6033 . . . . . . . . 9  |-  ( ph  ->  ( I `  ( S `  J )
)  e.  ( 0..^ M ) )
178171, 177sseldd 3510 . . . . . . . 8  |-  ( ph  ->  ( I `  ( S `  J )
)  e.  ( 0 ... M ) )
179168, 178ffvelrnd 6033 . . . . . . 7  |-  ( ph  ->  ( Q `  (
I `  ( S `  J ) ) )  e.  RR )
180 fzofzp1 11889 . . . . . . . . 9  |-  ( ( I `  ( S `
 J ) )  e.  ( 0..^ M )  ->  ( (
I `  ( S `  J ) )  +  1 )  e.  ( 0 ... M ) )
181177, 180syl 16 . . . . . . . 8  |-  ( ph  ->  ( ( I `  ( S `  J ) )  +  1 )  e.  ( 0 ... M ) )
182168, 181ffvelrnd 6033 . . . . . . 7  |-  ( ph  ->  ( Q `  (
( I `  ( S `  J )
)  +  1 ) )  e.  RR )
183164simprd 463 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
184183simprd 463 . . . . . . . 8  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
18515, 16, 17, 14, 65, 78, 174fourierdlem37 31767 . . . . . . . . . 10  |-  ( ph  ->  ( I : RR --> ( 0..^ M )  /\  ( x  e.  RR  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( Z `  ( E `  x )
) } ,  RR ,  <  )  e.  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ) ) )
186185simpld 459 . . . . . . . . 9  |-  ( ph  ->  I : RR --> ( 0..^ M ) )
187186, 84ffvelrnd 6033 . . . . . . . 8  |-  ( ph  ->  ( I `  ( S `  J )
)  e.  ( 0..^ M ) )
188 fveq2 5872 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( Q `  i )  =  ( Q `  ( I `
 ( S `  J ) ) ) )
189 oveq1 6302 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( i  +  1 )  =  ( ( I `  ( S `  J ) )  +  1 ) )
190189fveq2d 5876 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) )
191188, 190breq12d 4466 . . . . . . . . 9  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( Q `  i )  <  ( Q `  (
i  +  1 ) )  <->  ( Q `  ( I `  ( S `  J )
) )  <  ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )
192191rspccva 3218 . . . . . . . 8  |-  ( ( A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) )  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )  ->  ( Q `  ( I `  ( S `  J )
) )  <  ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
193184, 187, 192syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( Q `  (
I `  ( S `  J ) ) )  <  ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) )
19495, 187jca 532 . . . . . . . 8  |-  ( ph  ->  ( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) ) )
195 eleq1 2539 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( i  e.  ( 0..^ M )  <-> 
( I `  ( S `  J )
)  e.  ( 0..^ M ) ) )
196195anbi2d 703 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( ph  /\  i  e.  ( 0..^ M ) )  <-> 
( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) ) ) )
197188, 190oveq12d 6313 . . . . . . . . . . . 12  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  =  ( ( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )
198197reseq2d 5279 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  ( I `  ( S `  J
) ) ) (,) ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ) ) )
199197oveq1d 6310 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC )  =  ( ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
-cn-> CC ) )
200198, 199eleq12d 2549 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  e.  ( ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) -cn-> CC )  <-> 
( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )  e.  ( ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
-cn-> CC ) ) )
201196, 200imbi12d 320 . . . . . . . . 9  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )  <->  ( ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) )  -> 
( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )  e.  ( ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
-cn-> CC ) ) ) )
202 fourierdlem89.fcn . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
203201, 202vtoclg 3176 . . . . . . . 8  |-  ( ( I `  ( S `
 J ) )  e.  ( 0..^ M )  ->  ( ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) )  -> 
( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )  e.  ( ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
-cn-> CC ) ) )
204187, 194, 203sylc 60 . . . . . . 7  |-  ( ph  ->  ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )  e.  ( ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
-cn-> CC ) )
205 nfcv 2629 . . . . . . . . 9  |-  F/_ i
( I `  ( S `  J )
)
206 nfv 1683 . . . . . . . . . 10  |-  F/ i ( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )
207 fourierdlem89.21 . . . . . . . . . . . . 13  |-  V  =  ( i  e.  ( 0..^ M )  |->  R )
208 nfmpt1 4542 . . . . . . . . . . . . 13  |-  F/_ i
( i  e.  ( 0..^ M )  |->  R )
209207, 208nfcxfr 2627 . . . . . . . . . . . 12  |-  F/_ i V
210209, 205nffv 5879 . . . . . . . . . . 11  |-  F/_ i
( V `  (
I `  ( S `  J ) ) )
211 nfcv 2629 . . . . . . . . . . 11  |-  F/_ i
( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) )
212210, 211nfel 2642 . . . . . . . . . 10  |-  F/ i ( V `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) )
213206, 212nfim 1867 . . . . . . . . 9  |-  F/ i ( ( ph  /\  ( I `  ( S `  J )
)  e.  ( 0..^ M ) )  -> 
( V `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) ) )
214196biimpar 485 . . . . . . . . . . . . . 14  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ph  /\  i  e.  ( 0..^ M ) ) )
2152143adant2 1015 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ph  /\  i  e.  ( 0..^ M ) ) )
216 simp2 997 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) ) )
217215, 216mpd 15 . . . . . . . . . . . 12  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
218 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( V `  i )  =  ( V `  ( I `
 ( S `  J ) ) ) )
219218eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( V `  ( I `  ( S `  J )
) )  =  ( V `  i ) )
220219adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( V `  ( I `  ( S `  J
) ) )  =  ( V `  i
) )
221214simprd 463 . . . . . . . . . . . . . . . 16  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  i  e.  ( 0..^ M ) )
222 fourierdlem89.limc . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
223 elex 3127 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
)  ->  R  e.  _V )
224214, 222, 2233syl 20 . . . . . . . . . . . . . . . 16  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  R  e.  _V )
225207fvmpt2 5964 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ M )  /\  R  e.  _V )  ->  ( V `  i )  =  R )
226221, 224, 225syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( V `  i )  =  R )
227220, 226eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( V `  ( I `  ( S `  J
) ) )  =  R )
2282273adant2 1015 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( V `  ( I `  ( S `  J )
) )  =  R )
229198, 188oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) )  =  ( ( F  |`  ( ( Q `  ( I `  ( S `  J
) ) ) (,) ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ) ) lim CC  ( Q `  ( I `
 ( S `  J ) ) ) ) )
230229eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( F  |`  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
2312303ad2ant1 1017 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )
232228, 231eleq12d 2549 . . . . . . . . . . . 12  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ( V `
 ( I `  ( S `  J ) ) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( I `
 ( S `  J ) ) ) )  <->  R  e.  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) ) )
233217, 232mpbird 232 . . . . . . . . . . 11  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( V `  ( I `  ( S `  J )
) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( I `
 ( S `  J ) ) ) ) )
2342333exp 1195 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )  ->  (
( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )  ->  ( V `  ( I `  ( S `  J )
) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( I `
 ( S `  J ) ) ) ) ) ) )
235222a1ii 27 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )  ->  ( V `  ( I `  ( S `  J )
) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( I `
 ( S `  J ) ) ) ) )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) ) ) )
236234, 235impbid 191 . . . . . . . . 9  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  i )
) )  <->  ( ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) )  -> 
( V `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) ) ) ) )
237205, 213, 236, 222vtoclgf 3174 . . . . . . . 8  |-  ( ( I `  ( S `
 J ) )  e.  ( 0..^ M )  ->  ( ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) )  -> 
( V `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) ) ) )
238187, 194, 237sylc 60 . . . . . . 7  |-  ( ph  ->  ( V `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( I `  ( S `  J ) ) ) ) )
23950simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S `
 0 )  =  C  /\  ( S `
 N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) )
240239simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  A. i  e.  ( 0..^ N ) ( S `  i )  <  ( S `  ( i  +  1 ) ) )
241 fveq2 5872 . . . . . . . . . . . . 13  |-  ( i  =  J  ->  ( S `  i )  =  ( S `  J ) )
242 oveq1 6302 . . . . . . . . . . . . . 14  |-  ( i  =  J  ->  (
i  +  1 )  =  ( J  + 
1 ) )
243242fveq2d 5876 . . . . . . . . . . . . 13  |-  ( i  =  J  ->  ( S `  ( i  +  1 ) )  =  ( S `  ( J  +  1
) ) )
244241, 243breq12d 4466 . . . . . . . . . . . 12  |-  ( i  =  J  ->  (
( S `  i
)  <  ( S `  ( i  +  1 ) )  <->  ( S `  J )  <  ( S `  ( J  +  1 ) ) ) )
245244rspccva 3218 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( 0..^ N ) ( S `  i )  <  ( S `  ( i  +  1 ) )  /\  J  e.  ( 0..^ N ) )  ->  ( S `  J )  <  ( S `  ( J  +  1 ) ) )
246240, 54, 245syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
247 posdif 10057 . . . . . . . . . . 11  |-  ( ( ( S `  J
)  e.  RR  /\  ( S `  ( J  +  1 ) )  e.  RR )  -> 
( ( S `  J )  <  ( S `  ( J  +  1 ) )  <->  0  <  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
24884, 57, 247syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( S `  J )  <  ( S `  ( J  +  1 ) )  <->  0  <  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
249246, 248mpbid 210 . . . . . . . . 9  |-  ( ph  ->  0  <  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) )
25095, 54jca 532 . . . . . . . . . . 11  |-  ( ph  ->  ( ph  /\  J  e.  ( 0..^ N ) ) )
251 eleq1 2539 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
j  e.  ( 0..^ N )  <->  J  e.  ( 0..^ N ) ) )
252251anbi2d 703 . . . . . . . . . . . . 13  |-  ( j  =  J  ->  (
( ph  /\  j  e.  ( 0..^ N ) )  <->  ( ph  /\  J  e.  ( 0..^ N ) ) ) )
253 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( j  =  J  ->  (
j  +  1 )  =  ( J  + 
1 ) )
254253fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( j  =  J  ->  ( S `  ( j  +  1 ) )  =  ( S `  ( J  +  1
) ) )
255254fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( j  =  J  ->  ( E `  ( S `  ( j  +  1 ) ) )  =  ( E `  ( S `  ( J  +  1 ) ) ) )
256 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( j  =  J  ->  ( S `  j )  =  ( S `  J ) )
257256fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( j  =  J  ->  ( E `  ( S `  j ) )  =  ( E `  ( S `  J )
) )
258257fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( j  =  J  ->  ( Z `  ( E `  ( S `  j
) ) )  =  ( Z `  ( E `  ( S `  J ) ) ) )
259255, 258oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  j ) ) ) )  =  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) ) )
260254, 256oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  =  ( ( S `
 ( J  + 
1 ) )  -  ( S `  J ) ) )
261259, 260eqeq12d 2489 . . . . . . . . . . . . 13  |-  ( j  =  J  ->  (
( ( E `  ( S `  ( j  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( Z `  ( E `
 ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
262252, 261imbi12d 320 . . . . . . . . . . . 12  |-  ( j  =  J  ->  (
( ( ph  /\  j  e.  ( 0..^ N ) )  -> 
( ( E `  ( S `  ( j  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
) )  <->  ( ( ph  /\  J  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( Z `  ( E `
 ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) ) )
26314oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  x.  T )  =  ( k  x.  ( B  -  A )
)
264263oveq2i 6306 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  +  ( k  x.  T ) )  =  ( y  +  ( k  x.  ( B  -  A ) ) )
265264eleq1i 2544 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( k  x.  ( B  -  A
) ) )  e. 
ran  Q )
266265rexbii 2969 . . . . . . . . . . . . . . . . . . 19  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q )
267266rgenw 2828 . . . . . . . . . . . . . . . . . 18  |-  A. y  e.  ( C [,] D
) ( E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q  <->  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q
)
268 rabbi 3045 . . . . . . . . . . . . . . . . . 18  |-  ( A. y  e.  ( C [,] D ) ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q )  <->  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  =  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
)
269267, 268mpbi 208 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  =  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q }
270269uneq2i 3660 . . . . . . . . . . . . . . . 16  |-  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } )  =  ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } )
271270fveq2i 5875 . . . . . . . . . . . . . . 15  |-  ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) )  =  (
# `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
272271oveq1i 6305 . . . . . . . . . . . . . 14  |-  ( (
# `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 )  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  - 
1 )
27336, 272eqtri 2496 . . . . . . . . . . . . 13  |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  - 
1 )
274 isoeq5 6218 . . . . . . . . . . . . . . . . 17  |-  ( ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } )  =  ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } )  ->  (
f  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) ) )
275270, 274ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  <->  f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) )
276275ax-gen 1601 . . . . . . . . . . . . . . 15  |-  A. f
( f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) )  <->  f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) )
277 iotabi 5566 . . . . . . . . . . . . . . 15  |-  ( A. f ( f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) )  <->  f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) )  -> 
( iota f f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) ) )  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) ) ) )
278276, 277ax-mp 5 . . . . . . . . . . . . . 14  |-  ( iota f f  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) ) )  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) ) )
27943, 278eqtri 2496 . . . . . . . . . . . . 13  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) ) )
280 eqid 2467 . . . . . . . . . . . . 13  |-  ( ( S `  j )  +  ( B  -  ( E `  ( S `
 j ) ) ) )  =  ( ( S `  j
)  +  ( B  -  ( E `  ( S `  j ) ) ) )
28115, 14, 16, 17, 18, 19, 26, 273, 279, 65, 78, 280fourierdlem65 31795 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( j  +  1 ) ) )  -  ( Z `  ( E `
 ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) ) )
282262, 281vtoclg 3176 . . . . . . . . . . 11  |-  ( J  e.  ( 0..^ N )  ->  ( ( ph  /\  J  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( Z `  ( E `
 ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
28354, 250, 282sylc 60 . . . . . . . . . 10  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) )
284283eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  -  ( S `  J )
)  =  ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( Z `  ( E `  ( S `
 J ) ) ) ) )
285249, 284breqtrd 4477 . . . . . . . 8  |-  ( ph  ->  0  <  ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( Z `  ( E `  ( S `
 J ) ) ) ) )
28688, 68posdifd 10151 . . . . . . . 8  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) )  <  ( E `
 ( S `  ( J  +  1
) ) )  <->  0  <  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) ) ) )
287285, 286mpbird 232 . . . . . . 7  |-  ( ph  ->  ( Z `  ( E `  ( S `  J ) ) )  <  ( E `  ( S `  ( J  +  1 ) ) ) )
288 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  J  e.  ( 0..^ N ) )  ->  J  e.  ( 0..^ N ) )
289258, 255oveq12d 6313 . . . . . . . . . . . 12  |-  ( j  =  J  ->  (
( Z `  ( E `  ( S `  j ) ) ) (,) ( E `  ( S `  ( j  +  1 ) ) ) )  =  ( ( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) )
290256fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
I `  ( S `  j ) )  =  ( I `  ( S `  J )
) )
291290fveq2d 5876 . . . . . . . . . . . . 13  |-  ( j  =  J  ->  ( Q `  ( I `  ( S `  j
) ) )  =  ( Q `  (
I `  ( S `  J ) ) ) )
292290oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
( I `  ( S `  j )
)  +  1 )  =  ( ( I `
 ( S `  J ) )  +  1 ) )
293292fveq2d 5876 . . . . . . . . . . . . 13  |-  ( j  =  J  ->  ( Q `  ( (
I `  ( S `  j ) )  +  1 ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) )
294291, 293oveq12d 6313 . . . . . . . . . . . 12  |-  ( j  =  J  ->  (
( Q `  (
I `  ( S `  j ) ) ) (,) ( Q `  ( ( I `  ( S `  j ) )  +  1 ) ) )  =  ( ( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )
295289, 294sseq12d 3538 . . . . . . . . . . 11  |-  ( j  =  J  ->  (
( ( Z `  ( E `  ( S `
 j ) ) ) (,) ( E `
 ( S `  ( j  +  1 ) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  j ) ) ) (,) ( Q `  ( (
I `  ( S `  j ) )  +  1 ) ) )  <-> 
( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) )
296252, 295imbi12d 320 . . . . . . . . . 10  |-  ( j  =  J  ->  (
( ( ph  /\  j  e.  ( 0..^ N ) )  -> 
( ( Z `  ( E `  ( S `
 j ) ) ) (,) ( E `
 ( S `  ( j  +  1 ) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  j ) ) ) (,) ( Q `  ( (
I `  ( S `  j ) )  +  1 ) ) ) )  <->  ( ( ph  /\  J  e.  ( 0..^ N ) )  -> 
( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) ) )
297 eqid 2467 . . . . . . . . . . 11  |-  ( ( S `  j )  +  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  =  ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )
29814, 15, 16, 17, 18, 21, 25, 26, 31, 36, 43, 65, 78, 297, 174fourierdlem79 31809 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( Z `
 ( E `  ( S `  j ) ) ) (,) ( E `  ( S `  ( j  +  1 ) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  j ) ) ) (,) ( Q `  ( (
I `  ( S `  j ) )  +  1 ) ) ) )
299296, 298vtoclg 3176 . . . . . . . . 9  |-  ( J  e.  ( 0..^ N )  ->  ( ( ph  /\  J  e.  ( 0..^ N ) )  ->  ( ( Z `
 ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) )
300288, 299mpcom 36 . . . . . . . 8  |-  ( (
ph  /\  J  e.  ( 0..^ N ) )  ->  ( ( Z `
 ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )
30195, 54, 300syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )
302 eqid 2467 . . . . . . 7  |-  if ( ( Z `  ( E `  ( S `  J ) ) )  =  ( Q `  ( I `  ( S `  J )
) ) ,  ( V `  ( I `
 ( S `  J ) ) ) ,  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) `  ( Z `
 ( E `  ( S `  J ) ) ) ) )  =  if ( ( Z `  ( E `
 ( S `  J ) ) )  =  ( Q `  ( I `  ( S `  J )
) ) ,  ( V `  ( I `
 ( S `  J ) ) ) ,  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) `  ( Z `
 ( E `  ( S `  J ) ) ) ) )
303 eqid 2467 . . . . . . 7  |-  ( (
TopOpen ` fld )t  ( ( Q `  ( I `  ( S `  J )
) ) [,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )  =  ( (
TopOpen ` fld )t  ( ( Q `  ( I `  ( S `  J )
) ) [,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )
304179, 182, 193, 204, 238, 88, 68, 287, 301, 302, 303fourierdlem32 31762 . . . . . 6  |-  ( ph  ->  if ( ( Z `
 ( E `  ( S `  J ) ) )  =  ( Q `  ( I `
 ( S `  J ) ) ) ,  ( V `  ( I `  ( S `  J )
) ) ,  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) `  ( Z `  ( E `
 ( S `  J ) ) ) ) )  e.  ( ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( Z `  ( E `
 ( S `  J ) ) ) ) )
305 resabs1 5308 . . . . . . . 8  |-  ( ( ( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) )  C_  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) )  ->  (
( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )  |`  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) )  =  ( F  |`  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) ) )
306301, 305syl 16 . . . . . . 7  |-  ( ph  ->  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) )  =  ( F  |`  (
( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) )
307306oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( Z `  ( E `
 ( S `  J ) ) ) )  =  ( ( F  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( Z `  ( E `
 ( S `  J ) ) ) ) )
308304, 307eleqtrd 2557 . . . . 5  |-  ( ph  ->  if ( ( Z `
 ( E `  ( S `  J ) ) )  =  ( Q `  ( I `
 ( S `  J ) ) ) ,  ( V `  ( I `  ( S `  J )
) ) ,  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) `  ( Z `  ( E `
 ( S `  J ) ) ) ) )  e.  ( ( F  |`  (
( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( Z `  ( E `
 ( S `  J ) ) ) ) )
3095, 7, 11, 71, 72, 91, 161, 308limcperiod 31493 . . . 4  |-  ( ph  ->  if ( ( Z `
 ( E `  ( S `  J ) ) )  =  ( Q `  ( I `
 ( S `  J ) ) ) ,  ( V `  ( I `  ( S `  J )
) ) ,  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) `  ( Z `  ( E `
 ( S `  J ) ) ) ) )  e.  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) } ) lim CC  ( ( Z `  ( E `
 ( S `  J ) ) )  +  U ) ) )
31013oveq2i 6306 . . . . . . 7  |-  ( ( Z `  ( E `
 ( S `  J ) ) )  +  U )  =  ( ( Z `  ( E `  ( S `
 J ) ) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )
311310a1i 11 . . . . . 6  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) )  +  U )  =  ( ( Z `
 ( E `  ( S `  J ) ) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `
 ( S `  ( J  +  1
) ) ) ) ) )
31218, 21iccssred 31426 . . . . . . . . . . . . 13  |-  ( ph  ->  ( C [,] D
)  C_  RR )
31312a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  C_  CC )
314312, 313sstrd 3519 . . . . . . . . . . . 12  |-  ( ph  ->  ( C [,] D
)  C_  CC )
31526, 47, 46fourierdlem15 31745 . . . . . . . . . . . . 13  |-  ( ph  ->  S : ( 0 ... N ) --> ( C [,] D ) )
316315, 83ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  J
)  e.  ( C [,] D ) )
317314, 316sseldd 3510 . . . . . . . . . . 11  |-  ( ph  ->  ( S `  J
)  e.  CC )
318120, 317subcld 9942 . . . . . . . . . 10  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  -  ( S `  J )
)  e.  CC )
31988recnd 9634 . . . . . . . . . 10  |-  ( ph  ->  ( Z `  ( E `  ( S `  J ) ) )  e.  CC )
320119, 318, 319subsub23d 31374 . . . . . . . . 9  |-  ( ph  ->  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) )  =  ( Z `  ( E `
 ( S `  J ) ) )  <-> 
( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) ) )
321283, 320mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) )  =  ( Z `  ( E `  ( S `
 J ) ) ) )
322321eqcomd 2475 . . . . . . 7  |-  ( ph  ->  ( Z `  ( E `  ( S `  J ) ) )  =  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) ) )
323322oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )  =  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `
 ( S `  ( J  +  1
) ) ) ) ) )
324321, 319eqeltrd 2555 . . . . . . . 8  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) )  e.  CC )
325324, 120, 119addsub12d 9965 . . . . . . 7  |-  ( ph  ->  ( ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `
 (