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

Theorem fourierdlem91 31821
Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem91.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 ) ) ) } )
fourierdlem91.t  |-  T  =  ( B  -  A
)
fourierdlem91.m  |-  ( ph  ->  M  e.  NN )
fourierdlem91.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem91.f  |-  ( ph  ->  F : RR --> CC )
fourierdlem91.6  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fourierdlem91.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem91.l  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem91.c  |-  ( ph  ->  C  e.  RR )
fourierdlem91.d  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
fourierdlem91.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 ) ) ) } )
fourierdlem91.h  |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
fourierdlem91.n  |-  N  =  ( ( # `  H
)  -  1 )
fourierdlem91.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
fourierdlem91.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem91.J  |-  Z  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
fourierdlem91.17  |-  ( ph  ->  J  e.  ( 0..^ N ) )
fourierdlem91.u  |-  U  =  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) )
fourierdlem91.i  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ,  RR ,  <  ) )
fourierdlem91.w  |-  W  =  ( i  e.  ( 0..^ M )  |->  L )
Assertion
Ref Expression
fourierdlem91  |-  ( ph  ->  if ( ( E `
 ( S `  ( J  +  1
) ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ,  ( W `
 ( I `  ( S `  J ) ) ) ,  ( F `  ( E `
 ( S `  ( J  +  1
) ) ) ) )  e.  ( ( F  |`  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) ) ) lim CC  ( S `  ( J  +  1 ) ) ) )
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, H    x, H    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, W, 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)    S( m)    T( m, p)    U( f, i, k, m, p)    E( m, p)    F( f,
k, m, p)    H( y, i, k, m, p)    I( m, p)    J( f,
k, m, p)    L( x, y, f, i, k, m, p)    M( y,
f, k)    O( x, y, f, i, k, m, p)    W( f, i, k, m, p)    Z( f,
k, m, p)

