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

Theorem fourierdlem79 37317
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 . . . . . . . 8  |-  ( ph  ->  Q  e.  ( P `
 M ) )
2 fourierdlem79.m . . . . . . . . 9  |-  ( ph  ->  M  e.  NN )
3 fourierdlem79.p . . . . . . . . . 10  |-  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 37240 . . . . . . . . 9  |-  ( 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 17 . . . . . . . 8  |-  ( 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 . . . . . . 7  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
76simpld 457 . . . . . 6  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
8 elmapi 7477 . . . . . 6  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
97, 8syl 17 . . . . 5  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
109adantr 463 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Q : ( 0 ... M ) --> RR )
11 fourierdlem79.t . . . . . . . . 9  |-  T  =  ( B  -  A
)
12 fourierdlem79.e . . . . . . . . 9  |-  E  =  ( x  e.  RR  |->  ( x  +  (
( |_ `  (
( B  -  x
)  /  T ) )  x.  T ) ) )
13 fourierdlem79.l . . . . . . . . 9  |-  L  =  ( y  e.  ( A (,] B ) 
|->  if ( y  =  B ,  A , 
y ) )
14 fourierdlem79.i . . . . . . . . 9  |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ,  RR ,  <  ) )
153, 2, 1, 11, 12, 13, 14fourierdlem37 37275 . . . . . . . 8  |-  ( 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 457 . . . . . . 7  |-  ( ph  ->  I : RR --> ( 0..^ M ) )
17 fzossfz 11875 . . . . . . . 8  |-  ( 0..^ M )  C_  (
0 ... M )
1817a1i 11 . . . . . . 7  |-  ( ph  ->  ( 0..^ M ) 
C_  ( 0 ... M ) )
1916, 18fssd 5722 . . . . . 6  |-  ( ph  ->  I : RR --> ( 0 ... M ) )
2019adantr 463 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  I : RR --> ( 0 ... M
) )
21 fourierdlem79.c . . . . . . . . . . . . 13  |-  ( ph  ->  C  e.  RR )
22 fourierdlem79.d . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  RR )
23 fourierdlem79.cltd . . . . . . . . . . . . 13  |-  ( ph  ->  C  <  D )
24 fourierdlem79.o . . . . . . . . . . . . 13  |-  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 ) ) ) } )
25 fourierdlem79.h . . . . . . . . . . . . 13  |-  H  =  ( { C ,  D }  u.  { x  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
26 fourierdlem79.n . . . . . . . . . . . . 13  |-  N  =  ( ( # `  H
)  -  1 )
27 fourierdlem79.s . . . . . . . . . . . . 13  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
2811, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27fourierdlem54 37292 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  e.  NN  /\  S  e.  ( O `  N
) )  /\  S  Isom  <  ,  <  (
( 0 ... N
) ,  H ) ) )
2928simpld 457 . . . . . . . . . . 11  |-  ( ph  ->  ( N  e.  NN  /\  S  e.  ( O `
 N ) ) )
3029simprd 461 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ( O `
 N ) )
3130adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  e.  ( O `  N ) )
3229simpld 457 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  NN )
3332adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  N  e.  NN )
3424fourierdlem2 37240 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
3533, 34syl 17 . . . . . . . . 9  |-  ( (
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 ) ) ) ) ) )
3631, 35mpbid 210 . . . . . . . 8  |-  ( (
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 ) ) ) ) )
3736simpld 457 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  e.  ( RR  ^m  ( 0 ... N ) ) )
38 elmapi 7477 . . . . . . 7  |-  ( S  e.  ( RR  ^m  ( 0 ... N
) )  ->  S : ( 0 ... N ) --> RR )
3937, 38syl 17 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S : ( 0 ... N ) --> RR )
40 elfzofz 11872 . . . . . . 7  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ( 0 ... N
) )
4140adantl 464 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  e.  ( 0 ... N ) )
4239, 41ffvelrnd 6009 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR )
4320, 42ffvelrnd 6009 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( I `  ( S `  j ) )  e.  ( 0 ... M ) )
4410, 43ffvelrnd 6009 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  e.  RR )
4544rexrd 9672 . 2  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  e.  RR* )
4616adantr 463 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  I : RR --> ( 0..^ M ) )
4746, 42ffvelrnd 6009 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( I `  ( S `  j ) )  e.  ( 0..^ M ) )
48 fzofzp1 11944 . . . . 5  |-  ( ( I `  ( S `
 j ) )  e.  ( 0..^ M )  ->  ( (
I `  ( S `  j ) )  +  1 )  e.  ( 0 ... M ) )
4947, 48syl 17 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( I `
 ( S `  j ) )  +  1 )  e.  ( 0 ... M ) )
