Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem10 Unicode version

Theorem cvmliftlem10 23840
Description: Lemma for cvmlift 23845. The function  K is going to be our complete lifted path, formed by unioning together all the  Q functions (each of which is defined on one segment  [ ( M  -  1 )  /  N ,  M  /  N ] of the interval). Here we prove by induction that  K is a continuous function and a lift of  G by applying cvmliftlem6 23836, cvmliftlem7 23837 (to show it is a function and a lift), cvmliftlem8 23838 (to show it is continuous), and cvmliftlem9 23839 (to show that different 
Q functions agree on the intersection of their domains, so that the pasting lemma paste 17038 gives that  K is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
Hypotheses
Ref Expression
cvmliftlem.1  |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " k )  /\  A. u  e.  s  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  k ) ) ) ) } )
cvmliftlem.b  |-  B  = 
U. C
cvmliftlem.x  |-  X  = 
U. J
cvmliftlem.f  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
cvmliftlem.g  |-  ( ph  ->  G  e.  ( II 
Cn  J ) )
cvmliftlem.p  |-  ( ph  ->  P  e.  B )
cvmliftlem.e  |-  ( ph  ->  ( F `  P
)  =  ( G `
 0 ) )
cvmliftlem.n  |-  ( ph  ->  N  e.  NN )
cvmliftlem.t  |-  ( ph  ->  T : ( 1 ... N ) --> U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )
cvmliftlem.a  |-  ( ph  ->  A. k  e.  ( 1 ... N ) ( G " (
( ( k  - 
1 )  /  N
) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k
) ) )
cvmliftlem.l  |-  L  =  ( topGen `  ran  (,) )
cvmliftlem.q  |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N
) )  |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m
) ) ( x `
 ( ( m  -  1 )  /  N ) )  e.  b ) ) `  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. } >. } ) )
cvmliftlem.k  |-  K  = 
U_ k  e.  ( 1 ... N ) ( Q `  k
)
cvmliftlem10.1  |-  ( ch  <->  ( ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) )  /\  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) ) ) )
Assertion
Ref Expression
cvmliftlem10  |-  ( ph  ->  ( K  e.  ( ( Lt  ( 0 [,] ( N  /  N
) ) )  Cn  C )  /\  ( F  o.  K )  =  ( G  |`  ( 0 [,] ( N  /  N ) ) ) ) )
Distinct variable groups:    v, b,
z, B    j, b,
k, m, n, s, u, x, F, v, z    n, L, z    P, b, k, m, n, u, v, x, z    C, b, j, k, n, s, u, v, z    ph, j, n, s, x, z    N, b, k, m, n, u, v, x, z    S, b, j, k, n, s, u, v, x, z    j, X    G, b, j, k, m, n, s, u, v, x, z    T, b, j, k, m, s, u, v, x, z    J, b, j, k, n, s, u, v, x, z    Q, b, k, m, n, u, v, x, z
Allowed substitution hints:    ph( v, u, k, m, b)    ch( x, z, v, u, j, k, m, n, s, b)    B( x, u, j, k, m, n, s)    C( x, m)    P( j,
s)    Q( j, s)    S( m)    T( n)    J( m)    K( x, z, v, u, j, k, m, n, s, b)    L( x, v, u, j, k, m, s, b)    N( j, s)    X( x, z, v, u, k, m, n, s, b)

Proof of Theorem cvmliftlem10
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 cvmliftlem.n . . . 4  |-  ( ph  ->  N  e.  NN )
2 nnuz 10279 . . . 4  |-  NN  =  ( ZZ>= `  1 )
31, 2syl6eleq 2386 . . 3  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
4 eluzfz2 10820 . . 3  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
53, 4syl 15 . 2  |-  ( ph  ->  N  e.  ( 1 ... N ) )
6 eleq1 2356 . . . . . 6  |-  ( y  =  1  ->  (
y  e.  ( 1 ... N )  <->  1  e.  ( 1 ... N
) ) )
7 oveq2 5882 . . . . . . . . . . 11  |-  ( y  =  1  ->  (
1 ... y )  =  ( 1 ... 1
) )
8 1z 10069 . . . . . . . . . . . 12  |-  1  e.  ZZ
9 fzsn 10849 . . . . . . . . . . . 12  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
108, 9ax-mp 8 . . . . . . . . . . 11  |-  ( 1 ... 1 )  =  { 1 }
117, 10syl6eq 2344 . . . . . . . . . 10  |-  ( y  =  1  ->  (
1 ... y )  =  { 1 } )
1211iuneq1d 3944 . . . . . . . . 9  |-  ( y  =  1  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  { 1 }  ( Q `  k ) )
13 1ex 8849 . . . . . . . . . 10  |-  1  e.  _V
14 fveq2 5541 . . . . . . . . . 10  |-  ( k  =  1  ->  ( Q `  k )  =  ( Q ` 
1 ) )
1513, 14iunxsn 3997 . . . . . . . . 9  |-  U_ k  e.  { 1 }  ( Q `  k )  =  ( Q ` 
1 )
1612, 15syl6eq 2344 . . . . . . . 8  |-  ( y  =  1  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  ( Q `  1 ) )
17 oveq1 5881 . . . . . . . . . . 11  |-  ( y  =  1  ->  (
y  /  N )  =  ( 1  /  N ) )
1817oveq2d 5890 . . . . . . . . . 10  |-  ( y  =  1  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( 1  /  N
) ) )
1918oveq2d 5890 . . . . . . . . 9  |-  ( y  =  1  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] (
1  /  N ) ) ) )
2019oveq1d 5889 . . . . . . . 8  |-  ( y  =  1  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( 1  /  N
) ) )  Cn  C ) )
2116, 20eleq12d 2364 . . . . . . 7  |-  ( y  =  1  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  <-> 
( Q `  1
)  e.  ( ( Lt  ( 0 [,] (
1  /  N ) ) )  Cn  C
) ) )
2216coeq2d 4862 . . . . . . . 8  |-  ( y  =  1  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  ( Q `  1 )
) )
2318reseq2d 4971 . . . . . . . 8  |-  ( y  =  1  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( 1  /  N ) ) ) )
2422, 23eqeq12d 2310 . . . . . . 7  |-  ( y  =  1  ->  (
( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) )  <->  ( F  o.  ( Q `  1
) )  =  ( G  |`  ( 0 [,] ( 1  /  N ) ) ) ) )
2521, 24anbi12d 691 . . . . . 6  |-  ( y  =  1  ->  (
( U_ k  e.  ( 1 ... y ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
y  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( y  /  N ) ) ) )  <->  ( ( Q `
 1 )  e.  ( ( Lt  ( 0 [,] ( 1  /  N ) ) )  Cn  C )  /\  ( F  o.  ( Q `  1 )
)  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) ) ) )
266, 25imbi12d 311 . . . . 5  |-  ( y  =  1  ->  (
( y  e.  ( 1 ... N )  ->  ( U_ k  e.  ( 1 ... y
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( y  /  N ) ) ) ) )  <->  ( 1  e.  ( 1 ... N )  ->  (
( Q `  1
)  e.  ( ( Lt  ( 0 [,] (
1  /  N ) ) )  Cn  C
)  /\  ( F  o.  ( Q `  1
) )  =  ( G  |`  ( 0 [,] ( 1  /  N ) ) ) ) ) ) )
2726imbi2d 307 . . . 4  |-  ( y  =  1  ->  (
( ph  ->  ( y  e.  ( 1 ... N )  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) ) ) ) )  <->  ( ph  ->  ( 1  e.  ( 1 ... N )  -> 
( ( Q ` 
1 )  e.  ( ( Lt  ( 0 [,] ( 1  /  N
) ) )  Cn  C )  /\  ( F  o.  ( Q `  1 ) )  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) ) ) ) ) )
28 eleq1 2356 . . . . . 6  |-  ( y  =  n  ->  (
y  e.  ( 1 ... N )  <->  n  e.  ( 1 ... N
) ) )
29 oveq2 5882 . . . . . . . . 9  |-  ( y  =  n  ->  (
1 ... y )  =  ( 1 ... n
) )
3029iuneq1d 3944 . . . . . . . 8  |-  ( y  =  n  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  ( 1 ... n ) ( Q `  k ) )
31 oveq1 5881 . . . . . . . . . . 11  |-  ( y  =  n  ->  (
y  /  N )  =  ( n  /  N ) )
3231oveq2d 5890 . . . . . . . . . 10  |-  ( y  =  n  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( n  /  N
) ) )
3332oveq2d 5890 . . . . . . . . 9  |-  ( y  =  n  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] (
n  /  N ) ) ) )
3433oveq1d 5889 . . . . . . . 8  |-  ( y  =  n  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C ) )
3530, 34eleq12d 2364 . . . . . . 7  |-  ( y  =  n  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  <->  U_ k  e.  (
1 ... n ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N ) ) )  Cn  C ) ) )
3630coeq2d 4862 . . . . . . . 8  |-  ( y  =  n  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) ) )
3732reseq2d 4971 . . . . . . . 8  |-  ( y  =  n  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) )
3836, 37eqeq12d 2310 . . . . . . 7  |-  ( y  =  n  ->  (
( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) )  <->  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( n  /  N ) ) ) ) )
3935, 38anbi12d 691 . . . . . 6  |-  ( y  =  n  ->  (
( U_ k  e.  ( 1 ... y ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
y  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( y  /  N ) ) ) )  <->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) ) ) )
4028, 39imbi12d 311 . . . . 5  |-  ( y  =  n  ->  (
( y  e.  ( 1 ... N )  ->  ( U_ k  e.  ( 1 ... y
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( y  /  N ) ) ) ) )  <->  ( n  e.  ( 1 ... N
)  ->  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
n  /  N ) ) ) ) ) ) )
4140imbi2d 307 . . . 4  |-  ( y  =  n  ->  (
( ph  ->  ( y  e.  ( 1 ... N )  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) ) ) ) )  <->  ( ph  ->  ( n  e.  ( 1 ... N )  -> 
( U_ k  e.  ( 1 ... n ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( n  /  N ) ) ) ) ) ) ) )
42 eleq1 2356 . . . . . 6  |-  ( y  =  ( n  + 
1 )  ->  (
y  e.  ( 1 ... N )  <->  ( n  +  1 )  e.  ( 1 ... N
) ) )
43 oveq2 5882 . . . . . . . . 9  |-  ( y  =  ( n  + 
1 )  ->  (
1 ... y )  =  ( 1 ... (
n  +  1 ) ) )
4443iuneq1d 3944 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) )
45 oveq1 5881 . . . . . . . . . . 11  |-  ( y  =  ( n  + 
1 )  ->  (
y  /  N )  =  ( ( n  +  1 )  /  N ) )
4645oveq2d 5890 . . . . . . . . . 10  |-  ( y  =  ( n  + 
1 )  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )
4746oveq2d 5890 . . . . . . . . 9  |-  ( y  =  ( n  + 
1 )  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
4847oveq1d 5889 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )  Cn  C ) )
4944, 48eleq12d 2364 . . . . . . 7  |-  ( y  =  ( n  + 
1 )  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  <->  U_ k  e.  (
1 ... ( n  + 
1 ) ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )  Cn  C ) ) )
5044coeq2d 4862 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) ) )
5146reseq2d 4971 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) ) )
5250, 51eqeq12d 2310 . . . . . . 7  |-  ( y  =  ( n  + 
1 )  ->  (
( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) )  <->  ( F  o.  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( ( n  +  1 )  /  N ) ) ) ) )
5349, 52anbi12d 691 . . . . . 6  |-  ( y  =  ( n  + 
1 )  ->  (
( U_ k  e.  ( 1 ... y ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
y  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( y  /  N ) ) ) )  <->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) ) ) ) )
5442, 53imbi12d 311 . . . . 5  |-  ( y  =  ( n  + 
1 )  ->  (
( y  e.  ( 1 ... N )  ->  ( U_ k  e.  ( 1 ... y
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( y  /  N ) ) ) ) )  <->  ( (
n  +  1 )  e.  ( 1 ... N )  ->  ( U_ k  e.  (
1 ... ( n  + 
1 ) ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
( n  +  1 )  /  N ) ) ) ) ) ) )
5554imbi2d 307 . . . 4  |-  ( y  =  ( n  + 
1 )  ->  (
( ph  ->  ( y  e.  ( 1 ... N )  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) ) ) ) )  <->  ( ph  ->  ( ( n  +  1 )  e.  ( 1 ... N )  -> 
( U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( ( n  +  1 )  /  N ) ) ) ) ) ) ) )
56 eleq1 2356 . . . . . 6  |-  ( y  =  N  ->  (
y  e.  ( 1 ... N )  <->  N  e.  ( 1 ... N
) ) )
57 oveq2 5882 . . . . . . . . . 10  |-  ( y  =  N  ->  (
1 ... y )  =  ( 1 ... N
) )
5857iuneq1d 3944 . . . . . . . . 9  |-  ( y  =  N  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  ( 1 ... N ) ( Q `  k ) )
59 cvmliftlem.k . . . . . . . . 9  |-  K  = 
U_ k  e.  ( 1 ... N ) ( Q `  k
)
6058, 59syl6eqr 2346 . . . . . . . 8  |-  ( y  =  N  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  K )
61 oveq1 5881 . . . . . . . . . . 11  |-  ( y  =  N  ->  (
y  /  N )  =  ( N  /  N ) )
6261oveq2d 5890 . . . . . . . . . 10  |-  ( y  =  N  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( N  /  N
) ) )
6362oveq2d 5890 . . . . . . . . 9  |-  ( y  =  N  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] ( N  /  N ) ) ) )
6463oveq1d 5889 . . . . . . . 8  |-  ( y  =  N  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( N  /  N
) ) )  Cn  C ) )
6560, 64eleq12d 2364 . . . . . . 7  |-  ( y  =  N  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  <-> 
K  e.  ( ( Lt  ( 0 [,] ( N  /  N ) ) )  Cn  C ) ) )
6660coeq2d 4862 . . . . . . . 8  |-  ( y  =  N  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  K
) )
6762reseq2d 4971 . . . . . . . 8  |-  ( y  =  N  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( N  /  N ) ) ) )
6866, 67eqeq12d 2310 . . . . . . 7  |-  ( y  =  N  ->  (
( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) )  <->  ( F  o.  K )  =  ( G  |`  ( 0 [,] ( N  /  N ) ) ) ) )
6965, 68anbi12d 691 . . . . . 6  |-  ( y  =  N  ->  (
( U_ k  e.  ( 1 ... y ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
y  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( y  /  N ) ) ) )  <->  ( K  e.  ( ( Lt  ( 0 [,] ( N  /  N ) ) )  Cn  C )  /\  ( F  o.  K
)  =  ( G  |`  ( 0 [,] ( N  /  N ) ) ) ) ) )
7056, 69imbi12d 311 . . . . 5  |-  ( y  =  N  ->  (
( y  e.  ( 1 ... N )  ->  ( U_ k  e.  ( 1 ... y
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( y  /  N ) ) ) ) )  <->  ( N  e.  ( 1 ... N
)  ->  ( K  e.  ( ( Lt  ( 0 [,] ( N  /  N ) ) )  Cn  C )  /\  ( F  o.  K
)  =  ( G  |`  ( 0 [,] ( N  /  N ) ) ) ) ) ) )
7170imbi2d 307 . . . 4  |-  ( y  =  N  ->  (
( ph  ->  ( y  e.  ( 1 ... N )  ->  ( U_ k  e.  (
1 ... y ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( y  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... y ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
y  /  N ) ) ) ) ) )  <->  ( ph  ->  ( N  e.  ( 1 ... N )  -> 
( K  e.  ( ( Lt  ( 0 [,] ( N  /  N
) ) )  Cn  C )  /\  ( F  o.  K )  =  ( G  |`  ( 0 [,] ( N  /  N ) ) ) ) ) ) ) )
72 eluzfz1 10819 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... N
) )
733, 72syl 15 . . . . . . . 8  |-  ( ph  ->  1  e.  ( 1 ... N ) )
74 cvmliftlem.1 . . . . . . . . 9  |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " k )  /\  A. u  e.  s  ( A. v  e.  ( s  \  {
u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
Homeo  ( Jt  k ) ) ) ) } )
75 cvmliftlem.b . . . . . . . . 9  |-  B  = 
U. C
76 cvmliftlem.x . . . . . . . . 9  |-  X  = 
U. J
77 cvmliftlem.f . . . . . . . . 9  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
78 cvmliftlem.g . . . . . . . . 9  |-  ( ph  ->  G  e.  ( II 
Cn  J ) )
79 cvmliftlem.p . . . . . . . . 9  |-  ( ph  ->  P  e.  B )
80 cvmliftlem.e . . . . . . . . 9  |-  ( ph  ->  ( F `  P
)  =  ( G `
 0 ) )