Proof of Theorem fourierdlem91
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 fourierdlem91.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 fourierdlem91.u . . . . . . 7  |-  U  =  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) )
14 fourierdlem91.t . . . . . . . . . . . . . . 15  |-  T  =  ( B  -  A
)
15 fourierdlem91.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 fourierdlem91.m . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
17 fourierdlem91.q . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( P `
 M ) )
18 fourierdlem91.c . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR )
19 fourierdlem91.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 fourierdlem91.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 fourierdlem91.n . . . . . . . . . . . . . . . 16  |-  N  =  ( ( # `  H
)  -  1 )
33 fourierdlem91.h . . . . . . . . . . . . . . . . . 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 fourierdlem91.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 fourierdlem91.17 . . . . . . . . . 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 fourierdlem91.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 fourierdlem91.J . . . . . . . . . . 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 ) )
10014a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  =  ( B  -  A ) )
101100eqcomd 2475 . . . . . . . . . . . . . . . 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 fourierdlem91.6 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
158157idi 2 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
159158adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
160114, 116, 155, 156, 159fperiodmul 31404 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  ( ( U  /  T )  x.  T
) ) )  =  ( F `  y
) )
161112, 113, 1603eqtrd 2512 . . . . . 6  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  U ) )  =  ( F `  y
) )
16292, 94, 161syl2anc 661 . . . . 5  |-  ( (
ph  /\  y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) )  ->  ( F `  ( y  +  U
) )  =  ( F `  y ) )
16315fourierdlem2 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 ) ) ) ) ) )
16416, 163syl 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 ) ) ) ) ) )
16517, 164mpbid 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 ) ) ) ) )
166165simpld 459 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
167 elmapi 7452 . . . . . . . . . 10  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
168166, 167syl 16 . . . . . . . . 9  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
16995, 168syl 16 . . . . . . . 8  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
170 elfzofz 11823 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
171170ssriv 3513 . . . . . . . . . 10  |-  ( 0..^ M )  C_  (
0 ... M )
172171a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ M ) 
C_  ( 0 ... M ) )
17395, 16syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
17495, 17syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( P `
 M ) )
175 fourierdlem91.i . . . . . . . . . . . 12  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `  ( E `  x ) ) } ,  RR ,  <  ) )
17615, 173, 174, 14, 65, 78, 175fourierdlem37 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 ) ) } ) ) )
177176simpld 459 . . . . . . . . . 10  |-  ( ph  ->  I : RR --> ( 0..^ M ) )
178177, 84ffvelrnd 6033 . . . . . . . . 9  |-  ( ph  ->  ( I `  ( S `  J )
)  e.  ( 0..^ M ) )
179172, 178sseldd 3510 . . . . . . . 8  |-  ( ph  ->  ( I `  ( S `  J )
)  e.  ( 0 ... M ) )
180169, 179ffvelrnd 6033 . . . . . . 7  |-  ( ph  ->  ( Q `  (
I `  ( S `  J ) ) )  e.  RR )
181 fzofzp1 11889 . . . . . . . . 9  |-  ( ( I `  ( S `
 J ) )  e.  ( 0..^ M )  ->  ( (
I `  ( S `  J ) )  +  1 )  e.  ( 0 ... M ) )
182178, 181syl 16 . . . . . . . 8  |-  ( ph  ->  ( ( I `  ( S `  J ) )  +  1 )  e.  ( 0 ... M ) )
183169, 182ffvelrnd 6033 . . . . . . 7  |-  ( ph  ->  ( Q `  (
( I `  ( S `  J )
)  +  1 ) )  e.  RR )
184165simprd 463 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
185184simprd 463 . . . . . . . 8  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
18615, 16, 17, 14, 65, 78, 175fourierdlem37 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 ) ) } ) ) )
187186simpld 459 . . . . . . . . 9  |-  ( ph  ->  I : RR --> ( 0..^ M ) )
188187, 84ffvelrnd 6033 . . . . . . . 8  |-  ( ph  ->  ( I `  ( S `  J )
)  e.  ( 0..^ M ) )
189 fveq2 5872 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( Q `  i )  =  ( Q `  ( I `
 ( S `  J ) ) ) )
190 oveq1 6302 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( i  +  1 )  =  ( ( I `  ( S `  J ) )  +  1 ) )
191190fveq2d 5876 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) )
192189, 191breq12d 4466 . . . . . . . . 9  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( Q `  i )  <  ( Q `  (
i  +  1 ) )  <->  ( Q `  ( I `  ( S `  J )
) )  <  ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )
193192rspccva 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 ) ) )
194185, 188, 193syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( Q `  (
I `  ( S `  J ) ) )  <  ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) )
19595, 188jca 532 . . . . . . . 8  |-  ( ph  ->  ( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) ) )
196 eleq1 2539 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( i  e.  ( 0..^ M )  <-> 
( I `  ( S `  J )
)  e.  ( 0..^ M ) ) )
197196anbi2d 703 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( ph  /\  i  e.  ( 0..^ M ) )  <-> 
( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) ) ) )
198189, 191oveq12d 6313 . . . . . . . . . . . 12  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  =  ( ( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )
199198reseq2d 5279 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( F  |`  ( ( Q `  ( I `  ( S `  J
) ) ) (,) ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ) ) )
200198oveq1d 6310 . . . . . . . . . . 11  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC )  =  ( ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )
-cn-> CC ) )
201199, 200eleq12d 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 ) ) )
202197, 201imbi12d 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 ) ) ) )
203 fourierdlem91.fcn . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
204202, 203vtoclg 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 ) ) )
205188, 195, 204sylc 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 ) )
206 nfcv 2629 . . . . . . . . 9  |-  F/_ i
( I `  ( S `  J )
)
207 nfv 1683 . . . . . . . . . 10  |-  F/ i ( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )
208 fourierdlem91.w . . . . . . . . . . . . 13  |-  W  =  ( i  e.  ( 0..^ M )  |->  L )
209 nfmpt1 4542 . . . . . . . . . . . . 13  |-  F/_ i
( i  e.  ( 0..^ M )  |->  L )
210208, 209nfcxfr 2627 . . . . . . . . . . . 12  |-  F/_ i W
211210, 206nffv 5879 . . . . . . . . . . 11  |-  F/_ i
( W `  (
I `  ( S `  J ) ) )
212 nfcv 2629 . . . . . . . . . . 11  |-  F/_ i
( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) )
213211, 212nfel 2642 . . . . . . . . . 10  |-  F/ i ( W `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) )
214207, 213nfim 1867 . . . . . . . . 9  |-  F/ i ( ( ph  /\  ( I `  ( S `  J )
)  e.  ( 0..^ M ) )  -> 
( W `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) ) )
215197biimpar 485 . . . . . . . . . . . . . 14  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ph  /\  i  e.  ( 0..^ M ) ) )
2162153adant2 1015 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ph  /\  i  e.  ( 0..^ M ) ) )
217 simp2 997 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) ) )
218216, 217mpd 15 . . . . . . . . . . . 12  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
219 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( W `  i )  =  ( W `  ( I `
 ( S `  J ) ) ) )
