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

Theorem fourierdlem65 31795
Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem65.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 ) ) ) } )
fourierdlem65.t  |-  T  =  ( B  -  A
)
fourierdlem65.m  |-  ( ph  ->  M  e.  NN )
fourierdlem65.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem65.c  |-  ( ph  ->  C  e.  RR )
fourierdlem65.d  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
fourierdlem65.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 ) ) ) } )
fourierdlem65.n  |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  - 
1 )
fourierdlem65.s  |-  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 } ) ) )
fourierdlem65.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem65.l  |-  L  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
fourierdlem65.z  |-  Z  =  ( ( S `  j )  +  ( B  -  ( E `
 ( S `  j ) ) ) )
Assertion
Ref Expression
fourierdlem65  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( j  +  1 ) ) )  -  ( L `  ( E `
 ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( 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    i, E, k, x, y    i, M, m, p    f, N, y    i, N, m, p    x, N    Q, f, k, y    Q, i, x    Q, p    S, f, k, y    S, i, x    S, p    T, i, k, x, y    i, Z, k, y    ph, f,
k, y    i, j,
k, x, y    ph, i, x
Allowed substitution hints:    ph( j, m, p)    A( j)    B( j)    C( j, k)    D( j, k)    P( x, y, f, i, j, k, m, p)    Q( j, m)    S( j, m)    T( f, j, m, p)    E( f,
j, m, p)    L( x, y, f, i, j, k, m, p)    M( x, y, f, j, k)    N( j, k)    O( x, y, f, i, j, k, m, p)    Z( x, f, j, m, p)

Proof of Theorem fourierdlem65
StepHypRef Expression
1 fourierdlem65.l . . . . . 6  |-  L  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
21a1i 11 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  L  =  ( y  e.  ( A (,] B
)  |->  if ( y  =  B ,  A ,  y ) ) )
3 simpr 461 . . . . . . . 8  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =  ( E `
 ( S `  j ) ) )
4 simpl 457 . . . . . . . 8  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
( E `  ( S `  j )
)  =  B )
53, 4eqtrd 2508 . . . . . . 7  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =  B )
6 iftrue 3951 . . . . . . 7  |-  ( y  =  B  ->  if ( y  =  B ,  A ,  y )  =  A )
75, 6syl 16 . . . . . 6  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  A )
87adantll 713 . . . . 5  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  A )
9 fourierdlem65.p . . . . . . . . . . 11  |-  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 ) ) ) } )
10 fourierdlem65.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
11 fourierdlem65.q . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
129, 10, 11fourierdlem11 31741 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
1312simp1d 1008 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR )
1412simp2d 1009 . . . . . . . . 9  |-  ( ph  ->  B  e.  RR )
1512simp3d 1010 . . . . . . . . 9  |-  ( ph  ->  A  <  B )
16 fourierdlem65.t . . . . . . . . 9  |-  T  =  ( B  -  A
)
17 fourierdlem65.e . . . . . . . . 9  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
1813, 14, 15, 16, 17fourierdlem4 31734 . . . . . . . 8  |-  ( ph  ->  E : RR --> ( A (,] B ) )
1918adantr 465 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E : RR --> ( A (,] B ) )
20 fourierdlem65.c . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR )
21 ioossre 11598 . . . . . . . . . . . . . . . 16  |-  ( C (,) +oo )  C_  RR
22 fourierdlem65.d . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
2321, 22sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( ph  ->  D  e.  RR )
2420rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR* )
25 pnfxr 11333 . . . . . . . . . . . . . . . . 17  |- +oo  e.  RR*
2625a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  -> +oo  e.  RR* )
27 ioogtlb 31415 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR*  /\ +oo  e.  RR*  /\  D  e.  ( C (,) +oo ) )  ->  C  <  D )
2824, 26, 22, 27syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  <  D )
29 fourierdlem65.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 ) ) ) } )
30 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  x  ->  y  =  x )
3116eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  -  A )  =  T
3231oveq2i 6306 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  x.  ( B  -  A ) )  =  ( k  x.  T
)
3332a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  x  ->  (
k  x.  ( B  -  A ) )  =  ( k  x.  T ) )
3430, 33oveq12d 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  x  ->  (
y  +  ( k  x.  ( B  -  A ) ) )  =  ( x  +  ( k  x.  T
) ) )
3534eleq1d 2536 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  (
( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  ( x  +  ( k  x.  T ) )  e.  ran  Q ) )
3635adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  =  x  /\  k  e.  ZZ )  ->  ( ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q  <-> 
( x  +  ( k  x.  T ) )  e.  ran  Q
) )
3736rexbidva 2975 . . . . . . . . . . . . . . . . 17  |-  ( y  =  x  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  E. k  e.  ZZ  (
x  +  ( k  x.  T ) )  e.  ran  Q ) )
3837cbvrabv 3117 . . . . . . . . . . . . . . . 16  |-  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }  =  { x  e.  ( C [,] D )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q }
3938uneq2i 3660 . . . . . . . . . . . . . . 15  |-  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } )  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
40 fourierdlem65.n . . . . . . . . . . . . . . 15  |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  - 
1 )
41 fourierdlem65.s . . . . . . . . . . . . . . 15  |-  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 } ) ) )
4216, 9, 10, 11, 20, 23, 28, 29, 39, 40, 41fourierdlem54 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.  ( B  -  A )
) )  e.  ran  Q } ) ) ) )
4342simpld 459 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
4443simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  ( O `
 N ) )
4543simpld 459 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
4629fourierdlem2 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 ) ) ) ) ) )
4745, 46syl 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 ) ) ) ) ) )
4844, 47mpbid 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 ) ) ) ) )
4948simpld 459 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... N ) ) )
50 elmapi 7452 . . . . . . . . . 10  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
5149, 50syl 16 . . . . . . . . 9  |-  ( ph  ->  S : ( 0 ... N ) --> RR )
5251adantr 465 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> RR )
53 elfzofz 11823 . . . . . . . . 9  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
5453adantl 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
5552, 54ffvelrnd 6033 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
5619, 55ffvelrnd 6033 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E `  ( S `  j ) )  e.  ( A (,] B ) )
5756adantr 465 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  e.  ( A (,] B
) )
5813ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  e.  RR )
592, 8, 57, 58fvmptd 5962 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( L `  ( E `  ( S `  j
) ) )  =  A )
6059oveq2d 6311 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( L `
 ( E `  ( S `  j ) ) ) )  =  ( ( E `  ( S `  ( j  +  1 ) ) )  -  A ) )