81 cvmliftlem.t . . . . . . . . 9  |-  ( ph  ->  T : ( 1 ... N ) --> U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )
82 cvmliftlem.a . . . . . . . . 9  |-  ( ph  ->  A. k  e.  ( 1 ... N ) ( G " (
( ( k  - 
1 )  /  N
) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k
) ) )
83 cvmliftlem.l . . . . . . . . 9  |-  L  =  ( topGen `  ran  (,) )
84 cvmliftlem.q . . . . . . . . 9  |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N
) )  |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m
) ) ( x `
 ( ( m  -  1 )  /  N ) )  e.  b ) ) `  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. } >. } ) )
85 eqid 2296 . . . . . . . . 9  |-  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) )  =  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) )
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 23838 . . . . . . . 8  |-  ( (
ph  /\  1  e.  ( 1 ... N
) )  ->  ( Q `  1 )  e.  ( ( Lt  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) ) )  Cn  C ) )
8773, 86mpdan 649 . . . . . . 7  |-  ( ph  ->  ( Q `  1
)  e.  ( ( Lt  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) ) )  Cn  C
) )
88 1m1e0 9830 . . . . . . . . . . . 12  |-  ( 1  -  1 )  =  0
8988oveq1i 5884 . . . . . . . . . . 11  |-  ( ( 1  -  1 )  /  N )  =  ( 0  /  N
)
901nncnd 9778 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  CC )
911nnne0d 9806 . . . . . . . . . . . 12  |-  ( ph  ->  N  =/=  0 )
9290, 91div0d 9551 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  /  N
)  =  0 )
9389, 92syl5eq 2340 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  1 )  /  N
)  =  0 )
9493oveq1d 5889 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) )  =  ( 0 [,] ( 1  /  N ) ) )
9594oveq2d 5890 . . . . . . . 8  |-  ( ph  ->  ( Lt  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N
) ) )  =  ( Lt  ( 0 [,] ( 1  /  N
) ) ) )
9695oveq1d 5889 . . . . . . 7  |-  ( ph  ->  ( ( Lt  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( 1  /  N ) ) )  Cn  C ) )
9787, 96eleqtrd 2372 . . . . . 6  |-  ( ph  ->  ( Q `  1
)  e.  ( ( Lt  ( 0 [,] (
1  /  N ) ) )  Cn  C
) )
98 simpr 447 . . . . . . . . . 10  |-  ( (
ph  /\  1  e.  ( 1 ... N
) )  ->  1  e.  ( 1 ... N
) )
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 23837 . . . . . . . . . 10  |-  ( (
ph  /\  1  e.  ( 1 ... N
) )  ->  (
( Q `  (
1  -  1 ) ) `  ( ( 1  -  1 )  /  N ) )  e.  ( `' F " { ( G `  ( ( 1  -  1 )  /  N
) ) } ) )
10074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99cvmliftlem6 23836 . . . . . . . . 9  |-  ( (
ph  /\  1  e.  ( 1 ... N
) )  ->  (
( Q `  1
) : ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) ) --> B  /\  ( F  o.  ( Q `  1 ) )  =  ( G  |`  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) ) ) ) )
10173, 100mpdan 649 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
1 ) : ( ( ( 1  -  1 )  /  N
) [,] ( 1  /  N ) ) --> B  /\  ( F  o.  ( Q ` 
1 ) )  =  ( G  |`  (
( ( 1  -  1 )  /  N
) [,] ( 1  /  N ) ) ) ) )
102101simprd 449 . . . . . . 7  |-  ( ph  ->  ( F  o.  ( Q `  1 )
)  =  ( G  |`  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) ) ) )
10394reseq2d 4971 . . . . . . 7  |-  ( ph  ->  ( G  |`  (
( ( 1  -  1 )  /  N
) [,] ( 1  /  N ) ) )  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) )
104102, 103eqtrd 2328 . . . . . 6  |-  ( ph  ->  ( F  o.  ( Q `  1 )
)  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) )
10597, 104jca 518 . . . . 5  |-  ( ph  ->  ( ( Q ` 
1 )  e.  ( ( Lt  ( 0 [,] ( 1  /  N
) ) )  Cn  C )  /\  ( F  o.  ( Q `  1 ) )  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) ) )
106105a1d 22 . . . 4  |-  ( ph  ->  ( 1  e.  ( 1 ... N )  ->  ( ( Q `
 1 )  e.  ( ( Lt  ( 0 [,] ( 1  /  N ) ) )  Cn  C )  /\  ( F  o.  ( Q `  1 )
)  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) ) ) )
107 elnnuz 10280 . . . . . . . . . . 11  |-  ( n  e.  NN  <->  n  e.  ( ZZ>= `  1 )
)
108107biimpi 186 . . . . . . . . . 10  |-  ( n  e.  NN  ->  n  e.  ( ZZ>= `  1 )
)
109108adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  ( ZZ>= `  1 )
)
110 peano2fzr 10824 . . . . . . . . . 10  |-  ( ( n  e.  ( ZZ>= ` 
1 )  /\  (
n  +  1 )  e.  ( 1 ... N ) )  ->  n  e.  ( 1 ... N ) )
111110ex 423 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  1
)  ->  ( (
n  +  1 )  e.  ( 1 ... N )  ->  n  e.  ( 1 ... N
) ) )
112109, 111syl 15 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( n  +  1 )  e.  ( 1 ... N )  ->  n  e.  ( 1 ... N
) ) )
113112imim1d 69 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( n  e.  ( 1 ... N )  -> 
( U_ k  e.  ( 1 ... n ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( n  /  N ) ) ) ) )  ->  (
( n  +  1 )  e.  ( 1 ... N )  -> 
( U_ k  e.  ( 1 ... n ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
)  /\  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k
) )  =  ( G  |`  ( 0 [,] ( n  /  N ) ) ) ) ) ) )
114 cvmliftlem10.1 . . . . . . . . . . 11  |-  ( ch  <->  ( ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) )  /\  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) ) ) )
115 eqid 2296 . . . . . . . . . . . . 13  |-  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) )  =  U. ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )
116 0re 8854 . . . . . . . . . . . . . . 15  |-  0  e.  RR
117114simplbi 446 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) ) )
118117adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) ) )
119118simprd 449 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( n  +  1 )  e.  ( 1 ... N ) )
120 elfznn 10835 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  +  1 )  e.  ( 1 ... N )  ->  (
n  +  1 )  e.  NN )
121119, 120syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( n  +  1 )  e.  NN )
122121nnred 9777 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( n  +  1 )  e.  RR )
1231adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  N  e.  NN )
124122, 123nndivred 9810 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( n  + 
1 )  /  N
)  e.  RR )
125 iccssre 10747 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  ( ( n  + 
1 )  /  N
)  e.  RR )  ->  ( 0 [,] ( ( n  + 
1 )  /  N
) )  C_  RR )
126116, 124, 125sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  C_  RR )
127117simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  n  e.  NN )
128127adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  n  e.  NN )
129128nnred 9777 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  n  e.  RR )
130129, 123nndivred 9810 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  RR )
131 icccld 18292 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  ( n  /  N
)  e.  RR )  ->  ( 0 [,] ( n  /  N
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
132116, 130, 131sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
13383fveq2i 5544 . . . . . . . . . . . . . . 15  |-  ( Clsd `  L )  =  (
Clsd `  ( topGen ` 
ran  (,) ) )
134132, 133syl6eleqr 2387 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  e.  ( Clsd `  L ) )
135 ssun1 3351 . . . . . . . . . . . . . . 15  |-  ( 0 [,] ( n  /  N ) )  C_  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )
136116a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  0  e.  RR )
137128nnnn0d 10034 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  n  e.  NN0 )
138137nn0ge0d 10037 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  0  <_  n )
139123nnred 9777 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  N  e.  RR )
140123nngt0d 9805 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  0  <  N )
141 divge0 9641 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  RR  /\  0  <_  n )  /\  ( N  e.  RR  /\  0  <  N ) )  ->  0  <_  ( n  /  N ) )
142129, 138, 139, 140, 141syl22anc 1183 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  0  <_  ( n  /  N ) )
143129ltp1d 9703 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  n  <  ( n  +  1 ) )
144 ltdiv1 9636 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  RR  /\  ( n  +  1
)  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) )  ->  ( n  <  ( n  +  1 )  <->  ( n  /  N )  <  (
( n  +  1 )  /  N ) ) )
145129, 122, 139, 140, 144syl112anc 1186 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  <  (
n  +  1 )  <-> 
( n  /  N
)  <  ( (
n  +  1 )  /  N ) ) )
146143, 145mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  <  ( (
n  +  1 )  /  N ) )
147130, 124, 146ltled 8983 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  <_  ( (
n  +  1 )  /  N ) )
148 elicc2 10731 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  RR  /\  ( ( n  + 
1 )  /  N
)  e.  RR )  ->  ( ( n  /  N )  e.  ( 0 [,] (
( n  +  1 )  /  N ) )  <->  ( ( n  /  N )  e.  RR  /\  0  <_ 
( n  /  N
)  /\  ( n  /  N )  <_  (
( n  +  1 )  /  N ) ) ) )
149116, 124, 148sylancr 644 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N )  e.  ( 0 [,] ( ( n  +  1 )  /  N ) )  <-> 
( ( n  /  N )  e.  RR  /\  0  <_  ( n  /  N )  /\  (
n  /  N )  <_  ( ( n  +  1 )  /  N ) ) ) )
150130, 142, 147, 149mpbir3and 1135 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( 0 [,] ( ( n  +  1 )  /  N ) ) )
151 iccsplit 10784 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  ( ( n  + 
1 )  /  N
)  e.  RR  /\  ( n  /  N
)  e.  ( 0 [,] ( ( n  +  1 )  /  N ) ) )  ->  ( 0 [,] ( ( n  + 
1 )  /  N
) )  =  ( ( 0 [,] (
n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) ) )
152136, 124, 150, 151syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  =  ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) )
153135, 152syl5sseqr 3240 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  C_  ( 0 [,] ( ( n  +  1 )  /  N ) ) )
154 uniretop 18287 . . . . . . . . . . . . . . . 16  |-  RR  =  U. ( topGen `  ran  (,) )
15583unieqi 3853 . . . . . . . . . . . . . . . 16  |-  U. L  =  U. ( topGen `  ran  (,) )
156154, 155eqtr4i 2319 . . . . . . . . . . . . . . 15  |-  RR  =  U. L
157156restcldi 16920 . . . . . . . . . . . . . 14  |-  ( ( ( 0 [,] (
( n  +  1 )  /  N ) )  C_  RR  /\  (
0 [,] ( n  /  N ) )  e.  ( Clsd `  L
)  /\  ( 0 [,] ( n  /  N ) )  C_  ( 0 [,] (
( n  +  1 )  /  N ) ) )  ->  (
0 [,] ( n  /  N ) )  e.  ( Clsd `  ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) ) )
158126, 134, 153, 157syl3anc 1182 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  e.  ( Clsd `  ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) ) ) )
159 icccld 18292 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  /  N
)  e.  RR  /\  ( ( n  + 
1 )  /  N
)  e.  RR )  ->  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
160130, 124, 159syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
161160, 133syl6eleqr 2387 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  e.  ( Clsd `  L ) )
162 ssun2 3352 . . . . . . . . . . . . . . 15  |-  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) )  C_  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )
163162, 152syl5sseqr 3240 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  C_  ( 0 [,] ( ( n  +  1 )  /  N ) ) )
164156restcldi 16920 . . . . . . . . . . . . . 14  |-  ( ( ( 0 [,] (
( n  +  1 )  /  N ) )  C_  RR  /\  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) )  e.  ( Clsd `  L
)  /\  ( (
n  /  N ) [,] ( ( n  +  1 )  /  N ) )  C_  ( 0 [,] (
( n  +  1 )  /  N ) ) )  ->  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) )  e.  ( Clsd `  ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) ) )
165126, 161, 163, 164syl3anc 1182 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  e.  ( Clsd `  ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) ) ) )
166 retop 18286 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  e.  Top
16783, 166eqeltri 2366 . . . . . . . . . . . . . . 15  |-  L  e. 
Top
168156restuni 16909 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  Top  /\  ( 0 [,] (
( n  +  1 )  /  N ) )  C_  RR )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  =  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
169167, 126, 168sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  =  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
170152, 169eqtr3d 2330 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
171114simprbi 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) ) )
172171adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) ) )
173172simpld 445 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
) )
174 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  U. ( Lt  ( 0 [,] (
n  /  N ) ) )  =  U. ( Lt  ( 0 [,] ( n  /  N
) ) )
175174, 75cnf 16992 . . . . . . . . . . . . . . . . . 18  |-  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N ) ) )  Cn  C )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
n  /  N ) ) ) --> B )
176173, 175syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
n  /  N ) ) ) --> B )
177 iccssre 10747 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  ( n  /  N
)  e.  RR )  ->  ( 0 [,] ( n  /  N
) )  C_  RR )
178116, 130, 177sylancr 644 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  C_  RR )
179156restuni 16909 . . . . . . . . . . . . . . . . . . 19  |-  ( ( L  e.  Top  /\  ( 0 [,] (
n  /  N ) )  C_  RR )  ->  ( 0 [,] (
n  /  N ) )  =  U. ( Lt  ( 0 [,] (
n  /  N ) ) ) )
180167, 178, 179sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  =  U. ( Lt  ( 0 [,] (
n  /  N ) ) ) )
181180feq2d 5396 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k ) : ( 0 [,] ( n  /  N ) ) --> B  <->  U_ k  e.  ( 1 ... n ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
n  /  N ) ) ) --> B ) )
182176, 181mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
) : ( 0 [,] ( n  /  N ) ) --> B )
183 eqid 2296 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) )  =  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) )
184 simpr 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  (
n  +  1 )  e.  ( 1 ... N ) )
18574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem7 23837 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  (
( Q `  (
( n  +  1 )  -  1 ) ) `  ( ( ( n  +  1 )  -  1 )  /  N ) )  e.  ( `' F " { ( G `  ( ( ( n  +  1 )  - 
1 )  /  N
) ) } ) )
18674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185cvmliftlem6 23836 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  (
( Q `  (
n  +  1 ) ) : ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) ) --> B  /\  ( F  o.  ( Q `  ( n  +  1 ) ) )  =  ( G  |`  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) ) ) ) )
187119, 186syldan 456 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) ) : ( ( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) --> B  /\  ( F  o.  ( Q `  ( n  +  1
) ) )  =  ( G  |`  (
( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) ) )
188187simpld 445 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) ) : ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) ) --> B )
189128nncnd 9778 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  n  e.  CC )
190 ax-1cn 8811 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
191 pncan 9073 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  CC  /\  1  e.  CC )  ->  ( ( n  + 
1 )  -  1 )  =  n )
192189, 190, 191sylancl 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  ( ( n  + 
1 )  -  1 )  =  n )
193192oveq1d 5889 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( ( ( n  +  1 )  - 
1 )  /  N
)  =  ( n  /  N ) )
194193oveq1d 5889 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) )  =  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
195194feq2d 5396 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) ) : ( ( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) --> B  <->  ( Q `  ( n  +  1
) ) : ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) --> B ) )
196188, 195mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) ) : ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) --> B )
197 ffun 5407 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) : ( 0 [,] ( n  /  N
) ) --> B  ->  Fun  U_ k  e.  ( 1 ... n ) ( Q `  k
) )
198182, 197syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  Fun  U_ k  e.  ( 1 ... n ) ( Q `  k
) )
199128, 108syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  n  e.  ( ZZ>= ` 
1 ) )
200 eluzfz2 10820 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( ZZ>= `  1
)  ->  n  e.  ( 1 ... n
) )
201199, 200syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ch )  ->  n  e.  ( 1 ... n ) )
202 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  n  ->  ( Q `  k )  =  ( Q `  n ) )
203202ssiun2s 3962 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... n )  ->  ( Q `  n )  C_ 
U_ k  e.  ( 1 ... n ) ( Q `  k
) )
204201, 203syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( Q `  n
)  C_  U_ k  e.  ( 1 ... n
) ( Q `  k ) )
205 peano2rem 9129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  e.  RR  ->  (
n  -  1 )  e.  RR )
206129, 205syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  ( n  -  1 )  e.  RR )
207206, 123nndivred 9810 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  e.  RR )
208207rexrd 8897 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  e.  RR* )
209130rexrd 8897 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  RR* )
210129ltm1d 9705 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  ( n  -  1 )  <  n )
211 ltdiv1 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( n  -  1 )  e.  RR  /\  n  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) )  -> 
( ( n  - 
1 )  <  n  <->  ( ( n  -  1 )  /  N )  <  ( n  /  N ) ) )
212206, 129, 139, 140, 211syl112anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  <  n  <->  ( ( n  -  1 )  /  N )  <  ( n  /  N ) ) )
213210, 212mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  <  ( n  /  N ) )
214207, 130, 213ltled 8983 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  <_  ( n  /  N ) )
215 ubicc2 10769 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( n  - 
1 )  /  N
)  e.  RR*  /\  (
n  /  N )  e.  RR*  /\  (
( n  -  1 )  /  N )  <_  ( n  /  N ) )  -> 
( n  /  N
)  e.  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) )
216208, 209, 214, 215syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) )
217199, 119, 110syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  n  e.  ( 1 ... N ) )
218 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) )  =  ( ( ( n  -  1 )  /  N ) [,] (
n  /  N ) )
219 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  ( 1 ... N
) )
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218cvmliftlem7 23837 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( Q `  (
n  -  1 ) ) `  ( ( n  -  1 )  /  N ) )  e.  ( `' F " { ( G `  ( ( n  - 
1 )  /  N
) ) } ) )
22174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218, 219, 220cvmliftlem6 23836 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( Q `  n
) : ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) --> B  /\  ( F  o.  ( Q `  n ) )  =  ( G  |`  ( ( ( n  -  1 )  /  N ) [,] (
n  /  N ) ) ) ) )
222217, 221syldan 456 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ch )  ->  ( ( Q `  n ) : ( ( ( n  - 
1 )  /  N
) [,] ( n  /  N ) ) --> B  /\  ( F  o.  ( Q `  n ) )  =  ( G  |`  (
( ( n  - 
1 )  /  N
) [,] ( n  /  N ) ) ) ) )
223222simpld 445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( Q `  n
) : ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) --> B )
224 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Q `  n ) : ( ( ( n  -  1 )  /  N ) [,] ( n  /  N
) ) --> B  ->  dom  ( Q `  n
)  =  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) )
225223, 224syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ch )  ->  dom  ( Q `  n )  =  ( ( ( n  - 
1 )  /  N
) [,] ( n  /  N ) ) )
226216, 225eleqtrrd 2373 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  dom  ( Q `  n )
)
227 funssfv 5559 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Fun  U_ k  e.  ( 1 ... n ) ( Q `  k
)  /\  ( Q `  n )  C_  U_ k  e.  ( 1 ... n
) ( Q `  k )  /\  (
n  /  N )  e.  dom  ( Q `
 n ) )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k ) `  (
n  /  N ) )  =  ( ( Q `  n ) `
 ( n  /  N ) ) )
