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

Theorem fourierdlem79 31809
Description:  E projects every interval of the partition induced by  S on  H into a corresponding interval of the partition induced by  Q on  [ A ,  B ] (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem79.t  |-  T  =  ( B  -  A
)
fourierdlem79.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 ) ) ) } )
fourierdlem79.m  |-  ( ph  ->  M  e.  NN )
fourierdlem79.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem79.c  |-  ( ph  ->  C  e.  RR )
fourierdlem79.d  |-  ( ph  ->  D  e.  RR )
fourierdlem79.cltd  |-  ( ph  ->  C  <  D )
fourierdlem79.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 ) ) ) } )
fourierdlem79.h  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
fourierdlem79.n  |-  N  =  ( ( # `  H
)  -  1 )
fourierdlem79.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
fourierdlem79.e  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
fourierdlem79.l  |-  L  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
fourierdlem79.z  |-  Z  =  ( ( S `  j )  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )
fourierdlem79.i  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ,  RR ,  <  ) )
Assertion
Ref Expression
fourierdlem79  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( L `
 ( E `  ( S `  j ) ) ) (,) ( E `  ( S `  ( j  +  1 ) ) ) ) 
C_  ( ( Q `
 ( I `  ( S `  j ) ) ) (,) ( Q `  ( (
I `  ( S `  j ) )  +  1 ) ) ) )
Distinct variable groups:    A, i,
j, x    A, m, p, i    y, A, j, x    B, f    B, i, k, x    B, m, p    y, B    C, i, m, p    x, C    D, i, m, p    x, D    f, E    i, E, k, x    y, E    f, H    x, H    f, I    i, I, k, x    i, L, x    i, M, j, x    m, M, p   
f, N    i, N, k, x    m, N, p   
y, N    Q, f,
j    Q, i, k, x, j    Q, p    S, f    S, i, k, x    S, p    y, S    T, i,
k, x    k, Z, x    ph, f, j    ph, i,
k, x    ph, y
Allowed substitution hints:    ph( m, p)    A( f, k)    B( j)    C( y, f, j, k)    D( y, f, j, k)    P( x, y, f, i, j, k, m, p)    Q( y, m)    S( j, m)    T( y, f, j, m, p)    E( j, m, p)    H( y, i, j, k, m, p)    I( y, j, m, p)    L( y, f, j, k, m, p)    M( y,
f, k)    N( j)    O( x, y, f, i, j, k, m, p)    Z( y, f, i, j, m, p)

Proof of Theorem fourierdlem79
Dummy variable  l is distinct from all other variables.
StepHypRef Expression
1 fourierdlem79.q . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( P `
 M ) )
2 fourierdlem79.m . . . . . . . . . 10  |-  ( ph  ->  M  e.  NN )
3 fourierdlem79.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 ) ) ) } )
43fourierdlem2 31732 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
52, 4syl 16 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
61, 5mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
76simpld 459 . . . . . . 7  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
8 elmapi 7452 . . . . . . 7  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
97, 8syl 16 . . . . . 6  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
109adantr 465 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Q : ( 0 ... M ) --> RR )
11 fourierdlem79.t . . . . . . . . . 10  |-  T  =  ( B  -  A
)
12 fourierdlem79.e . . . . . . . . . 10  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
13 fourierdlem79.l . . . . . . . . . 10  |-  L  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
14 fourierdlem79.i . . . . . . . . . 10  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ,  RR ,  <  ) )
153, 2, 1, 11, 12, 13, 14fourierdlem37 31767 . . . . . . . . 9  |-  ( ph  ->  ( I : RR --> ( 0..^ M )  /\  ( x  e.  RR  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  x )
) } ,  RR ,  <  )  e.  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ) ) )
1615simpld 459 . . . . . . . 8  |-  ( ph  ->  I : RR --> ( 0..^ M ) )
17 fzossfz 11826 . . . . . . . . 9  |-  ( 0..^ M )  C_  (
0 ... M )
1817a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 0..^ M ) 
C_  ( 0 ... M ) )
19 fss 5745 . . . . . . . 8  |-  ( ( I : RR --> ( 0..^ M )  /\  (
0..^ M )  C_  ( 0 ... M
) )  ->  I : RR --> ( 0 ... M ) )
2016, 18, 19syl2anc 661 . . . . . . 7  |-  ( ph  ->  I : RR --> ( 0 ... M ) )
2120adantr 465 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  I : RR --> ( 0 ... M
) )
22 fourierdlem79.c . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  RR )
23 fourierdlem79.d . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  RR )
24 fourierdlem79.cltd . . . . . . . . . . . . . 14  |-  ( ph  ->  C  <  D )
25 fourierdlem79.o . . . . . . . . . . . . . 14  |-  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 ) ) ) } )
26 fourierdlem79.h . . . . . . . . . . . . . 14  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
27 fourierdlem79.n . . . . . . . . . . . . . 14  |-  N  =  ( ( # `  H
)  -  1 )
28 fourierdlem79.s . . . . . . . . . . . . . 14  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
2911, 3, 2, 1, 22, 23, 24, 25, 26, 27, 28fourierdlem54 31784 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  e.  NN  /\  S  e.  ( O `  N
) )  /\  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) ) )
3029simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
3130simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  ( O `
 N ) )