220219eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( W `  ( I `  ( S `  J )
) )  =  ( W `  i ) )
221220adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( W `  ( I `  ( S `  J
) ) )  =  ( W `  i
) )
222215simprd 463 . . . . . . . . . . . . . . . 16  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  i  e.  ( 0..^ M ) )
223 fourierdlem91.l . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
224 elex 3127 . . . . . . . . . . . . . . . . 17  |-  ( L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  ->  L  e.  _V )
225215, 223, 2243syl 20 . . . . . . . . . . . . . . . 16  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  L  e.  _V )
226208fvmpt2 5964 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ M )  /\  L  e.  _V )  ->  ( W `  i )  =  L )
227222, 225, 226syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( W `  i )  =  L )
228221, 227eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ph  /\  ( I `
 ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( W `  ( I `  ( S `  J
) ) )  =  L )
2292283adant2 1015 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( W `  ( I `  ( S `  J )
) )  =  L )
230199, 191oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  ( I `  ( S `  J
) ) ) (,) ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ) ) lim CC  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) ) )
231230eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( ( F  |`  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
2322313ad2ant1 1017 . . . . . . . . . . . . 13  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )
233229, 232eleq12d 2549 . . . . . . . . . . . 12  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( ( W `
 ( I `  ( S `  J ) ) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) )  <->  L  e.  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) ) )
234218, 233mpbird 232 . . . . . . . . . . 11  |-  ( ( i  =  ( I `
 ( S `  J ) )  /\  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  /\  ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) ) )  ->  ( W `  ( I `  ( S `  J )
) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) ) )
2352343exp 1195 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  ->  (
( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )  ->  ( W `  ( I `  ( S `  J )
) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) ) ) ) )
236223a1ii 27 . . . . . . . . . 10  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  (
I `  ( S `  J ) )  e.  ( 0..^ M ) )  ->  ( W `  ( I `  ( S `  J )
) )  e.  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `  ( ( I `  ( S `
 J ) )  +  1 ) ) ) )  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) ) ) )
237235, 236impbid 191 . . . . . . . . 9  |-  ( i  =  ( I `  ( S `  J ) )  ->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  <->  ( ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) )  -> 
( W `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) ) ) ) )
238206, 214, 237, 223vtoclgf 3174 . . . . . . . 8  |-  ( ( I `  ( S `
 J ) )  e.  ( 0..^ M )  ->  ( ( ph  /\  ( I `  ( S `  J ) )  e.  ( 0..^ M ) )  -> 
( W `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) ) ) )
239188, 195, 238sylc 60 . . . . . . 7  |-  ( ph  ->  ( W `  (
I `  ( S `  J ) ) )  e.  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) lim CC  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) ) )
24050simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S `
 0 )  =  C  /\  ( S `
 N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) )
