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

Theorem fourierdlem50 31780
Description: Continuity of  O and its limits with respect to the  S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem50.xre  |-  ( ph  ->  X  e.  RR )
fourierdlem50.p  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
fourierdlem50.m  |-  ( ph  ->  M  e.  NN )
fourierdlem50.v  |-  ( ph  ->  V  e.  ( P `
 M ) )
fourierdlem50.a  |-  ( ph  ->  A  e.  RR )
fourierdlem50.b  |-  ( ph  ->  B  e.  RR )
fourierdlem50.altb  |-  ( ph  ->  A  <  B )
fourierdlem50.ab  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
fourierdlem50.q  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
fourierdlem50.t  |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
fourierdlem50.n  |-  N  =  ( ( # `  T
)  -  1 )
fourierdlem50.s  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
fourierdlem50.j  |-  ( ph  ->  J  e.  ( 0..^ N ) )
fourierdlem50.u  |-  U  =  ( iota_ i  e.  ( 0..^ M ) ( ( S `  J
) (,) ( S `
 ( J  + 
1 ) ) ) 
C_  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
fourierdlem50.ch  |-  ( ch  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) ) )
Assertion
Ref Expression
fourierdlem50  |-  ( ph  ->  ( U  e.  ( 0..^ M )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  U ) (,) ( Q `  ( U  +  1 ) ) ) ) )
Distinct variable groups:    i, J, k    i, M, k    m, M, p, i    f, N    Q, i, k    S, f    S, i, k    T, f    U, i    i, V, k    V, p    i, X, k   
m, X, p    ph, f    ph, i, k
Allowed substitution hints:    ph( m, p)    ch( f, i, k, m, p)    A( f, i, k, m, p)    B( f,
i, k, m, p)    P( f, i, k, m, p)    Q( f, m, p)    S( m, p)    T( i,
k, m, p)    U( f, k, m, p)    J( f, m, p)    M( f)    N( i, k, m, p)    V( f, m)    X( f)

Proof of Theorem fourierdlem50
Dummy variables  x  h  l are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem50.u . . 3  |-  U  =  ( iota_ i  e.  ( 0..^ M ) ( ( S `  J
) (,) ( S `
 ( J  + 
1 ) ) ) 
C_  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
2 fourierdlem50.m . . . . . . . 8  |-  ( ph  ->  M  e.  NN )
3 fourierdlem50.a . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
4 fourierdlem50.b . . . . . . . 8  |-  ( ph  ->  B  e.  RR )
5 fourierdlem50.altb . . . . . . . . 9  |-  ( ph  ->  A  <  B )
63, 4, 5ltled 9744 . . . . . . . 8  |-  ( ph  ->  A  <_  B )
7 fourierdlem50.p . . . . . . . . . . . . 13  |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  m )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ m ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
8 fourierdlem50.v . . . . . . . . . . . . 13  |-  ( ph  ->  V  e.  ( P `
 M ) )
