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

Theorem fourierdlem64 31794
Description: The partition  V is finer than  Q, when  Q is moved on the same interval where  V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem64.t  |-  T  =  ( B  -  A
)
fourierdlem64.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 ) ) ) } )
fourierdlem64.m  |-  ( ph  ->  M  e.  NN )
fourierdlem64.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem64.c  |-  ( ph  ->  C  e.  RR )
fourierdlem64.d  |-  ( ph  ->  D  e.  RR )
fourierdlem64.cltd  |-  ( ph  ->  C  <  D )
fourierdlem64.h  |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
fourierdlem64.n  |-  N  =  ( ( # `  H
)  -  1 )
fourierdlem64.v  |-  V  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
fourierdlem64.j  |-  ( ph  ->  J  e.  ( 0..^ N ) )
fourierdlem64.l  |-  L  =  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )
fourierdlem64.i  |-  I  =  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )
Assertion
Ref Expression
fourierdlem64  |-  ( ph  ->  ( ( I  e.  ( 0..^ M )  /\  L  e.  ZZ )  /\  E. i  e.  ( 0..^ M ) E. l  e.  ZZ  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) ) )
Distinct variable groups:    A, i, m, p    B, i, m, p    C, m, p    y, C    D, m, p    y, D    f, H    j, H    y, H    i, I, k, y    j, I, k   
I, l, i    j, J, k    i, J, l   
j, L, k    L, l    y, L    j, M, k    i, M, m, p   
f, N    i, N, m, p    j, N    y, N    Q, j, k    Q, i, y    Q, l    Q, p    T, j, k    T, i, y    T, l    j, V, k    f, V    i, V, y    V, l    V, p    ph, f    ph, i,
k    ph, j
Allowed substitution hints:    ph( y, m, p, l)    A( y, f, j, k, l)    B( y, f, j, k, l)    C( f, i, j, k, l)    D( f, i, j, k, l)    P( y, f, i, j, k, m, p, l)    Q( f, m)    T( f, m, p)    H( i, k, m, p, l)    I(
f, m, p)    J( y, f, m, p)    L( f, i, m, p)    M( y, f, l)    N( k, l)    V( m)

Proof of Theorem fourierdlem64
Dummy variables  x  b  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem64.i . . 3  |-  I  =  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )
2 ssrab2 3590 . . . . 5  |-  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) }  C_  (
0..^ M )
32a1i 11 . . . 4  |-  ( ph  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  C_  ( 0..^ M ) )
4 fzossfz 11826 . . . . . . . 8  |-  ( 0..^ M )  C_  (
0 ... M )
5 fzssz 31366 . . . . . . . 8  |-  ( 0 ... M )  C_  ZZ
64, 5sstri 3518 . . . . . . 7  |-  ( 0..^ M )  C_  ZZ
72, 6sstri 3518 . . . . . 6  |-  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) }  C_  ZZ
87a1i 11 . . . . 5  |-  ( ph  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  C_  ZZ )
9 fourierdlem64.m . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  NN )
109nnnn0d 10864 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  NN0 )
11 nn0uz 11128 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
1211a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  NN0  =  ( ZZ>= ` 
0 ) )
1310, 12eleqtrd 2557 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
14 eluzfz1 11705 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
1513, 14syl 16 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 ... M ) )
165, 15sseldi 3507 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
1710nn0zd 10976 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
189nngt0d 10591 . . . . . . . . . 10  |-  ( ph  ->  0  <  M )
1916, 17, 183jca 1176 . . . . . . . . 9  |-  ( ph  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  <  M ) )
20 fzolb 11814 . . . . . . . . 9  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
2119, 20sylibr 212 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0..^ M ) )
22 fourierdlem64.l . . . . . . . . . . 11  |-  L  =  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )
23 ssrab2 3590 . . . . . . . . . . . . 13  |-  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) }  C_  ZZ
2423a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  C_  ZZ )
25 fourierdlem64.h . . . . . . . . . . . . . . . . . . . 20  |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
26 fourierdlem64.c . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  C  e.  RR )
27 fourierdlem64.d . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  D  e.  RR )
28 prssi 4189 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  { C ,  D }  C_  RR )
2926, 27, 28syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  { C ,  D }  C_  RR )
30 ssrab2 3590 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  C_  ( C [,] D
)
3130a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  C_  ( C [,] D ) )
3226, 27iccssred 31426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( C [,] D
)  C_  RR )
3331, 32sstrd 3519 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  C_  RR )
3429, 33unssd 3685 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  C_  RR )
3525, 34syl5eqss 3553 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  H  C_  RR )
36 fourierdlem64.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  =  ( B  -  A
)
37 fourierdlem64.p . . . . . . . . . . . . . . . . . . . . . . 23  |-  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 ) ) ) } )
38 fourierdlem64.q . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  Q  e.  ( P `
 M ) )
