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

Theorem fourierdlem64 37860
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 3547 . . . 4  |-  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) }  C_  (
0..^ M )
3 fzossfz 11940 . . . . . . . 8  |-  ( 0..^ M )  C_  (
0 ... M )
4 fzssz 11803 . . . . . . . 8  |-  ( 0 ... M )  C_  ZZ
53, 4sstri 3474 . . . . . . 7  |-  ( 0..^ M )  C_  ZZ
62, 5sstri 3474 . . . . . 6  |-  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) }  C_  ZZ
76a1i 11 . . . . 5  |-  ( ph  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  C_  ZZ )
8 0zd 10951 . . . . . . . 8  |-  ( ph  ->  0  e.  ZZ )
9 fourierdlem64.m . . . . . . . . 9  |-  ( ph  ->  M  e.  NN )
109nnzd 11041 . . . . . . . 8  |-  ( ph  ->  M  e.  ZZ )
119nngt0d 10655 . . . . . . . 8  |-  ( ph  ->  0  <  M )
12 fzolb 11928 . . . . . . . 8  |-  ( 0  e.  ( 0..^ M )  <->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  0  < 
M ) )
138, 10, 11, 12syl3anbrc 1190 . . . . . . 7  |-  ( ph  ->  0  e.  ( 0..^ M ) )
14 fourierdlem64.l . . . . . . . . . 10  |-  L  =  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )
15 ssrab2 3547 . . . . . . . . . . . 12  |-  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) }  C_  ZZ
1615a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  C_  ZZ )
17 fourierdlem64.h . . . . . . . . . . . . . . . . . . 19  |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
18 fourierdlem64.c . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  RR )
19 fourierdlem64.d . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  D  e.  RR )
20 prssi 4154 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  { C ,  D }  C_  RR )
2118, 19, 20syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { C ,  D }  C_  RR )
22 ssrab2 3547 . . . . . . . . . . . . . . . . . . . . . 22  |-  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  C_  ( C [,] D
)
2322a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  C_  ( C [,] D ) )
2418, 19iccssred 37439 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( C [,] D
)  C_  RR )
2523, 24sstrd 3475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  C_  RR )
2621, 25unssd 3643 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  C_  RR )
2717, 26syl5eqss 3509 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  C_  RR )
28 fourierdlem64.t . . . . . . . . . . . . . . . . . . . . . 22  |-  T  =  ( B  -  A
)
29 fourierdlem64.p . . . . . . . . . . . . . . . . . . . . . 22  |-  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 ) ) ) } )
30 fourierdlem64.q . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Q  e.  ( P `
 M ) )
31 fourierdlem64.cltd . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  C  <  D )
32 eqid 2423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) } )
33 fourierdlem64.n . . . . . . . . . . . . . . . . . . . . . 22  |-  N  =  ( ( # `  H
)  -  1 )
34 fourierdlem64.v . . . . . . . . . . . . . . . . . . . . . 22  |-  V  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  H ) )
3528, 29, 9, 30, 18, 19, 31, 32, 17, 33, 34fourierdlem54 37850 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
3635simprd 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  V  Isom  <  ,  <  ( ( 0 ... N
) ,  H ) )
37 isof1o 6229 . . . . . . . . . . . . . . . . . . . 20  |-  ( V 
Isom  <  ,  <  (
( 0 ... N
) ,  H )  ->  V : ( 0 ... N ) -1-1-onto-> H )
38 f1of 5829 . . . . . . . . . . . . . . . . . . . 20  |-  ( V : ( 0 ... N ) -1-1-onto-> H  ->  V :
( 0 ... N
) --> H )
3936, 37, 383syl 18 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  V : ( 0 ... N ) --> H )
40 fourierdlem64.j . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J  e.  ( 0..^ N ) )
41 elfzofz 11937 . . . . . . . . . . . . . . . . . . . 20  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
4240, 41syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  J  e.  ( 0 ... N ) )
4339, 42ffvelrnd 6036 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( V `  J
)  e.  H )
4427, 43sseldd 3466 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( V `  J
)  e.  RR )
4529fourierdlem2 37797 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  NN  ->  ( Q  e.  ( P `  M )  <->  ( Q  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
469, 45syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( Q  e.  ( P `  M )  <-> 
( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) ) )
4730, 46mpbid 214 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
4847simpld 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
49 elmapi 7499 . . . . . . . . . . . . . . . . . . 19  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
5048, 49syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
519nnnn0d 10927 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  NN0 )
52 nn0uz 11195 . . . . . . . . . . . . . . . . . . . 20  |-  NN0  =  ( ZZ>= `  0 )
5351, 52syl6eleq 2521 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
54 eluzfz1 11808 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
5553, 54syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  e.  ( 0 ... M ) )
5650, 55ffvelrnd 6036 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Q `  0
)  e.  RR )
5744, 56resubcld 10049 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( V `  J )  -  ( Q `  0 )
)  e.  RR )
5829, 9, 30fourierdlem11 37806 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) )
5958simp2d 1019 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR )
6058simp1d 1018 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR )
6159, 60resubcld 10049 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  -  A
)  e.  RR )
6228, 61syl5eqel 2515 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  RR )
6358simp3d 1020 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  <  B )
6460, 59posdifd 10202 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
6563, 64mpbid 214 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  ( B  -  A ) )
6665, 28syl6breqr 4462 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <  T )
6766gt0ne0d 10180 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  =/=  0 )
6857, 62, 67redivcld 10437 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T )  e.  RR )
69 btwnz 11039 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
7068, 69syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E. k  e.  ZZ  k  <  (
( ( V `  J )  -  ( Q `  0 )
)  /  T )  /\  E. z  e.  ZZ  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  <  z
) )
7170simpld 461 . . . . . . . . . . . . 13  |-  ( ph  ->  E. k  e.  ZZ  k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T ) )
72 zre 10943 . . . . . . . . . . . . . . 15  |-  ( k  e.  ZZ  ->  k  e.  RR )
7356ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( Q `  0 )  e.  RR )
74 simplr 761 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  k  e.  RR )
7562ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  T  e.  RR )
7674, 75remulcld 9673 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( k  x.  T )  e.  RR )
7773, 76readdcld 9672 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( Q `  0 )  +  ( k  x.  T ) )  e.  RR )
7844ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( V `  J )  e.  RR )
79 simpr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  k  <  ( ( ( V `  J )  -  ( Q `  0 )
)  /  T ) )
8057ad2antrr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( V `  J )  -  ( Q ` 
0 ) )  e.  RR )
8162, 66elrpd 11340 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T  e.  RR+ )
8281ad2antrr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  T  e.  RR+ )
8374, 80, 82ltmuldivd 11387 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( (
k  x.  T )  <  ( ( V `
 J )  -  ( Q `  0 ) )  <->  k  <  (
( ( V `  J )  -  ( Q `  0 )
)  /  T ) ) )
8479, 83mpbird 236 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( k  x.  T )  <  (
( V `  J
)  -  ( Q `
 0 ) ) )
8556adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  RR )  ->  ( Q `
 0 )  e.  RR )