5010, 49ffvelrnd 6009 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( ( I `  ( S `  j ) )  +  1 ) )  e.  RR )
5150rexrd 9672 . 2  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( ( I `  ( S `  j ) )  +  1 ) )  e.  RR* )
5214a1i 11 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  x ) ) } ,  RR ,  <  ) ) )
53 fveq2 5848 . . . . . . . . . 10  |-  ( x  =  ( S `  j )  ->  ( E `  x )  =  ( E `  ( S `  j ) ) )
5453fveq2d 5852 . . . . . . . . 9  |-  ( x  =  ( S `  j )  ->  ( L `  ( E `  x ) )  =  ( L `  ( E `  ( S `  j ) ) ) )
5554breq2d 4406 . . . . . . . 8  |-  ( x  =  ( S `  j )  ->  (
( Q `  i
)  <_  ( L `  ( E `  x
) )  <->  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) ) )
5655rabbidv 3050 . . . . . . 7  |-  ( x  =  ( S `  j )  ->  { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  x )
) }  =  {
i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `
 j ) ) ) } )
5756supeq1d 7938 . . . . . 6  |-  ( 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 ,  <  ) )
5857adantl 464 . . . . 5  |-  ( ( ( 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 ,  <  ) )
59 ltso 9695 . . . . . . 7  |-  <  Or  RR
6059supex 7955 . . . . . 6  |-  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  )  e. 
_V
6160a1i 11 . . . . 5  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  )  e.  _V )
6252, 58, 42, 61fvmptd 5937 . . . 4  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( I `  ( S `  j ) )  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )
6362fveq2d 5852 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  =  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) ) )
64 simpl 455 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ph )
6564, 42jca 530 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ph  /\  ( S `  j )  e.  RR ) )
66 eleq1 2474 . . . . . . . . 9  |-  ( x  =  ( S `  j )  ->  (
x  e.  RR  <->  ( S `  j )  e.  RR ) )
6766anbi2d 702 . . . . . . . 8  |-  ( x  =  ( S `  j )  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  ( S `  j
)  e.  RR ) ) )
6857, 56eleq12d 2484 . . . . . . . 8  |-  ( 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
) ) ) } ) )
6967, 68imbi12d 318 . . . . . . 7  |-  ( 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 ) ) ) } ) ) )
7015simprd 461 . . . . . . . 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 ) ) } ) )
7170imp 427 . . . . . . 7  |-  ( (
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
) ) } )
7269, 71vtoclg 3116 . . . . . 6  |-  ( ( 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 )
) ) } ) )
7342, 65, 72sylc 59 . . . . 5  |-  ( (
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 ) ) ) } )
74 nfrab1 2987 . . . . . . 7  |-  F/_ i { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) }
75 nfcv 2564 . . . . . . 7  |-  F/_ i RR
76 nfcv 2564 . . . . . . 7  |-  F/_ i  <
7774, 75, 76nfsup 7943 . . . . . 6  |-  F/_ i sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  )
78 nfcv 2564 . . . . . 6  |-  F/_ i
( 0..^ M )
79 nfcv 2564 . . . . . . . 8  |-  F/_ i Q
8079, 77nffv 5855 . . . . . . 7  |-  F/_ i
( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )
81 nfcv 2564 . . . . . . 7  |-  F/_ i  <_
82 nfcv 2564 . . . . . . 7  |-  F/_ i
( L `  ( E `  ( S `  j ) ) )
8380, 81, 82nfbr 4438 . . . . . 6  |-  F/ i ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `
 j ) ) )
84 fveq2 5848 . . . . . . 7  |-  ( 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 ,  <  ) ) )
8584breq1d 4404 . . . . . 6  |-  ( 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
) ) ) ) )
8677, 78, 83, 85elrabf 3204 . . . . 5  |-  ( 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 ) ) ) ) )
8773, 86sylib 196 . . . 4  |-  ( (
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 )
) ) ) )
8887simprd 461 . . 3  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( L `  ( E `  ( S `  j
) ) ) } ,  RR ,  <  ) )  <_  ( L `  ( E `  ( S `  j )
) ) )
8963, 88eqbrtrd 4414 . 2  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Q `  ( I `  ( S `  j )
) )  <_  ( L `  ( E `  ( S `  j
) ) ) )
902ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  M  e.  NN )
911ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  Q  e.  ( P `  M
) )
9221ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  C  e.  RR )
9322ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  D  e.  RR )
9423ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  C  <  D )
95 0le1 10115 . . . . . . . 8  |-  0  <_  1
9695a1i 11 . . . . . . 7  |-  ( ph  ->  0  <_  1 )
972nnge1d 10618 . . . . . . 7  |-  ( ph  ->  1  <_  M )
98 1zzd 10935 . . . . . . . 8  |-  ( ph  ->  1  e.  ZZ )
99 0zd 10916 . . . . . . . 8  |-  ( ph  ->  0  e.  ZZ )
1002nnzd 11006 . . . . . . . 8  |-  ( ph  ->  M  e.  ZZ )
101 elfz 11730 . . . . . . . 8  |-  ( ( 1  e.  ZZ  /\  0  e.  ZZ  /\  M  e.  ZZ )  ->  (
1  e.  ( 0 ... M )  <->  ( 0  <_  1  /\  1  <_  M ) ) )
10298, 99, 100, 101syl3anc 1230 . . . . . . 7  |-  ( ph  ->  ( 1  e.  ( 0 ... M )  <-> 
( 0  <_  1  /\  1  <_  M ) ) )
10396, 97, 102mpbir2and 923 . . . . . 6  |-  ( ph  ->  1  e.  ( 0 ... M ) )
104103ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  1  e.  ( 0 ... M
) )
105 simplr 754 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  j  e.  ( 0..^ N ) )
106 fourierdlem79.z . . . . . . . 8  |-  Z  =  ( ( S `  j )  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )
107 fzofzp1 11944 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 0..^ N )  ->  ( j  +  1 )  e.  ( 0 ... N
) )
108107adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  +  1 )  e.  ( 0 ... N ) )
10939, 108ffvelrnd 6009 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR )
110109, 42resubcld 10027 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  e.  RR )
111110rehalfcld 10825 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  e.  RR )
1129, 103ffvelrnd 6009 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q `  1
)  e.  RR )
1133, 2, 1fourierdlem11 37249 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
114113simp1d 1009 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  RR )
115112, 114resubcld 10027 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q ` 
1 )  -  A
)  e.  RR )
116115rehalfcld 10825 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  e.  RR )
117116adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( Q `  1 )  -  A )  / 
2 )  e.  RR )
118111, 117ifcld 3927 . . . . . . . . 9  |-  ( (
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 )
11942, 118readdcld 9652 . . . . . . . 8  |-  ( (
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 )
120106, 119syl5eqel 2494 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  RR )
121 2re 10645 . . . . . . . . . . . . . 14  |-  2  e.  RR
122121a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  2  e.  RR )
123 elfzoelz 11857 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0..^ N )  ->  j  e.  ZZ )
124123zred 11007 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0..^ N )  ->  j  e.  RR )
125124ltp1d 10515 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0..^ N )  ->  j  <  ( j  +  1 ) )
126125adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  j  <  (
j  +  1 ) )
12728simprd 461 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  H ) )
128127adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  S  Isom  <  ,  <  ( ( 0 ... N ) ,  H ) )
129 isorel 6204 . . . . . . . . . . . . . . . 16  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  H )  /\  ( j  e.  ( 0 ... N
)  /\  ( j  +  1 )  e.  ( 0 ... N
) ) )  -> 
( j  <  (
j  +  1 )  <-> 
( S `  j
)  <  ( S `  ( j  +  1 ) ) ) )
130128, 41, 108, 129syl12anc 1228 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( j  < 
( j  +  1 )  <->  ( S `  j )  <  ( S `  ( j  +  1 ) ) ) )
131126, 130mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  ( S `  ( j  +  1 ) ) )
13242, 109posdifd 10178 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  < 
( S `  (
j  +  1 ) )  <->  0  <  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) ) ) )
133131, 132mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  0  <  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) ) )
134 2pos 10667 . . . . . . . . . . . . . 14  |-  0  <  2
135134a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  0  <  2
)
136110, 122, 133, 135divgt0d 10520 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  0  <  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) )
137111, 136elrpd 11300 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  e.  RR+ )
138121a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  2  e.  RR )
1392nngt0d 10619 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  M )
140 fzolb 11863 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
14199, 100, 139, 140syl3anbrc 1181 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  e.  ( 0..^ M ) )
142 0re 9625 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
143 eleq1 2474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  0  ->  (
i  e.  ( 0..^ M )  <->  0  e.  ( 0..^ M ) ) )
144143anbi2d 702 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  0  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  0  e.  ( 0..^ M ) ) ) )
145 fveq2 5848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  0  ->  ( Q `  i )  =  ( Q ` 
0 ) )
146 oveq1 6284 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  0  ->  (
i  +  1 )  =  ( 0  +  1 ) )
147146fveq2d 5852 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  0  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( 0  +  1 ) ) )
148145, 147breq12d 4407 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  0  ->  (
( Q `  i
)  <  ( Q `  ( i  +  1 ) )  <->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
149144, 148imbi12d 318 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  0  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( Q `  i
)  <  ( Q `  ( i  +  1 ) ) )  <->  ( ( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) ) ) )
1506simprd 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
151150simprd 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
152151r19.21bi 2772 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  <  ( Q `  ( i  +  1 ) ) )
153149, 152vtoclg 3116 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  (
( ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q `  0 )  < 
( Q `  (
0  +  1 ) ) ) )
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  0  e.  ( 0..^ M ) )  ->  ( Q ` 
0 )  <  ( Q `  ( 0  +  1 ) ) )
155141, 154mpdan 666 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  <  ( Q `  ( 0  +  1 ) ) )
156150simpld 457 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
157156simpld 457 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  0
)  =  A )
158 0p1e1 10687 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  1 )  =  1
159158fveq2i 5851 . . . . . . . . . . . . . . . . 17  |-  ( Q `
 ( 0  +  1 ) )  =  ( Q `  1
)
160159a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  (
0  +  1 ) )  =  ( Q `
 1 ) )
161155, 157, 1603brtr3d 4423 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  <  ( Q `
 1 ) )