97, 2, 8fourierdlem15 31745 . . . . . . . . . . . 12  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
10 pire 22718 . . . . . . . . . . . . . . . . 17  |-  pi  e.  RR
1110renegcli 9892 . . . . . . . . . . . . . . . 16  |-  -u pi  e.  RR
1211a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u pi  e.  RR )
13 fourierdlem50.xre . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
1412, 13jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u pi  e.  RR  /\  X  e.  RR ) )
15 readdcl 9587 . . . . . . . . . . . . . 14  |-  ( (
-u pi  e.  RR  /\  X  e.  RR )  ->  ( -u pi  +  X )  e.  RR )
1614, 15syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
1710a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  pi  e.  RR )
1817, 13jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( pi  e.  RR  /\  X  e.  RR ) )
19 readdcl 9587 . . . . . . . . . . . . . 14  |-  ( ( pi  e.  RR  /\  X  e.  RR )  ->  ( pi  +  X
)  e.  RR )
2018, 19syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
2116, 20iccssred 31426 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
229, 21fssd 5746 . . . . . . . . . . 11  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
2322ffvelrnda 6032 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
2413adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
2523, 24resubcld 9999 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
26 fourierdlem50.q . . . . . . . . 9  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
2725, 26fmptd 6056 . . . . . . . 8  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
2826a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) ) )
29 fveq2 5872 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( V `  i )  =  ( V ` 
0 ) )
3029oveq1d 6310 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
3130adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  i  = 
0 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
32 nnssnn0 10810 . . . . . . . . . . . . . . 15  |-  NN  C_  NN0
3332a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  C_  NN0 )
34 nn0uz 11128 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
3533, 34syl6sseq 3555 . . . . . . . . . . . . 13  |-  ( ph  ->  NN  C_  ( ZZ>= ` 
0 ) )
3635, 2sseldd 3510 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
37 eluzfz1 11705 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
3836, 37syl 16 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 ... M ) )
3922, 38ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( V `  0
)  e.  RR )
4039, 13resubcld 9999 . . . . . . . . . . 11  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  e.  RR )
4128, 31, 38, 40fvmptd 5962 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  =  ( ( V `  0 )  -  X ) )
427fourierdlem2 31732 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  ->  ( V  e.  ( P `  M )  <->  ( V  e.  ( RR  ^m  (
0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
432, 42syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( V  e.  ( P `  M )  <-> 
( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) ) )
448, 43mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( V  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( V `  0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) ) )
4544simprd 463 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
4645simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( V ` 
0 )  =  (
-u pi  +  X
)  /\  ( V `  M )  =  ( pi  +  X ) ) )
4746simpld 459 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  0
)  =  ( -u pi  +  X ) )
4847oveq1d 6310 . . . . . . . . . 10  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  =  ( (
-u pi  +  X
)  -  X ) )
4912recnd 9634 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  e.  CC )
5013recnd 9634 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  CC )
5149, 50pncand 9943 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
5241, 48, 513eqtrd 2512 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
5312rexrd 9655 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  e.  RR* )
5417rexrd 9655 . . . . . . . . . 10  |-  ( ph  ->  pi  e.  RR* )
55 fourierdlem50.ab . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
563leidd 10131 . . . . . . . . . . . 12  |-  ( ph  ->  A  <_  A )
573, 4, 3, 56, 6eliccd 31425 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( A [,] B ) )
5855, 57sseldd 3510 . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( -u pi [,] pi ) )
59 iccgelb 11593 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  A  e.  ( -u pi [,] pi ) )  ->  -u pi  <_  A )
6053, 54, 58, 59syl3anc 1228 . . . . . . . . 9  |-  ( ph  -> 
-u pi  <_  A
)
6152, 60eqbrtrd 4473 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <_  A )
624leidd 10131 . . . . . . . . . . . 12  |-  ( ph  ->  B  <_  B )
633, 4, 4, 6, 62eliccd 31425 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( A [,] B ) )
6455, 63sseldd 3510 . . . . . . . . . 10  |-  ( ph  ->  B  e.  ( -u pi [,] pi ) )
65 iccleub 11592 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  B  e.  ( -u pi [,] pi ) )  ->  B  <_  pi )
6653, 54, 64, 65syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  B  <_  pi )
67 fveq2 5872 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  ( V `  i )  =  ( V `  M ) )
6867oveq1d 6310 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
( V `  i
)  -  X )  =  ( ( V `
 M )  -  X ) )