6114ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  B  e.  RR )
6215ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  <  B )
6355adantr 465 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  e.  RR )
64 simpr 461 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  =  B )
65 fzofzp1 11889 . . . . . . . . . . 11  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
6665adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
6752, 66ffvelrnd 6033 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
6867adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  ( j  +  1 ) )  e.  RR )
69 elfzoelz 11809 . . . . . . . . . . . . 13  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
70 zre 10880 . . . . . . . . . . . . 13  |-  ( j  e.  ZZ  ->  j  e.  RR )
7169, 70syl 16 . . . . . . . . . . . 12  |-  ( j  e.  ( 0..^ N )  ->  j  e.  RR )
7271adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  RR )
7372ltp1d 10488 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  <  (
j  +  1 ) )
7442simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) ) )
7574adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) )
76 isorel 6221 . . . . . . . . . . 11  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  /\  ( j  e.  ( 0 ... N )  /\  ( j  +  1 )  e.  ( 0 ... N ) ) )  ->  (
j  <  ( j  +  1 )  <->  ( S `  j )  <  ( S `  ( j  +  1 ) ) ) )
7775, 54, 66, 76syl12anc 1226 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  < 
( j  +  1 )  <->  ( S `  j )  <  ( S `  ( j  +  1 ) ) ) )
7873, 77mpbid 210 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
7978adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  <  ( S `  (
j  +  1 ) ) )
80 isof1o 6220 . . . . . . . . . . . . . 14  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  ->  S : ( 0 ... N ) -1-1-onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) )
8174, 80syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  S : ( 0 ... N ) -1-1-onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
82 f1ofo 5829 . . . . . . . . . . . . 13  |-  ( S : ( 0 ... N ) -1-1-onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
)  ->  S :
( 0 ... N
) -onto-> ( { C ,  D }  u.  {
y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q } ) )
8381, 82syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  S : ( 0 ... N ) -onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
8483ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  S : ( 0 ... N ) -onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
8514, 13resubcld 9999 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( B  -  A
)  e.  RR )
8616, 85syl5eqel 2559 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  RR )
8786adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  RR )
8855, 87readdcld 9635 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  T )  e.  RR )
8988adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  RR )
9020adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  e.  RR )
9129, 45, 44fourierdlem15 31745 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  S : ( 0 ... N ) --> ( C [,] D ) )
9291adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> ( C [,] D
) )
9392, 54ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  ( C [,] D ) )
9423adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  D  e.  RR )
95 elicc2 11601 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( S `  j )  e.  ( C [,] D )  <-> 
( ( S `  j )  e.  RR  /\  C  <_  ( S `  j )  /\  ( S `  j )  <_  D ) ) )
9690, 94, 95syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  e.  ( C [,] D
)  <->  ( ( S `
 j )  e.  RR  /\  C  <_ 
( S `  j
)  /\  ( S `  j )  <_  D
) ) )
9793, 96mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  e.  RR  /\  C  <_ 
( S `  j
)  /\  ( S `  j )  <_  D
) )
9897simp2d 1009 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  <_  ( S `  j )
)
9913, 14posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
10015, 99mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  0  <  ( B  -  A ) )
10131a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( B  -  A
)  =  T )
102100, 101breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  <  T )
10386, 102elrpd 11266 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  T  e.  RR+ )
104103adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  RR+ )
10555, 104ltaddrpd 11297 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  (
( S `  j
)  +  T ) )
10690, 55, 88, 98, 105lelttrd 9751 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  <  (
( S `  j
)  +  T ) )
10790, 88, 106ltled 9744 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  <_  (
( S `  j
)  +  T ) )
108107adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  C  <_  ( ( S `
 j )  +  T ) )
10994adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  D  e.  RR )
11067adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( S `  (
j  +  1 ) )  e.  RR )
111 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )
11289, 110ltnled 9743 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( ( S `
 j )  +  T )  <  ( S `  ( j  +  1 ) )  <->  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) ) )