162114, 112posdifd 10178 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  <  ( Q `  1 )  <->  0  <  ( ( Q `
 1 )  -  A ) ) )
163161, 162mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( ( Q `  1 )  -  A ) )
164134a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  2 )
165115, 138, 163, 164divgt0d 10520 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( ( ( Q `  1
)  -  A )  /  2 ) )
166116, 165elrpd 11300 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  e.  RR+ )
167166adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( Q `  1 )  -  A )  / 
2 )  e.  RR+ )
168137, 167ifcld 3927 . . . . . . . . . 10  |-  ( (
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+ )
16942, 168ltaddrpd 11332 . . . . . . . . 9  |-  ( (
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 ) ) ) )
17042, 119, 169ltled 9764 . . . . . . . 8  |-  ( (
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 ) ) ) )
171170, 106syl6breqr 4434 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <_  Z
)
17242, 111readdcld 9652 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  e.  RR )
173 iftrue 3890 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
174173adantl 464 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
175111leidd 10158 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  <_  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) )
176175adantr 463 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
177174, 176eqbrtrd 4414 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
178 iffalse 3893 . . . . . . . . . . . . 13  |-  ( -.  ( ( 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
) )
179178adantl 464 . . . . . . . . . . . 12  |-  ( ( ( 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
) )
180115ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( Q ` 
1 )  -  A
)  e.  RR )
181110adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  e.  RR )
182 2rp 11269 . . . . . . . . . . . . . 14  |-  2  e.  RR+
183182a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
2  e.  RR+ )
184 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  ->  -.  ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) )
185180, 181, 184nltled 9766 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( Q ` 
1 )  -  A
)  <_  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) ) )
186180, 181, 183, 185lediv1dd 11357 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )
187179, 186eqbrtrd 4414 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
188177, 187pm2.61dan 792 . . . . . . . . . 10  |-  ( (
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 ) )
189118, 111, 42, 188leadd2dd 10206 . . . . . . . . 9  |-  ( (
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 ) ) )
19042recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  CC )
191109recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  CC )
192190, 191addcomd 9815 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( S `  (
j  +  1 ) ) )  =  ( ( S `  (
j  +  1 ) )  +  ( S `
 j ) ) )