3231adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  e.  ( O `  N ) )
3330simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN )
3433adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  N  e.  NN )
3525fourierdlem2 31732 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
3634, 35syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( 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 ) ) ) ) ) )
3732, 36mpbid 210 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S  e.  ( RR  ^m  (
0 ... N ) )  /\  ( ( ( S `  0 )  =  C  /\  ( S `  N )  =  D )  /\  A. i  e.  ( 0..^ N ) ( S `
 i )  < 
( S `  (
i  +  1 ) ) ) ) )
3837simpld 459 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  e.  ( RR  ^m  ( 0 ... N ) ) )
39 elmapi 7452 . . . . . . . 8  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
4038, 39syl 16 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> RR )
41 elfzofz 11823 . . . . . . . 8  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
4241adantl 466 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
4340, 42ffvelrnd 6033 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
4421, 43ffvelrnd 6033 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( I `  ( S `  j ) )  e.  ( 0 ... M ) )
4510, 44ffvelrnd 6033 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  e.  RR )
4645rexrd 9655 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  e.  RR* )
4716adantr 465 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  I : RR --> ( 0..^ M ) )
4847, 43ffvelrnd 6033 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( I `  ( S `  j ) )  e.  ( 0..^ M ) )
49 fzofzp1 11889 . . . . . 6  |-  ( ( I `  ( S `
 j ) )  e.  ( 0..^ M )  ->  ( (
I `  ( S `  j ) )  +  1 )  e.  ( 0 ... M ) )
5048, 49syl 16 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( I `
 ( S `  j ) )  +  1 )  e.  ( 0 ... M ) )
5110, 50ffvelrnd 6033 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( ( I `  ( S `  j ) )  +  1 ) )  e.  RR )
5251rexrd 9655 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( ( I `  ( S `  j ) )  +  1 ) )  e.  RR* )
5346, 52jca 532 . 2  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( Q `
 ( I `  ( S `  j ) ) )  e.  RR*  /\  ( Q `  (
( I `  ( S `  j )
)  +  1 ) )  e.  RR* )
)
5414a1i 11 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ,  RR ,  <  ) ) )
55 fveq2 5872 . . . . . . . . . . 11  |-  ( x  =  ( S `  j )  ->  ( E `  x )  =  ( E `  ( S `  j ) ) )
5655fveq2d 5876 . . . . . . . . . 10  |-  ( x  =  ( S `  j )  ->  ( L `  ( E `  x ) )  =  ( L `  ( E `  ( S `  j ) ) ) )
5756breq2d 4465 . . . . . . . . 9  |-  ( x  =  ( S `  j )  ->  (
( Q `  i
)  <_  ( L `  ( E `  x
) )  <->  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) ) )
5857rabbidv 3110 . . . . . . . 8  |-  ( x  =  ( S `  j )  ->  { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  x )
) }  =  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `
 j ) ) ) } )
5958supeq1d 7918 . . . . . . 7  |-  ( x  =  ( S `  j )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  x
) ) } ,  RR ,  <  )  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  ) )
6059adantl 466 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  x  =  ( S `  j
) )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  x
) ) } ,  RR ,  <  )  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  ) )
61 ltso 9677 . . . . . . . 8  |-  <  Or  RR
6261supex 7935 . . . . . . 7  |-  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  )  e. 
_V
6362a1i 11 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  )  e.  _V )
6454, 60, 43, 63fvmptd 5962 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( I `  ( S `  j ) )  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )
6564fveq2d 5876 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  =  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) ) )
66 simpl 457 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ph )
6766, 43jca 532 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ph  /\  ( S `  j )  e.  RR ) )
68 eleq1 2539 . . . . . . . . . 10  |-  ( x  =  ( S `  j )  ->  (
x  e.  RR  <->  ( S `  j )  e.  RR ) )
6968anbi2d 703 . . . . . . . . 9  |-  ( x  =  ( S `  j )  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  ( S `  j
)  e.  RR ) ) )
7059, 58eleq12d 2549 . . . . . . . . 9  |-  ( x  =  ( S `  j )  ->  ( sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ,  RR ,  <  )  e.  { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) }  <->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  )  e.  { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ) )
7169, 70imbi12d 320 . . . . . . . 8  |-  ( x  =  ( S `  j )  ->  (
( ( ph  /\  x  e.  RR )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  x )
) } ,  RR ,  <  )  e.  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } )  <->  ( ( ph  /\  ( S `  j )  e.  RR )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  )  e.  { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ) ) )
7215simprd 463 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  RR  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  x )
) } ,  RR ,  <  )  e.  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ) )
7372imp 429 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  x
) ) } ,  RR ,  <  )  e. 
{ i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  x
) ) } )
7471, 73vtoclg 3176 . . . . . . 7  |-  ( ( S `  j )  e.  RR  ->  (
( ph  /\  ( S `  j )  e.  RR )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  )  e. 
{ i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ) )
7543, 67, 74sylc 60 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  )  e.  { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } )
76 nfrab1 3047 . . . . . . . 8  |-  F/_ i { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) }
77 nfcv 2629 . . . . . . . 8  |-  F/_ i RR
78 nfcv 2629 . . . . . . . 8  |-  F/_ i  <
7976, 77, 78nfsup 7923 . . . . . . 7  |-  F/_ i sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  )
80 nfcv 2629 . . . . . . 7  |-  F/_ i
( 0..^ M )
81 nfcv 2629 . . . . . . . . 9  |-  F/_ i Q
8281, 79nffv 5879 . . . . . . . 8  |-  F/_ i
( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )
83 nfcv 2629 . . . . . . . 8  |-  F/_ i  <_
84 nfcv 2629 . . . . . . . 8  |-  F/_ i
( L `  ( E `  ( S `  j ) ) )
8582, 83, 84nfbr 4497 . . . . . . 7  |-  F/ i ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `
 j ) ) )
86 fveq2 5872 . . . . . . . 8  |-  ( i  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `
 j ) ) ) } ,  RR ,  <  )  ->  ( Q `  i )  =  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  ) ) )
8786breq1d 4463 . . . . . . 7  |-  ( i  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `
 j ) ) ) } ,  RR ,  <  )  ->  (
( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) )  <->  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `  j
) ) ) ) )
8879, 80, 85, 87elrabf 3264 . . . . . 6  |-  ( sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  )  e.  { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) }  <-> 
( sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `
 j ) ) ) } ,  RR ,  <  )  e.  ( 0..^ M )  /\  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `
 j ) ) ) ) )
8975, 88sylib 196 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  )  e.  ( 0..^ M )  /\  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `  j )
) ) ) )
9089simprd 463 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `  j )
) ) )
9165, 90eqbrtrd 4473 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  <_  ( L `  ( E `  ( S `  j
) ) ) )
922ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  M  e.  NN )
931ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  Q  e.  ( P `  M
) )
9422ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  C  e.  RR )
9523ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  D  e.  RR )
9624ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  C  <  D )
97 0re 9608 . . . . . . . . . . 11  |-  0  e.  RR
98 1re 9607 . . . . . . . . . . 11  |-  1  e.  RR
99 0lt1 10087 . . . . . . . . . . 11  |-  0  <  1
10097, 98, 99ltleii 9719 . . . . . . . . . 10  |-  0  <_  1
101100a1i 11 . . . . . . . . 9  |-  ( ph  ->  0  <_  1 )
1022nnge1d 10590 . . . . . . . . 9  |-  ( ph  ->  1  <_  M )
103101, 102jca 532 . . . . . . . 8  |-  ( ph  ->  ( 0  <_  1  /\  1  <_  M ) )
104 1z 10906 . . . . . . . . . 10  |-  1  e.  ZZ
105104a1i 11 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
106 0z 10887 . . . . . . . . . 10  |-  0  e.  ZZ
107106a1i 11 . . . . . . . . 9  |-  ( ph  ->  0  e.  ZZ )
1082nnzd 10977 . . . . . . . . 9  |-  ( ph  ->  M  e.  ZZ )
109 elfz 11690 . . . . . . . . 9  |-  ( ( 1  e.  ZZ  /\  0  e.  ZZ  /\  M  e.  ZZ )  ->  (
1  e.  ( 0 ... M )  <->  ( 0  <_  1  /\  1  <_  M ) ) )
110105, 107, 108, 109syl3anc 1228 . . . . . . . 8  |-  ( ph  ->  ( 1  e.  ( 0 ... M )  <-> 
( 0  <_  1  /\  1  <_  M ) ) )
111103, 110mpbird 232 . . . . . . 7  |-  ( ph  ->  1  e.  ( 0 ... M ) )
112111ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  1  e.  ( 0 ... M
) )
113 simpr 461 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0..^ N ) )
114113adantr 465 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  j  e.  ( 0..^ N ) )
115 fourierdlem79.z . . . . . . . . . 10  |-  Z  =  ( ( S `  j )  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )
116 fzofzp1 11889 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
117116adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
11840, 117ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
119118, 43jca 532 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  e.  RR  /\  ( S `
 j )  e.  RR ) )
120 resubcl 9895 . . . . . . . . . . . . . 14  |-  ( ( ( S `  (
j  +  1 ) )  e.  RR  /\  ( S `  j )  e.  RR )  -> 
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  e.  RR )
121119, 120syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  e.  RR )
122 rehalfcl 10777 . . . . . . . . . . . . 13  |-  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  e.  RR  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  e.  RR )
123121, 122syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  e.  RR )
1249, 111ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Q `  1
)  e.  RR )
1253, 2, 1fourierdlem11 31741 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
126125simp1d 1008 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  RR )
127124, 126resubcld 9999 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q ` 
1 )  -  A
)  e.  RR )
128 2re 10617 . . . . . . . . . . . . . . 15  |-  2  e.  RR
129128a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  2  e.  RR )
130 2ne0 10640 . . . . . . . . . . . . . . 15  |-  2  =/=  0
131130a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  2  =/=  0 )
132127, 129, 131redivcld 10384 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  e.  RR )
133132adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( Q `  1 )  -  A )  / 
2 )  e.  RR )
134123, 133ifcld 3988 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  e.  RR )
13543, 134readdcld 9635 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  e.  RR )
136115, 135syl5eqel 2559 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  RR )
137128a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  2  e.  RR )
138 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
139 zre 10880 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ZZ  ->  j  e.  RR )
140138, 139syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0..^ N )  ->  j  e.  RR )
141 ltp1 10392 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  RR  ->  j  <  ( j  +  1 ) )
142140, 141syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0..^ N )  ->  j  <  ( j  +  1 ) )
143142adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  <  (
j  +  1 ) )
14429simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  H ) )
145144adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  H ) )
146 isorel 6221 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  /\  ( j  e.  ( 0 ... N
)  /\  ( j  +  1 )  e.  ( 0 ... N
) ) )  -> 
( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
147145, 42, 117, 146syl12anc 1226 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  < 
( j  +  1 )  <->  ( S `  j )  <  ( S `  ( j  +  1 ) ) ) )
148143, 147mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
14943, 118posdifd 10151 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  < 
( S `  (
j  +  1 ) )  <->  0  <  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) ) ) )
150148, 149mpbid 210 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  0  <  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) ) )
151 2pos 10639 . . . . . . . . . . . . . . . 16  |-  0  <  2
152151a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  0  <  2
)
153121, 137, 150, 152divgt0d 10493 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  0  <  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) )
154123, 153elrpd 11266 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  e.  RR+ )
1556simprd 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
156155simpld 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
157156simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q `  0
)  =  A )
158157eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  =  ( Q `
 0 ) )
1592nngt0d 10591 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  <  M )
160107, 108, 1593jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <  M ) )
161 fzolb 11814 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
162160, 161sylibr 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  e.  ( 0..^ M ) )
163 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
164163anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
165 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
166 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
167166fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
168165, 167breq12d 4466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
169164, 168imbi12d 320 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) ) ) )
170155simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
171170r19.21bi 2836 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
172169, 171vtoclg 3176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
17397, 172ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) )
174162, 173mpdan 668 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
175 1e0p1 11016 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  =  ( 0  +  1 )
176175eqcomi 2480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  +  1 )  =  1
177176fveq2i 5875 . . . . . . . . . . . . . . . . . . . 20  |-  ( Q `
 ( 0  +  1 ) )  =  ( Q `  1
)
178177a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q `  (
0  +  1 ) )  =  ( Q `
 1 ) )
179174, 178breqtrd 4477 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  1 ) )
180158, 179eqbrtrd 4473 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  <  ( Q `
 1 ) )