6968adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  i  =  M )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 M )  -  X ) )
70 eluzfz2 11706 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
7136, 70syl 16 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 0 ... M ) )
7222, 71ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( V `  M
)  e.  RR )
7372, 13resubcld 9999 . . . . . . . . . . 11  |-  ( ph  ->  ( ( V `  M )  -  X
)  e.  RR )
7428, 69, 71, 73fvmptd 5962 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  =  ( ( V `  M )  -  X ) )
7546simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  M
)  =  ( pi  +  X ) )
7675oveq1d 6310 . . . . . . . . . 10  |-  ( ph  ->  ( ( V `  M )  -  X
)  =  ( ( pi  +  X )  -  X ) )
7717recnd 9634 . . . . . . . . . . 11  |-  ( ph  ->  pi  e.  CC )
7877, 50pncand 9943 . . . . . . . . . 10  |-  ( ph  ->  ( ( pi  +  X )  -  X
)  =  pi )
7974, 76, 783eqtrrd 2513 . . . . . . . . 9  |-  ( ph  ->  pi  =  ( Q `
 M ) )
8066, 79breqtrd 4477 . . . . . . . 8  |-  ( ph  ->  B  <_  ( Q `  M ) )
81 fourierdlem50.j . . . . . . . 8  |-  ( ph  ->  J  e.  ( 0..^ N ) )
82 eqid 2467 . . . . . . . 8  |-  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
83 fourierdlem50.t . . . . . . . . . . 11  |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
84 prfi 7807 . . . . . . . . . . . . 13  |-  { A ,  B }  e.  Fin
8584a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  { A ,  B }  e.  Fin )
86 fzfid 12063 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
8726rnmptfi 31348 . . . . . . . . . . . . . 14  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
8886, 87syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  Q  e.  Fin )
89 infi 7755 . . . . . . . . . . . . 13  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
9088, 89syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
91 unfi 7799 . . . . . . . . . . . 12  |-  ( ( { A ,  B }  e.  Fin  /\  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )  -> 
( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
9285, 90, 91syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
9383, 92syl5eqel 2559 . . . . . . . . . 10  |-  ( ph  ->  T  e.  Fin )
943, 4jca 532 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
95 prssg 4188 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
963, 4, 95syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
9794, 96mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  { A ,  B }  C_  RR )
98 inss2 3724 . . . . . . . . . . . . . 14  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A (,) B )
99 ioossre 11598 . . . . . . . . . . . . . 14  |-  ( A (,) B )  C_  RR
10098, 99sstri 3518 . . . . . . . . . . . . 13  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  RR
101100a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  RR )
10297, 101unssd 3685 . . . . . . . . . . 11  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  RR )
10383, 102syl5eqss 3553 . . . . . . . . . 10  |-  ( ph  ->  T  C_  RR )
104 fourierdlem50.s . . . . . . . . . 10  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
105 fourierdlem50.n . . . . . . . . . 10  |-  N  =  ( ( # `  T
)  -  1 )
10693, 103, 104, 105fourierdlem36 31766 . . . . . . . . 9  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
107 isoeq5 6218 . . . . . . . . . 10  |-  ( T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  ->  ( S  Isom  <  ,  <  (
( 0 ... N
) ,  T )  <-> 
S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) ) ) )
10883, 107ax-mp 5 . . . . . . . . 9  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  <-> 
S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) ) )
109106, 108sylib 196 . . . . . . . 8  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) ) )
110 eqid 2467 . . . . . . . 8  |-  sup ( { x  e.  (
0..^ M )  |  ( Q `  x
)  <_  ( S `  J ) } ,  RR ,  <  )  =  sup ( { x  e.  ( 0..^ M )  |  ( Q `  x )  <_  ( S `  J ) } ,  RR ,  <  )
1112, 3, 4, 6, 27, 61, 80, 81, 82, 109, 110fourierdlem20 31750 . . . . . . 7  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( ( S `  J
) (,) ( S `
 ( J  + 
1 ) ) ) 
C_  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
112 fourierdlem50.ch . . . . . . . . . . . . . 14  |-  ( ch  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) ) )
113112biimpri 206 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  ->  ch )
114112biimpi 194 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `
 J ) (,) ( S `  ( J  +  1 ) ) )  C_  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
) ) )  C_  ( ( Q `  k ) (,) ( Q `  ( k  +  1 ) ) ) ) )
115 simp-4l 765 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  ->  ph )
116114, 115syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ph )
117 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  -> 
k  e.  ( 0..^ M ) )
118114, 117syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  k  e.  (
0..^ M ) )
119116, 118jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ph  /\  k  e.  ( 0..^ M ) ) )
120 simp-4r 766 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  -> 
i  e.  ( 0..^ M ) )
121114, 120syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  i  e.  (
0..^ M ) )
122 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( 0..^ M )  ->  k  e.  ( 0 ... M
) )
123122ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  -> 
k  e.  ( 0 ... M ) )
124114, 123syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  k  e.  (
0 ... M ) )
125116, 22syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  V : ( 0 ... M ) --> RR )
126125, 124ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( V `  k
)  e.  RR )
127116, 13syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  X  e.  RR )
128126, 127resubcld 9999 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( V `  k )  -  X
)  e.  RR )
129 nfv 1683 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ i ( ( k  e.  ( 0 ... M
)  /\  ( ( V `  k )  -  X )  e.  RR )  ->  ( Q `  k )  =  ( ( V `  k
)  -  X ) )
130 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  k  ->  (
i  e.  ( 0 ... M )  <->  k  e.  ( 0 ... M
) ) )
131 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  k  ->  ( V `  i )  =  ( V `  k ) )
132131oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  k  ->  (
( V `  i
)  -  X )  =  ( ( V `
 k )  -  X ) )
133132eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  k  ->  (
( ( V `  i )  -  X
)  e.  RR  <->  ( ( V `  k )  -  X )  e.  RR ) )
134130, 133anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  k  ->  (
( i  e.  ( 0 ... M )  /\  ( ( V `
 i )  -  X )  e.  RR ) 
<->  ( k  e.  ( 0 ... M )  /\  ( ( V `
 k )  -  X )  e.  RR ) ) )
135 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  k  ->  ( Q `  i )  =  ( Q `  k ) )
136135, 132eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  k  ->  (
( Q `  i
)  =  ( ( V `  i )  -  X )  <->  ( Q `  k )  =  ( ( V `  k
)  -  X ) ) )
137134, 136imbi12d 320 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  k  ->  (
( ( i  e.  ( 0 ... M
)  /\  ( ( V `  i )  -  X )  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )  <->  ( ( k  e.  ( 0 ... M )  /\  (
( V `  k
)  -  X )  e.  RR )  -> 
( Q `  k
)  =  ( ( V `  k )  -  X ) ) ) )
13826fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
139129, 137, 138chvar 1982 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  ( 0 ... M )  /\  ( ( V `  k )  -  X
)  e.  RR )  ->  ( Q `  k )  =  ( ( V `  k
)  -  X ) )
140124, 128, 139syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  k
)  =  ( ( V `  k )  -  X ) )
141140, 128eqeltrd 2555 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  k
)  e.  RR )
14227adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
143 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
144143adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
145142, 144ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
146116, 121, 145syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
147 isof1o 6220 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  ->  S : ( 0 ... N ) -1-1-onto-> T )
148106, 147syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  S : ( 0 ... N ) -1-1-onto-> T )
149 f1of 5822 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( S : ( 0 ... N ) -1-1-onto-> T  ->  S :
( 0 ... N
) --> T )
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  S : ( 0 ... N ) --> T )
151 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
15281, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
153150, 152ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  T )
154103, 153sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR )
155116, 154syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( S `  ( J  +  1 ) )  e.  RR )
156 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
15781, 156syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  J  e.  ( 0 ... N ) )
158150, 157ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( S `  J
)  e.  T )
159103, 158sseldd 3510 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( S `  J
)  e.  RR )
160116, 159syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( S `  J
)  e.  RR )
161114simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )
162141rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Q `  k
)  e.  RR* )
16327adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
164 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  ( 0..^ M )  ->  ( k  +  1 )  e.  ( 0 ... M
) )
165164adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( k  +  1 )  e.  ( 0 ... M ) )
166163, 165ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  e.  RR )
167166rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  e.  RR* )
168119, 167syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  e.  RR* )
169160rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( S `  J
)  e.  RR* )
170155rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( S `  ( J  +  1 ) )  e.  RR* )
171 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ZZ )
172171zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( J  e.  ( 0..^ N )  ->  J  e.  RR )
173172ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( J  e.  ( 0..^ N )  ->  J  <  ( J  +  1 ) )
17481, 173syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  J  <  ( J  +  1 ) )
175 isorel 6221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) )  /\  ( J  e.  (
0 ... N )  /\  ( J  +  1
)  e.  ( 0 ... N ) ) )  ->  ( J  <  ( J  +  1 )  <->  ( S `  J )  <  ( S `  ( J  +  1 ) ) ) )
176109, 157, 152, 175syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( J  <  ( J  +  1 )  <-> 
( S `  J
)  <  ( S `  ( J  +  1 ) ) ) )
177174, 176mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
178116, 177syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
179162, 168, 169, 170, 178ioossioobi 31444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( ( S `
 J ) (,) ( S `  ( J  +  1 ) ) )  C_  (
( Q `  k
) (,) ( Q `
 ( k  +  1 ) ) )  <-> 