193192oveq1d 6292 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  =  ( ( ( S `  ( j  +  1 ) )  +  ( S `  j ) )  /  2 ) )
194193oveq1d 6292 . . . . . . . . . . . . 13  |-  ( (
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 ) ) )
195 halfaddsub 10812 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
196191, 190, 195syl2anc 659 . . . . . . . . . . . . . 14  |-  ( (
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
) ) )
197196simprd 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  (
j  +  1 ) )  +  ( S `
 j ) )  /  2 )  -  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( S `
 j ) )
198194, 197eqtrd 2443 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 )  -  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( S `
 j ) )
199190, 191addcld 9644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( S `  (
j  +  1 ) ) )  e.  CC )
200199halfcld 10823 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  e.  CC )
201111recnd 9651 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  / 
2 )  e.  CC )
202200, 201, 190subsub23d 36827 . . . . . . . . . . . 12  |-  ( (
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 ) ) )
203198, 202mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 )  -  ( S `  j ) )  =  ( ( ( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )
204200, 190, 201subaddd 9984 . . . . . . . . . . 11  |-  ( (
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 ) ) )
205203, 204mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  =  ( ( ( S `  j
)  +  ( S `
 ( j  +  1 ) ) )  /  2 ) )
206 avglt2 10817 . . . . . . . . . . . 12  |-  ( ( ( S `  j
)  e.  RR  /\  ( S `  ( j  +  1 ) )  e.  RR )  -> 
( ( S `  j )  <  ( S `  ( j  +  1 ) )  <-> 
( ( ( S `
 j )  +  ( S `  (
j  +  1 ) ) )  /  2
)  <  ( S `  ( j  +  1 ) ) ) )
20742, 109, 206syl2anc 659 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  < 
( S `  (
j  +  1 ) )  <->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  <  ( S `  ( j  +  1 ) ) ) )
208131, 207mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( S `  j )  +  ( S `  ( j  +  1 ) ) )  / 
2 )  <  ( S `  ( j  +  1 ) ) )
209205, 208eqbrtrd 4414 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  <  ( S `
 ( j  +  1 ) ) )
