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

Theorem fourierdlem50 37846
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 9785 . . . . . . . 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 37810 . . . . . . . . . . . 12  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
10 pire 23405 . . . . . . . . . . . . . . . 16  |-  pi  e.  RR
1110renegcli 9937 . . . . . . . . . . . . . . 15  |-  -u pi  e.  RR
1211a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  e.  RR )
13 fourierdlem50.xre . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  RR )
1412, 13readdcld 9672 . . . . . . . . . . . . 13  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
1510a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  pi  e.  RR )
1615, 13readdcld 9672 . . . . . . . . . . . . 13  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
1714, 16iccssred 37439 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
189, 17fssd 5753 . . . . . . . . . . 11  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
1918ffvelrnda 6035 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
2013adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
2119, 20resubcld 10049 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  (
( V `  i
)  -  X )  e.  RR )
22 fourierdlem50.q . . . . . . . . 9  |-  Q  =  ( i  e.  ( 0 ... M ) 
|->  ( ( V `  i )  -  X
) )
2321, 22fmptd 6059 . . . . . . . 8  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
2422a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) ) )
25 fveq2 5879 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( V `  i )  =  ( V ` 
0 ) )
2625oveq1d 6318 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
2726adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  i  = 
0 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
28 nnssnn0 10874 . . . . . . . . . . . . . . 15  |-  NN  C_  NN0
2928a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  C_  NN0 )
30 nn0uz 11195 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
3129, 30syl6sseq 3511 . . . . . . . . . . . . 13  |-  ( ph  ->  NN  C_  ( ZZ>= ` 
0 ) )
3231, 2sseldd 3466 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
33 eluzfz1 11808 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
3432, 33syl 17 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 ... M ) )
3518, 34ffvelrnd 6036 . . . . . . . . . . . 12  |-  ( ph  ->  ( V `  0
)  e.  RR )
3635, 13resubcld 10049 . . . . . . . . . . 11  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  e.  RR )
3724, 27, 34, 36fvmptd 5968 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  =  ( ( V `  0 )  -  X ) )
387fourierdlem2 37797 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
392, 38syl 17 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
408, 39mpbid 214 . . . . . . . . . . . . . 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 ) ) ) ) )
4140simprd 465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
4241simpld 461 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( V ` 
0 )  =  (
-u pi  +  X
)  /\  ( V `  M )  =  ( pi  +  X ) ) )
4342simpld 461 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  0
)  =  ( -u pi  +  X ) )
4443oveq1d 6318 . . . . . . . . . 10  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  =  ( (
-u pi  +  X
)  -  X ) )
4512recnd 9671 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  e.  CC )
4613recnd 9671 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  CC )
4745, 46pncand 9989 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
4837, 44, 473eqtrd 2468 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
4912rexrd 9692 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  e.  RR* )
5015rexrd 9692 . . . . . . . . . 10  |-  ( ph  ->  pi  e.  RR* )
51 fourierdlem50.ab . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
523leidd 10182 . . . . . . . . . . . 12  |-  ( ph  ->  A  <_  A )
533, 4, 3, 52, 6eliccd 37438 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( A [,] B ) )
5451, 53sseldd 3466 . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( -u pi [,] pi ) )
55 iccgelb 11693 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  A  e.  ( -u pi [,] pi ) )  ->  -u pi  <_  A )
5649, 50, 54, 55syl3anc 1265 . . . . . . . . 9  |-  ( ph  -> 
-u pi  <_  A
)
5748, 56eqbrtrd 4442 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <_  A )
584leidd 10182 . . . . . . . . . . . 12  |-  ( ph  ->  B  <_  B )
593, 4, 4, 6, 58eliccd 37438 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( A [,] B ) )
6051, 59sseldd 3466 . . . . . . . . . 10  |-  ( ph  ->  B  e.  ( -u pi [,] pi ) )
61 iccleub 11692 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  B  e.  ( -u pi [,] pi ) )  ->  B  <_  pi )
6249, 50, 60, 61syl3anc 1265 . . . . . . . . 9  |-  ( ph  ->  B  <_  pi )
63 fveq2 5879 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  ( V `  i )  =  ( V `  M ) )
6463oveq1d 6318 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
( V `  i
)  -  X )  =  ( ( V `
 M )  -  X ) )
6564adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  i  =  M )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 M )  -  X ) )
66 eluzfz2 11809 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
6732, 66syl 17 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 0 ... M ) )
6818, 67ffvelrnd 6036 . . . . . . . . . . . 12  |-  ( ph  ->  ( V `  M
)  e.  RR )
6968, 13resubcld 10049 . . . . . . . . . . 11  |-  ( ph  ->  ( ( V `  M )  -  X
)  e.  RR )
7024, 65, 67, 69fvmptd 5968 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  =  ( ( V `  M )  -  X ) )
7142simprd 465 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  M
)  =  ( pi  +  X ) )
7271oveq1d 6318 . . . . . . . . . 10  |-  ( ph  ->  ( ( V `  M )  -  X
)  =  ( ( pi  +  X )  -  X ) )
7315recnd 9671 . . . . . . . . . . 11  |-  ( ph  ->  pi  e.  CC )
7473, 46pncand 9989 . . . . . . . . . 10  |-  ( ph  ->  ( ( pi  +  X )  -  X
)  =  pi )
7570, 72, 743eqtrrd 2469 . . . . . . . . 9  |-  ( ph  ->  pi  =  ( Q `
 M ) )
7662, 75breqtrd 4446 . . . . . . . 8  |-  ( ph  ->  B  <_  ( Q `  M ) )
77 fourierdlem50.j . . . . . . . 8  |-  ( ph  ->  J  e.  ( 0..^ N ) )
78 fourierdlem50.t . . . . . . . 8  |-  T  =  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )
79 prfi 7850 . . . . . . . . . . . 12  |-  { A ,  B }  e.  Fin
8079a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  { A ,  B }  e.  Fin )
81 fzfid 12187 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
8222rnmptfi 37290 . . . . . . . . . . . . 13  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
8381, 82syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ran  Q  e.  Fin )
84 infi 7799 . . . . . . . . . . . 12  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
8583, 84syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
86 unfi 7842 . . . . . . . . . . 11  |-  ( ( { A ,  B }  e.  Fin  /\  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )  -> 
( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
8780, 85, 86syl2anc 666 . . . . . . . . . 10  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
8878, 87syl5eqel 2515 . . . . . . . . 9  |-  ( ph  ->  T  e.  Fin )
893, 4jca 535 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
90 prssg 4153 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
913, 4, 90syl2anc 666 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
9289, 91mpbid 214 . . . . . . . . . . 11  |-  ( ph  ->  { A ,  B }  C_  RR )
93 inss2 3684 . . . . . . . . . . . . 13  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A (,) B )
94 ioossre 11698 . . . . . . . . . . . . 13  |-  ( A (,) B )  C_  RR
9593, 94sstri 3474 . . . . . . . . . . . 12  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  RR
9695a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  RR )
9792, 96unssd 3643 . . . . . . . . . 10  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  RR )
9878, 97syl5eqss 3509 . . . . . . . . 9  |-  ( ph  ->  T  C_  RR )
99 fourierdlem50.s . . . . . . . . 9  |-  S  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... N
) ,  T ) )
100 fourierdlem50.n . . . . . . . . 9  |-  N  =  ( ( # `  T
)  -  1 )
10188, 98, 99, 100fourierdlem36 37832 . . . . . . . 8  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
102 eqid 2423 . . . . . . . 8  |-  sup ( { x  e.  (
0..^ M )  |  ( Q `  x
)  <_  ( S `  J ) } ,  RR ,  <  )  =  sup ( { x  e.  ( 0..^ M )  |  ( Q `  x )  <_  ( S `  J ) } ,  RR ,  <  )
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 37815 . . . . . . 7  |-  ( ph  ->  E. i  e.  ( 0..^ M ) ( ( S `  J
) (,) ( S `
 ( J  + 
1 ) ) ) 
C_  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
104 fourierdlem50.ch . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) )
105104biimpi 198 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) )
106 simp-4l 775 . . . . . . . . . . . . . . . . . 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 ) ) ) )  ->  ph )
107105, 106syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ph )
108 simplr 761 . . . . . . . . . . . . . . . . . 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 ) ) ) )  -> 
k  e.  ( 0..^ M ) )
109105, 108syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  k  e.  (
0..^ M ) )
110107, 109jca 535 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ph  /\  k  e.  ( 0..^ M ) ) )
111 simp-4r 776 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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 ) )
112105, 111syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  i  e.  (
0..^ M ) )
113 elfzofz 11937 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  ( 0..^ M )  ->  k  e.  ( 0 ... M
) )
114113ad2antlr 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 ) )
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  k  e.  (
0 ... M ) )
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  V : ( 0 ... M ) --> RR )
117116, 115ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( V `  k
)  e.  RR )
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  X  e.  RR )
119117, 118resubcld 10049 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( V `  k )  -  X
)  e.  RR )
120 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  k  ->  ( V `  i )  =  ( V `  k ) )
121120oveq1d 6318 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  k  ->  (
( V `  i
)  -  X )  =  ( ( V `
 k )  -  X ) )