181126, 124posdifd 10151 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  <  ( Q `  1 )  <->  0  <  ( ( Q `
 1 )  -  A ) ) )
182180, 181mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( ( Q `  1 )  -  A ) )
183151a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  2 )
184127, 129, 182, 183divgt0d 10493 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  ( ( ( Q `  1
)  -  A )  /  2 ) )
185132, 184elrpd 11266 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  e.  RR+ )
186185adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( Q `  1 )  -  A )  / 
2 )  e.  RR+ )
187154, 186ifcld 3988 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  e.  RR+ )
18843, 187ltaddrpd 11297 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  (
( S `  j
)  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) ) )
18943, 135, 188ltled 9744 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <_  (
( S `  j
)  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) ) )
190115eqcomi 2480 . . . . . . . . . . 11  |-  ( ( S `  j )  +  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  =  Z
191190a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  =  Z )
192189, 191breqtrd 4477 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <_  Z
)
193115a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  =  ( ( S `  j
)  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) ) )
19443, 123readdcld 9635 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  e.  RR )
195 iftrue 3951 . . . . . . . . . . . . . . 15  |-  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  =  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )
196195adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  =  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )
197123leidd 10131 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  <_  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) )
198197adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  <_  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 ) )
199196, 198eqbrtrd 4473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )
200 iffalse 3954 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  =  ( ( ( Q `
 1 )  -  A )  /  2
) )
201200adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  =  ( ( ( Q `
 1 )  -  A )  /  2
) )
202 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  -.  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) )
203127ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( Q ` 
1 )  -  A
)  e.  RR )
204121adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  e.  RR )
205203, 204lenltd 9742 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( ( Q `
 1 )  -  A )  <_  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <->  -.  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ) )
206202, 205mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( Q ` 
1 )  -  A
)  <_  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) ) )
207 2rp 11237 . . . . . . . . . . . . . . . . 17  |-  2  e.  RR+
208207a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
2  e.  RR+ )
209203, 204, 208lediv1d 11310 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( ( Q `
 1 )  -  A )  <_  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <-> 
( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ) )
210206, 209mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )
211201, 210eqbrtrd 4473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )
212199, 211pm2.61dan 789 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )
213134, 123, 43leadd2d 10159 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 )  <-> 
( ( S `  j )  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  <_  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ) ) )
214212, 213mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  <_ 
( ( S `  j )  +  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ) )
21543recnd 9634 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  CC )
216118recnd 9634 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  CC )
217215, 216addcomd 9793 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( S `  (
j  +  1 ) ) )  =  ( ( S `  (
j  +  1 ) )  +  ( S `
 j ) ) )