210119, 172, 109, 189, 209lelttrd 9773 . . . . . . . 8  |-  ( (
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 ) ) )
211106, 210syl5eqbr 4427 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  <  ( S `  ( j  +  1 ) ) )
212109rexrd 9672 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  ( j  +  1 ) )  e.  RR* )
213 elico2 11640 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) )
21442, 212, 213syl2anc 659 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  e.  ( ( S `  j ) [,) ( S `  ( j  +  1 ) ) )  <->  ( Z  e.  RR  /\  ( S `
 j )  <_  Z  /\  Z  <  ( S `  ( j  +  1 ) ) ) ) )
215120, 171, 211, 214mpbir3and 1180 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  ( ( S `  j
) [,) ( S `
 ( j  +  1 ) ) ) )
216215adantr 463 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  Z  e.  ( ( S `  j ) [,) ( S `  ( j  +  1 ) ) ) )
217114ad2antrr 724 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  e.  RR )
218113simp2d 1010 . . . . . . . . 9  |-  ( ph  ->  B  e.  RR )
219218ad2antrr 724 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  B  e.  RR )
220113simp3d 1011 . . . . . . . . 9  |-  ( ph  ->  A  <  B )
221220ad2antrr 724 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  A  <  B )
22242adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( S `  j )  e.  RR )
223 simpr 459 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  j ) )  =  B )
224169, 106syl6breqr 4434 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  <  Z
)
225218, 114resubcld 10027 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  -  A
)  e.  RR )
22611, 225syl5eqel 2494 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e.  RR )
227226adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  T  e.  RR )
228111adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  e.  RR )
229116ad2antrr 724 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( Q ` 
1 )  -  A
)  /  2 )  e.  RR )
230110adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  e.  RR )
231115ad2antrr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( Q `  1
)  -  A )  e.  RR )
232182a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  2  e.  RR+ )
233 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )
234230, 231, 232, 233ltdiv1dd 11356 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  <  ( ( ( Q `  1 )  -  A )  / 
2 ) )
235228, 229, 234ltled 9764 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 )  <_  ( ( ( Q `  1 )  -  A )  / 
2 ) )
236174, 235eqbrtrd 4414 . . . . . . . . . . . . . 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
) )
237178adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
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
) )
238116leidd 10158 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( Q `  1
)  -  A )  /  2 ) )
239238adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( (
( Q `  1
)  -  A )  /  2 ) )
240237, 239eqbrtrd 4414 . . . . . . . . . . . . . . 15  |-  ( (
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
) )
241240adantlr 713 . . . . . . . . . . . . . 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
) )
242236, 241pm2.61dan 792 . . . . . . . . . . . . 13  |-  ( (
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
) )
243225rehalfcld 10825 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  -  A )  /  2
)  e.  RR )
244182a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  2  e.  RR+ )
245114rexrd 9672 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR* )
246218rexrd 9672 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  RR* )
2473, 2, 1fourierdlem15 37253 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q : ( 0 ... M ) --> ( A [,] B ) )
248247, 103ffvelrnd 6009 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( Q `  1
)  e.  ( A [,] B ) )
249 iccleub 11632 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( Q `
 1 )  e.  ( A [,] B
) )  ->  ( Q `  1 )  <_  B )
250245, 246, 248, 249syl3anc 1230 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( Q `  1
)  <_  B )
251112, 218, 114, 250lesub1dd 10207 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( Q ` 
1 )  -  A
)  <_  ( B  -  A ) )
252115, 225, 244, 251lediv1dd 11357 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <_  ( ( B  -  A )  /  2 ) )
25311eqcomi 2415 . . . . . . . . . . . . . . . . . 18  |-  ( B  -  A )  =  T
254253oveq1i 6287 . . . . . . . . . . . . . . . . 17  |-  ( ( B  -  A )  /  2 )  =  ( T  /  2
)
255114, 218posdifd 10178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
256220, 255mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <  ( B  -  A ) )
257256, 11syl6breqr 4434 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  T )
258226, 257elrpd 11300 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  e.  RR+ )
259 rphalflt 11291 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  RR+  ->  ( T  /  2 )  < 
T )
260258, 259syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( T  /  2
)  <  T )
261254, 260syl5eqbr 4427 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  -  A )  /  2
)  <  T )
262116, 243, 226, 252, 261lelttrd 9773 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <  T )
263116, 226, 262ltled 9764 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  <_  T )
264263adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( ( Q `  1 )  -  A )  / 
2 )  <_  T
)
265118, 117, 227, 242, 264letrd 9772 . . . . . . . . . . . 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 ) )  <_  T )
266118, 227, 42, 265leadd2dd 10206 . . . . . . . . . . 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 )  +  T
) )
267106, 266syl5eqbr 4427 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  <_  (
( S `  j
)  +  T ) )
26842rexrd 9672 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( S `  j )  e.  RR* )
26942, 227readdcld 9652 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( ( S `
 j )  +  T )  e.  RR )
270 elioc2 11639 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
271268, 269, 270syl2anc 659 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( Z  e.  ( ( S `  j ) (,] (
( S `  j
)  +  T ) )  <->  ( Z  e.  RR  /\  ( S `
 j )  < 
Z  /\  Z  <_  ( ( S `  j
)  +  T ) ) ) )
272120, 224, 267, 271mpbir3and 1180 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  Z  e.  ( ( S `  j
) (,] ( ( S `  j )  +  T ) ) )
273272adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  Z  e.  ( ( S `  j ) (,] (
( S `  j
)  +  T ) ) )
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 37264 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  Z )  =  ( A  +  ( Z  -  ( S `  j )
) ) )
275106a1i 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 ) ) ) )
276275oveq1d 6292 . . . . . . . . 9  |-  ( (
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 ) ) )
277276oveq2d 6293 . . . . . . . 8  |-  ( (
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 ) ) ) )
278277adantr 463 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
279118recnd 9651 . . . . . . . . . 10  |-  ( (
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 )
280190, 279pncan2d 9968 . . . . . . . . 9  |-  ( (
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
) ) )
281280oveq2d 6293 . . . . . . . 8  |-  ( (
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 ) ) ) )
282281adantr 463 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
283274, 278, 2823eqtrd 2447 . . . . . 6  |-  ( ( ( 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 ) ) ) )
284173oveq2d 6293 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
285284adantl 464 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
286114adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  A  e.  RR )
287286, 111readdcld 9652 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) )  e.  RR )
288287adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )  e.  RR )
289286, 117readdcld 9652 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  ( ( ( Q `
 1 )  -  A )  /  2
) )  e.  RR )
290289adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( Q `  1
)  -  A )  /  2 ) )  e.  RR )
291112ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( Q `  1 )  e.  RR )
292114ad2antrr 724 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  A  e.  RR )
293228, 229, 292, 234ltadd2dd 9774 . . . . . . . . . 10  |-  ( ( ( 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
) ) )
294112recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Q `  1
)  e.  CC )
295114recnd 9651 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  CC )
296 halfaddsub 10812 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
297294, 295, 296syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  +  ( ( ( Q `
 1 )  -  A )  /  2
) )  =  ( Q `  1 )  /\  ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  =  A ) )
298297simprd 461 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( Q `  1 )  +  A )  / 
2 )  -  (
( ( Q ` 
1 )  -  A
)  /  2 ) )  =  A )
299298oveq1d 6292 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) )  =  ( A  +  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )
300112, 114readdcld 9652 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( Q ` 
1 )  +  A
)  e.  RR )
301300rehalfcld 10825 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  e.  RR )
302301recnd 9651 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  e.  CC )
303116recnd 9651 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 1 )  -  A )  /  2
)  e.  CC )
304302, 303npcand 9970 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( ( Q `  1
)  +  A )  /  2 )  -  ( ( ( Q `
 1 )  -  A )  /  2
) )  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) )  =  ( ( ( Q `  1
)  +  A )  /  2 ) )
305299, 304eqtr3d 2445 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) )  =  ( ( ( Q `  1
)  +  A )  /  2 ) )
306112, 112readdcld 9652 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q ` 
1 )  +  ( Q `  1 ) )  e.  RR )
307114, 112, 112, 161ltadd2dd 9774 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( Q ` 
1 )  +  A
)  <  ( ( Q `  1 )  +  ( Q ` 
1 ) ) )
308300, 306, 244, 307ltdiv1dd 11356 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  <  ( (
( Q `  1
)  +  ( Q `
 1 ) )  /  2 ) )