122121, 22fvmptg 5960 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  ( 0 ... M )  /\  ( ( V `  k )  -  X
)  e.  RR )  ->  ( Q `  k )  =  ( ( V `  k
)  -  X ) )
123115, 119, 122syl2anc 666 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  k
)  =  ( ( V `  k )  -  X ) )
124123, 119eqeltrd 2511 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  k
)  e.  RR )
12523adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
126 fzofzp1 12009 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
127126adantl 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
128125, 127ffvelrnd 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
129107, 112, 128syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
130 isof1o 6229 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  ->  S : ( 0 ... N ) -1-1-onto-> T )
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  S : ( 0 ... N ) -1-1-onto-> T )
132 f1of 5829 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S : ( 0 ... N ) -1-1-onto-> T  ->  S :
( 0 ... N
) --> T )
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  S : ( 0 ... N ) --> T )
134 fzofzp1 12009 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
136133, 135ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  T )
13798, 136sseldd 3466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR )
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  ( J  +  1 ) )  e.  RR )
139 elfzofz 11937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  J  e.  ( 0 ... N ) )
141133, 140ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( S `  J
)  e.  T )
14298, 141sseldd 3466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( S `  J
)  e.  RR )
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( S `  J
)  e.  RR )
144105simprd 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )
145124rexrd 9692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  k
)  e.  RR* )
14623adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
147 fzofzp1 12009 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  ( 0..^ M )  ->  ( k  +  1 )  e.  ( 0 ... M
) )
148147adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( k  +  1 )  e.  ( 0 ... M ) )
149146, 148ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  e.  RR )
150149rexrd 9692 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  e.  RR* )
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  e.  RR* )
152143rexrd 9692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( S `  J
)  e.  RR* )
153138rexrd 9692 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( S `  ( J  +  1 ) )  e.  RR* )
154 elfzoelz 11922 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ZZ )
155154zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( J  e.  ( 0..^ N )  ->  J  e.  RR )
156155ltp1d 10539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( J  e.  ( 0..^ N )  ->  J  <  ( J  +  1 ) )
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  J  <  ( J  +  1 ) )
158 isoeq5 6227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) ) ) ) )
15978, 158ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  <-> 
S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) ) )
160101, 159sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) ) )
161 isorel 6230 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 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 ) ) ) )
162160, 140, 135, 161syl12anc 1263 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( J  <  ( J  +  1 )  <-> 
( S `  J
)  <  ( S `  ( J  +  1 ) ) ) )
163157, 162mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
165145, 151, 152, 153, 164ioossioobi 37455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( ( S `
 J ) (,) ( S `  ( J  +  1 ) ) )  C_  (
( Q `  k
) (,) ( Q `
 ( k  +  1 ) ) )  <-> 
( ( Q `  k )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) ) ) )
166144, 165mpbid 214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( Q `  k )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) ) )
167166simpld 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  k
)  <_  ( S `  J ) )
168124, 143, 138, 167, 164lelttrd 9795 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  k
)  <  ( S `  ( J  +  1 ) ) )
169 elfzofz 11937 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
170169ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0 ... M
) )
171170ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 ) )
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  i  e.  (
0 ... M ) )
173107, 172, 21syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( V `  i )  -  X
)  e.  RR )
17422fvmpt2 5971 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
175172, 173, 174syl2anc 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( Q `  i
)  =  ( ( V `  i )  -  X ) )
176175, 173eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  i
)  e.  RR )
177 simpllr 768 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )  -> 
( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
179176, 129, 143, 138, 164, 178fourierdlem10 37805 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( Q `  i )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) )
180179simprd 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
181124, 138, 129, 168, 180ltletrd 9797 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  k
)  <  ( Q `  ( i  +  1 ) ) )
182124, 129, 118, 181ltadd2dd 9796 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  k ) )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
183123oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  k ) )  =  ( X  +  ( ( V `
 k )  -  X ) ) )
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  X  e.  CC )
185117recnd 9671 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  k
)  e.  CC )
186184, 185pncan3d 9991 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  k
)  -  X ) )  =  ( V `
 k ) )
187183, 186eqtr2d 2465 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  k
)  =  ( X  +  ( Q `  k ) ) )
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( i  +  1 )  e.  ( 0 ... M ) )
18918adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
190189, 127ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
191107, 112, 190syl2anc 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR )
192191, 118resubcld 10049 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( V `  ( i  +  1 ) )  -  X
)  e.  RR )
193188, 192jca 535 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR ) )
194 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  (
k  e.  ( 0 ... M )  <->  ( i  +  1 )  e.  ( 0 ... M
) ) )
195 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( i  +  1 )  ->  ( V `  k )  =  ( V `  ( i  +  1 ) ) )
196195oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( i  +  1 )  ->  (
( V `  k
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
197196eleq1d 2492 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  (
( ( V `  k )  -  X
)  e.  RR  <->  ( ( V `  ( i  +  1 ) )  -  X )  e.  RR ) )
198194, 197anbi12d 716 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( i  +  1 )  ->  (
( k  e.  ( 0 ... M )  /\  ( ( V `
 k )  -  X )  e.  RR ) 