39 fourierdlem64.cltd . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  C  <  D )
40 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) ) } )  =  ( 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 ) ) ) } )
41 fourierdlem64.n . . . . . . . . . . . . . . . . . . . . . . 23  |-  N  =  ( ( # `  H
)  -  1 )
42 fourierdlem64.v . . . . . . . . . . . . . . . . . . . . . . 23  |-  V  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
4336, 37, 9, 38, 26, 27, 39, 40, 25, 41, 42fourierdlem54 31784 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( N  e.  NN  /\  V  e.  ( ( 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 ) ) ) } ) `
 N ) )  /\  V  Isom  <  ,  <  ( ( 0 ... N ) ,  H ) ) )
4443simprd 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  V  Isom  <  ,  <  ( ( 0 ... N
) ,  H ) )
45 isof1o 6220 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V 
Isom  <  ,  <  (
( 0 ... N
) ,  H )  ->  V : ( 0 ... N ) -1-1-onto-> H )
46 f1of 5822 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V : ( 0 ... N ) -1-1-onto-> H  ->  V :
( 0 ... N
) --> H )
4744, 45, 463syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  V : ( 0 ... N ) --> H )
48 fourierdlem64.j . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  J  e.  ( 0..^ N ) )
49 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . 21  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
5048, 49syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J  e.  ( 0 ... N ) )
5147, 50ffvelrnd 6033 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( V `  J
)  e.  H )
5235, 51sseldd 3510 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( V `  J
)  e.  RR )
5337fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) ) ) ) )
549, 53syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) ) ) )
5538, 54mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
5655simpld 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
57 elmapi 7452 . . . . . . . . . . . . . . . . . . . 20  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
5856, 57syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
5958, 15ffvelrnd 6033 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( Q `  0
)  e.  RR )
6052, 59resubcld 9999 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( V `  J )  -  ( Q `  0 )
)  e.  RR )
6137, 9, 38fourierdlem11 31741 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
6261simp2d 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  RR )
6361simp1d 1008 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR )
6462, 63resubcld 9999 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B  -  A
)  e.  RR )
6536, 64syl5eqel 2559 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  RR )
66 0re 9608 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
6766a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  e.  RR )
6861simp3d 1010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  <  B )
69 posdif 10057 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
7063, 62, 69syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
7168, 70mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  ( B  -  A ) )
7236eqcomi 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( B  -  A )  =  T
7372a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( B  -  A
)  =  T )
7471, 73breqtrd 4477 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  T )
7567, 74gtned 9731 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  =/=  0 )
7660, 65, 75redivcld 10384 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T )  e.  RR )
77 btwnz 10975 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( V `  J )  -  ( Q `  0 )
)  /  T )  e.  RR  ->  ( E. k  e.  ZZ  k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  /\  E. z  e.  ZZ  (
( ( V `  J )  -  ( Q `  0 )
)  /  T )  <  z ) )
7876, 77syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E. k  e.  ZZ  k  <  (
( ( V `  J )  -  ( Q `  0 )
)  /  T )  /\  E. z  e.  ZZ  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  <  z
) )
7978simpld 459 . . . . . . . . . . . . . 14  |-  ( ph  ->  E. k  e.  ZZ  k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T ) )
80 simpl 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ZZ )  ->  ph )
81 zre 10880 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ZZ  ->  k  e.  RR )
8281adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ZZ )  ->  k  e.  RR )
8359ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( Q `  0 )  e.  RR )
84 simplr 754 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  k  e.  RR )
8565ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  T  e.  RR )
8684, 85remulcld 9636 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( k  x.  T )  e.  RR )
8783, 86readdcld 9635 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( Q `  0 )  +  ( k  x.  T ) )  e.  RR )
8852ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( V `  J )  e.  RR )
89 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  k  <  ( ( ( V `  J )  -  ( Q `  0 )
)  /  T ) )
9060ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( V `  J )  -  ( Q ` 
0 ) )  e.  RR )
9165, 74elrpd 11266 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  T  e.  RR+ )
9291ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  T  e.  RR+ )
9384, 90, 92ltmuldivd 11311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( (
k  x.  T )  <  ( ( V `
 J )  -  ( Q `  0 ) )  <->  k  <  (
( ( V `  J )  -  ( Q `  0 )
)  /  T ) ) )
9489, 93mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( k  x.  T )  <  (
( V `  J
)  -  ( Q `
 0 ) ) )
9559adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  RR )  ->  ( Q `
 0 )  e.  RR )