3092942timesd 10821 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2  x.  ( Q `  1 )
)  =  ( ( Q `  1 )  +  ( Q ` 
1 ) ) )
310309eqcomd 2410 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q ` 
1 )  +  ( Q `  1 ) )  =  ( 2  x.  ( Q ` 
1 ) ) )
311310oveq1d 6292 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Q `
 1 )  +  ( Q `  1
) )  /  2
)  =  ( ( 2  x.  ( Q `
 1 ) )  /  2 ) )
312 2cnd 10648 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  e.  CC )
313 2ne0 10668 . . . . . . . . . . . . . . . 16  |-  2  =/=  0
314313a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  =/=  0 )
315294, 312, 314divcan3d 10365 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2  x.  ( Q `  1
) )  /  2
)  =  ( Q `
 1 ) )
316311, 315eqtrd 2443 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Q `
 1 )  +  ( Q `  1
) )  /  2
)  =  ( Q `
 1 ) )
317308, 316breqtrd 4418 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( Q `
 1 )  +  A )  /  2
)  <  ( Q `  1 ) )
318305, 317eqbrtrd 4414 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) )  <  ( Q `
 1 ) )
319318ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( Q `  1
)  -  A )  /  2 ) )  <  ( Q ` 
1 ) )
320288, 290, 291, 293, 319lttrd 9776 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( ( S `  ( j  +  1 ) )  -  ( S `  j ) )  < 
( ( Q ` 
1 )  -  A
) )  ->  ( A  +  ( (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  /  2 ) )  <  ( Q ` 
1 ) )
321285, 320eqbrtrd 4414 . . . . . . . 8  |-  ( ( ( 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 ) ) )  <  ( Q ` 
1 ) )
322178oveq2d 6293 . . . . . . . . . 10  |-  ( -.  ( ( 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  +  ( ( ( Q `
 1 )  -  A )  /  2
) ) )
323322adantl 464 . . . . . . . . 9  |-  ( ( ( 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  +  ( ( ( Q `
 1 )  -  A )  /  2
) ) )
324318ad2antrr 724 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  -.  (
( S `  (
j  +  1 ) )  -  ( S `
 j ) )  <  ( ( Q `
 1 )  -  A ) )  -> 
( A  +  ( ( ( Q ` 
1 )  -  A
)  /  2 ) )  <  ( Q `
 1 ) )
325323, 324eqbrtrd 4414 . . . . . . . 8  |-  ( ( ( 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 ) ) )  <  ( Q ` 
1 ) )
326321, 325pm2.61dan 792 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0..^ N ) )  ->  ( A  +  if ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `
 ( j  +  1 ) )  -  ( S `  j ) )  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  <  ( Q ` 
1 ) )
327326adantr 463 . . . . . 6  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( A  +  if (
( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  <  ( ( Q `  1 )  -  A ) ,  ( ( ( S `  ( j  +  1 ) )  -  ( S `  j )
)  /  2 ) ,  ( ( ( Q `  1 )  -  A )  / 
2 ) ) )  <  ( Q ` 
1 ) )
328283, 327eqbrtrd 4414 . . . . 5  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  Z )  <  ( Q `  1
) )
329 eqid 2402 . . . . 5  |-  ( ( Q `  1 )  -  ( ( E `
 Z )  -  Z ) )  =  ( ( Q ` 
1 )  -  (
( E `  Z
)  -  Z ) )
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 37301 . . . 4  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  ( E `  ( S `  ( j  +  1 ) ) )  <_ 
( Q `  1
) )
33114a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  x )
) } ,  RR ,  <  ) ) )
33257adantl 464 . . . . . . . . 9  |-  ( ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `  ( S `
 j ) )  =  B )  /\  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 ,  <  ) )