241240simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  A. i  e.  ( 0..^ N ) ( S `  i )  <  ( S `  ( i  +  1 ) ) )
242 fveq2 5872 . . . . . . . . . . . . 13  |-  ( i  =  J  ->  ( S `  i )  =  ( S `  J ) )
243 oveq1 6302 . . . . . . . . . . . . . 14  |-  ( i  =  J  ->  (
i  +  1 )  =  ( J  + 
1 ) )
244243fveq2d 5876 . . . . . . . . . . . . 13  |-  ( i  =  J  ->  ( S `  ( i  +  1 ) )  =  ( S `  ( J  +  1
) ) )
245242, 244breq12d 4466 . . . . . . . . . . . 12  |-  ( i  =  J  ->  (
( S `  i
)  <  ( S `  ( i  +  1 ) )  <->  ( S `  J )  <  ( S `  ( J  +  1 ) ) ) )
246245rspccva 3218 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( 0..^ N ) ( S `  i )  <  ( S `  ( i  +  1 ) )  /\  J  e.  ( 0..^ N ) )  ->  ( S `  J )  <  ( S `  ( J  +  1 ) ) )
247241, 54, 246syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
248 posdif 10057 . . . . . . . . . . 11  |-  ( ( ( S `  J
)  e.  RR  /\  ( S `  ( J  +  1 ) )  e.  RR )  -> 
( ( S `  J )  <  ( S `  ( J  +  1 ) )  <->  0  <  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
24984, 57, 248syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( S `  J )  <  ( S `  ( J  +  1 ) )  <->  0  <  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
250247, 249mpbid 210 . . . . . . . . 9  |-  ( ph  ->  0  <  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) )
251 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  J  e.  ( 0..^ N ) )  ->  J  e.  ( 0..^ N ) )
252 eleq1 2539 . . . . . . . . . . . . . . 15  |-  ( j  =  J  ->  (
j  e.  ( 0..^ N )  <->  J  e.  ( 0..^ N ) ) )
253252anbi2d 703 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
( ph  /\  j  e.  ( 0..^ N ) )  <->  ( ph  /\  J  e.  ( 0..^ N ) ) ) )
254 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  J  ->  (
j  +  1 )  =  ( J  + 
1 ) )
255254fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( j  =  J  ->  ( S `  ( j  +  1 ) )  =  ( S `  ( J  +  1
) ) )
256255fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( j  =  J  ->  ( E `  ( S `  ( j  +  1 ) ) )  =  ( E `  ( S `  ( J  +  1 ) ) ) )
257 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  J  ->  ( S `  j )  =  ( S `  J ) )
258257fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( j  =  J  ->  ( E `  ( S `  j ) )  =  ( E `  ( S `  J )
) )
259258fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( j  =  J  ->  ( Z `  ( E `  ( S `  j
) ) )  =  ( Z `  ( E `  ( S `  J ) ) ) )
260256, 259oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( j  =  J  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  j ) ) ) )  =  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) ) )
261255, 257oveq12d 6313 . . . . . . . . . . . . . . 15  |-  ( j  =  J  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  =  ( ( S `
 ( J  + 
1 ) )  -  ( S `  J ) ) )
262260, 261eqeq12d 2489 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
263253, 262imbi12d 320 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) )
26414oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  x.  T )  =  ( k  x.  ( B  -  A )
)
265264oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  +  ( k  x.  T ) )  =  ( y  +  ( k  x.  ( B  -  A ) ) )
266265eleq1i 2544 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( k  x.  ( B  -  A
) ) )  e. 
ran  Q )
267266rexbii 2969 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q )
268267rgenw 2828 . . . . . . . . . . . . . . . . . . 19  |-  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
)
269 rabbi 3045 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 }
)
270268, 269mpbi 208 . . . . . . . . . . . . . . . . . 18  |-  { 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 }
271270uneq2i 3660 . . . . . . . . . . . . . . . . 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 } )
272271fveq2i 5875 . . . . . . . . . . . . . . . 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 } ) )
273272oveq1i 6305 . . . . . . . . . . . . . . 15  |-  ( (
# `  ( { 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 )
27436, 273eqtri 2496 . . . . . . . . . . . . . 14  |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  - 
1 )
275 isoeq5 6218 . . . . . . . . . . . . . . . . . 18  |-  ( ( { 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 }
) ) ) )
276271, 275ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( 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 }
) ) )
277276ax-gen 1601 . . . . . . . . . . . . . . . 16  |-  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 }
) ) )
278 iotabi 5566 . . . . . . . . . . . . . . . 16  |-  ( 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 } ) ) ) )
279277, 278ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 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 } ) ) )
28043, 279eqtri 2496 . . . . . . . . . . . . . 14  |-  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 } ) ) )
281 eqid 2467 . . . . . . . . . . . . . 14  |-  ( ( S `  j )  +  ( B  -  ( E `  ( S `
 j ) ) ) )  =  ( ( S `  j
)  +  ( B  -  ( E `  ( S `  j ) ) ) )
28215, 14, 16, 17, 18, 19, 26, 274, 280, 65, 78, 281fourierdlem65 31795 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( j  +  1 ) ) )  -  ( Z `  ( E `
 ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) ) )