96 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  RR )  ->  k  e.  RR )
9765adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  RR )  ->  T  e.  RR )
9896, 97remulcld 9636 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  RR )  ->  ( k  x.  T )  e.  RR )
9952adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  RR )  ->  ( V `
 J )  e.  RR )
10095, 98, 99ltaddsub2d 10165 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  RR )  ->  ( ( ( Q `  0
)  +  ( k  x.  T ) )  <  ( V `  J )  <->  ( k  x.  T )  <  (
( V `  J
)  -  ( Q `
 0 ) ) ) )
101100adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( (
( Q `  0
)  +  ( k  x.  T ) )  <  ( V `  J )  <->  ( k  x.  T )  <  (
( V `  J
)  -  ( Q `
 0 ) ) ) )
10294, 101mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( Q `  0 )  +  ( k  x.  T ) )  < 
( V `  J
) )
10387, 88, 102ltled 9744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) )
104103ex 434 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  RR )  ->  ( k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  (
( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) ) )
10580, 82, 104syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  (
( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) ) )
106105reximdva 2942 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E. k  e.  ZZ  k  <  (
( ( V `  J )  -  ( Q `  0 )
)  /  T )  ->  E. k  e.  ZZ  ( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) ) )
10779, 106mpd 15 . . . . . . . . . . . . 13  |-  ( ph  ->  E. k  e.  ZZ  ( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) )
108 rabn0 3810 . . . . . . . . . . . . 13  |-  ( { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) }  =/=  (/)  <->  E. k  e.  ZZ  (
( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) )
109107, 108sylibr 212 . . . . . . . . . . . 12  |-  ( ph  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  =/=  (/) )
110 simpl 457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  ph )
11124sselda 3509 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  j  e.  ZZ )
112 oveq1 6302 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
113112oveq2d 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  j  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( j  x.  T
) ) )
114113breq1d 4463 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  j  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( j  x.  T ) )  <_ 
( V `  J
) ) )
115114elrab 3266 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  <->  ( j  e.  ZZ  /\  ( ( Q `  0 )  +  ( j  x.  T ) )  <_ 
( V `  J
) ) )
116115simprbi 464 . . . . . . . . . . . . . . . 16  |-  ( j  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  ->  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )
117116adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  ( ( Q `
 0 )  +  ( j  x.  T
) )  <_  ( V `  J )
)
118 simpll 753 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ZZ )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  ->  ph )
119 zre 10880 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ZZ  ->  j  e.  RR )
120119ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ZZ )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  e.  RR )
121 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ZZ )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( j  x.  T ) )  <_  ( V `  J ) )
122 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( j  x.  T ) )  <_  ( V `  J ) )
12359ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( Q `  0
)  e.  RR )
124 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  RR )  ->  j  e.  RR )
12565adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  RR )  ->  T  e.  RR )
126124, 125remulcld 9636 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  RR )  ->  ( j  x.  T )  e.  RR )
127126adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( j  x.  T
)  e.  RR )
12852ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( V `  J
)  e.  RR )
129123, 127, 128leaddsub2d 10166 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( ( Q `
 0 )  +  ( j  x.  T
) )  <_  ( V `  J )  <->  ( j  x.  T )  <_  ( ( V `
 J )  -  ( Q `  0 ) ) ) )
130122, 129mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( j  x.  T
)  <_  ( ( V `  J )  -  ( Q ` 
0 ) ) )
131 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  e.  RR )
13260ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( V `  J )  -  ( Q `  0 )
)  e.  RR )
13391ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  ->  T  e.  RR+ )
134131, 132, 133lemuldivd 11313 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( j  x.  T )  <_  (
( V `  J
)  -  ( Q `
 0 ) )  <-> 
j  <_  ( (
( V `  J
)  -  ( Q `
 0 ) )  /  T ) ) )
135130, 134mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  <_  ( (
( V `  J
)  -  ( Q `
 0 ) )  /  T ) )
136118, 120, 121, 135syl21anc 1227 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ZZ )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  <_  ( (
( V `  J
)  -  ( Q `
 0 ) )  /  T ) )