33360a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i
)  <_  ( L `  ( E `  ( S `  j )
) ) } ,  RR ,  <  )  e. 
_V )
334331, 332, 222, 333fvmptd 5937 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0..^ N ) )  /\  ( E `
 ( S `  j ) )  =  B )  ->  (
I `  ( S `  j ) )  =  sup ( { i  e.  ( 0..^ M )  |  ( Q `
 i )  <_ 
( L `  ( E `  ( S `  j ) ) ) } ,  RR ,  <  ) )
335 fveq2 5848 . . . . . . . . . . . . 13  |-  ( ( E `  ( S `
 j ) )  =  B  ->  ( L `  ( E `  ( S `  j
) ) )  =  ( L `  B
) )
33613a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y )
) )
337 iftrue 3890 . . . . . . . . . . . . . . 15  |-  ( y  =  B  ->  if ( y  =  B ,  A ,  y )  =  A )
338337adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  =  B )  ->  if ( y  =  B ,  A ,  y )  =  A )
339 ubioc1 11630 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  B  e.  ( A (,] B
) )
340245, 246, 220, 339syl3anc 1230 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  ( A (,] B ) )
341336, 338, 340, 114fvmptd 5937 . . . . . . . . . . . . 13  |-  ( ph  ->  ( L `  B