<->  ( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR ) ) )
199 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  ( Q `  k )  =  ( Q `  ( i  +  1 ) ) )
200199, 196eqeq12d 2445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( i  +  1 )  ->  (
( Q `  k
)  =  ( ( V `  k )  -  X )  <->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) ) )
201198, 200imbi12d 322 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) )
202201, 122vtoclg 3140 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  +  1 )  e.  ( 0 ... M )  ->  (
( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR )  ->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) ) )
203188, 193, 202sylc 63 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) )
204203oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
205191recnd 9671 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  CC )
206184, 205pncan3d 9991 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  (
i  +  1 ) )  -  X ) )  =  ( V `
 ( i  +  1 ) ) )
207204, 206eqtr2d 2465 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  (
i  +  1 ) )  =  ( X  +  ( Q `  ( i  +  1 ) ) ) )
208182, 187, 2073brtr4d 4452 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  k
)  <  ( V `  ( i  +  1 ) ) )
209 eleq1 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  (
l  e.  ( 0..^ M )  <->  i  e.  ( 0..^ M ) ) )
210209anbi2d 709 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) ) ) )
211 oveq1 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  (
l  +  1 )  =  ( i  +  1 ) )
212211fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  ( V `  ( l  +  1 ) )  =  ( V `  ( i  +  1 ) ) )
213212breq2d 4433 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( V `  k
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  k )  <  ( V `  ( i  +  1 ) ) ) )
214210, 213anbi12d 716 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) )
215 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  ( V `  l )  =  ( V `  i ) )
216215breq2d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  i  ->  (
( V `  k
)  <_  ( V `  l )  <->  ( V `  k )  <_  ( V `  i )
) )
217214, 216imbi12d 322 . . . . . . . . . . . . . . . . 17  |-  ( 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
) ) ) )
218 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  k  ->  (
h  e.  ( 0..^ M )  <->  k  e.  ( 0..^ M ) ) )
219218anbi2d 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  k  ->  (
( ph  /\  h  e.  ( 0..^ M ) )  <->  ( ph  /\  k  e.  ( 0..^ M ) ) ) )
220219anbi1d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  k  ->  (
( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) ) ) )
221 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  k  ->  ( V `  h )  =  ( V `  k ) )
222221breq1d 4431 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  k  ->  (
( V `  h
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  k )  <  ( V `  ( l  +  1 ) ) ) )
223220, 222anbi12d 716 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) ) )
224221breq1d 4431 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  k  ->  (
( V `  h
)  <_  ( V `  l )  <->  ( V `  k )  <_  ( V `  l )
) )
225223, 224imbi12d 322 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) ) )
226 elfzoelz 11922 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  e.  ( 0..^ M )  ->  h  e.  ZZ )
227226ad3antlr 736 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  e.  ZZ )
228 elfzoelz 11922 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  e.  ( 0..^ M )  ->  l  e.  ZZ )
229228ad2antlr 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
l  e.  ZZ )
230 simplr 761 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
23118adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
232 fzofzp1 12009 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  ( 0 ... M
) )
233232adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  ( l  +  1 )  e.  ( 0 ... M ) )
234231, 233ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
235234adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
236235adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
23718adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
238 elfzofz 11937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  e.  ( 0..^ M )  ->  h  e.  ( 0 ... M
) )
239238adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  h  e.  ( 0 ... M ) )
240237, 239ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  ( V `  h )  e.  RR )
241240ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  h )  e.  RR )
242228zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  l  e.  RR )
243 peano2re 9808 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  RR  ->  (
l  +  1 )  e.  RR )
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  RR )
245244ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( l  +  1 )  e.  RR )
246226zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  e.  ( 0..^ M )  ->  h  e.  RR )
247246ad3antlr 736 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  h  e.  RR )
248 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  h  <  ( l  +  1 ) )
249245, 247, 248nltled 9787 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( l  +  1 )  <_  h
)
250228peano2zd 11045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  ZZ )
251250ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( l  +  1 )  e.  ZZ )
252226ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ZZ )
253 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( l  +  1 )  <_  h )
254 eluz2 11167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  e.  ( ZZ>= `  (
l  +  1 ) )  <->  ( ( l  +  1 )  e.  ZZ  /\  h  e.  ZZ  /\  ( l  +  1 )  <_  h ) )
255251, 252, 253, 254syl3anbrc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ( ZZ>= `  ( l  +  1 ) ) )
256255adantlll 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ( ZZ>= `  ( l  +  1 ) ) )
257 simplll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ph )
258 0zd 10951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  0  e.  ZZ )
259 elfzoel2 11921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  e.  ( 0..^ M )  ->  M  e.  ZZ )
260259ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  M  e.  ZZ )
261 elfzelz 11802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  e.  ZZ )
262261adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ZZ )
263258, 260, 2623jca 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ ) )
264 0red 9646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  e.  RR )
265261zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  e.  RR )
266265adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  e.  RR )
267242adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  e.  RR )
268 elfzole1 11930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( l  e.  ( 0..^ M )  ->  0  <_  l )
269268adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <_  l )
270267, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  (
l  +  1 )  e.  RR )
271267ltp1d 10539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  <  ( l  +  1 ) )
272 elfzle1 11804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  (
l  +  1 )  <_  i )
273272adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  (
l  +  1 )  <_  i )
274267, 270, 266, 271, 273ltletrd 9797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  <  i )
275264, 267, 266, 269, 274lelttrd 9795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <  i )
276264, 266, 275ltled 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <_  i )
277276adantll 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  0  <_  i
)
278265adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  e.  RR )
279259zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  e.  ( 0..^ M )  ->  M  e.  RR )
280279adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  M  e.  RR )
281246adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  h  e.  RR )
282 elfzle2 11805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  <_  h )
283282adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <_  h )
284 elfzolt2 11931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( h  e.  ( 0..^ M )  ->  h  <  M )
285284adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  h  <  M )
286278, 281, 280, 283, 285lelttrd 9795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <  M )
287278, 280, 286ltled 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <_  M )
288287adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  <_  M
)
289263, 277, 288jca32 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 ) ) )
290 elfz2 11793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )  /\  (
0  <_  i  /\  i  <_  M ) ) )
291289, 290sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ( 0 ... M ) )
292291adantlll 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ( 0 ... M ) )
293257, 292, 19syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ( V `  i )  e.  RR )
294293adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  /\  i  e.  (
( l  +  1 ) ... h ) )  ->  ( V `  i )  e.  RR )
295 simplll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ph )
296 0zd 10951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  e.  ZZ )
297 elfzelz 11802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  e.  ZZ )
298297adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  ZZ )
299 0red 9646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  e.  RR )
300298zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  RR )
301242adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  e.  RR )
302268adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <_  l )
303301, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
l  +  1 )  e.  RR )
304301ltp1d 10539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  <  ( l  +  1 ) )
305 elfzle1 11804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  (
l  +  1 )  <_  i )
306305adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
l  +  1 )  <_  i )
307301, 303, 300, 304, 306ltletrd 9797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  <  i )
308299, 301, 300, 302, 307lelttrd 9795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <  i )
309299, 300, 308ltled 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <_  i )
310 eluz2 11167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  i  e.  ZZ  /\  0  <_ 
i ) )
311296, 298, 309, 310syl3anbrc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
312311adantll 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  e.  (
ZZ>= `  0 ) )
313 elfzoel2 11921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( l  e.  ( 0..^ M )  ->  M  e.  ZZ )
314313ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  M  e.  ZZ )
315297zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  e.  RR )
316315adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  RR )
317 peano2rem 9943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  e.  RR  ->  (
h  -  1 )  e.  RR )
318246, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  e.  RR )
319318adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
h  -  1 )  e.  RR )
320279adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  M  e.  RR )
321 elfzle2 11805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  <_  ( h  -  1 ) )
322321adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <_  ( h  -  1 ) )
323246ltm1d 10541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  < 
h )
324318, 246, 279, 323, 284lttrd 9798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  < 
M )
325324adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
h  -  1 )  <  M )
326316, 319, 320, 322, 325lelttrd 9795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <  M )
327326adantll 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <  M )
328327adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  <  M
)
329 elfzo2 11925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ M )  <->  ( i  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  i  <  M ) )
330312, 314, 328, 329syl3anbrc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  e.  ( 0..^ M ) )
331169, 19sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
33241simprd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
333332r19.21bi 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
334331, 190, 333ltled 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
335295, 330, 334syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
336335adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  /\  i  e.  (
( l  +  1 ) ... ( h  -  1 ) ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
337256, 294, 336monoord 12244 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( V `  (
l  +  1 ) )  <_  ( V `  h ) )
338249, 337syldan 473 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  ( l  +  1 ) )  <_  ( V `  h )
)
339236, 241, 338lensymd 9788 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
340339adantlr 720 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
341230, 340condan 802 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  <  ( l  +  1 ) )
342 zleltp1 10989 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h  e.  ZZ  /\  l  e.  ZZ )  ->  ( h  <_  l  <->  h  <  ( l  +  1 ) ) )
343227, 229, 342syl2anc 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( h  <_  l  <->  h  <  ( l  +  1 ) ) )
344341, 343mpbird 236 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  <_  l )
345 eluz2 11167 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  e.  ( ZZ>= `  h
)  <->  ( h  e.  ZZ  /\  l  e.  ZZ  /\  h  <_ 
l ) )
346227, 229, 344, 345syl3anbrc 1190 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
l  e.  ( ZZ>= `  h ) )
34718ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  ->  V : ( 0 ... M ) --> RR )
348 0zd 10951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
0  e.  ZZ )
349259ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  ->  M  e.  ZZ )
350 elfzelz 11802 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( h ... l )  ->  i  e.  ZZ )
351350adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ZZ )
352348, 349, 3513jca 1186 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )
)
353 0red 9646 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  e.  RR )
354246adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  h  e.  RR )
355350zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( h ... l )  ->  i  e.  RR )
356355adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  e.  RR )
357 elfzole1 11930 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  e.  ( 0..^ M )  ->  0  <_  h )
358357adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  <_  h )
359 elfzle1 11804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( h ... l )  ->  h  <_  i )
360359adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  h  <_  i )
361353, 354, 356, 358, 360letrd 9794 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  <_  i )
362361adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
0  <_  i )
363355adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  e.  RR )
364313zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( l  e.  ( 0..^ M )  ->  M  e.  RR )
365364adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  M  e.  RR )
366242adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  l  e.  RR )
367 elfzle2 11805 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( h ... l )  ->  i  <_  l )
368367adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <_  l )
369 elfzolt2 11931 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  l  <  M )
370369adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  l  <  M )
371363, 366, 365, 368, 370lelttrd 9795 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <  M )
372363, 365, 371ltled 9785 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <_  M )
373372adantll 719 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  <_  M )
374352, 362, 373jca32 538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) )
375374, 290sylibr 216 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ( 0 ... M ) )
376375adantlll 723 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ( 0 ... M ) )
377347, 376ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( V `  i
)  e.  RR )
378377adantlr 720 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... l ) )  -> 
( V `  i
)  e.  RR )
379 simp-4l 775 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  ->  ph )
380 0zd 10951 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  e.  ZZ )
381 elfzelz 11802 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  e.  ZZ )
382381adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ZZ )
383 0red 9646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  e.  RR )
384246adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  h  e.  RR )
385382zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  RR )
386357adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  <_  h )
387 elfzle1 11804 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  h  <_  i )
388387adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  h  <_  i )
389383, 384, 385, 386, 388letrd 9794 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  <_  i )
390380, 382, 389, 310syl3anbrc 1190 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
391390adantll 719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
392391adant423 37234 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  e.  ( ZZ>= ` 
0 ) )
393313ad3antlr 736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  ->  M  e.  ZZ )
394381zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  e.  RR )
395394adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  RR )
396242adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  e.  RR )
397364adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  M  e.  RR )
398 elfzle2 11805 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  <_  ( l  -  1 ) )
399398adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <_  ( l  -  1 ) )
400 zltlem1 10991 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  ZZ  /\  l  e.  ZZ )  ->  ( i  <  l  <->  i  <_  ( l  - 
1 ) ) )
401381, 228, 400syl2anr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  (
i  <  l  <->  i  <_  ( l  -  1 ) ) )
402399, 401mpbird 236 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  l )
403369adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  <  M )
404395, 396, 397, 402, 403lttrd 9798 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  M )
405404adantll 719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  <  M )
406405adantlr 720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  <  M )
407392, 393, 406, 329syl3anbrc 1190 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  e.  ( 0..^ M ) )
408379, 407, 334syl2anc 666 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
( V `  i
)  <_  ( V `  ( i  +  1 ) ) )
409346, 378, 408monoord 12244 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  h
)  <_  ( V `  l ) )
410225, 409chvarv 2069 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  k
)  <_  ( V `  l ) )
411217, 410chvarv 2069 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( i  +  1 ) ) )  -> 
( V `  k
)  <_  ( V `  i ) )
412110, 112, 208, 411syl21anc 1264 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  k
)  <_  ( V `  i ) )
413107, 112jca 535 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ph  /\  i  e.  ( 0..^ M ) ) )
414110, 149syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  e.  RR )
415179simpld 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  i
)  <_  ( S `  J ) )
416176, 143, 138, 415, 164lelttrd 9795 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  i
)  <  ( S `  ( J  +  1 ) ) )
417166simprd 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) )
418176, 138, 414, 416, 417ltletrd 9797 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  <  ( Q `  ( k  +  1 ) ) )
419176, 414, 118, 418ltadd2dd 9796 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  i ) )  <  ( X  +  ( Q `  ( k  +  1 ) ) ) )
420175oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  i ) )  =  ( X  +  ( ( V `
 i )  -  X ) ) )