113111, 112mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <  ( S `  ( j  +  1 ) ) )
11492, 66ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  ( C [,] D ) )
115 elicc2 11601 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( S `  ( j  +  1 ) )  e.  ( C [,] D )  <-> 
( ( S `  ( j  +  1 ) )  e.  RR  /\  C  <_  ( S `  ( j  +  1 ) )  /\  ( S `  ( j  +  1 ) )  <_  D ) ) )
11690, 94, 115syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  e.  ( C [,] D
)  <->  ( ( S `
 ( j  +  1 ) )  e.  RR  /\  C  <_ 
( S `  (
j  +  1 ) )  /\  ( S `
 ( j  +  1 ) )  <_  D ) ) )
117114, 116mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  e.  RR  /\  C  <_ 
( S `  (
j  +  1 ) )  /\  ( S `
 ( j  +  1 ) )  <_  D ) )
118117simp3d 1010 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  <_  D
)
119118adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( S `  (
j  +  1 ) )  <_  D )
12089, 110, 109, 113, 119ltletrd 9753 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <  D )
12189, 109, 120ltled 9744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <_  D )
12289, 108, 1213jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( ( S `
 j )  +  T )  e.  RR  /\  C  <_  ( ( S `  j )  +  T )  /\  (
( S `  j
)  +  T )  <_  D ) )
12320ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  C  e.  RR )
12423ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  D  e.  RR )
125 elicc2 11601 . . . . . . . . . . . . . . . . 17  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( ( S `
 j )  +  T )  e.  ( C [,] D )  <-> 
( ( ( S `
 j )  +  T )  e.  RR  /\  C  <_  ( ( S `  j )  +  T )  /\  (
( S `  j
)  +  T )  <_  D ) ) )
126123, 124, 125syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( ( S `
 j )  +  T )  e.  ( C [,] D )  <-> 
( ( ( S `
 j )  +  T )  e.  RR  /\  C  <_  ( ( S `  j )  +  T )  /\  (
( S `  j
)  +  T )  <_  D ) ) )
127122, 126mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  ( C [,] D ) )
128127adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  ( C [,] D ) )
12917a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
130 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( S `  j )  ->  x  =  ( S `  j ) )
131 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  ( S `  j )  ->  ( B  -  x )  =  ( B  -  ( S `  j ) ) )
132131oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( S `  j )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  j ) )  /  T ) )
133132fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( S `  j )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  j )
)  /  T ) ) )
134133oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( S `  j )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )
135130, 134oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( S `  j )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
136135adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  x  =  ( S `  j
) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
13714adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  B  e.  RR )
138137, 55resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( B  -  ( S `  j ) )  e.  RR )
139104rpne0d 11273 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  =/=  0
)
140138, 87, 139redivcld 10384 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( B  -  ( S `  j ) )  /  T )  e.  RR )
141140flcld 11915 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  e.  ZZ )
142141zred 10978 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  e.  RR )
143142, 87remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T )  e.  RR )
14455, 143readdcld 9635 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )  e.  RR )
145129, 136, 55, 144fvmptd 5962 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E `  ( S `  j ) )  =  ( ( S `  j )  +  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
146145oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  =  ( ( ( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  -  ( S `  j ) ) )
147146oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  =  ( ( ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )  -  ( S `
 j ) )  /  T ) )
14855recnd 9634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  CC )
149143recnd 9634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T )  e.  CC )
150148, 149pncan2d 9944 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )  -  ( S `  j ) )  =  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )
151150oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  -  ( S `  j ) )  /  T )  =  ( ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T )  /  T ) )
152142recnd 9634 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  e.  CC )
15387recnd 9634 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  CC )
154152, 153, 139divcan4d 10338 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T )  /  T )  =  ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) ) )
155147, 151, 1543eqtrd 2512 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  =  ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) ) )
156155, 141eqeltrd 2555 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  e.  ZZ )
157 peano2zm 10918 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  e.  ZZ  ->  ( (
( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  e.  ZZ )
158156, 157syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  e.  ZZ )
159158ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  e.  ZZ )
16031oveq2i 6306 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) )  =  ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  T )
161160oveq2i 6306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( S `  j
)  +  T )  +  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  ( B  -  A )
) )  =  ( ( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  T ) )
162161a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) ) )  =  ( ( ( S `
 j )  +  T )  +  ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  T ) ) )