228198, 204, 226, 227syl3anc 1182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k ) `  (
n  /  N ) )  =  ( ( Q `  n ) `
 ( n  /  N ) ) )
229192fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( Q `  (
( n  +  1 )  -  1 ) )  =  ( Q `
 n ) )
230229, 193fveq12d 5547 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( ( n  + 
1 )  -  1 ) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  n ) `
 ( n  /  N ) ) )
23174, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84cvmliftlem9 23839 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  (
( Q `  (
n  +  1 ) ) `  ( ( ( n  +  1 )  -  1 )  /  N ) )  =  ( ( Q `
 ( ( n  +  1 )  - 
1 ) ) `  ( ( ( n  +  1 )  - 
1 )  /  N
) ) )
232119, 231syldan 456 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  ( ( n  +  1 )  -  1 ) ) `
 ( ( ( n  +  1 )  -  1 )  /  N ) ) )
233193fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) )
234232, 233eqtr3d 2330 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( ( n  + 
1 )  -  1 ) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) )
235228, 230, 2343eqtr2d 2334 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k ) `  (
n  /  N ) )  =  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) )
236235opeq2d 3819 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  -> 
<. ( n  /  N
) ,  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) `
 ( n  /  N ) ) >.  =  <. ( n  /  N ) ,  ( ( Q `  (
n  +  1 ) ) `  ( n  /  N ) )
>. )
237236sneqd 3666 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  { <. ( n  /  N ) ,  (
U_ k  e.  ( 1 ... n ) ( Q `  k
) `  ( n  /  N ) ) >. }  =  { <. (
n  /  N ) ,  ( ( Q `
 ( n  + 
1 ) ) `  ( n  /  N
) ) >. } )
238 ffn 5405 . . . . . . . . . . . . . . . . . . . 20  |-  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) : ( 0 [,] ( n  /  N
) ) --> B  ->  U_ k  e.  (
1 ... n ) ( Q `  k )  Fn  ( 0 [,] ( n  /  N
) ) )
239182, 238syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
)  Fn  ( 0 [,] ( n  /  N ) ) )
240 0xr 8894 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  RR*
241240a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  0  e.  RR* )
242 ubicc2 10769 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR*  /\  (
n  /  N )  e.  RR*  /\  0  <_  ( n  /  N
) )  ->  (
n  /  N )  e.  ( 0 [,] ( n  /  N
) ) )
243241, 209, 142, 242syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( 0 [,] ( n  /  N ) ) )
244 fnressn 5721 . . . . . . . . . . . . . . . . . . 19  |-  ( (
U_ k  e.  ( 1 ... n ) ( Q `  k
)  Fn  ( 0 [,] ( n  /  N ) )  /\  ( n  /  N
)  e.  ( 0 [,] ( n  /  N ) ) )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  |`  { ( n  /  N ) } )  =  { <. ( n  /  N
) ,  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) `
 ( n  /  N ) ) >. } )
245239, 243, 244syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  |`  { ( n  /  N ) } )  =  { <. ( n  /  N
) ,  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) `
 ( n  /  N ) ) >. } )
246 ffn 5405 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Q `  ( n  +  1 ) ) : ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) --> B  -> 
( Q `  (
n  +  1 ) )  Fn  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
247196, 246syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) )  Fn  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
248124rexrd 8897 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  ( ( n  + 
1 )  /  N
)  e.  RR* )
249 lbicc2 10768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  /  N
)  e.  RR*  /\  (
( n  +  1 )  /  N )  e.  RR*  /\  (
n  /  N )  <_  ( ( n  +  1 )  /  N ) )  -> 
( n  /  N
)  e.  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
250209, 248, 147, 249syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
251 fnressn 5721 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( Q `  (
n  +  1 ) )  Fn  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) )  /\  ( n  /  N
)  e.  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  ->  ( ( Q `
 ( n  + 
1 ) )  |`  { ( n  /  N ) } )  =  { <. (
n  /  N ) ,  ( ( Q `
 ( n  + 
1 ) ) `  ( n  /  N
) ) >. } )
252247, 250, 251syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) )  |`  { ( n  /  N ) } )  =  { <. ( n  /  N
) ,  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) >. } )
253237, 245, 2523eqtr4d 2338 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  |`  { ( n  /  N ) } )  =  ( ( Q `  (
n  +  1 ) )  |`  { (
n  /  N ) } ) )
254 df-icc 10679 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
255 xrmaxle 10528 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  e.  RR*  /\  (
n  /  N )  e.  RR*  /\  z  e.  RR* )  ->  ( if ( 0  <_  (
n  /  N ) ,  ( n  /  N ) ,  0 )  <_  z  <->  ( 0  <_  z  /\  (
n  /  N )  <_  z ) ) )
256 xrlemin 10529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  e.  RR*  /\  (
n  /  N )  e.  RR*  /\  (
( n  +  1 )  /  N )  e.  RR* )  ->  (
z  <_  if (
( n  /  N
)  <_  ( (
n  +  1 )  /  N ) ,  ( n  /  N
) ,  ( ( n  +  1 )  /  N ) )  <-> 
( z  <_  (
n  /  N )  /\  z  <_  (
( n  +  1 )  /  N ) ) ) )
257254, 255, 256ixxin 10689 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 0  e.  RR*  /\  ( n  /  N
)  e.  RR* )  /\  ( ( n  /  N )  e.  RR*  /\  ( ( n  + 
1 )  /  N
)  e.  RR* )
)  ->  ( (
0 [,] ( n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) )  =  ( if ( 0  <_  ( n  /  N ) ,  ( n  /  N ) ,  0 ) [,]
if ( ( n  /  N )  <_ 
( ( n  + 
1 )  /  N
) ,  ( n  /  N ) ,  ( ( n  + 
1 )  /  N
) ) ) )
258241, 209, 209, 248, 257syl22anc 1183 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( if ( 0  <_  (
n  /  N ) ,  ( n  /  N ) ,  0 ) [,] if ( ( n  /  N
)  <_  ( (
n  +  1 )  /  N ) ,  ( n  /  N
) ,  ( ( n  +  1 )  /  N ) ) ) )
259 iftrue 3584 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  <_  ( n  /  N )  ->  if ( 0  <_  (
n  /  N ) ,  ( n  /  N ) ,  0 )  =  ( n  /  N ) )
260142, 259syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  if ( 0  <_ 
( n  /  N
) ,  ( n  /  N ) ,  0 )  =  ( n  /  N ) )
261 iftrue 3584 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  /  N )  <_  ( ( n  +  1 )  /  N )  ->  if ( ( n  /  N )  <_  (
( n  +  1 )  /  N ) ,  ( n  /  N ) ,  ( ( n  +  1 )  /  N ) )  =  ( n  /  N ) )
262147, 261syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  if ( ( n  /  N )  <_ 
( ( n  + 
1 )  /  N
) ,  ( n  /  N ) ,  ( ( n  + 
1 )  /  N
) )  =  ( n  /  N ) )
263260, 262oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( if ( 0  <_  ( n  /  N ) ,  ( n  /  N ) ,  0 ) [,]
if ( ( n  /  N )  <_ 
( ( n  + 
1 )  /  N
) ,  ( n  /  N ) ,  ( ( n  + 
1 )  /  N
) ) )  =  ( ( n  /  N ) [,] (
n  /  N ) ) )
264 iccid 10717 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  /  N )  e.  RR*  ->  ( ( n  /  N ) [,] ( n  /  N ) )  =  { ( n  /  N ) } )
265209, 264syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
n  /  N ) )  =  { ( n  /  N ) } )
266258, 263, 2653eqtrd 2332 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  { ( n  /  N ) } )
267266reseq2d 4971 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  |`  (
( 0 [,] (
n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  |`  { ( n  /  N ) } ) )
268266reseq2d 4971 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) )  |`  (
( 0 [,] (
n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( Q `  ( n  +  1 ) )  |`  { ( n  /  N ) } ) )
269253, 267, 2683eqtr4d 2338 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  |`  (
( 0 [,] (
n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( Q `  ( n  +  1 ) )  |`  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) ) )
270 fresaun 5428 . . . . . . . . . . . . . . . 16  |-  ( (
U_ k  e.  ( 1 ... n ) ( Q `  k
) : ( 0 [,] ( n  /  N ) ) --> B  /\  ( Q `  ( n  +  1
) ) : ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) --> B  /\  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  |`  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( Q `  (
n  +  1 ) )  |`  ( (
0 [,] ( n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) ) )  ->  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  u.  ( Q `  ( n  +  1
) ) ) : ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) --> B )
271182, 196, 269, 270syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) ) : ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) --> B )
272 fzsuc 10851 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( n  + 
1 ) )  =  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) )
273199, 272syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( 1 ... (
n  +  1 ) )  =  ( ( 1 ... n )  u.  { ( n  +  1 ) } ) )
274273iuneq1d 3944 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
)  =  U_ k  e.  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) ( Q `  k ) )
275 iunxun 3999 . . . . . . . . . . . . . . . . . 18  |-  U_ k  e.  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) ( Q `  k )  =  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  U_ k  e.  { (
n  +  1 ) }  ( Q `  k ) )
276 ovex 5899 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  +  1 )  e. 
_V
277 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  ( n  + 
1 )  ->  ( Q `  k )  =  ( Q `  ( n  +  1
) ) )
278276, 277iunxsn 3997 . . . . . . . . . . . . . . . . . . 19  |-  U_ k  e.  { ( n  + 
1 ) }  ( Q `  k )  =  ( Q `  ( n  +  1
) )
279278uneq2i 3339 . . . . . . . . . . . . . . . . . 18  |-  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  u.  U_ k  e. 
{ ( n  + 
1 ) }  ( Q `  k )
)  =  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  u.  ( Q `  ( n  +  1
) ) )
280275, 279eqtri 2316 . . . . . . . . . . . . . . . . 17  |-  U_ k  e.  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) ( Q `  k )  =  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )
281274, 280syl6req 2345 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  =  U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k ) )
282281feq1d 5395 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) ) : ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) --> B  <->  U_ k  e.  (
1 ... ( n  + 
1 ) ) ( Q `  k ) : ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) --> B ) )
283271, 282mpbid 201 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) : ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) --> B )
284170feq2d 5396 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k ) : ( ( 0 [,] (
n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) ) --> B  <->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) --> B ) )
285283, 284mpbid 201 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) --> B )
286281reseq1d 4970 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  |`  ( 0 [,] ( n  /  N ) ) )  =  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
0 [,] ( n  /  N ) ) ) )
287 fresaunres1 5430 . . . . . . . . . . . . . . . . 17  |-  ( (
U_ k  e.  ( 1 ... n ) ( Q `  k
) : ( 0 [,] ( n  /  N ) ) --> B  /\  ( Q `  ( n  +  1
) ) : ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) --> B  /\  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  |`  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( Q `  (
n  +  1 ) )  |`  ( (
0 [,] ( n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) ) )  ->  ( ( U_ k  e.  (
1 ... n ) ( Q `  k )  u.  ( Q `  ( n  +  1
) ) )  |`  ( 0 [,] (
n  /  N ) ) )  =  U_ k  e.  ( 1 ... n ) ( Q `  k ) )
288182, 196, 269, 287syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  |`  ( 0 [,] ( n  /  N ) ) )  =  U_ k  e.  ( 1 ... n
) ( Q `  k ) )
289286, 288eqtr3d 2330 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
0 [,] ( n  /  N ) ) )  =  U_ k  e.  ( 1 ... n
) ( Q `  k ) )
290289, 173eqeltrd 2370 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
0 [,] ( n  /  N ) ) )  e.  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
) )
291167a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  L  e.  Top )
292 ovex 5899 . . . . . . . . . . . . . . . . 17  |-  ( 0 [,] ( ( n  +  1 )  /  N ) )  e. 
_V
293292a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  e.  _V )
294 restabs 16912 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  Top  /\  ( 0 [,] (
n  /  N ) )  C_  ( 0 [,] ( ( n  +  1 )  /  N ) )  /\  ( 0 [,] (
( n  +  1 )  /  N ) )  e.  _V )  ->  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( 0 [,] ( n  /  N ) ) )  =  ( Lt  ( 0 [,] ( n  /  N ) ) ) )
295291, 153, 293, 294syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( 0 [,] ( n  /  N ) ) )  =  ( Lt  ( 0 [,] ( n  /  N ) ) ) )
296295oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( 0 [,] (
n  /  N ) ) )  Cn  C
)  =  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
) )
297290, 296eleqtrrd 2373 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
0 [,] ( n  /  N ) ) )  e.  ( ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )t  ( 0 [,] ( n  /  N ) ) )  Cn  C ) )
298281reseq1d 4970 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  |`  ( (
n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  =  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )
299 fresaunres2 5429 . . . . . . . . . . . . . . . . 17  |-  ( (
U_ k  e.  ( 1 ... n ) ( Q `  k
) : ( 0 [,] ( n  /  N ) ) --> B  /\  ( Q `  ( n  +  1
) ) : ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) --> B  /\  ( U_ k  e.  ( 1 ... n ) ( Q `  k )  |`  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( Q `  (
n  +  1 ) )  |`  ( (
0 [,] ( n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) ) )  ->  ( ( U_ k  e.  (
1 ... n ) ( Q `  k )  u.  ( Q `  ( n  +  1
) ) )  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  =  ( Q `  ( n  +  1 ) ) )
300182, 196, 269, 299syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  |`  ( (
n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Q `  ( n  +  1
) ) )
301298, 300eqtr3d 2330 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Q `
 ( n  + 
1 ) ) )
30274, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 23838 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  ( Q `  ( n  +  1 ) )  e.  ( ( Lt  ( ( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C ) )
303119, 302syldan 456 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) )  e.  ( ( Lt  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
304194oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( Lt  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] ( ( n  + 
1 )  /  N
) ) )  =  ( Lt  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) )
305304oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( ( Lt  ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C )  =  ( ( Lt  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C ) )
306303, 305eleqtrd 2372 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) )  e.  ( ( Lt  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
307301, 306eqeltrd 2370 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  e.  ( ( Lt  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
308 restabs 16912 . . . . . . . . . . . . . . . 16  |-  ( ( L  e.  Top  /\  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  C_  ( 0 [,] ( ( n  +  1 )  /  N ) )  /\  ( 0 [,] (
( n  +  1 )  /  N ) )  e.  _V )  ->  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Lt  ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )
309291, 163, 293, 308syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Lt  ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )
310309oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
)  =  ( ( Lt  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
311307, 310eleqtrrd 2373 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  e.  ( ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )t  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C ) )
312115, 75, 158, 165, 170, 285, 297, 311paste 17038 . . . . . . . . . . . 12  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
313152reseq2d 4971 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) )  =  ( G  |`  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) ) )
314172simprd 449 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
n  /  N ) ) ) )
315187simprd 449 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( F  o.  ( Q `  ( n  +  1 ) ) )  =  ( G  |`  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
316194reseq2d 4971 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( G  |`  (
( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( G  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
317315, 316eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( F  o.  ( Q `  ( n  +  1 ) ) )  =  ( G  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
318314, 317uneq12d 3343 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) )  u.  ( F  o.  ( Q `  ( n  +  1
) ) ) )  =  ( ( G  |`  ( 0 [,] (
n  /  N ) ) )  u.  ( G  |`  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) ) )
319 coundi 5190 . . . . . . . . . . . . . 14  |-  ( F  o.  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) ) )  =  ( ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) )  u.  ( F  o.  ( Q `  ( n  +  1
) ) ) )
320 resundi 4985 . . . . . . . . . . . . . 14  |-  ( G  |`  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( G  |`  (
0 [,] ( n  /  N ) ) )  u.  ( G  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
321318, 319, 3203eqtr4g 2353 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( F  o.  ( U_ k  e.  (
1 ... n ) ( Q `  k )  u.  ( Q `  ( n  +  1
) ) ) )  =  ( G  |`  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) ) )
322281coeq2d 4862 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( F  o.  ( U_ k  e.  (
1 ... n ) ( Q `  k )  u.  ( Q `  ( n  +  1
) ) ) )  =  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) ) )
323313, 321, 3223eqtr2rd 2335 . . . . . . . . . . . 12  |-  ( (
ph  /\  ch )  ->  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
324312, 323jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) ) ) )
325114, 324sylan2br 462 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
n  e.  NN  /\  ( n  +  1
)  e.  ( 1 ... N ) )  /\  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) ) ) )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) ) ) )
326325expr 598 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N
) ) )  -> 
( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n
) ( Q `  k ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) )  ->  ( U_ k  e.  (
1 ... ( n  + 
1 ) ) ( Q `  k )  e.  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
( n  +  1 )  /  N ) ) ) ) ) )
327326expr 598 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( n  +  1 )  e.  ( 1 ... N )  ->  (
( U_ k  e.  ( 1 ... n ) ( Q `  k
)