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

Theorem fourierdlem65 37975
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 462 . . . . . . . 8  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =  ( E `
 ( S `  j ) ) )
4 simpl 458 . . . . . . . 8  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
( E `  ( S `  j )
)  =  B )
53, 4eqtrd 2463 . . . . . . 7  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =  B )
65iftrued 3919 . . . . . 6  |-  ( ( ( E `  ( S `  j )
)  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  A )
76adantll 718 . . . . 5  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  A )
8 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 ) ) ) } )
9 fourierdlem65.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
10 fourierdlem65.q . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
118, 9, 10fourierdlem11 37920 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
1211simp1d 1017 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR )
1311simp2d 1018 . . . . . . . . 9  |-  ( ph  ->  B  e.  RR )
1411simp3d 1019 . . . . . . . . 9  |-  ( ph  ->  A  <  B )
15 fourierdlem65.t . . . . . . . . 9  |-  T  =  ( B  -  A
)
16 fourierdlem65.e . . . . . . . . 9  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
1712, 13, 14, 15, 16fourierdlem4 37913 . . . . . . . 8  |-  ( ph  ->  E : RR --> ( A (,] B ) )
1817adantr 466 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E : RR --> ( A (,] B ) )
19 fourierdlem65.c . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR )
20 ioossre 11703 . . . . . . . . . . . . . . . 16  |-  ( C (,) +oo )  C_  RR
21 fourierdlem65.d . . . . . . . . . . . . . . . 16  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
2220, 21sseldi 3462 . . . . . . . . . . . . . . 15  |-  ( ph  ->  D  e.  RR )
2319rexrd 9697 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR* )
24 pnfxr 11419 . . . . . . . . . . . . . . . . 17  |- +oo  e.  RR*
2524a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  -> +oo  e.  RR* )
26 ioogtlb 37541 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR*  /\ +oo  e.  RR*  /\  D  e.  ( C (,) +oo ) )  ->  C  <  D )
2723, 25, 21, 26syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  <  D )
28 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 ) ) ) } )
29 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  x  ->  y  =  x )
3015eqcomi 2435 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B  -  A )  =  T
3130oveq2i 6316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  x.  ( B  -  A ) )  =  ( k  x.  T
)
3231a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  x  ->  (
k  x.  ( B  -  A ) )  =  ( k  x.  T ) )
3329, 32oveq12d 6323 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  x  ->  (
y  +  ( k  x.  ( B  -  A ) ) )  =  ( x  +  ( k  x.  T
) ) )
3433eleq1d 2491 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  x  ->  (
( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  ( x  +  ( k  x.  T ) )  e.  ran  Q ) )
3534rexbidv 2936 . . . . . . . . . . . . . . . . 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 ) )
3635cbvrabv 3079 . . . . . . . . . . . . . . . 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 }
3736uneq2i 3617 . . . . . . . . . . . . . . 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 } )
38 fourierdlem65.n . . . . . . . . . . . . . . 15  |-  N  =  ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )  - 
1 )
39 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 } ) ) )
4015, 8, 9, 10, 19, 22, 27, 28, 37, 38, 39fourierdlem54 37964 . . . . . . . . . . . . . 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 } ) ) ) )
4140simpld 460 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
4241simprd 464 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  ( O `
 N ) )
4341simpld 460 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
4428fourierdlem2 37911 . . . . . . . . . . . . 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 ) ) ) ) ) )
4543, 44syl 17 . . . . . . . . . . . 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 ) ) ) ) ) )
4642, 45mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( S  e.  ( RR  ^m  ( 0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) )
4746simpld 460 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( RR 
^m  ( 0 ... N ) ) )
48 elmapi 7504 . . . . . . . . . 10  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
4947, 48syl 17 . . . . . . . . 9  |-  ( ph  ->  S : ( 0 ... N ) --> RR )
5049adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> RR )
51 elfzofz 11942 . . . . . . . . 9  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
5251adantl 467 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
5350, 52ffvelrnd 6038 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
5418, 53ffvelrnd 6038 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E `  ( S `  j ) )  e.  ( A (,] B ) )
5554adantr 466 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  e.  ( A (,] B
) )
5612ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  e.  RR )
572, 7, 55, 56fvmptd 5970 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( L `  ( E `  ( S `  j
) ) )  =  A )
5857oveq2d 6321 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( L `
 ( E `  ( S `  j ) ) ) )  =  ( ( E `  ( S `  ( j  +  1 ) ) )  -  A ) )
5913ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  B  e.  RR )
6014ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  <  B )
6153adantr 466 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  e.  RR )
62 simpr 462 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  =  B )
63 fzofzp1 12014 . . . . . . . . 9  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
6463adantl 467 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
6550, 64ffvelrnd 6038 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
6665adantr 466 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  ( j  +  1 ) )  e.  RR )
67 elfzoelz 11927 . . . . . . . . . . 11  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
6867zred 11047 . . . . . . . . . 10  |-  ( j  e.  ( 0..^ N )  ->  j  e.  RR )
6968adantl 467 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  RR )
7069ltp1d 10544 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  <  (
j  +  1 ) )
7140simprd 464 . . . . . . . . . 10  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) ) )
7271adantr 466 . . . . . . . . 9  |-  ( (
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 }
) ) )
73 isorel 6232 . . . . . . . . 9  |-  ( ( 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 ) ) ) )
7472, 52, 64, 73syl12anc 1262 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  < 
( j  +  1 )  <->  ( S `  j )  <  ( S `  ( j  +  1 ) ) ) )
7570, 74mpbid 213 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
7675adantr 466 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  <  ( S `  (
j  +  1 ) ) )
77 isof1o 6231 . . . . . . . . . . 11  |-  ( 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 }
) )
78 f1ofo 5838 . . . . . . . . . . 11  |-  ( 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 } ) )
7971, 77, 783syl 18 . . . . . . . . . 10  |-  ( ph  ->  S : ( 0 ... N ) -onto-> ( { C ,  D }  u.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  ( B  -  A )
) )  e.  ran  Q } ) )
8079ad3antrrr 734 . . . . . . . . 9  |-  ( ( ( ( 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 } ) )
8119ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  C  e.  RR )
8222ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  D  e.  RR )
8313, 12resubcld 10054 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  -  A
)  e.  RR )
8415, 83syl5eqel 2511 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  RR )
8584adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  RR )
8653, 85readdcld 9677 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  T )  e.  RR )
8786adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  RR )
8819adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  e.  RR )
8928, 43, 42fourierdlem15 37924 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  S : ( 0 ... N ) --> ( C [,] D ) )
9089adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> ( C [,] D
) )
9190, 52ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  ( C [,] D ) )
9222adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  D  e.  RR )
93 elicc2 11706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( S `  j )  e.  ( C [,] D )  <-> 
( ( S `  j )  e.  RR  /\  C  <_  ( S `  j )  /\  ( S `  j )  <_  D ) ) )
9488, 92, 93syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  e.  ( C [,] D
)  <->  ( ( S `
 j )  e.  RR  /\  C  <_ 
( S `  j
)  /\  ( S `  j )  <_  D
) ) )
9591, 94mpbid 213 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  e.  RR  /\  C  <_ 
( S `  j
)  /\  ( S `  j )  <_  D
) )
9695simp2d 1018 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  <_  ( S `  j )
)
9712, 13posdifd 10207 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
9814, 97mpbid 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <  ( B  -  A ) )
9998, 15syl6breqr 4464 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  T )
10084, 99elrpd 11345 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  e.  RR+ )
101100adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  RR+ )
10253, 101ltaddrpd 11378 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  (
( S `  j
)  +  T ) )
10388, 53, 86, 96, 102lelttrd 9800 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  <  (
( S `  j
)  +  T ) )
10488, 86, 103ltled 9790 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  C  <_  (
( S `  j
)  +  T ) )
105104adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  C  <_  ( ( S `
 j )  +  T ) )