163145adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  =  ( ( S `  j )  +  ( ( |_ `  (
( B  -  ( S `  j )
)  /  T ) )  x.  T ) ) )
164 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( E `  ( S `  j )
)  -  ( S `
 j ) )  =  ( B  -  ( S `  j ) ) )
165164eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E `  ( S `
 j ) )  =  B  ->  ( B  -  ( S `  j ) )  =  ( ( E `  ( S `  j ) )  -  ( S `
 j ) ) )
166165oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( B  -  ( S `  j )
)  /  T )  =  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T ) )
167166fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E `  ( S `
 j ) )  =  B  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  =  ( |_ `  (
( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T ) ) )
168167oveq1d 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( |_ `  (
( B  -  ( S `  j )
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T ) )  x.  T ) )
169168oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
170169adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
171155, 152eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  e.  CC )
172 ax-1cn 9562 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  CC
173172a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  1  e.  CC )
174171, 173, 153subdird 10025 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
)  =  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  ( 1  x.  T
) ) )
17586recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  CC )
176175mulid2d 9626 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( 1  x.  T
)  =  T )
177176oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  -  (
1  x.  T ) )  =  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  T ) )
178177adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  x.  T )  -  (
1  x.  T ) )  =  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  T ) )
179174, 178eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
)  =  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  T ) )
180179oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  T )  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
) )  =  ( ( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  T ) ) )
181171, 153jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  e.  CC  /\  T  e.  CC ) )
182 mulcl 9588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  e.  CC  /\  T  e.  CC )  ->  (
( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  e.  CC )
183181, 182syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  e.  CC )
184183, 153jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  x.  T )  e.  CC  /\  T  e.  CC ) )
185 subcl 9831 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  x.  T
)  e.  CC  /\  T  e.  CC )  ->  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  -  T
)  e.  CC )
186184, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  x.  T )  -  T
)  e.  CC )
187148, 153, 186addassd 9630 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  T )  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  -  T
) )  =  ( ( S `  j
)  +  ( T  +  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  x.  T )  -  T
) ) ) )
188153, 183pncan3d 9945 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( T  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  -  T
) )  =  ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T ) )
189188oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( T  +  ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  x.  T
)  -  T ) ) )  =  ( ( S `  j
)  +  ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  x.  T ) ) )
190187, 189eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  T )  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  -  T
) )  =  ( ( S `  j
)  +  ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  x.  T ) ) )
191 flid 11925 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  e.  ZZ  ->  ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  =  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )
192156, 191syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  =  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )
193192eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  =  ( |_ `  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) ) )
194193oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  =  ( ( |_ `  (
( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T ) )  x.  T ) )
195194oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  x.  T
) )  =  ( ( S `  j
)  +  ( ( |_ `  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )  x.  T ) ) )
196180, 190, 1953eqtrd 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  T )  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
) )  =  ( ( S `  j
)  +  ( ( |_ `  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )  x.  T ) ) )
197196eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  x.  T ) )  =  ( ( ( S `  j
)  +  T )  +  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
) ) )
198197adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  j
)  +  ( ( |_ `  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )  x.  T ) )  =  ( ( ( S `  j )  +  T )  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
) ) )
199163, 170, 1983eqtrrd 2513 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  T ) )  =  ( E `  ( S `  j )
) )
200162, 199, 643eqtrd 2512 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) ) )  =  B )
2019fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) ) ) ) )
20210, 201syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) ) ) )
20311, 202mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
204203simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
205204simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
206205simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Q `  M
)  =  B )
207206eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  =  ( Q `
 M ) )
2089, 10, 11fourierdlem15 31745 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
209 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Q : ( 0 ... M ) --> ( A [,] B )  ->  Q  Fn  ( 0 ... M ) )
210208, 209syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
21110nnnn0d 10864 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  M  e.  NN0 )
212 nn0uz 11128 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
213211, 212syl6eleq 2565 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
214 eluzfz2 11706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
215213, 214syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  ( 0 ... M ) )
216 fnfvelrn 6029 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Q  Fn  ( 0 ... M )  /\  M  e.  ( 0 ... M ) )  ->  ( Q `  M )  e.  ran  Q )
217210, 215, 216syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q `  M
)  e.  ran  Q
)
218207, 217eqeltrd 2555 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  ran  Q
)
219218ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  B  e.  ran  Q )
220200, 219eqeltrd 2555 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) ) )  e. 
ran  Q )
221220adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( ( S `
 j )  +  T )  +  ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A ) ) )  e.  ran  Q
)
222 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  ->  (
k  x.  ( B  -  A ) )  =  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  ( B  -  A )
) )
223222oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  ->  (
( ( S `  j )  +  T
)  +  ( k  x.  ( B  -  A ) ) )  =  ( ( ( S `  j )  +  T )  +  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  x.  ( B  -  A )
) ) )
224223eleq1d 2536 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  ->  (
( ( ( S `
 j )  +  T )  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  ( ( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) ) )  e. 
ran  Q ) )
225224rspcev 3219 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  e.  ZZ  /\  ( ( ( S `
 j )  +  T )  +  ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A ) ) )  e.  ran  Q
)  ->  E. k  e.  ZZ  ( ( ( S `  j )  +  T )  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q )
226159, 221, 225syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  E. k  e.  ZZ  ( ( ( S `
 j )  +  T )  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q
)
227128, 226jca 532 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( ( S `
 j )  +  T )  e.  ( C [,] D )  /\  E. k  e.  ZZ  ( ( ( S `  j )  +  T )  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q ) )