137110, 111, 117, 136syl21anc 1227 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  j  <_  (
( ( V `  J )  -  ( Q `  0 )
)  /  T ) )
138137ralrimiva 2881 . . . . . . . . . . . . 13  |-  ( ph  ->  A. j  e.  {
k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T ) )
139 breq2 4457 . . . . . . . . . . . . . . 15  |-  ( b  =  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  (
j  <_  b  <->  j  <_  ( ( ( V `  J )  -  ( Q `  0 )
)  /  T ) ) )
140139ralbidv 2906 . . . . . . . . . . . . . 14  |-  ( b  =  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  ( A. j  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  b  <->  A. j  e.  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } j  <_  (
( ( V `  J )  -  ( Q `  0 )
)  /  T ) ) )
141140rspcev 3219 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T )  e.  RR  /\  A. j  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) } j  <_ 
( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  E. b  e.  RR  A. j  e. 
{ k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } j  <_  b
)
14276, 138, 141syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  E. b  e.  RR  A. j  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  b )
143 suprzcl 10952 . . . . . . . . . . . 12  |-  ( ( { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  C_  ZZ  /\  {
k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) }  =/=  (/) 
/\  E. b  e.  RR  A. j  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  b )  ->  sup ( { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )  e.  {
k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )
14424, 109, 142, 143syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )  e. 
{ k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } )
14522, 144syl5eqel 2559 . . . . . . . . . 10  |-  ( ph  ->  L  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } )
146 oveq1 6302 . . . . . . . . . . . . 13  |-  ( k  =  L  ->  (
k  x.  T )  =  ( L  x.  T ) )
147146oveq2d 6311 . . . . . . . . . . . 12  |-  ( k  =  L  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( L  x.  T
) ) )
148147breq1d 4463 . . . . . . . . . . 11  |-  ( k  =  L  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
149148elrab 3266 . . . . . . . . . 10  |-  ( L  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  <->  ( L  e.  ZZ  /\  ( ( Q `  0 )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
150145, 149sylib 196 . . . . . . . . 9  |-  ( ph  ->  ( L  e.  ZZ  /\  ( ( Q ` 
0 )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
151150simprd 463 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
0 )  +  ( L  x.  T ) )  <_  ( V `  J ) )
15221, 151jca 532 . . . . . . 7  |-  ( ph  ->  ( 0  e.  ( 0..^ M )  /\  ( ( Q ` 
0 )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
153 fveq2 5872 . . . . . . . . . 10  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
154153oveq1d 6310 . . . . . . . . 9  |-  ( j  =  0  ->  (
( Q `  j
)  +  ( L  x.  T ) )  =  ( ( Q `
 0 )  +  ( L  x.  T
) ) )
155154breq1d 4463 . . . . . . . 8  |-  ( j  =  0  ->  (
( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
156155elrab 3266 . . . . . . 7  |-  ( 0  e.  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) } 
<->  ( 0  e.  ( 0..^ M )  /\  ( ( Q ` 
0 )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
157152, 156sylibr 212 . . . . . 6  |-  ( ph  ->  0  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } )
158 ne0i 3796 . . . . . 6  |-  ( 0  e.  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) }  ->  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) }  =/=  (/) )
159157, 158syl 16 . . . . 5  |-  ( ph  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  =/=  (/) )
1609nnred 10563 . . . . . 6  |-  ( ph  ->  M  e.  RR )
161 simpl 457 . . . . . . . 8  |-  ( (
ph  /\  k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } )  ->  ph )
1623sselda 3509 . . . . . . . 8  |-  ( (
ph  /\  k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } )  ->  k  e.  ( 0..^ M ) )
1636sseli 3505 . . . . . . . . . . 11  |-  ( k  e.  ( 0..^ M )  ->  k  e.  ZZ )
164163, 81syl 16 . . . . . . . . . 10  |-  ( k  e.  ( 0..^ M )  ->  k  e.  RR )
165164adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  e.  RR )
166160adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  M  e.  RR )
167 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  e.  ( 0..^ M ) )
168 elfzolt2 11817 . . . . . . . . . 10  |-  ( k  e.  ( 0..^ M )  ->  k  <  M )
169167, 168syl 16 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  <  M
)
170165, 166, 169ltled 9744 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  <_  M
)
171161, 162, 170syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } )  ->  k  <_  M
)
172171ralrimiva 2881 . . . . . 6  |-  ( ph  ->  A. k  e.  {
j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } k  <_  M )
173 breq2 4457 . . . . . . . 8  |-  ( b  =  M  ->  (
k  <_  b  <->  k  <_  M ) )
174173ralbidv 2906 . . . . . . 7  |-  ( b  =  M  ->  ( A. k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } k  <_ 
b  <->  A. k  e.  {
j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } k  <_  M ) )
175174rspcev 3219 . . . . . 6  |-  ( ( M  e.  RR  /\  A. k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } k  <_  M )  ->  E. b  e.  RR  A. k  e. 
{ j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) } k  <_  b )
176160, 172, 175syl2anc 661 . . . . 5  |-  ( ph  ->  E. b  e.  RR  A. k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } k  <_ 
b )
177 suprzcl 10952 . . . . 5  |-  ( ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  C_  ZZ  /\  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) }  =/=  (/)  /\  E. b  e.  RR  A. k  e. 
{ j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) } k  <_  b )  ->  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } )
1788, 159, 176, 177syl3anc 1228 . . . 4  |-  ( ph  ->  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )  e.  {
j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } )
1793, 178sseldd 3510 . . 3  |-  ( ph  ->  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )  e.  ( 0..^ M ) )
1801, 179syl5eqel 2559 . 2  |-  ( ph  ->  I  e.  ( 0..^ M ) )
18123, 144sseldi 3507 . . 3  |-  ( ph  ->  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )  e.  ZZ )
18222, 181syl5eqel 2559 . 2  |-  ( ph  ->  L  e.  ZZ )
1834, 180sseldi 3507 . . . . . . . . . 10  |-  ( ph  ->  I  e.  ( 0 ... M ) )
18458, 183ffvelrnd 6033 . . . . . . . . 9  |-  ( ph  ->  ( Q `  I
)  e.  RR )
185182zred 10978 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR )
186185, 65remulcld 9636 . . . . . . . . 9  |-  ( ph  ->  ( L  x.  T
)  e.  RR )
187184, 186readdcld 9635 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  I )  +  ( L  x.  T ) )  e.  RR )
188187rexrd 9655 . . . . . . 7  |-  ( ph  ->  ( ( Q `  I )  +  ( L  x.  T ) )  e.  RR* )
189188adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  e.  RR* )
190 fzofzp1 11889 . . . . . . . . . . 11  |-  ( I  e.  ( 0..^ M )  ->  ( I  +  1 )  e.  ( 0 ... M
) )
191180, 190syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( I  +  1 )  e.  ( 0 ... M ) )
19258, 191ffvelrnd 6033 . . . . . . . . 9  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  RR )
193192, 186readdcld 9635 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR )
194193rexrd 9655 . . . . . . 7  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR* )
195194adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  RR* )
196 elioore 11571 . . . . . . 7  |-  ( x  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  ->  x  e.  RR )
197196adantl 466 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  x  e.  RR )
198187adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  e.  RR )
19952adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  e.  RR )
2001, 178syl5eqel 2559 . . . . . . . . . 10  |-  ( ph  ->  I  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } )
201 fveq2 5872 . . . . . . . . . . . . 13  |-  ( j  =  I  ->  ( Q `  j )  =  ( Q `  I ) )
202201oveq1d 6310 . . . . . . . . . . . 12  |-  ( j  =  I  ->  (
( Q `  j
)  +  ( L  x.  T ) )  =  ( ( Q `
 I )  +  ( L  x.  T
) ) )
203202breq1d 4463 . . . . . . . . . . 11  |-  ( j  =  I  ->  (
( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  I )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
204203elrab 3266 . . . . . . . . . 10  |-  ( I  e.  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) } 
<->  ( I  e.  ( 0..^ M )  /\  ( ( Q `  I )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
205200, 204sylib 196 . . . . . . . . 9  |-  ( ph  ->  ( I  e.  ( 0..^ M )  /\  ( ( Q `  I )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
206205simprd 463 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  I )  +  ( L  x.  T ) )  <_  ( V `  J ) )
207206adantr 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  <_  ( V `  J ) )
208199rexrd 9655 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  e.  RR* )
209 fzofzp1 11889 . . . . . . . . . . . . 13  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
21048, 209syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
21147, 210ffvelrnd 6033 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  H )
21235, 211sseldd 3510 . . . . . . . . . 10  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  RR )
213212rexrd 9655 . . . . . . . . 9  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  RR* )
214213adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  ( J  +  1 ) )  e.  RR* )
215 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )
216 ioogtlb 31415 . . . . . . . 8  |-  ( ( ( V `  J
)  e.  RR*  /\  ( V `  ( J  +  1 ) )  e.  RR*  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  <  x )
217208, 214, 215, 216syl3anc 1228 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  <  x )
218198, 199, 197, 207, 217lelttrd 9751 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  <  x )
219 id 22 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( ph  /\  x  e.  ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) ) )
220 id 22 . . . . . . . . 9  |-  ( ph  ->  ph )
22181ssriv 3513 . . . . . . . . . . . . . . . 16  |-  ZZ  C_  RR
22223, 221sstri 3518 . . . . . . . . . . . . . . 15  |-  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) }  C_  RR
223222a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  C_  RR )
224109ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  =/=  (/) )
225142ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  E. b  e.  RR  A. j  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  b )
226182peano2zd 10981 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( L  +  1 )  e.  ZZ )
227226ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( L  +  1 )  e.  ZZ )
228 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( I  =  ( M  - 
1 )  ->  (
I  +  1 )  =  ( ( M  -  1 )  +  1 ) )
229228adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
I  +  1 )  =  ( ( M  -  1 )  +  1 ) )
230160recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  M  e.  CC )
231 ax-1cn 9562 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  1  e.  CC
232231a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  1  e.  CC )
233230, 232npcand 9946 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  =  M )
234233adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( M  -  1 )  +  1 )  =  M )
235229, 234eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
I  +  1 )  =  M )
236235fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  ( I  +  1 ) )  =  ( Q `  M ) )
23755simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
238237simpld 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
239238simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( Q `  M
)  =  B )
240239adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  M )  =  B )
24162recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  B  e.  CC )
24263recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  e.  CC )
243241, 242npcand 9946 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( B  -  A )  +  A
)  =  B )
244243eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  =  ( ( B  -  A )  +  A ) )
24573oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( B  -  A )  +  A
)  =  ( T  +  A ) )
246238simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( Q `  0
)  =  A )
247246eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  =  ( Q `
 0 ) )
248247oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( T  +  A
)  =  ( T  +  ( Q ` 
0 ) ) )
249244, 245, 2483eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  =  ( T  +  ( Q ` 
0 ) ) )
250249adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  B  =  ( T  +  ( Q `  0 ) ) )
251236, 240, 2503eqtrd 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  ( I  +  1 ) )  =  ( T  +  ( Q `  0 ) ) )
25265recnd 9634 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  T  e.  CC )
253246, 242eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( Q `  0
)  e.  CC )
254252, 253addcomd 9793 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( T  +  ( Q `  0 ) )  =  ( ( Q `  0 )  +  T ) )
255254adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( T  +  ( Q `  0 ) )  =  ( ( Q `
 0 )  +  T ) )