( ( Q `  k )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) ) ) )
180161, 179mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( Q `  k )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) ) )
181180simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  k
)  <_  ( S `  J ) )
182141, 160, 155, 181, 178lelttrd 9751 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  k
)  <  ( S `  ( J  +  1 ) ) )
183 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  -> 
( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
184114, 183syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
185 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
186185ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0 ... M
) )
187186ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )  -> 
i  e.  ( 0 ... M ) )
188114, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  i  e.  (
0 ... M ) )
189116, 188, 25syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( V `  i )  -  X
)  e.  RR )
190188, 189, 138syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( Q `  i
)  =  ( ( V `  i )  -  X ) )
191190, 189eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Q `  i
)  e.  RR )
192191rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  i
)  e.  RR* )
193146rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR* )
194192, 193, 169, 170, 178ioossioobi 31444 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( ( S `
 J ) (,) ( S `  ( J  +  1 ) ) )  C_  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  <-> 
( ( Q `  i )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) ) )
195184, 194mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( Q `  i )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) )
196195simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
197141, 155, 146, 182, 196ltletrd 9753 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  k
)  <  ( Q `  ( i  +  1 ) ) )
198141, 146, 127, 197ltadd2dd 9752 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  k ) )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
199140oveq2d 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( X  +  ( Q `  k ) )  =  ( X  +  ( ( V `
 k )  -  X ) ) )
200116, 50syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  X  e.  CC )
201 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  C_  CC
202201, 126sseldi 3507 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( V `  k
)  e.  CC )
203200, 202pncan3d 9945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( X  +  ( ( V `  k
)  -  X ) )  =  ( V `
 k ) )
204199, 203eqtrd 2508 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( Q `  k ) )  =  ( V `
 k ) )
205204eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  k
)  =  ( X  +  ( Q `  k ) ) )
206121, 143syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( i  +  1 )  e.  ( 0 ... M ) )
20722adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
208207, 144ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
209116, 121, 208syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR )
210209, 127resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( V `  ( i  +  1 ) )  -  X
)  e.  RR )
211206, 210jca 532 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR ) )
212 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( i  +  1 )  ->  (
k  e.  ( 0 ... M )  <->  ( i  +  1 )  e.  ( 0 ... M
) ) )
213 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  ( i  +  1 )  ->  ( V `  k )  =  ( V `  ( i  +  1 ) ) )
214213oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  ( i  +  1 )  ->  (
( V `  k
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
215214eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( i  +  1 )  ->  (
( ( V `  k )  -  X
)  e.  RR  <->  ( ( V `  ( i  +  1 ) )  -  X )  e.  RR ) )
216212, 215anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( i  +  1 )  ->  (
( k  e.  ( 0 ... M )  /\  ( ( V `
 k )  -  X )  e.  RR ) 