228 oveq1 6302 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( ( S `
 j )  +  T )  ->  (
y  +  ( k  x.  ( B  -  A ) ) )  =  ( ( ( S `  j )  +  T )  +  ( k  x.  ( B  -  A )
) ) )
229228eleq1d 2536 . . . . . . . . . . . . . . 15  |-  ( y  =  ( ( S `
 j )  +  T )  ->  (
( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  ( ( ( S `  j )  +  T
)  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q ) )
230229rexbidv 2978 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( S `
 j )  +  T )  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  E. k  e.  ZZ  (
( ( S `  j )  +  T
)  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q ) )
231230elrab 3266 . . . . . . . . . . . . 13  |-  ( ( ( S `  j
)  +  T )  e.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q }  <->  ( ( ( S `  j )  +  T )  e.  ( C [,] D
)  /\  E. k  e.  ZZ  ( ( ( S `  j )  +  T )  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q ) )
232227, 231sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
)
233 elun2 3677 . . . . . . . . . . . 12  |-  ( ( ( S `  j
)  +  T )  e.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q }  ->  ( ( S `  j )  +  T )  e.  ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
234232, 233syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
235 foelrn 6051 . . . . . . . . . . 11  |-  ( ( S : ( 0 ... N ) -onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } )  /\  (
( S `  j
)  +  T )  e.  ( { C ,  D }  u.  {
y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q } ) )  ->  E. i  e.  (
0 ... N ) ( ( S `  j
)  +  T )  =  ( S `  i ) )
23684, 234, 235syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  E. i  e.  (
0 ... N ) ( ( S `  j
)  +  T )  =  ( S `  i ) )
237 eqcom 2476 . . . . . . . . . . . 12  |-  ( ( ( S `  j
)  +  T )  =  ( S `  i )  <->  ( S `  i )  =  ( ( S `  j
)  +  T ) )
238237rexbii 2969 . . . . . . . . . . 11  |-  ( E. i  e.  ( 0 ... N ) ( ( S `  j
)  +  T )  =  ( S `  i )  <->  E. i  e.  ( 0 ... N
) ( S `  i )  =  ( ( S `  j
)  +  T ) )
239238imbi2i 312 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  E. i  e.  (
0 ... N ) ( ( S `  j
)  +  T )  =  ( S `  i ) )  <->  ( (
( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  E. i  e.  (
0 ... N ) ( S `  i )  =  ( ( S `
 j )  +  T ) ) )