256251, 255eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  ( I  +  1 ) )  =  ( ( Q `
 0 )  +  T ) )
257256oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  =  ( ( ( Q `  0 )  +  T )  +  ( L  x.  T
) ) )
258186recnd 9634 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( L  x.  T
)  e.  CC )
259253, 252, 258addassd 9630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 0 )  +  T )  +  ( L  x.  T ) )  =  ( ( Q `  0 )  +  ( T  +  ( L  x.  T
) ) ) )
260252mulid2d 9626 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1  x.  T
)  =  T )
261260eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  T  =  ( 1  x.  T ) )
262261oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( T  +  ( L  x.  T ) )  =  ( ( 1  x.  T )  +  ( L  x.  T ) ) )
263260, 252eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1  x.  T
)  e.  CC )
264263, 258addcomd 9793 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 1  x.  T )  +  ( L  x.  T ) )  =  ( ( L  x.  T )  +  ( 1  x.  T ) ) )
265185recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  L  e.  CC )
266265, 232, 252adddird 9633 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( L  + 
1 )  x.  T
)  =  ( ( L  x.  T )  +  ( 1  x.  T ) ) )
267266eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( L  x.  T )  +  ( 1  x.  T ) )  =  ( ( L  +  1 )  x.  T ) )
268262, 264, 2673eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( T  +  ( L  x.  T ) )  =  ( ( L  +  1 )  x.  T ) )
269268oveq2d 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( Q ` 
0 )  +  ( T  +  ( L  x.  T ) ) )  =  ( ( Q `  0 )  +  ( ( L  +  1 )  x.  T ) ) )
270259, 269eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( Q `
 0 )  +  T )  +  ( L  x.  T ) )  =  ( ( Q `  0 )  +  ( ( L  +  1 )  x.  T ) ) )
271270adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( ( Q ` 
0 )  +  T
)  +  ( L  x.  T ) )  =  ( ( Q `
 0 )  +  ( ( L  + 
1 )  x.  T
) ) )
272257, 271eqtr2d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( Q `  0
)  +  ( ( L  +  1 )  x.  T ) )  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
273272adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( ( L  +  1 )  x.  T ) )  =  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) )
274 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
275273, 274eqbrtrd 4473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( ( L  +  1 )  x.  T ) )  <_  ( V `  J ) )
276227, 275jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( L  + 
1 )  e.  ZZ  /\  ( ( Q ` 
0 )  +  ( ( L  +  1 )  x.  T ) )  <_  ( V `  J ) ) )
277 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( L  + 
1 )  ->  (
k  x.  T )  =  ( ( L  +  1 )  x.  T ) )
278277oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( L  + 
1 )  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( ( L  + 
1 )  x.  T
) ) )
279278breq1d 4463 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( L  + 
1 )  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( ( L  +  1 )  x.  T ) )  <_ 
( V `  J
) ) )
280279elrab 3266 . . . . . . . . . . . . . . 15  |-  ( ( L  +  1 )  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  <->  ( ( L  +  1 )  e.  ZZ  /\  (
( Q `  0
)  +  ( ( L  +  1 )  x.  T ) )  <_  ( V `  J ) ) )
281276, 280sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( L  +  1 )  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } )
282 suprub 10516 . . . . . . . . . . . . . 14  |-  ( ( ( { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  C_  RR  /\ 
{ k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  =/=  (/)  /\  E. b  e.  RR  A. j  e. 
{ k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } j  <_  b
)  /\  ( L  +  1 )  e. 
{ k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } )  ->  ( L  +  1 )  <_  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  ) )
283223, 224, 225, 281, 282syl31anc 1231 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( L  +  1 )  <_  sup ( { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  ) )
28422eqcomi 2480 . . . . . . . . . . . . . 14  |-  sup ( { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )  =  L
285284a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  sup ( { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )  =  L )
286283, 285breqtrd 4477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( L  +  1 )  <_  L )
287185ltp1d 10488 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  <  ( L  +  1 ) )
288 peano2re 9764 . . . . . . . . . . . . . . . 16  |-  ( L  e.  RR  ->  ( L  +  1 )  e.  RR )
289185, 288syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  +  1 )  e.  RR )
290185, 289ltnled 9743 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  <  ( L  +  1 )  <->  -.  ( L  +  1 )  <_  L )
)
291287, 290mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  ( L  + 
1 )  <_  L
)
292291ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  -.  ( L  +  1 )  <_  L )
293286, 292pm2.65da 576 . . . . . . . . . . 11  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  -.  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
294 simpl 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  ph )
2956, 180sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  e.  ZZ )
296295zred 10978 . . . . . . . . . . . . . 14  |-  ( ph  ->  I  e.  RR )
297296adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  I  e.  RR )
298 peano2rem 9898 . . . . . . . . . . . . . . 15  |-  ( M  e.  RR  ->  ( M  -  1 )  e.  RR )
299160, 298syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M  -  1 )  e.  RR )
300299adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  -> 
( M  -  1 )  e.  RR )
301 elfzolt2 11817 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 0..^ M )  ->  I  <  M )
3026sseli 3505 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  ( 0..^ M )  ->  I  e.  ZZ )
303 elfzoel2 11808 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  ( 0..^ M )  ->  M  e.  ZZ )
304 zltlem1 10927 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  ZZ  /\  M  e.  ZZ )  ->  ( I  <  M  <->  I  <_  ( M  - 
1 ) ) )
305302, 303, 304syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 0..^ M )  ->  ( I  <  M  <->  I  <_  ( M  -  1 ) ) )
306301, 305mpbid 210 . . . . . . . . . . . . . . 15  |-  ( I  e.  ( 0..^ M )  ->  I  <_  ( M  -  1 ) )
307180, 306syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  I  <_  ( M  -  1 ) )
308307adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  I  <_  ( M  - 
1 ) )
309 neqne 31339 . . . . . . . . . . . . . . 15  |-  ( -.  I  =  ( M  -  1 )  ->  I  =/=  ( M  - 
1 ) )
310309necomd 2738 . . . . . . . . . . . . . 14  |-  ( -.  I  =  ( M  -  1 )  -> 
( M  -  1 )  =/=  I )
311310adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  -> 
( M  -  1 )  =/=  I )
312297, 300, 308, 311leneltd 31394 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  I  <  ( M  - 
1 ) )
3137, 221sstri 3518 . . . . . . . . . . . . . . . 16  |-  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) }  C_  RR
314313a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  C_  RR )
315159ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  =/=  (/) )
316176ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  E. b  e.  RR  A. k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } k  <_ 
b )
317191adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  e.  ( 0 ... M
) )
318296adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  I  e.  RR )
319299adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( M  -  1 )  e.  RR )
320 1re 9607 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  1  e.  RR )
322 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  I  <  ( M  -  1 ) )
323318, 319, 321, 322ltadd1dd 10175 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  < 
( ( M  - 
1 )  +  1 ) )
324233adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( ( M  -  1 )  +  1 )  =  M )
325323, 324breqtrd 4477 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  < 
M )
326317, 325jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( (
I  +  1 )  e.  ( 0 ... M )  /\  (
I  +  1 )  <  M ) )
327 elfzfzo 31358 . . . . . . . . . . . . . . . . . . 19  |-  ( ( I  +  1 )  e.  ( 0..^ M )  <->  ( ( I  +  1 )  e.  ( 0 ... M
)  /\  ( I  +  1 )  < 
M ) )
328326, 327sylibr 212 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  e.  ( 0..^ M ) )
329328adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( I  +  1 )  e.  ( 0..^ M ) )
330 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
331329, 330jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( I  + 
1 )  e.  ( 0..^ M )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
332 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( I  + 
1 )  ->  ( Q `  j )  =  ( Q `  ( I  +  1
) ) )
333332oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( I  + 
1 )  ->  (
( Q `  j
)  +  ( L  x.  T ) )  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
334333breq1d 4463 . . . . . . . . . . . . . . . . 17  |-  ( j  =  ( I  + 
1 )  ->  (
( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
335334elrab 3266 . . . . . . . . . . . . . . . 16  |-  ( ( I  +  1 )  e.  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) } 
<->  ( ( I  + 
1 )  e.  ( 0..^ M )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
336331, 335sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( I  +  1 )  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } )
337 suprub 10516 . . . . . . . . . . . . . . 15  |-  ( ( ( { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) }  C_  RR  /\  {
j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) }  =/=  (/) 
/\  E. b  e.  RR  A. k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } k  <_ 
b )  /\  (
I  +  1 )  e.  { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) } )  ->  (
I  +  1 )  <_  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  ) )
338314, 315, 316, 336, 337syl31anc 1231 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( I  +  1 )  <_  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  ) )
3391eqcomi 2480 . . . . . . . . . . . . . . 15  |-  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )  =  I
340339a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `
 j )  +  ( L  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )  =  I )