218217oveq1d 6310 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  =  ( ( ( S `  ( j  +  1 ) )  +  ( S `  j ) )  /  2 ) )
219218oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 )  -  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( ( ( ( S `  ( j  +  1 ) )  +  ( S `  j ) )  /  2 )  -  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 ) ) )
220 halfaddsub 10784 . . . . . . . . . . . . . . . . 17  |-  ( ( ( S `  (
j  +  1 ) )  e.  CC  /\  ( S `  j )  e.  CC )  -> 
( ( ( ( ( S `  (
j  +  1 ) )  +  ( S `
 j ) )  /  2 )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( S `
 ( j  +  1 ) )  /\  ( ( ( ( S `  ( j  +  1 ) )  +  ( S `  j ) )  / 
2 )  -  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) )  =  ( S `
 j ) ) )
221216, 215, 220syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( S `  ( j  +  1 ) )  +  ( S `  j ) )  /  2 )  +  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 ) )  =  ( S `  (
j  +  1 ) )  /\  ( ( ( ( S `  ( j  +  1 ) )  +  ( S `  j ) )  /  2 )  -  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 ) )  =  ( S `  j
) ) )
222221simprd 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  (
j  +  1 ) )  +  ( S `
 j ) )  /  2 )  -  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( S `
 j ) )