86 simpr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  RR )  ->  k  e.  RR )
8762adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  RR )  ->  T  e.  RR )
8886, 87remulcld 9673 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  RR )  ->  ( k  x.  T )  e.  RR )
8944adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  RR )  ->  ( V `
 J )  e.  RR )
9085, 88, 89ltaddsub2d 10216 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  RR )  ->  ( ( ( Q `  0
)  +  ( k  x.  T ) )  <  ( V `  J )  <->  ( k  x.  T )  <  (
( V `  J
)  -  ( Q `
 0 ) ) ) )
9190adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( (
( Q `  0
)  +  ( k  x.  T ) )  <  ( V `  J )  <->  ( k  x.  T )  <  (
( V `  J
)  -  ( Q `
 0 ) ) ) )
9284, 91mpbird 236 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( Q `  0 )  +  ( k  x.  T ) )  < 
( V `  J
) )
9377, 78, 92ltled 9785 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  RR )  /\  k  <  ( ( ( V `
 J )  -  ( Q `  0 ) )  /  T ) )  ->  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) )
9493ex 436 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  RR )  ->  ( k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  (
( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) ) )
9572, 94sylan2 477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  <  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  (
( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) ) )
9695reximdva 2901 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E. k  e.  ZZ  k  <  (
( ( V `  J )  -  ( Q `  0 )
)  /  T )  ->  E. k  e.  ZZ  ( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) ) )
9771, 96mpd 15 . . . . . . . . . . . 12  |-  ( ph  ->  E. k  e.  ZZ  ( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) )
98 rabn0 3783 . . . . . . . . . . . 12  |-  ( { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) }  =/=  (/)  <->  E. k  e.  ZZ  (
( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) )
9997, 98sylibr 216 . . . . . . . . . . 11  |-  ( ph  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  =/=  (/) )
100 simpl 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  ph )
10116sselda 3465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  j  e.  ZZ )
102 oveq1 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  j  ->  (
k  x.  T )  =  ( j  x.  T ) )
103102oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  j  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( j  x.  T
) ) )
104103breq1d 4431 . . . . . . . . . . . . . . . . 17  |-  ( k  =  j  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( j  x.  T ) )  <_ 
( V `  J
) ) )
105104elrab 3230 . . . . . . . . . . . . . . . 16  |-  ( j  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  <->  ( j  e.  ZZ  /\  ( ( Q `  0 )  +  ( j  x.  T ) )  <_ 
( V `  J
) ) )
106105simprbi 466 . . . . . . . . . . . . . . 15  |-  ( j  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  ->  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )
107106adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  ( ( Q `
 0 )  +  ( j  x.  T
) )  <_  ( V `  J )
)
108 zre 10943 . . . . . . . . . . . . . . 15  |-  ( j  e.  ZZ  ->  j  e.  RR )
109 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( j  x.  T ) )  <_  ( V `  J ) )
11056ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( Q `  0
)  e.  RR )
111 simpr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  RR )  ->  j  e.  RR )
11262adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  RR )  ->  T  e.  RR )
113111, 112remulcld 9673 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  RR )  ->  ( j  x.  T )  e.  RR )
114113adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( j  x.  T
)  e.  RR )
11544ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( V `  J
)  e.  RR )
116110, 114, 115leaddsub2d 10217 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) )
117109, 116mpbid 214 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( j  x.  T
)  <_  ( ( V `  J )  -  ( Q ` 
0 ) ) )
118 simplr 761 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  e.  RR )
11957ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( V `  J )  -  ( Q `  0 )
)  e.  RR )
12081ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  ->  T  e.  RR+ )
121118, 119, 120lemuldivd 11389 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
( ( j  x.  T )  <_  (
( V `  J
)  -  ( Q `
 0 ) )  <-> 
j  <_  ( (
( V `  J
)  -  ( Q `
 0 ) )  /  T ) ) )
122117, 121mpbid 214 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  RR )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  <_  ( (
( V `  J
)  -  ( Q `
 0 ) )  /  T ) )
123108, 122sylanl2 656 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ZZ )  /\  (
( Q `  0
)  +  ( j  x.  T ) )  <_  ( V `  J ) )  -> 
j  <_  ( (
( V `  J
)  -  ( Q `
 0 ) )  /  T ) )
124100, 101, 107, 123syl21anc 1264 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  { k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } )  ->  j  <_  (
( ( V `  J )  -  ( Q `  0 )
)  /  T ) )
125124ralrimiva 2840 . . . . . . . . . . . 12  |-  ( ph  ->  A. j  e.  {
k  e.  ZZ  | 
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T ) )
126 breq2 4425 . . . . . . . . . . . . . 14  |-  ( b  =  ( ( ( V `  J )  -  ( Q ` 
0 ) )  /  T )  ->  (
j  <_  b  <->  j  <_  ( ( ( V `  J )  -  ( Q `  0 )
)  /  T ) ) )
127126ralbidv 2865 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
128127rspcev 3183 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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
)
12968, 125, 128syl2anc 666 . . . . . . . . . . 11  |-  ( ph  ->  E. b  e.  RR  A. j  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } j  <_  b )
130 suprzcl 11017 . . . . . . . . . . 11  |-  ( ( { 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 ) } )
13116, 99, 129, 130syl3anc 1265 . . . . . . . . . 10  |-  ( ph  ->  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )  e. 
{ k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } )
13214, 131syl5eqel 2515 . . . . . . . . 9  |-  ( ph  ->  L  e.  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } )
133 oveq1 6310 . . . . . . . . . . . 12  |-  ( k  =  L  ->  (
k  x.  T )  =  ( L  x.  T ) )
134133oveq2d 6319 . . . . . . . . . . 11  |-  ( k  =  L  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( L  x.  T
) ) )
135134breq1d 4431 . . . . . . . . . 10  |-  ( k  =  L  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
136135elrab 3230 . . . . . . . . 9  |-  ( L  e.  { k  e.  ZZ  |  ( ( Q `  0 )  +  ( k  x.  T ) )  <_ 
( V `  J
) }  <->  ( L  e.  ZZ  /\  ( ( Q `  0 )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
137132, 136sylib 200 . . . . . . . 8  |-  ( ph  ->  ( L  e.  ZZ  /\  ( ( Q ` 
0 )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
138137simprd 465 . . . . . . 7  |-  ( ph  ->  ( ( Q ` 
0 )  +  ( L  x.  T ) )  <_  ( V `  J ) )
139 fveq2 5879 . . . . . . . . . 10  |-  ( j  =  0  ->  ( Q `  j )  =  ( Q ` 
0 ) )
140139oveq1d 6318 . . . . . . . . 9  |-  ( j  =  0  ->  (
( Q `  j
)  +  ( L  x.  T ) )  =  ( ( Q `
 0 )  +  ( L  x.  T
) ) )
141140breq1d 4431 . . . . . . . 8  |-  ( j  =  0  ->  (
( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
142141elrab 3230 . . . . . . 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 ) ) )
14313, 138, 142sylanbrc 669 . . . . . 6  |-  ( ph  ->  0  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } )
144 ne0i 3768 . . . . . 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 ) }  =/=  (/) )
145143, 144syl 17 . . . . 5  |-  ( ph  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  =/=  (/) )
1469nnred 10626 . . . . . 6  |-  ( ph  ->  M  e.  RR )
1472a1i 11 . . . . . . . . 9  |-  ( ph  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  C_  ( 0..^ M ) )
148147sselda 3465 . . . . . . . 8  |-  ( (
ph  /\  k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } )  ->  k  e.  ( 0..^ M ) )
149 elfzoelz 11922 . . . . . . . . . . 11  |-  ( k  e.  ( 0..^ M )  ->  k  e.  ZZ )
150149zred 11042 . . . . . . . . . 10  |-  ( k  e.  ( 0..^ M )  ->  k  e.  RR )
151150adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  e.  RR )
152146adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  M  e.  RR )
153 elfzolt2 11931 . . . . . . . . . 10  |-  ( k  e.  ( 0..^ M )  ->  k  <  M )
154153adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  <  M
)
155151, 152, 154ltled 9785 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  k  <_  M
)
156148, 155syldan 473 . . . . . . 7  |-  ( (
ph  /\  k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } )  ->  k  <_  M
)
157156ralrimiva 2840 . . . . . 6  |-  ( ph  ->  A. k  e.  {
j  e.  ( 0..^ M )  |  ( ( Q `  j
)  +  ( L  x.  T ) )  <_  ( V `  J ) } k  <_  M )
158 breq2 4425 . . . . . . . 8  |-  ( b  =  M  ->  (
k  <_  b  <->  k  <_  M ) )
159158ralbidv 2865 . . . . . . 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 ) )
160159rspcev 3183 . . . . . 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 )
161146, 157, 160syl2anc 666 . . . . 5  |-  ( ph  ->  E. b  e.  RR  A. k  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } k  <_ 
b )
162 suprzcl 11017 . . . . 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
) } )
1637, 145, 161, 162syl3anc 1265 . . . 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 ) } )
1642, 163sseldi 3463 . . 3  |-  ( ph  ->  sup ( { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } ,  RR ,  <  )  e.  ( 0..^ M ) )
1651, 164syl5eqel 2515 . 2  |-  ( ph  ->  I  e.  ( 0..^ M ) )
16615, 131sseldi 3463 . . 3  |-  ( ph  ->  sup ( { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) } ,  RR ,  <  )  e.  ZZ )
16714, 166syl5eqel 2515 . 2  |-  ( ph  ->  L  e.  ZZ )
1683, 165sseldi 3463 . . . . . . . . . 10  |-  ( ph  ->  I  e.  ( 0 ... M ) )
16950, 168ffvelrnd 6036 . . . . . . . . 9  |-  ( ph  ->  ( Q `  I
)  e.  RR )
170167zred 11042 . . . . . . . . . 10  |-  ( ph  ->  L  e.  RR )
171170, 62remulcld 9673 . . . . . . . . 9  |-  ( ph  ->  ( L  x.  T
)  e.  RR )
172169, 171readdcld 9672 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  I )  +  ( L  x.  T ) )  e.  RR )
173172rexrd 9692 . . . . . . 7  |-  ( ph  ->  ( ( Q `  I )  +  ( L  x.  T ) )  e.  RR* )
174173adantr 467 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  e.  RR* )
175 fzofzp1 12009 . . . . . . . . . . 11  |-  ( I  e.  ( 0..^ M )  ->  ( I  +  1 )  e.  ( 0 ... M
) )
176165, 175syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( I  +  1 )  e.  ( 0 ... M ) )
17750, 176ffvelrnd 6036 . . . . . . . . 9  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  RR )
178177, 171readdcld 9672 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR )
179178rexrd 9692 . . . . . . 7  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR* )
180179adantr 467 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  RR* )
181 elioore 11668 . . . . . . 7  |-  ( x  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  ->  x  e.  RR )
182181adantl 468 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  x  e.  RR )
183172adantr 467 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  e.  RR )
18444adantr 467 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  e.  RR )
1851, 163syl5eqel 2515 . . . . . . . . . 10  |-  ( ph  ->  I  e.  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) } )
186 fveq2 5879 . . . . . . . . . . . . 13  |-  ( j  =  I  ->  ( Q `  j )  =  ( Q `  I ) )
187186oveq1d 6318 . . . . . . . . . . . 12  |-  ( j  =  I  ->  (
( Q `  j
)  +  ( L  x.  T ) )  =  ( ( Q `
 I )  +  ( L  x.  T
) ) )
188187breq1d 4431 . . . . . . . . . . 11  |-  ( j  =  I  ->  (
( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  I )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
189188elrab 3230 . . . . . . . . . 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 ) ) )
190185, 189sylib 200 . . . . . . . . 9  |-  ( ph  ->  ( I  e.  ( 0..^ M )  /\  ( ( Q `  I )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
191190simprd 465 . . . . . . . 8  |-  ( ph  ->  ( ( Q `  I )  +  ( L  x.  T ) )  <_  ( V `  J ) )
192191adantr 467 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  <_  ( V `  J ) )
193184rexrd 9692 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  e.  RR* )
194 fzofzp1 12009 . . . . . . . . . . . . 13  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
19540, 194syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
19639, 195ffvelrnd 6036 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  H )
19727, 196sseldd 3466 . . . . . . . . . 10  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  RR )
198197rexrd 9692 . . . . . . . . 9  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  RR* )
199198adantr 467 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  ( J  +  1 ) )  e.  RR* )
200 simpr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )
201 ioogtlb 37429 . . . . . . . 8  |-  ( ( ( V `  J
)  e.  RR*  /\  ( V `  ( J  +  1 ) )  e.  RR*  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  <  x )
202193, 199, 200, 201syl3anc 1265 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( V `  J )  <  x )
203183, 184, 182, 192, 202lelttrd 9795 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( Q `  I
)  +  ( L  x.  T ) )  <  x )
204 zssre 10946 . . . . . . . . . . . . . . . 16  |-  ZZ  C_  RR
20515, 204sstri 3474 . . . . . . . . . . . . . . 15  |-  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) }  C_  RR
206205a1i 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 )
20799ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) }  =/=  (/) )
208129ad2antrr 731 . . . . . . . . . . . . . 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 )
209167peano2zd 11045 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( L  +  1 )  e.  ZZ )
210209ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( L  +  1 )  e.  ZZ )
211 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( I  =  ( M  - 
1 )  ->  (
I  +  1 )  =  ( ( M  -  1 )  +  1 ) )
212146recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  CC )
213 1cnd 9661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  e.  CC )
214212, 213npcand 9992 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  =  M )
215211, 214sylan9eqr 2486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
I  +  1 )  =  M )
216215fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  ( I  +  1 ) )  =  ( Q `  M ) )
21747simprd 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( ( Q `
 0 )  =  A  /\  ( Q `
 M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) )
218217simpld 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( Q ` 
0 )  =  A  /\  ( Q `  M )  =  B ) )
219218simprd 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Q `  M
)  =  B )
220219adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  M )  =  B )
22159recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  CC )
22260recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  e.  CC )
223221, 222npcand 9992 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( B  -  A )  +  A
)  =  B )
224223eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  =  ( ( B  -  A )  +  A ) )
22528eqcomi 2436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( B  -  A )  =  T
226225a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( B  -  A
)  =  T )
227226oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( B  -  A )  +  A
)  =  ( T  +  A ) )
228218simpld 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( Q `  0
)  =  A )
229228eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A  =  ( Q `
 0 ) )
230229oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( T  +  A
)  =  ( T  +  ( Q ` 
0 ) ) )
231224, 227, 2303eqtrd 2468 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  =  ( T  +  ( Q ` 
0 ) ) )
232231adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  B  =  ( T  +  ( Q `  0 ) ) )
233216, 220, 2323eqtrd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  ( I  +  1 ) )  =  ( T  +  ( Q `  0 ) ) )
23462recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  T  e.  CC )
235228, 222eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Q `  0
)  e.  CC )
236234, 235addcomd 9837 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( T  +  ( Q `  0 ) )  =  ( ( Q `  0 )  +  T ) )
237236adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( T  +  ( Q `  0 ) )  =  ( ( Q `
 0 )  +  T ) )