240236, 239mpbi 208 . . . . . . . . 9  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  E. i  e.  (
0 ... N ) ( S `  i )  =  ( ( S `
 j )  +  T ) )
241105ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  j
)  <  ( ( S `  j )  +  T ) )
242237biimpri 206 . . . . . . . . . . . . . . . . 17  |-  ( ( S `  i )  =  ( ( S `
 j )  +  T )  ->  (
( S `  j
)  +  T )  =  ( S `  i ) )
243242adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  =  ( S `
 i ) )
244241, 243breqtrd 4477 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  j
)  <  ( S `  i ) )
245243, 237sylib 196 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  i
)  =  ( ( S `  j )  +  T ) )
246113adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <  ( S `  ( j  +  1 ) ) )
247245, 246eqbrtrd 4473 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  i
)  <  ( S `  ( j  +  1 ) ) )
248244, 247jca 532 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  <  ( S `  i )  /\  ( S `  i
)  <  ( S `  ( j  +  1 ) ) ) )
249248adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  =  ( ( S `  j
)  +  T ) )  ->  ( ( S `  j )  <  ( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )
250 simplll 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  =  ( ( S `  j
)  +  T ) )  ->  ( ph  /\  j  e.  ( 0..^ N ) ) )
251 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  =  ( ( S `  j
)  +  T ) )  ->  i  e.  ( 0 ... N
) )
252 elfzelz 11700 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0 ... N )  ->  i  e.  ZZ )
253252ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  i  e.  ZZ )
25469ad3antlr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  j  e.  ZZ )
255 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  ( S `  j )  <  ( S `  i )
)
25675ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) )
25754ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  j  e.  ( 0 ... N
) )
258 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  i  e.  ( 0 ... N
) )
259 isorel 6221 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  /\  ( j  e.  ( 0 ... N )  /\  i  e.  ( 0 ... N ) ) )  ->  (
j  <  i  <->  ( S `  j )  <  ( S `  i )
) )
260256, 257, 258, 259syl12anc 1226 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  ( j  <  i  <->  ( S `  j )  <  ( S `  i )
) )
261255, 260mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  j  <  i )
262261adantrr 716 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  j  <  i )
263 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  ( S `  i )  <  ( S `  ( j  +  1 ) ) )
26475ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q }
) ) )
265 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  i  e.  ( 0 ... N
) )
26666ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
267 isorel 6221 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  /\  ( i  e.  ( 0 ... N )  /\  ( j  +  1 )  e.  ( 0 ... N ) ) )  ->  (
i  <  ( j  +  1 )  <->  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )
268264, 265, 266, 267syl12anc 1226 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  ( i  <  ( j  +  1 )  <->  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )
269263, 268mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  i  <  ( j  +  1 ) )
270269adantrl 715 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  i  <  ( j  +  1 ) )
271 btwnnz 10949 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ZZ  /\  j  <  i  /\  i  <  ( j  +  1 ) )  ->  -.  i  e.  ZZ )
272254, 262, 270, 271syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  -.  i  e.  ZZ )
273253, 272pm2.65da 576 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N
) )  ->  -.  ( ( S `  j )  <  ( S `  i )  /\  ( S `  i
)  <  ( S `  ( j  +  1 ) ) ) )
274250, 251, 273syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  =  ( ( S `  j
)  +  T ) )  ->  -.  (
( S `  j
)  <  ( S `  i )  /\  ( S `  i )  <  ( S `  (
j  +  1 ) ) ) )
275249, 274pm2.65da 576 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  ->  -.  ( S `  i )  =  ( ( S `  j
)  +  T ) )
276275ralrimiva 2881 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  A. i  e.  (
0 ... N )  -.  ( S `  i
)  =  ( ( S `  j )  +  T ) )
277 ralnex 2913 . . . . . . . . . . 11  |-  ( A. i  e.  ( 0 ... N )  -.  ( S `  i
)  =  ( ( S `  j )  +  T )  <->  -.  E. i  e.  ( 0 ... N
) ( S `  i )  =  ( ( S `  j
)  +  T ) )
278276, 277sylib 196 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  -.  E. i  e.  ( 0 ... N ) ( S `  i
)  =  ( ( S `  j )  +  T ) )
279278adantlr 714 . . . . . . . . 9  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  ->  -.  E. i  e.  ( 0 ... N ) ( S `  i
)  =  ( ( S `  j )  +  T ) )
280240, 279condan 792 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )
28168, 79, 2803jca 1176 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  (
j  +  1 ) )  e.  RR  /\  ( S `  j )  <  ( S `  ( j  +  1 ) )  /\  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) ) )
28263rexrd 9655 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  e.  RR* )
28387adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  T  e.  RR )
28463, 283readdcld 9635 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  j
)  +  T )  e.  RR )
285 elioc2 11599 . . . . . . . 8  |-  ( ( ( S `  j
)  e.  RR*  /\  (
( S `  j
)  +  T )  e.  RR )  -> 
( ( S `  ( j  +  1 ) )  e.  ( ( S `  j
) (,] ( ( S `  j )  +  T ) )  <-> 
( ( S `  ( j  +  1 ) )  e.  RR  /\  ( S `  j
)  <  ( S `  ( j  +  1 ) )  /\  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) ) ) )
286282, 284, 285syl2anc 661 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  (
j  +  1 ) )  e.  ( ( S `  j ) (,] ( ( S `
 j )  +  T ) )  <->  ( ( S `  ( j  +  1 ) )  e.  RR  /\  ( S `  j )  <  ( S `  (
j  +  1 ) )  /\  ( S `
 ( j  +  1 ) )  <_ 
( ( S `  j )  +  T
) ) ) )
287281, 286mpbird 232 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  ( j  +  1 ) )  e.  ( ( S `
 j ) (,] ( ( S `  j )  +  T
) ) )
28858, 61, 62, 16, 17, 63, 64, 287fourierdlem26 31756 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  ( j  +  1 ) ) )  =  ( A  +  ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) ) ) )
289288oveq1d 6310 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  A )  =  ( ( A  +  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) ) )  -  A
) )
29058recnd 9634 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  e.  CC )
29167recnd 9634 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  CC )
292291, 148subcld 9942 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  e.  CC )
293292adantr 465 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  e.  CC )
294290, 293pncan2d 9944 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( A  +  ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) ) )  -  A )  =  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) ) )
295 eqidd 2468 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  =  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) ) )
296289, 294, 2953eqtrd 2512 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  A )  =  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) ) )
29760, 296eqtrd 2508 . 2  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( L `
 ( E `  ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
) )
2981a1i 11 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  L  =  ( y  e.  ( A (,] B
)  |->  if ( y  =  B ,  A ,  y ) ) )
299 eqcom 2476 . . . . . . . . . . . 12  |-  ( y  =  ( E `  ( S `  j ) )  <->  ( E `  ( S `  j ) )  =  y )
300299biimpi 194 . . . . . . . . . . 11  |-  ( y  =  ( E `  ( S `  j ) )  ->  ( E `  ( S `  j
) )  =  y )
301300adantl 466 . . . . . . . . . 10  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
( E `  ( S `  j )
)  =  y )
302 id 22 . . . . . . . . . . . 12  |-  ( -.  ( E `  ( S `  j )
)  =  B  ->  -.  ( E `  ( S `  j )
)  =  B )
303302neqned 2670 . . . . . . . . . . 11  |-  ( -.  ( E `  ( S `  j )
)  =  B  -> 
( E `  ( S `  j )
)  =/=  B )
304303adantr 465 . . . . . . . . . 10  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
( E `  ( S `  j )
)  =/=  B )
305 pm13.18 2778 . . . . . . . . . 10  |-  ( ( ( E `  ( S `  j )
)  =  y  /\  ( E `  ( S `
 j ) )  =/=  B )  -> 
y  =/=  B )
306301, 304, 305syl2anc 661 . . . . . . . . 9  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =/=  B )
307306neneqd 2669 . . . . . . . 8  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  -.  y  =  B
)
308 iffalse 3954 . . . . . . . 8  |-  ( -.  y  =  B  ->  if ( y  =  B ,  A ,  y )  =  y )
309307, 308syl 16 . . . . . . 7  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  y )
310 simpr 461 . . . . . . 7  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =  ( E `
 ( S `  j ) ) )
311309, 310eqtrd 2508 . . . . . 6  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  ( E `
 ( S `  j ) ) )
312311adantll 713 . . . . 5  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  y  =  ( E `  ( S `
 j ) ) )  ->  if (
y  =  B ,  A ,  y )  =  ( E `  ( S `  j ) ) )
31356adantr 465 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  e.  ( A (,] B
) )
314298, 312, 313, 313fvmptd 5962 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  ( L `  ( E `  ( S `  j
) ) )  =  ( E `  ( S `  j )
) )
315314oveq2d 6311 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( L `
 ( E `  ( S `  j ) ) ) )  =  ( ( E `  ( S `  ( j  +  1 ) ) )  -  ( E `
 ( S `  j ) ) ) )
316 id 22 . . . . . . . 8  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  x  =  ( S `  ( j  +  1 ) ) )
317 oveq2 6303 . . . . . . . . . . 11  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  ( B  -  x )  =  ( B  -  ( S `  ( j  +  1 ) ) ) )
318317oveq1d 6310 . . . . . . . . . 10  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )
319318fveq2d 5876 . . . . . . . . 9  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  ( j  +  1 ) ) )  /  T ) ) )
320319oveq1d 6310 . . . . . . . 8  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) )
321316, 320oveq12d 6313 . . . . . . 7  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 ( j  +  1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) ) )
322321adantl 466 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  x  =  ( S `  (
j  +  1 ) ) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 ( j  +  1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) ) )
323137, 67resubcld 9999 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( B  -  ( S `  ( j  +  1 ) ) )  e.  RR )
324323, 87, 139redivcld 10384 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T )  e.  RR )
325324flcld 11915 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  e.  ZZ )
326325zred 10978 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  e.  RR )
327326, 87remulcld 9636 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T )  e.  RR )
32867, 327