283263, 282vtoclg 3176 . . . . . . . . . . . 12  |-  ( J  e.  ( 0..^ N )  ->  ( ( ph  /\  J  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( Z `  ( E `
 ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) ) )
284251, 283mpcom 36 . . . . . . . . . . 11  |-  ( (
ph  /\  J  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( J  +  1
) ) )  -  ( Z `  ( E `
 ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1 ) )  -  ( S `  J ) ) )
28595, 54, 284syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) )  =  ( ( S `  ( J  +  1
) )  -  ( S `  J )
) )
286285eqcomd 2475 . . . . . . . . 9  |-  ( ph  ->  ( ( S `  ( J  +  1
) )  -  ( S `  J )
)  =  ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( Z `  ( E `  ( S `
 J ) ) ) ) )
287250, 286breqtrd 4477 . . . . . . . 8  |-  ( ph  ->  0  <  ( ( E `  ( S `
 ( J  + 
1 ) ) )  -  ( Z `  ( E `  ( S `
 J ) ) ) ) )
28888, 68posdifd 10151 . . . . . . . 8  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) )  <  ( E `
 ( S `  ( J  +  1
) ) )  <->  0  <  ( ( E `  ( S `  ( J  +  1 ) ) )  -  ( Z `
 ( E `  ( S `  J ) ) ) ) ) )
289287, 288mpbird 232 . . . . . . 7  |-  ( ph  ->  ( Z `  ( E `  ( S `  J ) ) )  <  ( E `  ( S `  ( J  +  1 ) ) ) )
290259, 256oveq12d 6313 . . . . . . . . . . . 12  |-  ( j  =  J  ->  (
( Z `  ( E `  ( S `  j ) ) ) (,) ( E `  ( S `  ( j  +  1 ) ) ) )  =  ( ( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) )
291257fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
I `  ( S `  j ) )  =  ( I `  ( S `  J )
) )
292291fveq2d 5876 . . . . . . . . . . . . 13  |-  ( j  =  J  ->  ( Q `  ( I `  ( S `  j
) ) )  =  ( Q `  (
I `  ( S `  J ) ) ) )
293291oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( j  =  J  ->  (
( I `  ( S `  j )
)  +  1 )  =  ( ( I `
 ( S `  J ) )  +  1 ) )