238233, 237eqtrd 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  ( Q `  ( I  +  1 ) )  =  ( ( Q `
 0 )  +  T ) )
239238oveq1d 6318 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  =  ( ( ( Q `  0 )  +  T )  +  ( L  x.  T
) ) )
240171recnd 9671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  x.  T
)  e.  CC )
241235, 234, 240addassd 9667 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( Q `
 0 )  +  T )  +  ( L  x.  T ) )  =  ( ( Q `  0 )  +  ( T  +  ( L  x.  T
) ) ) )
242234mulid2d 9663 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1  x.  T
)  =  T )
243242, 234eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1  x.  T
)  e.  CC )
244243, 240addcomd 9837 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1  x.  T )  +  ( L  x.  T ) )  =  ( ( L  x.  T )  +  ( 1  x.  T ) ) )
245242eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  T  =  ( 1  x.  T ) )
246245oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( T  +  ( L  x.  T ) )  =  ( ( 1  x.  T )  +  ( L  x.  T ) ) )
247170recnd 9671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  L  e.  CC )
248247, 213, 234adddird 9670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( L  + 
1 )  x.  T
)  =  ( ( L  x.  T )  +  ( 1  x.  T ) ) )
249244, 246, 2483eqtr4d 2474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( T  +  ( L  x.  T ) )  =  ( ( L  +  1 )  x.  T ) )
250249oveq2d 6319 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( Q ` 
0 )  +  ( T  +  ( L  x.  T ) ) )  =  ( ( Q `  0 )  +  ( ( L  +  1 )  x.  T ) ) )
251241, 250eqtrd 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( Q `
 0 )  +  T )  +  ( L  x.  T ) )  =  ( ( Q `  0 )  +  ( ( L  +  1 )  x.  T ) ) )
252251adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( ( Q ` 
0 )  +  T
)  +  ( L  x.  T ) )  =  ( ( Q `
 0 )  +  ( ( L  + 
1 )  x.  T
) ) )
253239, 252eqtr2d 2465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  (
( Q `  0
)  +  ( ( L  +  1 )  x.  T ) )  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
254253adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( ( L  +  1 )  x.  T ) )  =  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) )
255 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
256254, 255eqbrtrd 4442 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( ( Q ` 
0 )  +  ( ( L  +  1 )  x.  T ) )  <_  ( V `  J ) )
257 oveq1 6310 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( L  + 
1 )  ->  (
k  x.  T )  =  ( ( L  +  1 )  x.  T ) )
258257oveq2d 6319 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( L  + 
1 )  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( ( L  + 
1 )  x.  T
) ) )
259258breq1d 4431 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( L  + 
1 )  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( ( L  +  1 )  x.  T ) )  <_ 
( V `  J
) ) )
260259elrab 3230 . . . . . . . . . . . . . . 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 ) ) )
261210, 256, 260sylanbrc 669 . . . . . . . . . . . . . 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 ) } )
262 suprub 10572 . . . . . . . . . . . . . 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 ,  <  ) )
263206, 207, 208, 261, 262syl31anc 1268 . . . . . . . . . . . . 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 ,  <  ) )
264263, 14syl6breqr 4462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( L  +  1 )  <_  L )
265170ltp1d 10539 . . . . . . . . . . . . . 14  |-  ( ph  ->  L  <  ( L  +  1 ) )
266 peano2re 9808 . . . . . . . . . . . . . . . 16  |-  ( L  e.  RR  ->  ( L  +  1 )  e.  RR )
267170, 266syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( L  +  1 )  e.  RR )
268170, 267ltnled 9784 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( L  <  ( L  +  1 )  <->  -.  ( L  +  1 )  <_  L )
)
269265, 268mpbid 214 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  ( L  + 
1 )  <_  L
)
270269ad2antrr 731 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  I  =  ( M  - 
1 ) )  /\  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  -.  ( L  +  1 )  <_  L )
271264, 270pm2.65da 579 . . . . . . . . . . 11  |-  ( (
ph  /\  I  =  ( M  -  1
) )  ->  -.  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
2725, 165sseldi 3463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  e.  ZZ )
273272zred 11042 . . . . . . . . . . . . . 14  |-  ( ph  ->  I  e.  RR )
274273adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  I  e.  RR )
275 peano2rem 9943 . . . . . . . . . . . . . . 15  |-  ( M  e.  RR  ->  ( M  -  1 )  e.  RR )
276146, 275syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M  -  1 )  e.  RR )
277276adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  -> 
( M  -  1 )  e.  RR )
278 elfzolt2 11931 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 0..^ M )  ->  I  <  M )
279 elfzoelz 11922 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  ( 0..^ M )  ->  I  e.  ZZ )
280 elfzoel2 11921 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  ( 0..^ M )  ->  M  e.  ZZ )
281 zltlem1 10991 . . . . . . . . . . . . . . . . 17  |-  ( ( I  e.  ZZ  /\  M  e.  ZZ )  ->  ( I  <  M  <->  I  <_  ( M  - 
1 ) ) )
282279, 280, 281syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 0..^ M )  ->  ( I  <  M  <->  I  <_  ( M  -  1 ) ) )
283278, 282mpbid 214 . . . . . . . . . . . . . . 15  |-  ( I  e.  ( 0..^ M )  ->  I  <_  ( M  -  1 ) )
284165, 283syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  I  <_  ( M  -  1 ) )
285284adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  I  <_  ( M  - 
1 ) )
286 neqne 37241 . . . . . . . . . . . . . . 15  |-  ( -.  I  =  ( M  -  1 )  ->  I  =/=  ( M  - 
1 ) )
287286necomd 2696 . . . . . . . . . . . . . 14  |-  ( -.  I  =  ( M  -  1 )  -> 
( M  -  1 )  =/=  I )
288287adantl 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  -> 
( M  -  1 )  =/=  I )
289274, 277, 285, 288leneltd 9791 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  I  <  ( M  - 
1 ) )
2906, 204sstri 3474 . . . . . . . . . . . . . . . 16  |-  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_ 
( V `  J
) }  C_  RR
291290a1i 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 )
292145ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  { j  e.  ( 0..^ M )  |  ( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J ) }  =/=  (/) )
293161ad2antrr 731 . . . . . . . . . . . . . . 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 )
294176adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  e.  ( 0 ... M
) )
295273adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  I  e.  RR )
296276adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( M  -  1 )  e.  RR )
297 1red 9660 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  1  e.  RR )
298 simpr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  I  <  ( M  -  1 ) )
299295, 296, 297, 298ltadd1dd 10226 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  < 
( ( M  - 
1 )  +  1 ) )
300214adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( ( M  -  1 )  +  1 )  =  M )
301299, 300breqtrd 4446 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  < 
M )
302 elfzfzo 37334 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  +  1 )  e.  ( 0..^ M )  <->  ( ( I  +  1 )  e.  ( 0 ... M
)  /\  ( I  +  1 )  < 
M ) )
303294, 301, 302sylanbrc 669 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  ( I  +  1 )  e.  ( 0..^ M ) )
304303anim1i 571 . . . . . . . . . . . . . . . 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 ) ) )
305 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( I  + 
1 )  ->  ( Q `  j )  =  ( Q `  ( I  +  1
) ) )
306305oveq1d 6318 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( I  + 
1 )  ->  (
( Q `  j
)  +  ( L  x.  T ) )  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
307306breq1d 4431 . . . . . . . . . . . . . . . . 17  |-  ( j  =  ( I  + 
1 )  ->  (
( ( Q `  j )  +  ( L  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  <_ 
( V `  J
) ) )
308307elrab 3230 . . . . . . . . . . . . . . . 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 ) ) )
309304, 308sylibr 216 . . . . . . . . . . . . . . 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
) } )
310 suprub 10572 . . . . . . . . . . . . . . 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 ,  <  ) )
311291, 292, 293, 309, 310syl31anc 1268 . . . . . . . . . . . . . 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 ,  <  ) )
312311, 1syl6breqr 4462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  -> 
( I  +  1 )  <_  I )
313273ltp1d 10539 . . . . . . . . . . . . . . 15  |-  ( ph  ->  I  <  ( I  +  1 ) )
314 peano2re 9808 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  RR  ->  (
I  +  1 )  e.  RR )
315273, 314syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  e.  RR )
316273, 315ltnled 9784 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( I  <  (
I  +  1 )  <->  -.  ( I  +  1 )  <_  I )
)
317313, 316mpbid 214 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( I  + 
1 )  <_  I
)
318317ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  I  <  ( M  -  1 ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )  ->  -.  ( I  +  1 )  <_  I )
319312, 318pm2.65da 579 . . . . . . . . . . . 12  |-  ( (
ph  /\  I  <  ( M  -  1 ) )  ->  -.  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
320289, 319syldan 473 . . . . . . . . . . 11  |-  ( (
ph  /\  -.  I  =  ( M  - 
1 ) )  ->  -.  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) )
321271, 320pm2.61dan 799 . . . . . . . . . 10  |-  ( ph  ->  -.  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  <_  ( V `  J )
)
32244, 178ltnled 9784 . . . . . . . . . 10  |-  ( ph  ->  ( ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <->  -.  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  ( V `  J ) ) )
323321, 322mpbird 236 . . . . . . . . 9  |-  ( ph  ->  ( V `  J
)  <  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) )
324197adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  e.  RR )
32519adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  D  e.  RR )
326178adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
32718rexrd 9692 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  RR* )
32819rexrd 9692 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  RR* )
32918, 19, 31ltled 9785 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  C  <_  D )
330 lbicc2 11750 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  C  <_  D )  ->  C  e.  ( C [,] D
) )
331327, 328, 329, 330syl3anc 1265 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  C  e.  ( C [,] D ) )
332 ubicc2 11751 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  C  <_  D )  ->  D  e.  ( C [,] D
) )
333327, 328, 329, 332syl3anc 1265 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  e.  ( C [,] D ) )
334331, 333jca 535 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( C  e.  ( C [,] D )  /\  D  e.  ( C [,] D ) ) )
335 prssg 4153 . . . . . . . . . . . . . . . . . . 19  |-  ( ( C  e.  RR  /\  D  e.  RR )  ->  ( ( C  e.  ( C [,] D
)  /\  D  e.  ( C [,] D ) )  <->  { C ,  D }  C_  ( C [,] D ) ) )
33618, 19, 335syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( C  e.  ( C [,] D
)  /\  D  e.  ( C [,] D ) )  <->  { C ,  D }  C_  ( C [,] D ) ) )
337334, 336mpbid 214 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { C ,  D }  C_  ( C [,] D ) )
338337, 23unssd 3643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  C_  ( C [,] D ) )
33917, 338syl5eqss 3509 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H  C_  ( C [,] D ) )
340339, 196sseldd 3466 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( V `  ( J  +  1 ) )  e.  ( C [,] D ) )
341 iccleub 11692 . . . . . . . . . . . . . 14  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  ( V `
 ( J  + 
1 ) )  e.  ( C [,] D
) )  ->  ( V `  ( J  +  1 ) )  <_  D )
342327, 328, 340, 341syl3anc 1265 . . . . . . . . . . . . 13  |-  ( ph  ->  ( V `  ( J  +  1 ) )  <_  D )
343342adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  <_  D
)
344 simpr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
345324, 325, 326, 343, 344letrd 9794 . . . . . . . . . . 11  |-  ( (
ph  /\  D  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  ( J  +  1 ) )  <_  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
346345adantlr 720 . . . . . . . . . 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
) ) )
347 simpr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  -.  D  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
348178adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
34919adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  D  e.  RR )
350348, 349ltnled 9784 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  D  <->  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) ) )
351347, 350mpbird 236 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  D  <_  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )
352351adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  -.  D  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  D )
353 simpll 759 . . . . . . . . . . . . 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 ) ) ) )
354 simpr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  ->  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) ) )
355178adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR )
356197adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( V `  ( J  +  1 ) )  e.  RR )
357355, 356ltnled 9784 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
358354, 357mpbird 236 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( V `  ( J  +  1 ) )  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <  ( V `
 ( J  + 
1 ) ) )
359358adant423 37234 . . . . . . . . . . . . 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
) ) )
36018ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  C  e.  RR )
36119ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  D  e.  RR )
362178ad2antrr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  RR )
36318adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  e.  RR )
364178adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
36544adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  J )  e.  RR )
366339, 43sseldd 3466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V `  J
)  e.  ( C [,] D ) )
367 iccgelb 11693 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  RR*  /\  D  e.  RR*  /\  ( V `
 J )  e.  ( C [,] D
) )  ->  C  <_  ( V `  J
) )
368327, 328, 366, 367syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  C  <_  ( V `  J ) )
369368adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  <_  ( V `  J ) )
370 simpr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
371363, 365, 364, 369, 370lelttrd 9795 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  <  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
372363, 364, 371ltled 9785 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( V `  J )  <  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )  ->  C  <_  ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) ) )
373372adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  C  <_  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
374178adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  RR )
37519adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  D  e.  RR )
376 simpr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )
377374, 375, 376ltled 9785 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  < 
D )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <_  D )
378377adantlr 720 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  <_  D )
379360, 361, 362, 373, 378eliccd 37438 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
380167znegcld 11044 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
-u L  e.  ZZ )
381247, 234mulneg1d 10073 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( -u L  x.  T )  =  -u ( L  x.  T
) )
382381oveq2d 6319 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  =  ( ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  -u ( L  x.  T )
) )
383178recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  CC )
384383, 240negsubd 9994 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  -u ( L  x.  T
) )  =  ( ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  -  ( L  x.  T ) ) )
385177recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  CC )
386385, 240pncand 9989 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  -  ( L  x.  T )
)  =  ( Q `
 ( I  + 
1 ) ) )
387382, 384, 3863eqtrd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  =  ( Q `  ( I  +  1 ) ) )
388 ffn 5744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Q : ( 0 ... M ) --> RR  ->  Q  Fn  ( 0 ... M ) )
38950, 388syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Q  Fn  ( 0 ... M ) )
390 fnfvelrn 6032 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Q  Fn  ( 0 ... M )  /\  ( I  +  1
)  e.  ( 0 ... M ) )  ->  ( Q `  ( I  +  1
) )  e.  ran  Q )
391389, 176, 390syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Q `  (
I  +  1 ) )  e.  ran  Q
)
392387, 391eqeltrd 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  (
-u L  x.  T
) )  e.  ran  Q )
393 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  -u L  ->  (
k  x.  T )  =  ( -u L  x.  T ) )
394393oveq2d 6319 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  -u L  ->  (
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  ( k  x.  T ) )  =  ( ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  +  ( -u L  x.  T ) ) )
395394eleq1d 2492 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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
) )
396395rspcev 3183 . . . . . . . . . . . . . . . . . . 19  |-  ( (
-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 )
397380, 392, 396syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E. k  e.  ZZ  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  ( k  x.  T ) )  e.  ran  Q
)
398397ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  ->  E. k  e.  ZZ  ( ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  +  ( k  x.  T ) )  e.  ran  Q
)
399 oveq1 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  ->  (
y  +  ( k  x.  T ) )  =  ( ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  +  ( k  x.  T
) ) )
400399eleq1d 2492 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  ( k  x.  T ) )  e.  ran  Q ) )
401400rexbidv 2940 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  (
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  +  ( k  x.  T ) )  e.  ran  Q ) )
402401elrab 3230 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  <->  ( ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  ( C [,] D
)  /\  E. k  e.  ZZ  ( ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  +  ( k  x.  T
) )  e.  ran  Q ) )
403379, 398, 402sylanbrc 669 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)
404 elun2 3635 . . . . . . . . . . . . . . . 16  |-  ( ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  e.  { y  e.  ( C [,] D
)  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  ->  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) )
405403, 404syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )
40617eqcomi 2436 . . . . . . . . . . . . . . 15  |-  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } )  =  H
407405, 406syl6eleq 2521 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( V `  J )  <  ( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) ) )  /\  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  <  D )  -> 
( ( Q `  ( I  +  1
) )  +  ( L  x.  T ) )  e.  H )
408407adantr 467 . . . . . . . . . . . . 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 ) )  e.  H )
409 f1ofo 5836 . . . . . . . . . . . . . . . . . 18  |-  ( V : ( 0 ... N ) -1-1-onto-> H  ->  V :
( 0 ... N
) -onto-> H )
41036, 37, 4093syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  V : ( 0 ... N ) -onto-> H )
411 foelrn 6054 . . . . . . . . . . . . . . . . 17  |-  ( ( V : ( 0 ... N ) -onto-> H  /\  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  e.  H
)  ->  E. j  e.  ( 0 ... N
) ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  =  ( V `  j ) )
412410, 411sylan 474 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  H )  ->  E. j  e.  ( 0 ... N
) ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) )  =  ( V `  j ) )
413 id 23 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  =  ( V `  j )  ->  (
( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  =  ( V `  j ) )
414413eqcomd 2431 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Q `  (
I  +  1 ) )  +  ( L  x.  T ) )  =  ( V `  j )  ->  ( V `  j )  =  ( ( Q `
 ( I  + 
1 ) )  +  ( L  x.  T
) ) )
415414a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( ( Q `  ( I  +  1 ) )  +  ( L  x.  T ) )  e.  H