341338, 340breqtrd 4477 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( I  +  1 )  <_  I )
342296ltp1d 10488 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  <  ( I  +  1 ) )
343 peano2re 9764 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  RR  ->  (
I  +  1 )  e.  RR )
344296, 343syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  e.  RR )
345296, 344ltnled 9743 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( I  <  (
I  +  1 )  <->  -.  ( I  +  1 )  <_  I )
)
346342, 345mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( I  + 
1 )  <_  I
)
347346ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  -.  ( I  +  1 )  <_  I )
348341, 347pm2.65da 576 . . . . . . . . . . . 12  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  -.  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
349294, 312, 348syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  -.  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
350293, 349pm2.61dan 789 . . . . . . . . . 10  |-  ( ph  ->  -.  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  <_  ( V `  J )
)
35152, 193ltnled 9743 . . . . . . . . . 10  |-  ( ph  ->  ( ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <->  -.  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
352350, 351mpbird 232 . . . . . . . . 9  |-  ( ph  ->  ( V `  J
)  <  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) )
353212adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  e.  RR )
35427adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  D  e.  RR )
355193adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
35626rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  RR* )
35727rexrd 9655 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  RR* )
35826, 27, 39ltled 9744 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  C  <_  D )
359 lbicc2 11648 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  C  <_  D )  ->  C  e.  ( C [,] D
) )
360356, 357, 358, 359syl3anc 1228 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  C  e.  ( C [,] D ) )
361 ubicc2 11649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  C  <_  D )  ->  D  e.  ( C [,] D
) )
362356, 357, 358, 361syl3anc 1228 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  e.  ( C [,] D ) )
363360, 362jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( C  e.  ( C [,] D )  /\  D  e.  ( C [,] D ) ) )
364 prssg 4188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( C  e.  ( C [,] D
)  /\  D  e.  ( C [,] D ) )  <->  { C ,  D }  C_  ( C [,] D ) ) )
36526, 27, 364syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( C  e.  ( C [,] D
)  /\  D  e.  ( C [,] D ) )  <->  { C ,  D }  C_  ( C [,] D ) ) )
366363, 365mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { C ,  D }  C_  ( C [,] D ) )
367366, 31unssd 3685 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  C_  ( C [,] D ) )
36825, 367syl5eqss 3553 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H  C_  ( C [,] D ) )
369368, 211sseldd 3510 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  ( C [,] D ) )
370 iccleub 11592 . . . . . . . . . . . . . 14  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  ( V `
 ( J  + 
1 ) )  e.  ( C [,] D
) )  ->  ( V `  ( J  +  1 ) )  <_  D )
371356, 357, 369, 370syl3anc 1228 . . . . . . . . . . . . 13  |-  ( ph  ->  ( V `  ( J  +  1 ) )  <_  D )
372371adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  <_  D
)
373 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
374353, 354, 355, 372, 373letrd 9750 . . . . . . . . . . 11  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  <_  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
375374adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
376 simpl 457 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  -.  D  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) ) )
377 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  -.  D  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
378193adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
37927adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  D  e.  RR )
380378, 379ltnled 9743 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  D  <->  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) ) )
381377, 380mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )
382381adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  -.  D  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  D )
383 simpll 753 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( V `  J )  <  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  D )  /\  -.  ( V `
 ( J  + 
1 ) )  <_ 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  ( ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) ) )
384 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  ->  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) )
385193adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR )
386212adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( V `  ( J  +  1 ) )  e.  RR )
387385, 386ltnled 9743 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  <  ( V `  ( J  +  1 ) )  <->  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) ) )
388384, 387mpbird 232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  ( V `
 ( J  + 
1 ) ) )
389388adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  ( V `
 ( J  + 
1 ) ) )
390389adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( V `  J )  <  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  D )  /\  -.  ( V `
 ( J  + 
1 ) )  <_ 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  ( V `  ( J  +  1
) ) )
39126ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  C  e.  RR )
39227ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  D  e.  RR )
393193ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR )
39426adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  e.  RR )
395193adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
39652adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  J )  e.  RR )
397368, 51sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V `  J
)  e.  ( C [,] D ) )
398 iccgelb 11593 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  ( V `
 J )  e.  ( C [,] D
) )  ->  C  <_  ( V `  J
) )
399356, 357, 397, 398syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  C  <_  ( V `  J ) )
400399adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  <_  ( V `  J ) )
401 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
402394, 396, 395, 400, 401lelttrd 9751 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  <  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
403394, 395, 402ltled 9744 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
404403adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  C  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
405193adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
40627adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  D  e.  RR )
407 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )
408405, 406, 407ltled 9744 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  D )
409408adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  D )
410391, 392, 393, 404, 409eliccd 31425 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  ( C [,] D ) )
411182znegcld 10980 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u L  e.  ZZ )
412265, 252mulneg1d 10021 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( -u L  x.  T )  =  -u ( L  x.  T
) )
413412oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  =  ( ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  -u ( L  x.  T )
) )
414193recnd 9634 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  CC )
415414, 258negsubd 9948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  -u ( L  x.  T
) )  =  ( ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  -  ( L  x.  T ) ) )
416192recnd 9634 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  CC )
417416, 258pncand 9943 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  -  ( L  x.  T )
)  =  ( Q `
 ( I  + 
1 ) ) )
418413, 415, 4173eqtrd 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  =  ( Q `  ( I  +  1 ) ) )
419 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
42058, 419syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
421 fnfvelrn 6029 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Q  Fn  ( 0 ... M )  /\  ( I  +  1
)  e.  ( 0 ... M ) )  ->  ( Q `  ( I  +  1
) )  e.  ran  Q )
422420, 191, 421syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  ran  Q
)
423418, 422eqeltrd 2555 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  e.  ran  Q )
424 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  -u L  ->  (
k  x.  T )  =  ( -u L  x.  T ) )
425424oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  -u L  ->  (
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  ( k  x.  T ) )  =  ( ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  +  ( -u L  x.  T ) ) )
426425eleq1d 2536 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  -u L  ->  (
( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  ( k  x.  T ) )  e.  ran  Q  <->  ( ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  ( -u L  x.  T )
)  e.  ran  Q
) )
427426rspcev 3219 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
-u L  e.  ZZ  /\  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  e.  ran  Q )  ->  E. k  e.  ZZ  ( ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  +  ( k  x.  T
) )  e.  ran  Q )
428411, 423, 427syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E. k  e.  ZZ  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  ( k  x.  T ) )  e.  ran  Q
)
429428ad2antrr 725 . . . . . . . . . . . . . . . . . 18