294293fveq2d 5876 . . . . . . . . . . . . 13  |-  ( j  =  J  ->  ( Q `  ( (
I `  ( S `  j ) )  +  1 ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) )
295292, 294oveq12d 6313 . . . . . . . . . . . 12  |-  ( j  =  J  ->  (
( Q `  (
I `  ( S `  j ) ) ) (,) ( Q `  ( ( I `  ( S `  j ) )  +  1 ) ) )  =  ( ( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) )
296290, 295sseq12d 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 ) ) ) ) )
297253, 296imbi12d 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 ) ) ) ) ) )
29833, 31eqtri 2496 . . . . . . . . . . 11  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
299 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
) ) )
30014, 15, 16, 17, 18, 21, 25, 26, 298, 32, 37, 65, 78, 299, 175fourierdlem79 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 ) ) ) )
301297, 300vtoclg 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 ) ) ) ) )
302251, 301mpcom 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 ) ) ) )
30395, 54, 302syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )
304 eqid 2467 . . . . . . 7  |-  if ( ( E `  ( S `  ( J  +  1 ) ) )  =  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) ,  ( W `  (
I `  ( S `  J ) ) ) ,  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) `  ( E `
 ( S `  ( J  +  1
) ) ) ) )  =  if ( ( E `  ( S `  ( J  +  1 ) ) )  =  ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) ,  ( W `  (
I `  ( S `  J ) ) ) ,  ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) ) `  ( E `
 ( S `  ( J  +  1
) ) ) ) )
305 eqid 2467 . . . . . . 7  |-  ( (
TopOpen ` fld )t  ( ( ( Q `
 ( I `  ( S `  J ) ) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) )  u.  { ( Q `
 ( ( I `
 ( S `  J ) )  +  1 ) ) } ) )  =  ( ( TopOpen ` fld )t  ( ( ( Q `  ( I `
 ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) )  u.  {
( Q `  (
( I `  ( S `  J )
)  +  1 ) ) } ) )
306180, 183, 194, 205, 239, 88, 68, 289, 303, 304, 305fourierdlem33 31763 . . . . . 6  |-  ( ph  ->  if ( ( E `
 ( S `  ( J  +  1
) ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ,  ( W `
 ( I `  ( S `  J ) ) ) ,  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) `  ( E `  ( S `
 ( J  + 
1 ) ) ) ) )  e.  ( ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( E `  ( S `
 ( J  + 
1 ) ) ) ) )
307 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
) ) ) ) ) )
308303, 307syl 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 ) ) ) ) ) )
309308oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( ( ( F  |`  ( ( Q `  ( I `  ( S `  J )
) ) (,) ( Q `  ( (
I `  ( S `  J ) )  +  1 ) ) ) )  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( E `  ( S `
 ( J  + 
1 ) ) ) )  =  ( ( F  |`  ( ( Z `  ( E `  ( S `  J
) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( E `  ( S `
 ( J  + 
1 ) ) ) ) )
310306, 309eleqtrd 2557 . . . . 5  |-  ( ph  ->  if ( ( E `
 ( S `  ( J  +  1
) ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ,  ( W `
 ( I `  ( S `  J ) ) ) ,  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) `  ( E `  ( S `
 ( J  + 
1 ) ) ) ) )  e.  ( ( F  |`  (
( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) ) lim CC  ( E `  ( S `
 ( J  + 
1 ) ) ) ) )
3115, 7, 11, 71, 72, 91, 162, 310limcperiod 31493 . . . 4  |-  ( ph  ->  if ( ( E `
 ( S `  ( J  +  1
) ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ,  ( W `
 ( I `  ( S `  J ) ) ) ,  ( ( F  |`  (
( Q `  (
I `  ( S `  J ) ) ) (,) ( Q `  ( ( I `  ( S `  J ) )  +  1 ) ) ) ) `  ( E `  ( S `
 ( J  + 
1 ) ) ) ) )  e.  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) } ) lim CC  ( ( E `  ( S `
 ( J  + 
1 ) ) )  +  U ) ) )
31213oveq2i 6306 . . . . . . 7  |-  ( ( E `  ( S `
 ( J  + 
1 ) ) )  +  U )  =  ( ( E `  ( S `  ( J  +  1 ) ) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )
313312a1i 11 . . . . . 6  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  +  U )  =  ( ( E `
 ( S `  ( J  +  1
) ) )  +  ( ( S `  ( J  +  1
) )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) ) )
314119, 120pncan3d 9945 . . . . . 6  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  +  ( ( S `  ( J  +  1 ) )  -  ( E `  ( S `  ( J  +  1 ) ) ) ) )  =  ( S `  ( J  +  1 ) ) )
315313, 314eqtrd 2508 . . . . 5  |-  ( ph  ->  ( ( E `  ( S `  ( J  +  1 ) ) )  +  U )  =  ( S `  ( J  +  1
) ) )
316315oveq2d 6311 . . . 4  |-  ( ph  ->  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `  J ) ) ) (,) ( E `  ( S `  ( J  +  1 ) ) ) ) x  =  ( y  +  U
) } ) lim CC  ( ( E `  ( S `  ( J  +  1 ) ) )  +  U ) )  =  ( ( F  |`  { x  e.  CC  |  E. y  e.  ( ( Z `  ( E `  ( S `
 J ) ) ) (,) ( E `
 ( S `  ( J  +  1
) ) ) ) x  =  ( y  +  U ) } ) lim CC  ( S `
 ( J  + 
1 ) ) ) )
317311, 316eleqtrd 2557 . . 3  |-  ( ph  ->  if ( ( E `
 ( S `  ( J  +  1
) ) )  =  ( Q `  (
( I `  ( S `  J )
)  +  1 ) ) ,  ( W `
 ( I `  ( S `  J