<->  ( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR ) ) )
217 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( i  +  1 )  ->  ( Q `  k )  =  ( Q `  ( i  +  1 ) ) )
218217, 214eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( i  +  1 )  ->  (
( Q `  k
)  =  ( ( V `  k )  -  X )  <->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) ) )
219216, 218imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  (
( ( k  e.  ( 0 ... M
)  /\  ( ( V `  k )  -  X )  e.  RR )  ->  ( Q `  k )  =  ( ( V `  k
)  -  X ) )  <->  ( ( ( i  +  1 )  e.  ( 0 ... M )  /\  (
( V `  (
i  +  1 ) )  -  X )  e.  RR )  -> 
( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) ) ) )
220219, 139vtoclg 3176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  +  1 )  e.  ( 0 ... M )  ->  (
( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) ) )
221206, 211, 220sylc 60 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) )
222221oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
223201, 209sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  CC )
224200, 223pncan3d 9945 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( ( V `  (
i  +  1 ) )  -  X ) )  =  ( V `
 ( i  +  1 ) ) )
225222, 224eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  (
i  +  1 ) )  =  ( X  +  ( Q `  ( i  +  1 ) ) ) )
226205, 225breq12d 4466 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( V `  k )  <  ( V `  ( i  +  1 ) )  <-> 
( X  +  ( Q `  k ) )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) ) )
227198, 226mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  k
)  <  ( V `  ( i  +  1 ) ) )
228 nfv 1683 . . . . . . . . . . . . . . . . . 18  |-  F/ l ( ( ( (
ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( i  +  1 ) ) )  ->  ( V `  k )  <_  ( V `  i )
)
229 eleq1 2539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  (
l  e.  ( 0..^ M )  <->  i  e.  ( 0..^ M ) ) )
230229anbi2d 703 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  (
( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) ) ) )
231 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  i  ->  (
l  +  1 )  =  ( i  +  1 ) )
232231fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  ( V `  ( l  +  1 ) )  =  ( V `  ( i  +  1 ) ) )
233232breq2d 4465 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  (
( V `  k
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  k )  <  ( V `  ( i  +  1 ) ) ) )
234230, 233anbi12d 710 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( l  +  1 ) ) )  <->  ( (
( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 k )  < 
( V `  (
i  +  1 ) ) ) ) )
235 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  ( V `  l )  =  ( V `  i ) )
236235breq2d 4465 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( V `  k
)  <_  ( V `  l )  <->  ( V `  k )  <_  ( V `  i )
) )
237234, 236imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  i  ->  (
( ( ( (
ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( l  +  1 ) ) )  ->  ( V `  k )  <_  ( V `  l )
)  <->  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) )  /\  ( V `
 k )  < 
( V `  (
i  +  1 ) ) )  ->  ( V `  k )  <_  ( V `  i
) ) ) )
238 nfv 1683 . . . . . . . . . . . . . . . . . . 19  |-  F/ h
( ( ( (
ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( l  +  1 ) ) )  ->  ( V `  k )  <_  ( V `  l )
)
239 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  k  ->  (
h  e.  ( 0..^ M )  <->  k  e.  ( 0..^ M ) ) )
240239anbi2d 703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  k  ->  (
( ph  /\  h  e.  ( 0..^ M ) )  <->  ( ph  /\  k  e.  ( 0..^ M ) ) ) )
241240anbi1d 704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  k  ->  (
( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) ) ) )
242 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  k  ->  ( V `  h )  =  ( V `  k ) )
243242breq1d 4463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  k  ->  (
( V `  h
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  k )  <  ( V `  ( l  +  1 ) ) ) )
244241, 243anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  k  ->  (
( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  <->  ( (
( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `
 k )  < 
( V `  (
l  +  1 ) ) ) ) )
245242breq1d 4463 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  k  ->  (
( V `  h
)  <_  ( V `  l )  <->  ( V `  k )  <_  ( V `  l )
) )
246244, 245imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  k  ->  (
( ( ( (
ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  ( V `  h )  <_  ( V `  l )
)  <->  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `
 k )  < 
( V `  (
l  +  1 ) ) )  ->  ( V `  k )  <_  ( V `  l
) ) ) )
247 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  e.  ( 0..^ M )  ->  h  e.  ZZ )
248247ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  e.  ZZ )
249 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( l  e.  ( 0..^ M )  ->  l  e.  ZZ )
250249ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
l  e.  ZZ )
251 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
252 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) ) )
253 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  h  <  ( l  +  1 ) )
254249zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( l  e.  ( 0..^ M )  ->  l  e.  RR )
255 peano2re 9764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( l  e.  RR  ->  (
l  +  1 )  e.  RR )
256254, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  RR )
257256ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( l  +  1 )  e.  RR )
258247zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( h  e.  ( 0..^ M )  ->  h  e.  RR )
259258ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  h  e.  RR )
260257, 259lenltd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( ( l  +  1 )  <_  h 
<->  -.  h  <  (
l  +  1 ) ) )
261253, 260mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( l  +  1 )  <_  h
)
262249peano2zd 10981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  ZZ )
263262ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( l  +  1 )  e.  ZZ )
264247ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ZZ )
265 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( l  +  1 )  <_  h )
266263, 264, 2653jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( ( l  +  1 )  e.  ZZ  /\  h  e.  ZZ  /\  ( l  +  1 )  <_  h )
)
267 eluz2 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( h  e.  ( ZZ>= `  (
l  +  1 ) )  <->  ( ( l  +  1 )  e.  ZZ  /\  h  e.  ZZ  /\  ( l  +  1 )  <_  h ) )
268266, 267sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ( ZZ>= `  ( l  +  1 ) ) )
269268adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ( ZZ>= `  ( l  +  1 ) ) )
270 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ph )
271 0z 10887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  0  e.  ZZ
272271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  0  e.  ZZ )
273 elfzoel2 11808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( h  e.  ( 0..^ M )  ->  M  e.  ZZ )
274273ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  M  e.  ZZ )
275 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  e.  ZZ )
276275adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ZZ )
277272, 274, 2763jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ ) )
278 0re 9608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  0  e.  RR
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  e.  RR )
280275zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  e.  RR )
281280adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  e.  RR )
282254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  e.  RR )
283 elfzole1 11816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( l  e.  ( 0..^ M )  ->  0  <_  l )
284283adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <_  l )
285282, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  (
l  +  1 )  e.  RR )
286282ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  <  ( l  +  1 ) )
287 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  (
l  +  1 )  <_  i )
288287adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  (
l  +  1 )  <_  i )
289282, 285, 281, 286, 288ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  <  i )
290279, 282, 281, 284, 289lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <  i )
291279, 281, 290ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <_  i )
292291adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  0  <_  i
)
293280adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  e.  RR )
294273zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( h  e.  ( 0..^ M )  ->  M  e.  RR )
295294adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  M  e.  RR )
296258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  h  e.  RR )
297 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  <_  h )
298297adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <_  h )
299 elfzolt2 11817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( h  e.  ( 0..^ M )  ->  h  <  M )
300299adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  h  <  M )
301293, 296, 295, 298, 300lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <  M )
302293, 295, 301ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <_  M )
303302adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  <_  M
)
304277, 292, 303jca32 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )  /\  (
0  <_  i  /\  i  <_  M ) ) )
305 elfz2 11691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )  /\  (
0  <_  i  /\  i  <_  M ) ) )
306304, 305sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ( 0 ... M ) )
307306adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ( 0 ... M ) )
308270, 307, 23syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ( V `  i )  e.  RR )
309308adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  /\  i  e.  (
( l  +  1 ) ... h ) )  ->  ( V `  i )  e.  RR )
310 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ph )
311271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  e.  ZZ )
312 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  e.  ZZ )
313312adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  ZZ )
314278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  e.  RR )
315313zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  RR )
316254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  e.  RR )
317283adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <_  l )
318316, 255syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
l  +  1 )  e.  RR )
319316ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  <  ( l  +  1 ) )
320 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  (
l  +  1 )  <_  i )
321320adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
l  +  1 )  <_  i )
322316, 318, 315, 319, 321ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  <  i )
323314, 316, 315, 317, 322lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <  i )
324314, 315, 323ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <_  i )
325311, 313, 3243jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
0  e.  ZZ  /\  i  e.  ZZ  /\  0  <_  i ) )
326 eluz2 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  i  e.  ZZ  /\  0  <_ 
i ) )
327325, 326sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
328327adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  e.  (
ZZ>= `  0 ) )
329 elfzoel2 11808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( l  e.  ( 0..^ M )  ->  M  e.  ZZ )
330329ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  M  e.  ZZ )
331312zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  e.  RR )
332331adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  RR )
333 peano2rem 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( h  e.  RR  ->  (
h  -  1 )  e.  RR )
334258, 333syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  e.  RR )
335334adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
h  -  1 )  e.  RR )
336294adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  M  e.  RR )
337 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  <_  ( h  -  1 ) )
338337adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <_  ( h  -  1 ) )
339258ltm1d 10490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  < 
h )
340334, 258, 294, 339, 299lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  < 
M )
341340adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
h  -  1 )  <  M )
342332, 335, 336, 338, 341lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <  M )
343342adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <  M )
344343adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  <  M
)
345328, 330, 3443jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ( i  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  i  <  M ) )
346 elfzo2 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ M )  <->  ( i  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  i  <  M ) )
347345, 346sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  e.  ( 0..^ M ) )
348185, 23sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
34945simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
350349r19.21bi 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
351348, 208, 350ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
352310, 347, 351syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
353352adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  /\  i  e.  (
( l  +  1 ) ... ( h  -  1 ) ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
354269, 309, 353monoord 12117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( V `  (
l  +  1 ) )  <_  ( V `  h ) )
355252, 261, 354syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  ( l  +  1 ) )  <_  ( V `  h )
)
35622adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
357 fzofzp1 11889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  ( 0 ... M
) )
358357adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  ( l  +  1 )  e.  ( 0 ... M ) )
359356, 358ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
360359adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
361360adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
36222adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
363 elfzofz 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( h  e.  ( 0..^ M )  ->  h  e.  ( 0 ... M
) )
364363adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  h  e.  ( 0 ... M ) )
365362, 364ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  ( V `  h )  e.  RR )
366365ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  h )  e.  RR )
367361, 366lenltd 9742 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( ( V `
 ( l  +  1 ) )  <_ 
( V `  h
)  <->  -.  ( V `  h )  <  ( V `  ( l  +  1 ) ) ) )
368355, 367mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
369368adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
370251, 369condan 792 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  <  ( l  +  1 ) )
371 zleltp1 10925 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ZZ  /\  l  e.  ZZ )  ->  ( h  <_  l  <->  h  <  ( l  +  1 ) ) )
372248, 250, 371syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( h  <_  l  <->  h  <  ( l  +  1 ) ) )
373370, 372mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  <_  l )
374248, 250, 3733jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( h  e.  ZZ  /\  l  e.  ZZ  /\  h  <_  l ) )
375 eluz2 11100 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  e.  ( ZZ>= `  h
)  <->  ( h  e.  ZZ  /\  l  e.  ZZ  /\  h  <_ 
l ) )
376374, 375sylibr 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
l  e.  ( ZZ>= `  h ) )
37722ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  ->  V : ( 0 ... M ) --> RR )
378271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
0  e.  ZZ )
379273ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  ->  M  e.  ZZ )
380 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( h ... l )  ->  i  e.  ZZ )
381380adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ZZ )
382378, 379, 3813jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )
)
383278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  e.  RR )
384258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  h  e.  RR )
385380zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( h ... l )  ->  i  e.  RR )
386385adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  e.  RR )
387 elfzole1 11816 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  e.  ( 0..^ M )  ->  0  <_  h )
388387adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  <_  h )
389 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( h ... l )  ->  h  <_  i )
390389adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  h  <_  i )
391383, 384, 386, 388, 390letrd 9750 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  <_  i )
392391adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
0  <_  i )
393385adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  e.  RR )
394329zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  M  e.  RR )
395394adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  M  e.  RR )
396254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  l  e.  RR )
397 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( h ... l )  ->  i  <_  l )
398397adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <_  l )
399 elfzolt2 11817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( l  e.  ( 0..^ M )  ->  l  <  M )
400399adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  l  <  M )
401393, 396, 395, 398, 400lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <  M )
402393, 395, 401ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <_  M )
403402adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  <_  M )
404382, 392, 403jca32 535 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( ( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )  /\  (
0  <_  i  /\  i  <_  M ) ) )
405404, 305sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ( 0 ... M ) )
406405adantlll 717 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ( 0 ... M ) )
407377, 406ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( V `  i
)  e.  RR )
408407adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... l ) )  -> 
( V `  i
)  e.  RR )
409 simp-4l 765 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  ->  ph )
410271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  e.  ZZ )
411 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  e.  ZZ )
412411adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ZZ )
413278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  e.  RR )
414258adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  h  e.  RR )
415412zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  RR )
416387adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  <_  h )
417 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  h  <_  i )
418417adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  h  <_  i )
419413, 414, 415, 416, 418letrd 9750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  <_  i )
420410, 412, 4193jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  (
0  e.  ZZ  /\  i  e.  ZZ  /\  0  <_  i ) )
421420, 326sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
422421adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
423422adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  e.  ( ZZ>= ` 
0 ) )
424423adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  e.  ( ZZ>= ` 
0 ) )
425329ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  ->  M  e.  ZZ )
426411zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  e.  RR )
427426adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  RR )
428254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  e.  RR )
429394adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  M  e.  RR )
430 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  <_  ( l  -  1 ) )
431430adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <_  ( l  -  1 ) )
432411adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ZZ )
433249adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  e.  ZZ )
434 zltlem1 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( i  e.  ZZ  /\  l  e.  ZZ )  ->  ( i  <  l  <->  i  <_  ( l  - 
1 ) ) )
435432, 433, 434syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  (
i  <  l  <->  i  <_  ( l  -  1 ) ) )
436431, 435mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  l )
437399adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  <  M )
438427, 428, 429, 436, 437lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  M )
439438adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  M )
440439adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  <  M )
441440adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  <  M )
442424, 425, 4413jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
( i  e.  (
ZZ>= `  0 )  /\  M  e.  ZZ  /\  i  <  M ) )
443442, 346sylibr 212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  e.  ( 0..^ M ) )
444409, 443, 351syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
( V `  i
)  <_  ( V `  ( i  +  1 ) ) )
445376, 408, 444monoord 12117 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  h
)  <_  ( V `  l ) )
446238, 246, 445chvar 1982 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  k
)  <_  ( V `  l ) )
447228, 237, 446chvar 1982 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( i  +  1 ) ) )  -> 
( V `  k
)  <_  ( V `  i ) )
448119, 121, 227, 447syl21anc 1227 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  k
)  <_  ( V `  i ) )
449116, 121jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ph  /\  i  e.  ( 0..^ M ) ) )
450119, 166syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  e.  RR )
451195simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  i
)  <_  ( S `  J ) )
452191, 160, 155, 451, 178lelttrd 9751 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  i
)  <  ( S `  ( J  +  1 ) ) )
453180simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) )
454191, 155, 450, 452, 453ltletrd 9753 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  i
)  <  ( Q `  ( k  +  1 ) ) )
455191, 450, 127, 454ltadd2dd 9752 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  i ) )  <  ( X  +  ( Q `  ( k  +  1 ) ) ) )
456190oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( Q `  i ) )  =  ( X  +  ( ( V `
 i )  -  X ) ) )