223219, 222eqtrd 2508 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 )  -  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( S `
 j ) )
224215, 216jca 532 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  e.  CC  /\  ( S `
 ( j  +  1 ) )  e.  CC ) )
225 addcl 9586 . . . . . . . . . . . . . . . . 17  |-  ( ( ( S `  j
)  e.  CC  /\  ( S `  ( j  +  1 ) )  e.  CC )  -> 
( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  e.  CC )
226224, 225syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( S `  (
j  +  1 ) ) )  e.  CC )
227 halfcl 10776 . . . . . . . . . . . . . . . 16  |-  ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  e.  CC  ->  (
( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  /  2 )  e.  CC )
228226, 227syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  e.  CC )
229123recnd 9634 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  e.  CC )
230228, 229, 215subsub23d 31374 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  /  2 )  -  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 ) )  =  ( S `  j
)  <->  ( ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 )  -  ( S `  j ) )  =  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ) )
231223, 230mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 )  -  ( S `  j ) )  =  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )
232228, 215, 229subaddd 9960 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  /  2 )  -  ( S `  j ) )  =  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 )  <-> 
( ( S `  j )  +  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) )  =  ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 ) ) )
233231, 232mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 ) )
234 avglt2 10789 . . . . . . . . . . . . . 14  |-  ( ( ( S `  j
)  e.  RR  /\  ( S `  ( j  +  1 ) )  e.  RR )  -> 
( ( S `  j )  <  ( S `  ( j  +  1 ) )  <-> 
( ( ( S `
 j )  +  ( S `  (
j  +  1 ) ) )  /  2
)  <  ( S `  ( j  +  1 ) ) ) )
23543, 118, 234syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  < 
( S `  (
j  +  1 ) )  <->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  <  ( S `  ( j  +  1 ) ) ) )
236148, 235mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  <  ( S `  ( j  +  1 ) ) )
237233, 236eqbrtrd 4473 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  <  ( S `
 ( j  +  1 ) ) )
238135, 194, 118, 214, 237lelttrd 9751 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  < 
( S `  (
j  +  1 ) ) )
239193, 238eqbrtrd 4473 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  <  ( S `  ( j  +  1 ) ) )
240136, 192, 2393jca 1176 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  e.  RR  /\  ( S `
 j )  <_  Z  /\  Z  <  ( S `  ( j  +  1 ) ) ) )
241118rexrd 9655 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR* )
242 elico2 11600 . . . . . . . . 9  |-  ( ( ( S `  j
)  e.  RR  /\  ( S `  ( j  +  1 ) )  e.  RR* )  ->  ( Z  e.  ( ( S `  j ) [,) ( S `  (
j  +  1 ) ) )  <->  ( Z  e.  RR  /\  ( S `
 j )  <_  Z  /\  Z  <  ( S `  ( j  +  1 ) ) ) ) )
24343, 241, 242syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  e.  ( ( S `  j ) [,) ( S `  ( j  +  1 ) ) )  <->  ( Z  e.  RR  /\  ( S `
 j )  <_  Z  /\  Z  <  ( S `  ( j  +  1 ) ) ) ) )
244240, 243mpbird 232 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  ( ( S `  j
) [,) ( S `
 ( j  +  1 ) ) ) )
245244adantr 465 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  Z  e.  ( ( S `  j ) [,) ( S `  ( j  +  1 ) ) ) )
246126ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  e.  RR )
247125simp2d 1009 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR )
24866, 247syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  B  e.  RR )
249248adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  B  e.  RR )
250125simp3d 1010 . . . . . . . . . 10  |-  ( ph  ->  A  <  B )
251250ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  <  B )
25243adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  e.  RR )
253 simpr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  =  B )
254188, 191breqtrd 4477 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  Z
)
255247, 126resubcld 9999 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  -  A
)  e.  RR )
25611, 255syl5eqel 2559 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  RR )
257256adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  RR )
258123adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  e.  RR )
259133adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( Q ` 
1 )  -  A
)  /  2 )  e.  RR )
260 simpr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )
261121adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  e.  RR )
262127ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( Q `  1
)  -  A )  e.  RR )
263207a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  2  e.  RR+ )
264261, 262, 263ltdiv1d 11309 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A )  <->  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 )  < 
( ( ( Q `
 1 )  -  A )  /  2
) ) )
265260, 264mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  <  ( ( ( Q `  1 )  -  A )  / 
2 ) )
266258, 259, 265ltled 9744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  <_  ( ( ( Q `  1 )  -  A )  / 
2 ) )
267196, 266eqbrtrd 4473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( Q `
 1 )  -  A )  /  2
) )
268200adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  =  ( ( ( Q `
 1 )  -  A )  /  2
) )
269132leidd 10131 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( Q `  1
)  -  A )  /  2 ) )
270269adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( Q `  1
)  -  A )  /  2 ) )
271268, 270eqbrtrd 4473 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( Q `
 1 )  -  A )  /  2
) )
272271adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( Q `
 1 )  -  A )  /  2
) )
273267, 272pm2.61dan 789 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_ 
( ( ( Q `
 1 )  -  A )  /  2
) )
274255, 129, 131redivcld 10384 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  -  A )  /  2
)  e.  RR )
275126rexrd 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  RR* )
276247rexrd 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  B  e.  RR* )
2773, 2, 1fourierdlem15 31745 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
278277, 111ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Q `  1
)  e.  ( A [,] B ) )
279 iccleub 11592 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 1 )  e.  ( A [,] B
) )  ->  ( Q `  1 )  <_  B )
280275, 276, 278, 279syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Q `  1
)  <_  B )
281124, 247, 126lesub1d 10171 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( Q ` 
1 )  <_  B  <->  ( ( Q `  1
)  -  A )  <_  ( B  -  A ) ) )
282280, 281mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( Q ` 
1 )  -  A
)  <_  ( B  -  A ) )
283207a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  2  e.  RR+ )
284127, 255, 283lediv1d 11310 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  <_  ( B  -  A )  <->  ( ( ( Q ` 
1 )  -  A
)  /  2 )  <_  ( ( B  -  A )  / 
2 ) ) )
285282, 284mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( ( B  -  A )  /  2 ) )
28611eqcomi 2480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  -  A )  =  T
287286oveq1i 6305 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( B  -  A )  /  2 )  =  ( T  /  2
)
288287a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( B  -  A )  /  2
)  =  ( T  /  2 ) )
289126, 247posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
290250, 289mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  <  ( B  -  A ) )
291286a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( B  -  A
)  =  T )
292290, 291breqtrd 4477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  0  <  T )
293256, 292elrpd 11266 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  RR+ )
294 rphalflt 11258 . . . . . . . . . . . . . . . . . . . 20  |-  ( T  e.  RR+  ->  ( T  /  2 )  < 
T )
295293, 294syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( T  /  2
)  <  T )
296288, 295eqbrtrd 4473 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  -  A )  /  2
)  <  T )
297132, 274, 256, 285, 296lelttrd 9751 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <  T )
298132, 256, 297ltled 9744 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <_  T )
299298adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( Q `  1 )  -  A )  / 
2 )  <_  T
)
300134, 133, 257, 273, 299letrd 9750 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_  T )
301134, 257, 43leadd2d 10159 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  <_  T 
<->  ( ( S `  j )  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  <_  ( ( S `
 j )  +  T ) ) )
302300, 301mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  <_ 
( ( S `  j )  +  T
) )
303193, 302eqbrtrd 4473 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  <_  (
( S `  j
)  +  T ) )
304136, 254, 3033jca 1176 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  e.  RR  /\  ( S `
 j )  < 
Z  /\  Z  <_  ( ( S `  j
)  +  T ) ) )
30543rexrd 9655 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR* )
30643, 257readdcld 9635 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  T )  e.  RR )
307 elioc2 11599 . . . . . . . . . . . 12  |-  ( ( ( S `  j
)  e.  RR*  /\  (
( S `  j
)  +  T )  e.  RR )  -> 
( Z  e.  ( ( S `  j
) (,] ( ( S `  j )  +  T ) )  <-> 
( Z  e.  RR  /\  ( S `  j
)  <  Z  /\  Z  <_  ( ( S `
 j )  +  T ) ) ) )
308305, 306, 307syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  e.  ( ( S `  j ) (,] (
( S `  j
)  +  T ) )  <->  ( Z  e.  RR  /\  ( S `
 j )  < 
Z  /\  Z  <_  ( ( S `  j
)  +  T ) ) ) )
309304, 308mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  ( ( S `  j
) (,] ( ( S `  j )  +  T ) ) )
310309adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  Z  e.  ( ( S `  j ) (,] (
( S `  j
)  +  T ) ) )
311246, 249, 251, 11, 12, 252, 253, 310fourierdlem26 31756 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  Z )  =  ( A  +  ( Z  -  ( S `  j )
) ) )
312193oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  -  ( S `  j ) )  =  ( ( ( S `  j
)  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  -  ( S `  j ) ) )
313312oveq2d 6311 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  ( Z  -  ( S `  j )
) )  =  ( A  +  ( ( ( S `  j
)  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  -  ( S `  j ) ) ) )
314313adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( A  +  ( Z  -  ( S `  j ) ) )  =  ( A  +  ( ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  -  ( S `  j ) ) ) )
315134recnd 9634 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) )  e.  CC )
316215, 315pncan2d 9944 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  if ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  -  ( S `  j ) )  =  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )
317316oveq2d 6311 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  ( ( ( S `
 j )  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) ,  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) ,  ( ( ( Q `
 1 )  -  A )  /  2
) ) )  -  ( S `  j ) ) )  =  ( A  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) ) )
318317adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( A  +  ( (
( S `  j
)  +  if ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  -  ( S `  j ) ) )  =  ( A  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) ) )
319311, 314, 3183eqtrd 2512 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  Z )  =  ( A  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) ) )
320195oveq2d 6311 . . . . . . . . . . 11  |-  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A )  ->  ( A  +  if (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  =  ( A  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ) )
321320adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  if (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  =  ( A  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ) )
32266, 126syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  A  e.  RR )
323322, 123readdcld 9635 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  e.  RR )
324323adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )  e.  RR )
325322, 133readdcld 9635 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  ( ( ( Q `
 1 )  -  A )  /  2
) )  e.  RR )
326325adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( Q `  1
)  -  A )  /  2 ) )  e.  RR )
327124ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( Q `  1 )  e.  RR )
328322adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  A  e.  RR )
329258, 259, 328ltadd2d 9749 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 )  <  ( ( ( Q `  1 )  -  A )  / 
2 )  <->  ( A  +  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 ) )  < 
( A  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) ) ) )
330265, 329mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )  <  ( A  +  ( ( ( Q `
 1 )  -  A )  /  2
) ) )
331124, 126jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( Q ` 
1 )  e.  RR  /\  A  e.  RR ) )
332 readdcl 9587 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  1
)  e.  RR  /\  A  e.  RR )  ->  ( ( Q ` 
1 )  +  A
)  e.  RR )
333331, 332syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( Q ` 
1 )  +  A
)  e.  RR )
334 rehalfcl 10777 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Q `  1
)  +  A )  e.  RR  ->  (
( ( Q ` 
1 )  +  A
)  /  2 )  e.  RR )
335333, 334syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  e.  RR )
336335recnd 9634 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  e.  CC )
337132recnd 9634 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  e.  CC )
338336, 337npcand 9946 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) )  =  ( ( ( Q `  1
)  +  A )  /  2 ) )
339338eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  =  ( ( ( ( ( Q `
 1 )  +  A )  /  2
)  -  ( ( ( Q `  1
)  -  A )  /  2 ) )  +  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )
340124recnd 9634 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Q `  1
)  e.  CC )
341126recnd 9634 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  CC )
342 halfaddsub 10784 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  1
)  e.  CC  /\  A  e.  CC )  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  +  ( ( ( Q `
 1 )  -  A )  /  2
) )  =  ( Q `  1 )  /\  ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  =  A ) )
343340, 341, 342syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  +  ( ( ( Q `
 1 )  -  A )  /  2
) )  =  ( Q `  1 )  /\  ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  =  A ) )
344343simprd 463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( Q `  1 )  +  A )  / 
2 )  -  (
( ( Q ` 
1 )  -  A
)  /  2 ) )  =  A )
345344oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  +  ( ( ( Q ` 
1 )