10665adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( S `  (
j  +  1 ) )  e.  RR )
107 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )
10887, 106ltnled 9789 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( ( S `
 j )  +  T )  <  ( S `  ( j  +  1 ) )  <->  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) ) )
109107, 108mpbird 235 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <  ( S `  ( j  +  1 ) ) )
11090, 64ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  ( C [,] D ) )
111 elicc2 11706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) )
11288, 92, 111syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  e.  ( C [,] D
)  <->  ( ( S `
 ( j  +  1 ) )  e.  RR  /\  C  <_ 
( S `  (
j  +  1 ) )  /\  ( S `
 ( j  +  1 ) )  <_  D ) ) )
113110, 112mpbid 213 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  e.  RR  /\  C  <_ 
( S `  (
j  +  1 ) )  /\  ( S `
 ( j  +  1 ) )  <_  D ) )
114113simp3d 1019 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  <_  D
)
115114adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( S `  (
j  +  1 ) )  <_  D )
11687, 106, 82, 109, 115ltletrd 9802 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <  D )
11787, 82, 116ltled 9790 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <_  D )
11881, 82, 87, 105, 117eliccd 37550 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  ( C [,] D ) )
119118adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( S `  j )  +  T
)  e.  ( C [,] D ) )
12016a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) ) )
121 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( S `  j )  ->  x  =  ( S `  j ) )
122 oveq2 6313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( S `  j )  ->  ( B  -  x )  =  ( B  -  ( S `  j ) ) )
123122oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( S `  j )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  j ) )  /  T ) )
124123fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( S `  j )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  j )
)  /  T ) ) )
125124oveq1d 6320 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( S `  j )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )
126121, 125oveq12d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( S `  j )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
127126adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  x  =  ( S `  j
) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
12813adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  B  e.  RR )
129128, 53resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( B  -  ( S `  j ) )  e.  RR )
130129, 101rerpdivcld 11376 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( B  -  ( S `  j ) )  /  T )  e.  RR )
131130flcld 12040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  e.  ZZ )
132131zred 11047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  e.  RR )
133132, 85remulcld 9678 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T )  e.  RR )
13453, 133readdcld 9677 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )  e.  RR )
135120, 127, 53, 134fvmptd 5970 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E `  ( S `  j ) )  =  ( ( S `  j )  +  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
136135oveq1d 6320 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  =  ( ( ( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  -  ( S `  j ) ) )
137136oveq1d 6320 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  =  ( ( ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )  -  ( S `
 j ) )  /  T ) )
13853recnd 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  CC )
139133recnd 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T )  e.  CC )
140138, 139pncan2d 9995 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( ( |_
`  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) )  -  ( S `  j ) )  =  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )
141140oveq1d 6320 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  -  ( S `  j ) )  /  T )  =  ( ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T )  /  T ) )
142132recnd 9676 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  e.  CC )
14385recnd 9676 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  CC )
144101rpne0d 11353 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  =/=  0
)
145142, 143, 144divcan4d 10396 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T )  /  T )  =  ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) ) )
146137, 141, 1453eqtrd 2467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  =  ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) ) )
147146, 131eqeltrd 2507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  e.  ZZ )
148 peano2zm 10987 . . . . . . . . . . . . . 14  |-  ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  e.  ZZ  ->  ( (
( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  e.  ZZ )
149147, 148syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  e.  ZZ )
150149ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  -> 
( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  e.  ZZ )
15130oveq2i 6316 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) )  =  ( ( ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  T )
152151oveq2i 6316 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
153152a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
154135adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  =  ( ( S `  j )  +  ( ( |_ `  (
( B  -  ( S `  j )
)  /  T ) )  x.  T ) ) )
155 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( E `  ( S `  j )
)  -  ( S `
 j ) )  =  ( B  -  ( S `  j ) ) )
156155eqcomd 2430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E `  ( S `
 j ) )  =  B  ->  ( B  -  ( S `  j ) )  =  ( ( E `  ( S `  j ) )  -  ( S `
 j ) ) )
157156oveq1d 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( B  -  ( S `  j )
)  /  T )  =  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T ) )
158157fveq2d 5885 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E `  ( S `
 j ) )  =  B  ->  ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  =  ( |_ `  (
( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T ) ) )
159158oveq1d 6320 . . . . . . . . . . . . . . . . . 18  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( |_ `  (
( B  -  ( S `  j )
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T ) )  x.  T ) )
160159oveq2d 6321 . . . . . . . . . . . . . . . . 17  |-  ( ( E `  ( S `
 j ) )  =  B  ->  (
( S `  j
)  +  ( ( |_ `  ( ( B  -  ( S `
 j ) )  /  T ) )  x.  T ) )  =  ( ( S `
 j )  +  ( ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  x.  T ) ) )
161160adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
162146, 142eqeltrd 2507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  e.  CC )
163 1cnd 9666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  1  e.  CC )
164162, 163, 143subdird 10082 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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
) ) )
16584recnd 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  T  e.  CC )
166165mulid2d 9668 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 1  x.  T
)  =  T )
167166oveq2d 6321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  -  (
1  x.  T ) )  =  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  T ) )
168167adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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 ) )
169164, 168eqtrd 2463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  T
)  =  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  x.  T )  -  T ) )
170169oveq2d 6321 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) ) )
171162, 143mulcld 9670 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  e.  CC )
172138, 143, 171ppncand 10033 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) ) )
173 flid 12050 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  e.  ZZ  ->  ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  =  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )
174147, 173syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T ) )  =  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) )
175174eqcomd 2430 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( E `  ( S `
 j ) )  -  ( S `  j ) )  /  T )  =  ( |_ `  ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T ) ) )
176175oveq1d 6320 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  x.  T )  =  ( ( |_ `  (
( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T ) )  x.  T ) )
177176oveq2d 6321 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 ) ) )
178170, 172, 1773eqtrrd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
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
) ) )
179178adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
180154, 161, 1793eqtrrd 2468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  T ) )  =  ( E `  ( S `  j )
) )
181153, 180, 623eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( ( S `  j )  +  T
)  +  ( ( ( ( ( E `
 ( S `  j ) )  -  ( S `  j ) )  /  T )  -  1 )  x.  ( B  -  A
) ) )  =  B )
1828fourierdlem2 37911 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) ) ) )
1839, 182syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) ) )
18410, 183mpbid 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
185184simprd 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
186185simpld 460 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
187186simprd 464 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Q `  M
)  =  B )
188187eqcomd 2430 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  =  ( Q `
 M ) )