457201a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  RR  C_  CC )
458116, 188, 23syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( V `  i
)  e.  RR )
459457, 458sseldd 3510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( V `  i
)  e.  CC )
460200, 459pncan3d 9945 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( ( V `  i
)  -  X ) )  =  ( V `
 i ) )
461456, 460eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  i
)  =  ( X  +  ( Q `  i ) ) )
46226a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `  i
)  -  X ) ) )
463 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  ( k  +  1 )  ->  ( V `  i )  =  ( V `  ( k  +  1 ) ) )
464463oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  ( k  +  1 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 ( k  +  1 ) )  -  X ) )
465464adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  =  ( k  +  1 ) )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 ( k  +  1 ) )  -  X ) )
46622adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
467466, 165ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( V `  ( k  +  1 ) )  e.  RR )
46813adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  X  e.  RR )
469467, 468resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( ( V `
 ( k  +  1 ) )  -  X )  e.  RR )
470462, 465, 165, 469fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  =  ( ( V `  (
k  +  1 ) )  -  X ) )
471116, 118, 470syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  =  ( ( V `  ( k  +  1 ) )  -  X ) )
472471oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( Q `  ( k  +  1 ) ) )  =  ( X  +  ( ( V `
 ( k  +  1 ) )  -  X ) ) )