421107, 172, 19syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( V `  i
)  e.  RR )
422421recnd 9671 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  i
)  e.  CC )
423184, 422pncan3d 9991 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  i
)  -  X ) )  =  ( V `
 i ) )
424420, 423eqtr2d 2465 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  i
)  =  ( X  +  ( Q `  i ) ) )
42522a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `  i
)  -  X ) ) )
426 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  ( k  +  1 )  ->  ( V `  i )  =  ( V `  ( k  +  1 ) ) )
427426oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  ( k  +  1 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 ( k  +  1 ) )  -  X ) )
428427adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  =  ( k  +  1 ) )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 ( k  +  1 ) )  -  X ) )
42918adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
430429, 148ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( V `  ( k  +  1 ) )  e.  RR )
43113adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  X  e.  RR )
432430, 431resubcld 10049 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( ( V `
 ( k  +  1 ) )  -  X )  e.  RR )
433425, 428, 148, 432fvmptd 5968 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  =  ( ( V `  (
k  +  1 ) )  -  X ) )
434107, 109, 433syl2anc 666 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  =  ( ( V `  ( k  +  1 ) )  -  X ) )
435434oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  ( k  +  1 ) ) )  =  ( X  +  ( ( V `
 ( k  +  1 ) )  -  X ) ) )
436110, 430syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( V `  (
k  +  1 ) )  e.  RR )
437436recnd 9671 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  (
k  +  1 ) )  e.  CC )
438184, 437pncan3d 9991 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  (
k  +  1 ) )  -  X ) )  =  ( V `
 ( k  +  1 ) ) )
439435, 438eqtr2d 2465 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  (
k  +  1 ) )  =  ( X  +  ( Q `  ( k  +  1 ) ) ) )
440419, 424, 4393brtr4d 4452 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  <  ( V `  ( k  +  1 ) ) )
441 eleq1 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  (
l  e.  ( 0..^ M )  <->  k  e.  ( 0..^ M ) ) )
442441anbi2d 709 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) ) ) )
443 oveq1 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  k  ->  (
l  +  1 )  =  ( k  +  1 ) )
444443fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  ( V `  ( l  +  1 ) )  =  ( V `  ( k  +  1 ) ) )
445444breq2d 4433 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  (
( V `  i
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  i )  <  ( V `  ( k  +  1 ) ) ) )
446442, 445anbi12d 716 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) )
447 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  ( V `  l )  =  ( V `  k ) )
448447breq2d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  k  ->  (
( V `  i
)  <_  ( V `  l )  <->  ( V `  i )  <_  ( V `  k )
) )
449446, 448imbi12d 322 . . . . . . . . . . . . . . . . 17  |-  ( 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 `
 i )  < 
( V `  (
k  +  1 ) ) )  ->  ( V `  i )  <_  ( V `  k
) ) ) )
450 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  i  ->  (
h  e.  ( 0..^ M )  <->  i  e.  ( 0..^ M ) ) )
451450anbi2d 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  i  ->  (
( ph  /\  h  e.  ( 0..^ M ) )  <->  ( ph  /\  i  e.  ( 0..^ M ) ) ) )
452451anbi1d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  i  ->  (
( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) ) ) )
453 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  i  ->  ( V `  h )  =  ( V `  i ) )
454453breq1d 4431 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  i  ->  (
( V `  h
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  i )  <  ( V `  ( l  +  1 ) ) ) )
455452, 454anbi12d 716 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  i  ->  (
( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  <->  ( (
( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
( V `  (
l  +  1 ) ) ) ) )
456453breq1d 4431 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  i  ->  (
( V `  h
)  <_  ( V `  l )  <->  ( V `  i )  <_  ( V `  l )
) )
457455, 456imbi12d 322 . . . . . . . . . . . . . . . . . 18  |-  ( h  =  i  ->  (
( ( ( (
ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  ( V `  h )  <_  ( V `  l )
)  <->  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `
 i )  < 
( V `  (
l  +  1 ) ) )  ->  ( V `  i )  <_  ( V `  l
) ) ) )
458457, 409chvarv 2069 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  i
)  <_  ( V `  l ) )
459449, 458chvarv 2069 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( k  +  1 ) ) )  -> 
( V `  i
)  <_  ( V `  k ) )
460413, 109, 440, 459syl21anc 1264 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  i
)  <_  ( V `  k ) )
461117, 421letri3d 9779 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( V `  k )  =  ( V `  i )  <-> 
( ( V `  k )  <_  ( V `  i )  /\  ( V `  i
)  <_  ( V `  k ) ) ) )
462412, 460, 461mpbir2and 931 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( V `  k
)  =  ( V `
 i ) )
4637, 2, 8fourierdlem34 37830 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  V : ( 0 ... M ) -1-1-> RR )
464107, 463syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  V : ( 0 ... M ) -1-1-> RR )
465 f1fveq 6176 . . . . . . . . . . . . . . 15  |-  ( ( V : ( 0 ... M ) -1-1-> RR  /\  ( k  e.  ( 0 ... M )  /\  i  e.  ( 0 ... M ) ) )  ->  (
( V `  k
)  =  ( V `
 i )  <->  k  =  i ) )
466464, 115, 172, 465syl12anc 1263 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( V `  k )  =  ( V `  i )  <-> 
k  =  i ) )
467462, 466mpbid 214 . . . . . . . . . . . . 13  |-  ( ch 
->  k  =  i
)
468104, 467sylbir 217 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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  =  i )
469468ex 436 . . . . . . . . . . 11  |-  ( ( ( ( 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  =  i ) )
470 simpl 459 . . . . . . . . . . . . . 14  |-  ( ( ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  /\  k  =  i )  -> 
( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
471 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  ( Q `  k )  =  ( Q `  i ) )
472 oveq1 6310 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
473472fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  ( Q `  ( k  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
474471, 473oveq12d 6321 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  (
( Q `  k
) (,) ( Q `
 ( k  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
475474eqcomd 2431 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 k ) (,) ( Q `  (
k  +  1 ) ) ) )
476475adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  /\  k  =  i )  -> 
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  =  ( ( Q `  k ) (,) ( Q `  ( k  +  1 ) ) ) )
477470, 476sseqtrd 3501 . . . . . . . . . . . . 13  |-  ( ( ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) )  /\  k  =  i )  -> 
( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )
478477ex 436 . . . . . . . . . . . 12  |-  ( ( ( S `  J
) (,) ( S `
 ( J  + 
1 ) ) ) 
C_  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  (
k  =  i  -> 
( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) ) )
479478ad2antlr 732 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )  /\  k  e.  ( 0..^ M ) )  -> 
( k  =  i  ->  ( ( S `
 J ) (,) ( S `  ( J  +  1 ) ) )  C_  (
( Q `  k
) (,) ( Q `
 ( k  +  1 ) ) ) ) )
480469, 479impbid 194 . . . . . . . . . 10  |-  ( ( ( ( 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  =  i ) )
481480ralrimiva 2840 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )