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

Theorem fourierdlem50 32142
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 9750 . . . . . . . 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 32107 . . . . . . . . . . . 12  |-  ( ph  ->  V : ( 0 ... M ) --> ( ( -u pi  +  X ) [,] (
pi  +  X ) ) )
10 pire 22977 . . . . . . . . . . . . . . . 16  |-  pi  e.  RR
1110renegcli 9899 . . . . . . . . . . . . . . 15  |-  -u pi  e.  RR
1211a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u pi  e.  RR )
13 fourierdlem50.xre . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  RR )
1412, 13readdcld 9640 . . . . . . . . . . . . 13  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
1510a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  pi  e.  RR )
1615, 13readdcld 9640 . . . . . . . . . . . . 13  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
1714, 16iccssred 31742 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  C_  RR )
189, 17fssd 5746 . . . . . . . . . . 11  |-  ( ph  ->  V : ( 0 ... M ) --> RR )
1918ffvelrnda 6032 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  ( V `  i )  e.  RR )
2013adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... M
) )  ->  X  e.  RR )
2119, 20resubcld 10008 . . . . . . . . 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 6056 . . . . . . . 8  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
2422a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  Q  =  ( i  e.  ( 0 ... M )  |->  ( ( V `  i )  -  X ) ) )
25 fveq2 5872 . . . . . . . . . . . . 13  |-  ( i  =  0  ->  ( V `  i )  =  ( V ` 
0 ) )
2625oveq1d 6311 . . . . . . . . . . . 12  |-  ( i  =  0  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
2726adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  i  = 
0 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 0 )  -  X ) )
28 nnssnn0 10819 . . . . . . . . . . . . . . 15  |-  NN  C_  NN0
2928a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  NN  C_  NN0 )
30 nn0uz 11140 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
3129, 30syl6sseq 3545 . . . . . . . . . . . . 13  |-  ( ph  ->  NN  C_  ( ZZ>= ` 
0 ) )
3231, 2sseldd 3500 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
33 eluzfz1 11718 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
3432, 33syl 16 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 ... M ) )
3518, 34ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( V `  0
)  e.  RR )
3635, 13resubcld 10008 . . . . . . . . . . 11  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  e.  RR )
3724, 27, 34, 36fvmptd 5961 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  0
)  =  ( ( V `  0 )  -  X ) )
387fourierdlem2 32094 . . . . . . . . . . . . . . . 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 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 ) ) ) ) ) )
408, 39mpbid 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 ) ) ) ) )
4140simprd 463 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( V `
 0 )  =  ( -u pi  +  X )  /\  ( V `  M )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ M ) ( V `
 i )  < 
( V `  (
i  +  1 ) ) ) )
4241simpld 459 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( V ` 
0 )  =  (
-u pi  +  X
)  /\  ( V `  M )  =  ( pi  +  X ) ) )
4342simpld 459 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  0
)  =  ( -u pi  +  X ) )
4443oveq1d 6311 . . . . . . . . . 10  |-  ( ph  ->  ( ( V ` 
0 )  -  X
)  =  ( (
-u pi  +  X
)  -  X ) )
4512recnd 9639 . . . . . . . . . . 11  |-  ( ph  -> 
-u pi  e.  CC )
4613recnd 9639 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  CC )
4745, 46pncand 9951 . . . . . . . . . 10  |-  ( ph  ->  ( ( -u pi  +  X )  -  X
)  =  -u pi )
4837, 44, 473eqtrd 2502 . . . . . . . . 9  |-  ( ph  ->  ( Q `  0
)  =  -u pi )
4912rexrd 9660 . . . . . . . . . 10  |-  ( ph  -> 
-u pi  e.  RR* )
5015rexrd 9660 . . . . . . . . . 10  |-  ( ph  ->  pi  e.  RR* )
51 fourierdlem50.ab . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  ( -u pi [,] pi ) )
523leidd 10140 . . . . . . . . . . . 12  |-  ( ph  ->  A  <_  A )
533, 4, 3, 52, 6eliccd 31741 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  ( A [,] B ) )
5451, 53sseldd 3500 . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( -u pi [,] pi ) )
55 iccgelb 11606 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  A  e.  ( -u pi [,] pi ) )  ->  -u pi  <_  A )
5649, 50, 54, 55syl3anc 1228 . . . . . . . . 9  |-  ( ph  -> 
-u pi  <_  A
)
5748, 56eqbrtrd 4476 . . . . . . . 8  |-  ( ph  ->  ( Q `  0
)  <_  A )
584leidd 10140 . . . . . . . . . . . 12  |-  ( ph  ->  B  <_  B )
593, 4, 4, 6, 58eliccd 31741 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( A [,] B ) )
6051, 59sseldd 3500 . . . . . . . . . 10  |-  ( ph  ->  B  e.  ( -u pi [,] pi ) )
61 iccleub 11605 . . . . . . . . . 10  |-  ( (
-u pi  e.  RR*  /\  pi  e.  RR*  /\  B  e.  ( -u pi [,] pi ) )  ->  B  <_  pi )
6249, 50, 60, 61syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  B  <_  pi )
63 fveq2 5872 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  ( V `  i )  =  ( V `  M ) )
6463oveq1d 6311 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
( V `  i
)  -  X )  =  ( ( V `
 M )  -  X ) )
6564adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  i  =  M )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 M )  -  X ) )
66 eluzfz2 11719 . . . . . . . . . . . 12  |-  ( M  e.  ( ZZ>= `  0
)  ->  M  e.  ( 0 ... M
) )
6732, 66syl 16 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 0 ... M ) )
6818, 67ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( ph  ->  ( V `  M
)  e.  RR )
6968, 13resubcld 10008 . . . . . . . . . . 11  |-  ( ph  ->  ( ( V `  M )  -  X
)  e.  RR )
7024, 65, 67, 69fvmptd 5961 . . . . . . . . . 10  |-  ( ph  ->  ( Q `  M
)  =  ( ( V `  M )  -  X ) )
7142simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  ( V `  M
)  =  ( pi  +  X ) )
7271oveq1d 6311 . . . . . . . . . 10  |-  ( ph  ->  ( ( V `  M )  -  X
)  =  ( ( pi  +  X )  -  X ) )
7315recnd 9639 . . . . . . . . . . 11  |-  ( ph  ->  pi  e.  CC )
7473, 46pncand 9951 . . . . . . . . . 10  |-  ( ph  ->  ( ( pi  +  X )  -  X
)  =  pi )
7570, 72, 743eqtrrd 2503 . . . . . . . . 9  |-  ( ph  ->  pi  =  ( Q `
 M ) )
7662, 75breqtrd 4480 . . . . . . . 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 7813 . . . . . . . . . . . 12  |-  { A ,  B }  e.  Fin
8079a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  { A ,  B }  e.  Fin )
81 fzfid 12086 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
8222rnmptfi 31650 . . . . . . . . . . . . 13  |-  ( ( 0 ... M )  e.  Fin  ->  ran  Q  e.  Fin )
8381, 82syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ran  Q  e.  Fin )
84 infi 7762 . . . . . . . . . . . 12  |-  ( ran 
Q  e.  Fin  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
8583, 84syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  e.  Fin )
86 unfi 7805 . . . . . . . . . . 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 661 . . . . . . . . . 10  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  e.  Fin )
8878, 87syl5eqel 2549 . . . . . . . . 9  |-  ( ph  ->  T  e.  Fin )
893, 4jca 532 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
90 prssg 4187 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
913, 4, 90syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A  e.  RR  /\  B  e.  RR )  <->  { A ,  B }  C_  RR ) )
9289, 91mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  { A ,  B }  C_  RR )
93 inss2 3715 . . . . . . . . . . . . 13  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  ( A (,) B )
94 ioossre 11611 . . . . . . . . . . . . 13  |-  ( A (,) B )  C_  RR
9593, 94sstri 3508 . . . . . . . . . . . 12  |-  ( ran 
Q  i^i  ( A (,) B ) )  C_  RR
9695a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( ran  Q  i^i  ( A (,) B ) )  C_  RR )
9792, 96unssd 3676 . . . . . . . . . 10  |-  ( ph  ->  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) )  C_  RR )
9878, 97syl5eqss 3543 . . . . . . . . 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 32128 . . . . . . . 8  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  T ) )
102 eqid 2457 . . . . . . . 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 32112 . . . . . . 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 194 . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ph )
108 simplr 755 . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  k  e.  (
0..^ M ) )
110107, 109jca 532 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ph  /\  k  e.  ( 0..^ M ) ) )
111 simp-4r 768 . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  i  e.  (
0..^ M ) )
113 elfzofz 11841 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  ( 0..^ M )  ->  k  e.  ( 0 ... M
) )
114113ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  k  e.  (
0 ... M ) )
116107, 18syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  V : ( 0 ... M ) --> RR )
117116, 115ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( V `  k
)  e.  RR )
118107, 13syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  X  e.  RR )
119117, 118resubcld 10008 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( V `  k )  -  X
)  e.  RR )
120 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  k  ->  ( V `  i )  =  ( V `  k ) )
121120oveq1d 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  k  ->  (
( V `  i
)  -  X )  =  ( ( V `
 k )  -  X ) )
122121, 22fvmptg 5954 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  ( 0 ... M )  /\  ( ( V `  k )  -  X
)  e.  RR )  ->  ( Q `  k )  =  ( ( V `  k
)  -  X ) )
123115, 119, 122syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  k
)  =  ( ( V `  k )  -  X ) )
124123, 119eqeltrd 2545 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  k
)  e.  RR )
12523adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
126 fzofzp1 11912 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
127126adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
128125, 127ffvelrnd 6033 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
129107, 112, 128syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  e.  RR )
130 isof1o 6222 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( S 
Isom  <  ,  <  (
( 0 ... N
) ,  T )  ->  S : ( 0 ... N ) -1-1-onto-> T )
131101, 130syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  S : ( 0 ... N ) -1-1-onto-> T )
132 f1of 5822 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S : ( 0 ... N ) -1-1-onto-> T  ->  S :
( 0 ... N
) --> T )
133131, 132syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  S : ( 0 ... N ) --> T )
134 fzofzp1 11912 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( J  e.  ( 0..^ N )  ->  ( J  +  1 )  e.  ( 0 ... N
) )
13577, 134syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( J  +  1 )  e.  ( 0 ... N ) )
136133, 135ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  T )
13798, 136sseldd 3500 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( S `  ( J  +  1 ) )  e.  RR )
138107, 137syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  ( J  +  1 ) )  e.  RR )
139 elfzofz 11841 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ( 0 ... N
) )
14077, 139syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  J  e.  ( 0 ... N ) )
141133, 140ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( S `  J
)  e.  T )
14298, 141sseldd 3500 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( S `  J
)  e.  RR )
143107, 142syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( S `  J
)  e.  RR )
144105simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  k ) (,) ( Q `  (
k  +  1 ) ) ) )
145124rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  k
)  e.  RR* )
14623adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
147 fzofzp1 11912 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  ( 0..^ M )  ->  ( k  +  1 )  e.  ( 0 ... M
) )
148147adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( k  +  1 )  e.  ( 0 ... M ) )
149146, 148ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  e.  RR )
150149rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  e.  RR* )
151110, 150syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  e.  RR* )
152143rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( S `  J
)  e.  RR* )
153138rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( S `  ( J  +  1 ) )  e.  RR* )
154 elfzoelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( J  e.  ( 0..^ N )  ->  J  e.  ZZ )
155154zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( J  e.  ( 0..^ N )  ->  J  e.  RR )
156155ltp1d 10496 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( J  e.  ( 0..^ N )  ->  J  <  ( J  +  1 ) )
15777, 156syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  J  <  ( J  +  1 ) )
158 isoeq5 6220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  S  Isom  <  ,  <  ( ( 0 ... N
) ,  ( { A ,  B }  u.  ( ran  Q  i^i  ( A (,) B ) ) ) ) )
161 isorel 6223 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( J  <  ( J  +  1 )  <-> 
( S `  J
)  <  ( S `  ( J  +  1 ) ) ) )
163157, 162mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
164107, 163syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( S `  J
)  <  ( S `  ( J  +  1 ) ) )
165145, 151, 152, 153, 164ioossioobi 31760 . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( Q `  k )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) ) )
167166simpld 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  k
)  <_  ( S `  J ) )
168124, 143, 138, 167, 164lelttrd 9757 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  k
)  <  ( S `  ( J  +  1 ) ) )
169 elfzofz 11841 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
170169ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  ( ( S `  J ) (,) ( S `  ( J  +  1
) ) )  C_  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  i  e.  ( 0 ... M
) )
171170ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  i  e.  (
0 ... M ) )
173107, 172, 21syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( ( V `  i )  -  X
)  e.  RR )
17422fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0 ... M )  /\  ( ( V `  i )  -  X
)  e.  RR )  ->  ( Q `  i )  =  ( ( V `  i
)  -  X ) )
175172, 173, 174syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( Q `  i
)  =  ( ( V `  i )  -  X ) )
176175, 173eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Q `  i
)  e.  RR )
177 simpllr 760 . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( S `  J ) (,) ( S `  ( J  +  1 ) ) )  C_  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) )
179176, 129, 143, 138, 164, 178fourierdlem10 32102 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( Q `  i )  <_  ( S `  J )  /\  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) ) )
180179simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  ( J  +  1 ) )  <_  ( Q `  ( i  +  1 ) ) )
181124, 138, 129, 168, 180ltletrd 9759 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  k
)  <  ( Q `  ( i  +  1 ) ) )
182124, 129, 118, 181ltadd2dd 9758 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  k ) )  <  ( X  +  ( Q `  ( i  +  1 ) ) ) )
183123oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  k ) )  =  ( X  +  ( ( V `
 k )  -  X ) ) )
184107, 46syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  X  e.  CC )
185117recnd 9639 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  k
)  e.  CC )
186184, 185pncan3d 9953 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  k
)  -  X ) )  =  ( V `
 k ) )
187183, 186eqtr2d 2499 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  k
)  =  ( X  +  ( Q `  k ) ) )
188112, 126syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( i  +  1 )  e.  ( 0 ... M ) )
18918adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
190189, 127ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  ( i  +  1 ) )  e.  RR )
191107, 112, 190syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  RR )
192191, 118resubcld 10008 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( ( V `  ( i  +  1 ) )  -  X
)  e.  RR )
193188, 192jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( i  +  1 )  e.  ( 0 ... M )  /\  ( ( V `
 ( i  +  1 ) )  -  X )  e.  RR ) )
194 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  (
k  e.  ( 0 ... M )  <->  ( i  +  1 )  e.  ( 0 ... M
) ) )
195 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( i  +  1 )  ->  ( V `  k )  =  ( V `  ( i  +  1 ) ) )
196195oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( i  +  1 )  ->  (
( V `  k
)  -  X )  =  ( ( V `
 ( i  +  1 ) )  -  X ) )
197196eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  (
( ( V `  k )  -  X
)  e.  RR  <->  ( ( V `  ( i  +  1 ) )  -  X )  e.  RR ) )
198194, 197anbi12d 710 . . . . . . . . . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( i  +  1 )  ->  ( Q `  k )  =  ( Q `  ( i  +  1 ) ) )
200199, 196eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( i  +  1 )  ->  (
( Q `  k
)  =  ( ( V `  k )  -  X )  <->  ( Q `  ( i  +  1 ) )  =  ( ( V `  (
i  +  1 ) )  -  X ) ) )
201198, 200imbi12d 320 . . . . . . . . . . . . . . . . . . . . 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 3167 . . . . . . . . . . . . . . . . . . . 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 60 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
i  +  1 ) )  =  ( ( V `  ( i  +  1 ) )  -  X ) )
204203oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  ( i  +  1 ) ) )  =  ( X  +  ( ( V `
 ( i  +  1 ) )  -  X ) ) )
205191recnd 9639 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  (
i  +  1 ) )  e.  CC )
206184, 205pncan3d 9953 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  (
i  +  1 ) )  -  X ) )  =  ( V `
 ( i  +  1 ) ) )
207204, 206eqtr2d 2499 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  (
i  +  1 ) )  =  ( X  +  ( Q `  ( i  +  1 ) ) ) )
208182, 187, 2073brtr4d 4486 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  k
)  <  ( V `  ( i  +  1 ) ) )
209 eleq1 2529 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  (
l  e.  ( 0..^ M )  <->  i  e.  ( 0..^ M ) ) )
210209anbi2d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) ) ) )
211 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  i  ->  (
l  +  1 )  =  ( i  +  1 ) )
212211fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  i  ->  ( V `  ( l  +  1 ) )  =  ( V `  ( i  +  1 ) ) )
213212breq2d 4468 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  (
( V `  k
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  k )  <  ( V `  ( i  +  1 ) ) ) )
214210, 213anbi12d 710 . . . . . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  i  ->  ( V `  l )  =  ( V `  i ) )
216215breq2d 4468 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  i  ->  (
( V `  k
)  <_  ( V `  l )  <->  ( V `  k )  <_  ( V `  i )
) )
217214, 216imbi12d 320 . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  k  ->  (
h  e.  ( 0..^ M )  <->  k  e.  ( 0..^ M ) ) )
219218anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  k  ->  (
( ph  /\  h  e.  ( 0..^ M ) )  <->  ( ph  /\  k  e.  ( 0..^ M ) ) ) )
220219anbi1d 704 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  k  ->  (
( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) ) ) )
221 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  k  ->  ( V `  h )  =  ( V `  k ) )
222221breq1d 4466 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  k  ->  (
( V `  h
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  k )  <  ( V `  ( l  +  1 ) ) ) )
223220, 222anbi12d 710 . . . . . . . . . . . . . . . . . . 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 4466 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  k  ->  (
( V `  h
)  <_  ( V `  l )  <->  ( V `  k )  <_  ( V `  l )
) )
225223, 224imbi12d 320 . . . . . . . . . . . . . . . . . 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 11826 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  e.  ( 0..^ M )  ->  h  e.  ZZ )
227226ad3antlr 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  e.  ZZ )
228 elfzoelz 11826 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  e.  ( 0..^ M )  ->  l  e.  ZZ )
229228ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
l  e.  ZZ )
230 simplr 755 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
23118adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
232 fzofzp1 11912 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  ( 0 ... M
) )
233232adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  ( l  +  1 )  e.  ( 0 ... M ) )
234231, 233ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  l  e.  ( 0..^ M ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
235234adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
236235adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  ( l  +  1 ) )  e.  RR )
23718adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
238 elfzofz 11841 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  e.  ( 0..^ M )  ->  h  e.  ( 0 ... M
) )
239238adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  h  e.  ( 0 ... M ) )
240237, 239ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  h  e.  ( 0..^ M ) )  ->  ( V `  h )  e.  RR )
241240ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  h )  e.  RR )
242228zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  l  e.  RR )
243 peano2re 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  RR  ->  (
l  +  1 )  e.  RR )
244242, 243syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  RR )
245244ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( l  +  1 )  e.  RR )
246226zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  e.  ( 0..^ M )  ->  h  e.  RR )
247246ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  h  e.  RR )
248 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  h  <  ( l  +  1 ) )
249245, 247, 248nltled 31680 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( l  +  1 )  <_  h
)
250228peano2zd 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( l  e.  ( 0..^ M )  ->  ( l  +  1 )  e.  ZZ )
251250ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( l  +  1 )  e.  ZZ )
252226ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ZZ )
253 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( l  +  1 )  <_  h )
254 eluz2 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  e.  ( ZZ>= `  (
l  +  1 ) )  <->  ( ( l  +  1 )  e.  ZZ  /\  h  e.  ZZ  /\  ( l  +  1 )  <_  h ) )
255251, 252, 253, 254syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ( ZZ>= `  ( l  +  1 ) ) )
256255adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  h  e.  ( ZZ>= `  ( l  +  1 ) ) )
257 simplll 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ph )
258 0zd 10897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  0  e.  ZZ )
259 elfzoel2 11825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  e.  ( 0..^ M )  ->  M  e.  ZZ )
260259ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  M  e.  ZZ )
261 elfzelz 11713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  e.  ZZ )
262261adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ZZ )
263258, 260, 2623jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  e.  RR )
265261zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  e.  RR )
266265adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  e.  RR )
267242adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  e.  RR )
268 elfzole1 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( l  e.  ( 0..^ M )  ->  0  <_  l )
269268adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <_  l )
270267, 243syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  (
l  +  1 )  e.  RR )
271267ltp1d 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  <  ( l  +  1 ) )
272 elfzle1 11714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  (
l  +  1 )  <_  i )
273272adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  (
l  +  1 )  <_  i )
274267, 270, 266, 271, 273ltletrd 9759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  l  <  i )
275264, 267, 266, 269, 274lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <  i )
276264, 266, 275ltled 9750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  0  <_  i )
277276adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  0  <_  i
)
278265adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  e.  RR )
279259zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  e.  ( 0..^ M )  ->  M  e.  RR )
280279adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  M  e.  RR )
281246adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  h  e.  RR )
282 elfzle2 11715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  ( ( l  +  1 ) ... h )  ->  i  <_  h )
283282adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <_  h )
284 elfzolt2 11835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( h  e.  ( 0..^ M )  ->  h  <  M )
285284adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  h  <  M )
286278, 281, 280, 283, 285lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <  M )
287278, 280, 286ltled 9750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... h
) )  ->  i  <_  M )
288287adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  <_  M
)
289263, 277, 288jca32 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0 ... M )  <->  ( (
0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )  /\  (
0  <_  i  /\  i  <_  M ) ) )
291289, 290sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ( 0 ... M ) )
292291adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  i  e.  ( 0 ... M ) )
293257, 292, 19syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... h ) )  ->  ( V `  i )  e.  RR )
294293adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  /\  i  e.  (
( l  +  1 ) ... h ) )  ->  ( V `  i )  e.  RR )
295 simplll 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ph )
296 0zd 10897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  e.  ZZ )
297 elfzelz 11713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  e.  ZZ )
298297adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  ZZ )
299 0red 9614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  e.  RR )
300298zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  RR )
301242adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  e.  RR )
302268adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <_  l )
303301, 243syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
l  +  1 )  e.  RR )
304301ltp1d 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  <  ( l  +  1 ) )
305 elfzle1 11714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  (
l  +  1 )  <_  i )
306305adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
l  +  1 )  <_  i )
307301, 303, 300, 304, 306ltletrd 9759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  l  <  i )
308299, 301, 300, 302, 307lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <  i )
309299, 300, 308ltled 9750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  0  <_  i )
310 eluz2 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  i  e.  ZZ  /\  0  <_ 
i ) )
311296, 298, 309, 310syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
312311adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  e.  (
ZZ>= `  0 ) )
313 elfzoel2 11825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( l  e.  ( 0..^ M )  ->  M  e.  ZZ )
314313ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  M  e.  ZZ )
315297zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  e.  RR )
316315adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  e.  RR )
317 peano2rem 9905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  e.  RR  ->  (
h  -  1 )  e.  RR )
318246, 317syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  e.  RR )
319318adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
h  -  1 )  e.  RR )
320279adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  M  e.  RR )
321 elfzle2 11715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( ( l  +  1 ) ... ( h  -  1 ) )  ->  i  <_  ( h  -  1 ) )
322321adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <_  ( h  -  1 ) )
323246ltm1d 10498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  < 
h )
324318, 246, 279, 323, 284lttrd 9760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( h  e.  ( 0..^ M )  ->  ( h  -  1 )  < 
M )
325324adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  (
h  -  1 )  <  M )
326316, 319, 320, 322, 325lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <  M )
327326adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  i  e.  ( ( l  +  1 ) ... (
h  -  1 ) ) )  ->  i  <  M )
328327adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  <  M
)
329 elfzo2 11829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ M )  <->  ( i  e.  ( ZZ>= `  0 )  /\  M  e.  ZZ  /\  i  <  M ) )
330312, 314, 328, 329syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  i  e.  ( 0..^ M ) )
331169, 19sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  e.  RR )
33241simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  A. i  e.  ( 0..^ M ) ( V `  i )  <  ( V `  ( i  +  1 ) ) )
333332r19.21bi 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <  ( V `  ( i  +  1 ) ) )
334331, 190, 333ltled 9750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
335295, 330, 334syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( (
l  +  1 ) ... ( h  - 
1 ) ) )  ->  ( V `  i )  <_  ( V `  ( i  +  1 ) ) )
336335adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 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 12140 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( l  +  1 )  <_  h )  ->  ( V `  (
l  +  1 ) )  <_  ( V `  h ) )
338249, 337syldan 470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  ( V `  ( l  +  1 ) )  <_  ( V `  h )
)
339236, 241, 338leimnltd 31675 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  -.  h  <  ( l  +  1 ) )  ->  -.  ( V `  h )  <  ( V `  ( l  +  1 ) ) )
340339adantlr 714 . . . . . . . . . . . . . . . . . . . . . 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 794 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  <  ( l  +  1 ) )
342 zleltp1 10935 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h  e.  ZZ  /\  l  e.  ZZ )  ->  ( h  <_  l  <->  h  <  ( l  +  1 ) ) )
343227, 229, 342syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( h  <_  l  <->  h  <  ( l  +  1 ) ) )
344341, 343mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  ->  h  <_  l )
345 eluz2 11112 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  e.  ( ZZ>= `  h
)  <->  ( h  e.  ZZ  /\  l  e.  ZZ  /\  h  <_ 
l ) )
346227, 229, 344, 345syl3anbrc 1180 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
l  e.  ( ZZ>= `  h ) )
34718ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  ->  V : ( 0 ... M ) --> RR )
348 0zd 10897 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
0  e.  ZZ )
349259ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  ->  M  e.  ZZ )
350 elfzelz 11713 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( h ... l )  ->  i  e.  ZZ )
351350adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ZZ )
352348, 349, 3513jca 1176 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( 0  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )
)
353 0red 9614 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  e.  RR )
354246adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  h  e.  RR )
355350zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( h ... l )  ->  i  e.  RR )
356355adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  e.  RR )
357 elfzole1 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  e.  ( 0..^ M )  ->  0  <_  h )
358357adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  <_  h )
359 elfzle1 11714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( h ... l )  ->  h  <_  i )
360359adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  h  <_  i )
361353, 354, 356, 358, 360letrd 9756 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  0  <_  i )
362361adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
0  <_  i )
363355adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  e.  RR )
364313zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( l  e.  ( 0..^ M )  ->  M  e.  RR )
365364adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  M  e.  RR )
366242adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  l  e.  RR )
367 elfzle2 11715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( h ... l )  ->  i  <_  l )
368367adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <_  l )
369 elfzolt2 11835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( l  e.  ( 0..^ M )  ->  l  <  M )
370369adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  l  <  M )
371363, 366, 365, 368, 370lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <  M )
372363, 365, 371ltled 9750 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... l
) )  ->  i  <_  M )
373372adantll 713 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  <_  M )
374352, 362, 373jca32 535 . . . . . . . . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h  e.  ( 0..^ M )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ( 0 ... M ) )
376375adantlll 717 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
i  e.  ( 0 ... M ) )
377347, 376ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... l ) )  -> 
( V `  i
)  e.  RR )
378377adantlr 714 . . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  ->  ph )
380 0zd 10897 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  e.  ZZ )
381 elfzelz 11713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  e.  ZZ )
382381adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ZZ )
383 0red 9614 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  e.  RR )
384246adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  h  e.  RR )
385382zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  RR )
386357adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  <_  h )
387 elfzle1 11714 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  h  <_  i )
388387adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  h  <_  i )
389383, 384, 385, 386, 388letrd 9756 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  0  <_  i )
390380, 382, 389, 310syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
391390adantll 713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  ( ZZ>= `  0 )
)
392391adant423 31628 . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  ->  M  e.  ZZ )
394381zred 10990 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  e.  RR )
395394adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  e.  RR )
396242adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  e.  RR )
397364adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  M  e.  RR )
398 elfzle2 11715 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( h ... ( l  -  1 ) )  ->  i  <_  ( l  -  1 ) )
399398adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <_  ( l  -  1 ) )
400 zltlem1 10937 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( i  e.  ZZ  /\  l  e.  ZZ )  ->  ( i  <  l  <->  i  <_  ( l  - 
1 ) ) )
401381, 228, 400syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  (
i  <  l  <->  i  <_  ( l  -  1 ) ) )
402399, 401mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  l )
403369adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  l  <  M )
404395, 396, 397, 402, 403lttrd 9760 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( l  e.  ( 0..^ M )  /\  i  e.  ( h ... (
l  -  1 ) ) )  ->  i  <  M )
405404adantll 713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  i  e.  ( h ... ( l  -  1 ) ) )  -> 
i  <  M )
406405adantlr 714 . . . . . . . . . . . . . . . . . . . . 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 1180 . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . 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 12140 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  h )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  h
)  <_  ( V `  l ) )
410225, 409chvarv 2015 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  k
)  <_  ( V `  l ) )
411217, 410chvarv 2015 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  e.  ( 0..^ M ) )  /\  ( V `  k )  <  ( V `  ( i  +  1 ) ) )  -> 
( V `  k
)  <_  ( V `  i ) )
412110, 112, 208, 411syl21anc 1227 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  k
)  <_  ( V `  i ) )
413107, 112jca 532 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ph  /\  i  e.  ( 0..^ M ) ) )
414110, 149syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  e.  RR )
415179simpld 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Q `  i
)  <_  ( S `  J ) )
416176, 143, 138, 415, 164lelttrd 9757 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  i
)  <  ( S `  ( J  +  1 ) ) )
417166simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( S `  ( J  +  1 ) )  <_  ( Q `  ( k  +  1 ) ) )
418176, 138, 414, 416, 417ltletrd 9759 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( Q `  i
)  <  ( Q `  ( k  +  1 ) ) )
419176, 414, 118, 418ltadd2dd 9758 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( X  +  ( Q `  i ) )  <  ( X  +  ( Q `  ( k  +  1 ) ) ) )
420175oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  i ) )  =  ( X  +  ( ( V `
 i )  -  X ) ) )
421107, 172, 19syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( V `  i
)  e.  RR )
422421recnd 9639 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  i
)  e.  CC )
423184, 422pncan3d 9953 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  i
)  -  X ) )  =  ( V `
 i ) )
424420, 423eqtr2d 2499 . . . . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  ( k  +  1 )  ->  ( V `  i )  =  ( V `  ( k  +  1 ) ) )
427426oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  ( k  +  1 )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 ( k  +  1 ) )  -  X ) )
428427adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( 0..^ M ) )  /\  i  =  ( k  +  1 ) )  ->  (
( V `  i
)  -  X )  =  ( ( V `
 ( k  +  1 ) )  -  X ) )
42918adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  V : ( 0 ... M ) --> RR )
430429, 148ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( V `  ( k  +  1 ) )  e.  RR )
43113adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  X  e.  RR )
432430, 431resubcld 10008 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( ( V `
 ( k  +  1 ) )  -  X )  e.  RR )
433425, 428, 148, 432fvmptd 5961 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( 0..^ M ) )  ->  ( Q `  ( k  +  1 ) )  =  ( ( V `  (
k  +  1 ) )  -  X ) )
434107, 109, 433syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( Q `  (
k  +  1 ) )  =  ( ( V `  ( k  +  1 ) )  -  X ) )
435434oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( Q `  ( k  +  1 ) ) )  =  ( X  +  ( ( V `
 ( k  +  1 ) )  -  X ) ) )
436110, 430syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( V `  (
k  +  1 ) )  e.  RR )
437436recnd 9639 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( V `  (
k  +  1 ) )  e.  CC )
438184, 437pncan3d 9953 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( X  +  ( ( V `  (
k  +  1 ) )  -  X ) )  =  ( V `
 ( k  +  1 ) ) )
439435, 438eqtr2d 2499 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( V `  (
k  +  1 ) )  =  ( X  +  ( Q `  ( k  +  1 ) ) ) )
440419, 424, 4393brtr4d 4486 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( V `  i
)  <  ( V `  ( k  +  1 ) ) )
441 eleq1 2529 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  (
l  e.  ( 0..^ M )  <->  k  e.  ( 0..^ M ) ) )
442441anbi2d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) ) ) )
443 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( l  =  k  ->  (
l  +  1 )  =  ( k  +  1 ) )
444443fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  k  ->  ( V `  ( l  +  1 ) )  =  ( V `  ( k  +  1 ) ) )
445444breq2d 4468 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  (
( V `  i
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  i )  <  ( V `  ( k  +  1 ) ) ) )
446442, 445anbi12d 710 . . . . . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  k  ->  ( V `  l )  =  ( V `  k ) )
448447breq2d 4468 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  k  ->  (
( V `  i
)  <_  ( V `  l )  <->  ( V `  i )  <_  ( V `  k )
) )
449446, 448imbi12d 320 . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h  =  i  ->  (
h  e.  ( 0..^ M )  <->  i  e.  ( 0..^ M ) ) )
451450anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  i  ->  (
( ph  /\  h  e.  ( 0..^ M ) )  <->  ( ph  /\  i  e.  ( 0..^ M ) ) ) )
452451anbi1d 704 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  i  ->  (
( ( ph  /\  h  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  <->  ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) ) ) )
453 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  i  ->  ( V `  h )  =  ( V `  i ) )
454453breq1d 4466 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  i  ->  (
( V `  h
)  <  ( V `  ( l  +  1 ) )  <->  ( V `  i )  <  ( V `  ( l  +  1 ) ) ) )
455452, 454anbi12d 710 . . . . . . . . . . . . . . . . . . 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 4466 . . . . . . . . . . . . . . . . . . 19  |-  ( h  =  i  ->  (
( V `  h
)  <_  ( V `  l )  <->  ( V `  i )  <_  ( V `  l )
) )
457455, 456imbi12d 320 . . . . . . . . . . . . . . . . . 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 2015 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  l  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( l  +  1 ) ) )  -> 
( V `  i
)  <_  ( V `  l ) )
459449, 458chvarv 2015 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  k  e.  ( 0..^ M ) )  /\  ( V `  i )  <  ( V `  ( k  +  1 ) ) )  -> 
( V `  i
)  <_  ( V `  k ) )
460413, 109, 440, 459syl21anc 1227 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( V `  i
)  <_  ( V `  k ) )
461117, 421letri3d 9744 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( V `  k )  =  ( V `  i )  <-> 
( ( V `  k )  <_  ( V `  i )  /\  ( V `  i
)  <_  ( V `  k ) ) ) )
462412, 460, 461mpbir2and 922 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( V `  k
)  =  ( V `
 i ) )
4637, 2, 8fourierdlem34 32126 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  V : ( 0 ... M ) -1-1-> RR )
464107, 463syl 16 . . . . . . . . . . . . . . 15  |-  ( ch 
->  V : ( 0 ... M ) -1-1-> RR )
465 f1fveq 6171 . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( V `  k )  =  ( V `  i )  <-> 
k  =  i ) )
467462, 466mpbid 210 . . . . . . . . . . . . 13  |-  ( ch 
->  k  =  i
)
468104, 467sylbir 213 . . . . . . . . . . . 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 434 . . . . . . . . . . 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 457 . . . . . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  ( Q `  k )  =  ( Q `  i ) )
472 oveq1 6303 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
473472fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  ( Q `  ( k  +  1 ) )  =  ( Q `  ( i  +  1 ) ) )
474471, 473oveq12d 6314 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  (
( Q `  k
) (,) ( Q `
 ( k  +  1 ) ) )  =  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )
475474eqcomd 2465 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 k ) (,) ( Q `  (
k  +  1 ) ) ) )
476475adantl 466 . . . . . . . . . . . . . 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 3535 . . . . . . . . . . . . 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 434 . . . . . . . . . . . 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 726 . . . . . . . . . . 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 191 . . . . . . . . . 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 2871 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ M )