473119, 467syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( V `  (
k  +  1 ) )  e.  RR )
474473recnd 9634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( V `  (
k  +  1 ) )  e.  CC )
475200, 474pncan3d 9945 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( X  +  ( ( V `  (
k  +  1 ) )  -  X ) )  =  ( V `
 ( k  +  1 ) ) )
476472, 475eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  (
k  +  1 ) )  =  ( X  +  ( Q `  ( k  +  1 ) ) ) )
477461, 476breq12d 4466 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( V `  i )  <  ( V `  ( k  +  1 ) )  <-> 
( X  +  ( Q `  i ) )  <  ( X  +  ( Q `  ( k  +  1 ) ) ) ) )
478455, 477mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  i
)  <  ( V `  ( k  +  1 ) ) )
479 nfv 1683 . . . . . . . . . . . . . . . . . 18  |-  F/ l ( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( k  +  1 ) ) )  ->  ( V `  i )  <_  ( V `  k )
)
480 eleq1 2539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  k  ->  (
l  e.  ( 0..^ M )  <->  k  e.  ( 0..^ M ) ) )
481480anbi2d 703 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) ) ) )
482 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l  =  k  ->  (
l  +  1 )  =  ( k  +  1 ) )
483482fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  k  ->  ( V `  ( l  +  1 ) )  =  ( V `  ( k  +  1 ) ) )
484483breq2d 4465 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  (
( V `  i
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  i )  <  ( V `  ( k  +  1 ) ) ) )
485481, 484anbi12d 710 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  (
( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( l  +  1 ) ) )  <->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
( V `  (
k  +  1 ) ) ) ) )
486 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  ( V `  l )  =  ( V `  k ) )
487486breq2d 4465 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  (
( V `  i
)  <_  ( V `  l )  <->  ( V `  i )  <_  ( V `  k )
) )
488485, 487imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  k  ->  (
( ( ( (
ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( l  +  1 ) ) )  ->  ( V `  i )  <_  ( V `  l )
)  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) )  /\  ( V `