1898, 9, 10fourierdlem15 37924 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
190 ffn 5746 . . . . . . . . . . . . . . . . . 18  |-  ( Q : ( 0 ... M ) --> ( A [,] B )  ->  Q  Fn  ( 0 ... M ) )
191189, 190syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
1929nnnn0d 10932 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  NN0 )
193 nn0uz 11200 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
194192, 193syl6eleq 2517 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
195 eluzfz2 11814 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
196194, 195syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ( 0 ... M ) )
197 fnfvelrn 6034 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  Fn  ( 0 ... M )  /\  M  e.  ( 0 ... M ) )  ->  ( Q `  M )  e.  ran  Q )
198191, 196, 197syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  M
)  e.  ran  Q
)
199188, 198eqeltrd 2507 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  ran  Q
)
200199ad2antrr 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  B  e.  ran  Q )
201181, 200eqeltrd 2507 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
202201adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( 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
)
203 oveq1 6312 . . . . . . . . . . . . . . 15  |-  ( k  =  ( ( ( ( E `  ( S `  j )
)  -  ( S `
 j ) )  /  T )  - 
1 )  ->  (
k  x.  ( B  -  A ) )  =  ( ( ( ( ( E `  ( S `  j ) )  -  ( S `
 j ) )  /  T )  - 
1 )  x.  ( B  -  A )
) )
204203oveq2d 6321 . . . . . . . . . . . . . 14  |-  ( 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 )
) ) )
205204eleq1d 2491 . . . . . . . . . . . . 13  |-  ( 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 ) )
206205rspcev 3182 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 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 )
207150, 202, 206syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ( 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
)
208 oveq1 6312 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( S `
 j )  +  T )  ->  (
y  +  ( k  x.  ( B  -  A ) ) )  =  ( ( ( S `  j )  +  T )  +  ( k  x.  ( B  -  A )
) ) )
209208eleq1d 2491 . . . . . . . . . . . . 13  |-  ( y  =  ( ( S `
 j )  +  T )  ->  (
( y  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q  <->  ( ( ( S `  j )  +  T
)  +  ( k  x.  ( B  -  A ) ) )  e.  ran  Q ) )
210209rexbidv 2936 . . . . . . . . . . . 12  |-  ( 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 ) )
211210elrab 3228 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
212119, 207, 211sylanbrc 668 . . . . . . . . . 10  |-  ( ( ( ( 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 }
)
213 elun2 3634 . . . . . . . . . 10  |-  ( ( ( 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 } ) )
214212, 213syl 17 . . . . . . . . 9  |-  ( ( ( ( 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 } ) )
215 foelrn 6056 . . . . . . . . 9  |-  ( ( 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 ) )
21680, 214, 215syl2anc 665 . . . . . . . 8  |-  ( ( ( ( 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 ) )
217 eqcom 2431 . . . . . . . . 9  |-  ( ( ( S `  j
)  +  T )  =  ( S `  i )  <->  ( S `  i )  =  ( ( S `  j
)  +  T ) )
218217rexbii 2924 . . . . . . . 8  |-  ( E. i  e.  ( 0 ... N ) ( ( S `  j
)  +  T )  =  ( S `  i )  <->  E. i  e.  ( 0 ... N
) ( S `  i )  =  ( ( S `  j
)  +  T ) )
219216, 218sylib 199 . . . . . . 7  |-  ( ( ( ( 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 ) )
220102ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  j
)  <  ( ( S `  j )  +  T ) )
221217biimpri 209 . . . . . . . . . . . . . 14  |-  ( ( S `  i )  =  ( ( S `
 j )  +  T )  ->  (
( S `  j
)  +  T )  =  ( S `  i ) )
222221adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  =  ( S `
 i ) )
223220, 222breqtrd 4448 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  j
)  <  ( S `  i ) )
224109adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( ( S `  j )  +  T
)  <  ( S `  ( j  +  1 ) ) )
225222, 224eqbrtrrd 4446 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  ( S `  i )  =  ( ( S `
 j )  +  T ) )  -> 
( S `  i
)  <  ( S `  ( j  +  1 ) ) )
226223, 225jca 534 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) )
227226adantlr 719 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) ) ) )
228 simplll 766 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) ) )
229 simplr 760 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  =  ( ( S `  j
)  +  T ) )  ->  i  e.  ( 0 ... N
) )
230 elfzelz 11807 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0 ... N )  ->  i  e.  ZZ )
231230ad2antlr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  i  e.  ZZ )
23267ad3antlr 735 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  j  e.  ZZ )
233 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  ( S `  j )  <  ( S `  i )
)
23472ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 }
) ) )
23552ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  j  e.  ( 0 ... N
) )
236 simplr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  i  e.  ( 0 ... N
) )
237 isorel 6232 . . . . . . . . . . . . . . . 16  |-  ( ( 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 )
) )
238234, 235, 236, 237syl12anc 1262 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  ( j  <  i  <->  ( S `  j )  <  ( S `  i )
) )
239233, 238mpbird 235 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  j )  <  ( S `  i )
)  ->  j  <  i )
240239adantrr 721 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  j  <  i )
241 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  ( S `  i )  <  ( S `  ( j  +  1 ) ) )
24272ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 }
) ) )
243 simplr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  i  e.  ( 0 ... N
) )
24464ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
245 isorel 6232 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
246242, 243, 244, 245syl12anc 1262 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  ( i  <  ( j  +  1 )  <->  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )
247241, 246mpbird 235 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) )  ->  i  <  ( j  +  1 ) )
248247adantrl 720 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  i  <  ( j  +  1 ) )
249 btwnnz 11019 . . . . . . . . . . . . 13  |-  ( ( j  e.  ZZ  /\  j  <  i  /\  i  <  ( j  +  1 ) )  ->  -.  i  e.  ZZ )
250232, 240, 248, 249syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N ) )  /\  ( ( S `
 j )  < 
( S `  i
)  /\  ( S `  i )  <  ( S `  ( j  +  1 ) ) ) )  ->  -.  i  e.  ZZ )
251231, 250pm2.65da 578 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  i  e.  ( 0 ... N
) )  ->  -.  ( ( S `  j )  <  ( S `  i )  /\  ( S `  i
)  <  ( S `  ( j  +  1 ) ) ) )
252228, 229, 251syl2anc 665 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) ) ) )
253227, 252pm2.65da 578 . . . . . . . . 9  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  (
j  +  1 ) )  <_  ( ( S `  j )  +  T ) )  /\  i  e.  ( 0 ... N ) )  ->  -.  ( S `  i )  =  ( ( S `  j
)  +  T ) )
254253nrexdv 2878 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )  ->  -.  E. i  e.  ( 0 ... N ) ( S `  i
)  =  ( ( S `  j )  +  T ) )
255254adantlr 719 . . . . . . 7  |-  ( ( ( ( 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 ) )
256219, 255condan 801 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  ( j  +  1 ) )  <_  ( ( S `
 j )  +  T ) )
25761rexrd 9697 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  e.  RR* )
25884ad2antrr 730 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  T  e.  RR )
25961, 258readdcld 9677 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  j
)  +  T )  e.  RR )
260 elioc2 11704 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
261257, 259, 260syl2anc 665 . . . . . 6  |-  ( ( ( 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
) ) ) )
26266, 76, 256, 261mpbir3and 1188 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  ( j  +  1 ) )  e.  ( ( S `
 j ) (,] ( ( S `  j )  +  T
) ) )
26356, 59, 60, 15, 16, 61, 62, 262fourierdlem26 37935 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  ( j  +  1 ) ) )  =  ( A  +  ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) ) ) )
264263oveq1d 6320 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  A )  =  ( ( A  +  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) ) )  -  A
) )
26556recnd 9676 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  e.  CC )
26665recnd 9676 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  CC )
267266, 138subcld 9993 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  e.  CC )
268267adantr 466 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  e.  CC )
269265, 268pncan2d 9995 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( A  +  ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) ) )  -  A )  =  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) ) )
27058, 264, 2693eqtrd 2467 . 2  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( L `
 ( E `  ( S `  j ) ) ) )  =  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
) )
2711a1i 11 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  L  =  ( y  e.  ( A (,] B
)  |->  if ( y  =  B ,  A ,  y ) ) )
272 eqcom 2431 . . . . . . . . . . . 12  |-  ( y  =  ( E `  ( S `  j ) )  <->  ( E `  ( S `  j ) )  =  y )
273272biimpi 197 . . . . . . . . . . 11  |-  ( y  =  ( E `  ( S `  j ) )  ->  ( E `  ( S `  j
) )  =  y )
274273adantl 467 . . . . . . . . . 10  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
( E `  ( S `  j )
)  =  y )
275 neqne 37347 . . . . . . . . . . 11  |-  ( -.  ( E `  ( S `  j )
)  =  B  -> 
( E `  ( S `  j )
)  =/=  B )
276275adantr 466 . . . . . . . . . 10  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
( E `  ( S `  j )
)  =/=  B )
277274, 276eqnetrrd 2714 . . . . . . . . 9  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =/=  B )
278277neneqd 2621 . . . . . . . 8  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  -.  y  =  B
)
279278iffalsed 3922 . . . . . . 7  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  y )
280 simpr 462 . . . . . . 7  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  -> 
y  =  ( E `
 ( S `  j ) ) )
281279, 280eqtrd 2463 . . . . . 6  |-  ( ( -.  ( E `  ( S `  j ) )  =  B  /\  y  =  ( E `  ( S `  j
) ) )  ->  if ( y  =  B ,  A ,  y )  =  ( E `
 ( S `  j ) ) )
282281adantll 718 . . . . 5  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  y  =  ( E `  ( S `
 j ) ) )  ->  if (
y  =  B ,  A ,  y )  =  ( E `  ( S `  j ) ) )
28354adantr 466 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  e.  ( A (,] B
) )
284271, 282, 283, 283fvmptd 5970 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  ( L `  ( E `  ( S `  j
) ) )  =  ( E `  ( S `  j )
) )
285284oveq2d 6321 . . 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 ) ) ) )
286 id 22 . . . . . . . 8  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  x  =  ( S `  ( j  +  1 ) ) )
287 oveq2 6313 . . . . . . . . . . 11  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  ( B  -  x )  =  ( B  -  ( S `  ( j  +  1 ) ) ) )
288287oveq1d 6320 . . . . . . . . . 10  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  (
( B  -  x
)  /  T )  =  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )
289288fveq2d 5885 . . . . . . . . 9  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  ( |_ `  ( ( B  -  x )  /  T ) )  =  ( |_ `  (
( B  -  ( S `  ( j  +  1 ) ) )  /  T ) ) )
290289oveq1d 6320 . . . . . . . 8  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T )  =  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) )
291286, 290oveq12d 6323 . . . . . . 7  |-  ( x  =  ( S `  ( j  +  1 ) )  ->  (
x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) )  =  ( ( S `
 ( j  +  1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) ) )
292291adantl 467 . . . . . 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 ) ) )
293128, 65resubcld 10054 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( B  -  ( S `  ( j  +  1 ) ) )  e.  RR )
294293, 101rerpdivcld 11376 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T )  e.  RR )
295294flcld 12040 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  e.  ZZ )
296295zred 11047 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  e.  RR )
297296, 85remulcld 9678 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T )  e.  RR )
29865, 297readdcld 9677 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  +  ( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) )  e.  RR )
299120, 292, 65, 298fvmptd 5970 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E `  ( S `  ( j  +  1 ) ) )  =  ( ( S `  ( j  +  1 ) )  +  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) ) )
300299, 135oveq12d 6323 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( E `
 ( S `  ( j  +  1 ) ) )  -  ( E `  ( S `
 j ) ) )  =  ( ( ( S `  (
j  +  1 ) )  +  ( ( |_ `  ( ( B  -  ( S `
 ( j  +  1 ) ) )  /  T ) )  x.  T ) )  -  ( ( S `
 j )  +  ( ( |_ `  ( ( B  -  ( S `  j ) )  /  T ) )  x.  T ) ) ) )
301300adantr 466 . . 3  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  (
( E `  ( S `  ( j  +  1 ) ) )  -  ( E `
 ( S `  j ) ) )  =  ( ( ( S `  ( j  +  1 ) )  +  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  x.  T ) )  -  ( ( S `  j )  +  ( ( |_ `  (
( B  -  ( S `  j )
)  /  T ) )  x.  T ) ) ) )
302 flle 12041 . . . . . . . . . . . . 13  |-  ( ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T )  e.  RR  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  <_ 
( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )
303294, 302syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  <_  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )
30453, 65, 75ltled 9790 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <_  ( S `  ( j  +  1 ) ) )
30553, 65, 128, 304lesub2dd 10237 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( B  -  ( S `  ( j  +  1 ) ) )  <_  ( B  -  ( S `  j ) ) )
306293, 129, 101, 305lediv1dd 11403 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T )  <_  (
( B  -  ( S `  j )
)  /  T ) )
307296, 294, 130, 303, 306letrd 9799 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  <_  ( ( B  -  ( S `  j ) )  /  T ) )
308307adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j ) )  =  B )  ->  ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  <_ 
( ( B  -  ( S `  j ) )  /  T ) )
309296adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( B  -  ( S `  j )
)  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  -> 
( |_ `  (
( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  e.  RR )
310 1red 9665 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( B  -  ( S `  j )
)  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  -> 
1  e.  RR )
311309, 310readdcld 9677 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( B  -  ( S `  j )
)  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  -> 
( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  e.  RR )
312130adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( B  -  ( S `  j )
)  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  -> 
( ( B  -  ( S `  j ) )  /  T )  e.  RR )
313 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( B  -  ( S `  j )
)  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  ->  -.  ( ( B  -  ( S `  j ) )  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )
314311, 312, 313nltled 9792 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( B  -  ( S `  j )
)  /  T )  <  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  -> 
( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  <_  ( ( B  -  ( S `  j ) )  /  T ) )
315314adantlr 719 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  -.  ( ( B  -  ( S `
 j ) )  /  T )  < 
( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 ) )  ->  ( ( |_ `  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  <_  (
( B  -  ( S `  j )
)  /  T ) )
31679ad3antrrr 734 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  <_  (
( B  -  ( 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 } ) )
31788ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  <_  (
( B  -  ( S `  j )
)  /  T ) )  ->  C  e.  RR )
31892ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  <_  (
( B  -  ( S `  j )
)  /  T ) )  ->  D  e.  RR )
319 fourierdlem65.z . . . . . . . . . . . . . . . . . . 19  |-  Z  =  ( ( S `  j )  +  ( B  -  ( E `
 ( S `  j ) ) ) )
320135, 134eqeltrd 2507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( E `  ( S `  j ) )  e.  RR )
321128, 320resubcld 10054 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( B  -  ( E `  ( S `
 j ) ) )  e.  RR )
32253, 321readdcld 9677 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( B  -  ( E `  ( S `  j ) ) ) )  e.  RR )
323319, 322syl5eqel 2511 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  RR )
324323ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  ( E `  ( S `  j )
)  =  B )  /\  ( ( |_
`  ( ( B  -  ( S `  ( j  +  1 ) ) )  /  T ) )  +  1 )  <_  (
( B  -  ( S `  j )
)  /  T ) )  ->  Z  e.  RR )
32512rexrd 9697 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  e.  RR* )
326325adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (