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

Theorem cvmliftlem10 29578
Description: Lemma for cvmlift 29583. 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 29574, cvmliftlem7 29575 (to show it is a function and a lift), cvmliftlem8 29576 (to show it is continuous), and cvmliftlem9 29577 (to show that different 
Q functions agree on the intersection of their domains, so that the pasting lemma paste 20086 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 11161 . . . 4  |-  NN  =  ( ZZ>= `  1 )
31, 2syl6eleq 2500 . . 3  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
4 eluzfz2 11746 . . 3  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
53, 4syl 17 . 2  |-  ( ph  ->  N  e.  ( 1 ... N ) )
6 eleq1 2474 . . . . . 6  |-  ( y  =  1  ->  (
y  e.  ( 1 ... N )  <->  1  e.  ( 1 ... N
) ) )
7 oveq2 6285 . . . . . . . . . . 11  |-  ( y  =  1  ->  (
1 ... y )  =  ( 1 ... 1
) )
8 1z 10934 . . . . . . . . . . . 12  |-  1  e.  ZZ
9 fzsn 11778 . . . . . . . . . . . 12  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
108, 9ax-mp 5 . . . . . . . . . . 11  |-  ( 1 ... 1 )  =  { 1 }
117, 10syl6eq 2459 . . . . . . . . . 10  |-  ( y  =  1  ->  (
1 ... y )  =  { 1 } )
1211iuneq1d 4295 . . . . . . . . 9  |-  ( y  =  1  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  { 1 }  ( Q `  k ) )
13 1ex 9620 . . . . . . . . . 10  |-  1  e.  _V
14 fveq2 5848 . . . . . . . . . 10  |-  ( k  =  1  ->  ( Q `  k )  =  ( Q ` 
1 ) )
1513, 14iunxsn 4353 . . . . . . . . 9  |-  U_ k  e.  { 1 }  ( Q `  k )  =  ( Q ` 
1 )
1612, 15syl6eq 2459 . . . . . . . 8  |-  ( y  =  1  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  ( Q `  1 ) )
17 oveq1 6284 . . . . . . . . . . 11  |-  ( y  =  1  ->  (
y  /  N )  =  ( 1  /  N ) )
1817oveq2d 6293 . . . . . . . . . 10  |-  ( y  =  1  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( 1  /  N
) ) )
1918oveq2d 6293 . . . . . . . . 9  |-  ( y  =  1  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] (
1  /  N ) ) ) )
2019oveq1d 6292 . . . . . . . 8  |-  ( y  =  1  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( 1  /  N
) ) )  Cn  C ) )
2116, 20eleq12d 2484 . . . . . . 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 4985 . . . . . . . 8  |-  ( y  =  1  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  ( Q `  1 )
) )
2318reseq2d 5093 . . . . . . . 8  |-  ( y  =  1  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( 1  /  N ) ) ) )
2422, 23eqeq12d 2424 . . . . . . 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 709 . . . . . 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 318 . . . . 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 314 . . . 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 2474 . . . . . 6  |-  ( y  =  n  ->  (
y  e.  ( 1 ... N )  <->  n  e.  ( 1 ... N
) ) )
29 oveq2 6285 . . . . . . . . 9  |-  ( y  =  n  ->  (
1 ... y )  =  ( 1 ... n
) )
3029iuneq1d 4295 . . . . . . . 8  |-  ( y  =  n  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  ( 1 ... n ) ( Q `  k ) )
31 oveq1 6284 . . . . . . . . . . 11  |-  ( y  =  n  ->  (
y  /  N )  =  ( n  /  N ) )
3231oveq2d 6293 . . . . . . . . . 10  |-  ( y  =  n  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( n  /  N
) ) )
3332oveq2d 6293 . . . . . . . . 9  |-  ( y  =  n  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] (
n  /  N ) ) ) )
3433oveq1d 6292 . . . . . . . 8  |-  ( y  =  n  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( n  /  N
) ) )  Cn  C ) )
3530, 34eleq12d 2484 . . . . . . 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 4985 . . . . . . . 8  |-  ( y  =  n  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) ) )
3732reseq2d 5093 . . . . . . . 8  |-  ( y  =  n  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( n  /  N ) ) ) )
3836, 37eqeq12d 2424 . . . . . . 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 709 . . . . . 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 318 . . . . 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 314 . . . 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 2474 . . . . . 6  |-  ( y  =  ( n  + 
1 )  ->  (
y  e.  ( 1 ... N )  <->  ( n  +  1 )  e.  ( 1 ... N
) ) )
43 oveq2 6285 . . . . . . . . 9  |-  ( y  =  ( n  + 
1 )  ->  (
1 ... y )  =  ( 1 ... (
n  +  1 ) ) )
4443iuneq1d 4295 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) )
45 oveq1 6284 . . . . . . . . . . 11  |-  ( y  =  ( n  + 
1 )  ->  (
y  /  N )  =  ( ( n  +  1 )  /  N ) )
4645oveq2d 6293 . . . . . . . . . 10  |-  ( y  =  ( n  + 
1 )  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )
4746oveq2d 6293 . . . . . . . . 9  |-  ( y  =  ( n  + 
1 )  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
4847oveq1d 6292 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )  Cn  C ) )
4944, 48eleq12d 2484 . . . . . . 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 4985 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) ) )
5146reseq2d 5093 . . . . . . . 8  |-  ( y  =  ( n  + 
1 )  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) ) )
5250, 51eqeq12d 2424 . . . . . . 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 709 . . . . . 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 318 . . . . 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 314 . . . 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 2474 . . . . . 6  |-  ( y  =  N  ->  (
y  e.  ( 1 ... N )  <->  N  e.  ( 1 ... N
) ) )
57 oveq2 6285 . . . . . . . . . 10  |-  ( y  =  N  ->  (
1 ... y )  =  ( 1 ... N
) )
5857iuneq1d 4295 . . . . . . . . 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 2461 . . . . . . . 8  |-  ( y  =  N  ->  U_ k  e.  ( 1 ... y
) ( Q `  k )  =  K )
61 oveq1 6284 . . . . . . . . . . 11  |-  ( y  =  N  ->  (
y  /  N )  =  ( N  /  N ) )
6261oveq2d 6293 . . . . . . . . . 10  |-  ( y  =  N  ->  (
0 [,] ( y  /  N ) )  =  ( 0 [,] ( N  /  N
) ) )
6362oveq2d 6293 . . . . . . . . 9  |-  ( y  =  N  ->  ( Lt  ( 0 [,] (
y  /  N ) ) )  =  ( Lt  ( 0 [,] ( N  /  N ) ) ) )
6463oveq1d 6292 . . . . . . . 8  |-  ( y  =  N  ->  (
( Lt  ( 0 [,] ( y  /  N
) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( N  /  N
) ) )  Cn  C ) )
6560, 64eleq12d 2484 . . . . . . 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 4985 . . . . . . . 8  |-  ( y  =  N  ->  ( F  o.  U_ k  e.  ( 1 ... y
) ( Q `  k ) )  =  ( F  o.  K
) )
6762reseq2d 5093 . . . . . . . 8  |-  ( y  =  N  ->  ( G  |`  ( 0 [,] ( y  /  N
) ) )  =  ( G  |`  (
0 [,] ( N  /  N ) ) ) )
6866, 67eqeq12d 2424 . . . . . . 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 709 . . . . . 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 318 . . . . 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 314 . . . 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 11745 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... N
) )
733, 72syl 17 . . . . . . . 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 2402 . . . . . . . . 9  |-  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) )  =  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) )
8674, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem8 29576 . . . . . . . 8  |-  ( (
ph  /\  1  e.  ( 1 ... N
) )  ->  ( Q `  1 )  e.  ( ( Lt  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) ) )  Cn  C ) )
8773, 86mpdan 666 . . . . . . 7  |-  ( ph  ->  ( Q `  1
)  e.  ( ( Lt  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) ) )  Cn  C
) )
88 1m1e0 10644 . . . . . . . . . . . 12  |-  ( 1  -  1 )  =  0
8988oveq1i 6287 . . . . . . . . . . 11  |-  ( ( 1  -  1 )  /  N )  =  ( 0  /  N
)
901nncnd 10591 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  CC )
911nnne0d 10620 . . . . . . . . . . . 12  |-  ( ph  ->  N  =/=  0 )
9290, 91div0d 10359 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  /  N
)  =  0 )
9389, 92syl5eq 2455 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  -  1 )  /  N
)  =  0 )
9493oveq1d 6292 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) )  =  ( 0 [,] ( 1  /  N ) ) )
9594oveq2d 6293 . . . . . . . 8  |-  ( ph  ->  ( Lt  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N
) ) )  =  ( Lt  ( 0 [,] ( 1  /  N
) ) ) )
9695oveq1d 6292 . . . . . . 7  |-  ( ph  ->  ( ( Lt  ( ( ( 1  -  1 )  /  N ) [,] ( 1  /  N ) ) )  Cn  C )  =  ( ( Lt  ( 0 [,] ( 1  /  N ) ) )  Cn  C ) )
9787, 96eleqtrd 2492 . . . . . 6  |-  ( ph  ->  ( Q `  1
)  e.  ( ( Lt  ( 0 [,] (
1  /  N ) ) )  Cn  C
) )
98 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  1  e.  ( 1 ... N
) )  ->  1  e.  ( 1 ... N
) )
9974, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85cvmliftlem7 29575 . . . . . . . . . 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 29574 . . . . . . . . 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 666 . . . . . . . 8  |-  ( ph  ->  ( ( Q ` 
1 ) : ( ( ( 1  -  1 )  /  N
) [,] ( 1  /  N ) ) --> B  /\  ( F  o.  ( Q ` 
1 ) )  =  ( G  |`  (
( ( 1  -  1 )  /  N
) [,] ( 1  /  N ) ) ) ) )
102101simprd 461 . . . . . . 7  |-  ( ph  ->  ( F  o.  ( Q `  1 )
)  =  ( G  |`  ( ( ( 1  -  1 )  /  N ) [,] (
1  /  N ) ) ) )
10394reseq2d 5093 . . . . . . 7  |-  ( ph  ->  ( G  |`  (
( ( 1  -  1 )  /  N
) [,] ( 1  /  N ) ) )  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) )
104102, 103eqtrd 2443 . . . . . 6  |-  ( ph  ->  ( F  o.  ( Q `  1 )
)  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) )
10597, 104jca 530 . . . . 5  |-  ( ph  ->  ( ( Q ` 
1 )  e.  ( ( Lt  ( 0 [,] ( 1  /  N
) ) )  Cn  C )  /\  ( F  o.  ( Q `  1 ) )  =  ( G  |`  ( 0 [,] (
1  /  N ) ) ) ) )
106105a1d 25 . . . 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 11162 . . . . . . . . . . 11  |-  ( n  e.  NN  <->  n  e.  ( ZZ>= `  1 )
)
108107biimpi 194 . . . . . . . . . 10  |-  ( n  e.  NN  ->  n  e.  ( ZZ>= `  1 )
)
109108adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  ( ZZ>= `  1 )
)
110 peano2fzr 11751 . . . . . . . . . 10  |-  ( ( n  e.  ( ZZ>= ` 
1 )  /\  (
n  +  1 )  e.  ( 1 ... N ) )  ->  n  e.  ( 1 ... N ) )
111110ex 432 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  1
)  ->  ( (
n  +  1 )  e.  ( 1 ... N )  ->  n  e.  ( 1 ... N
) ) )
112109, 111syl 17 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( n  +  1 )  e.  ( 1 ... N )  ->  n  e.  ( 1 ... N
) ) )
113112imim1d 75 . . . . . . 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 2402 . . . . . . . . . . . . 13  |-  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) )  =  U. ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) )
116 0re 9625 . . . . . . . . . . . . . . 15  |-  0  e.  RR
117114simplbi 458 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) ) )
118117adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) ) )
119118simprd 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( n  +  1 )  e.  ( 1 ... N ) )
120 elfznn 11766 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  +  1 )  e.  ( 1 ... N )  ->  (
n  +  1 )  e.  NN )
121119, 120syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( n  +  1 )  e.  NN )
122121nnred 10590 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( n  +  1 )  e.  RR )
1231adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  N  e.  NN )
124122, 123nndivred 10624 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( n  + 
1 )  /  N
)  e.  RR )
125 iccssre 11658 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  ( ( n  + 
1 )  /  N
)  e.  RR )  ->  ( 0 [,] ( ( n  + 
1 )  /  N
) )  C_  RR )
126116, 124, 125sylancr 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  C_  RR )
127117simpld 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  n  e.  NN )
128127adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  n  e.  NN )
129128nnred 10590 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  n  e.  RR )
130129, 123nndivred 10624 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  RR )
131 icccld 21564 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  ( n  /  N
)  e.  RR )  ->  ( 0 [,] ( n  /  N
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
132116, 130, 131sylancr 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
13383fveq2i 5851 . . . . . . . . . . . . . . 15  |-  ( Clsd `  L )  =  (
Clsd `  ( topGen ` 
ran  (,) ) )
134132, 133syl6eleqr 2501 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  e.  ( Clsd `  L ) )
135 ssun1 3605 . . . . . . . . . . . . . . 15  |-  ( 0 [,] ( n  /  N ) )  C_  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )
136116a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  0  e.  RR )
137128nnnn0d 10892 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  n  e.  NN0 )
138137nn0ge0d 10895 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  0  <_  n )
139123nnred 10590 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  N  e.  RR )
140123nngt0d 10619 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  0  <  N )
141 divge0 10451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  e.  RR  /\  0  <_  n )  /\  ( N  e.  RR  /\  0  <  N ) )  ->  0  <_  ( n  /  N ) )
142129, 138, 139, 140, 141syl22anc 1231 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  0  <_  ( n  /  N ) )
143129ltp1d 10515 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  n  <  ( n  +  1 ) )
144 ltdiv1 10446 . . . . . . . . . . . . . . . . . . . 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 1234 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  <  (
n  +  1 )  <-> 
( n  /  N
)  <  ( (
n  +  1 )  /  N ) ) )
146143, 145mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  <  ( (
n  +  1 )  /  N ) )
147130, 124, 146ltled 9764 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  <_  ( (
n  +  1 )  /  N ) )
148 elicc2 11641 . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . 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 1180 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( 0 [,] ( ( n  +  1 )  /  N ) ) )
151 iccsplit 11705 . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  =  ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) )
153135, 152syl5sseqr 3490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  C_  ( 0 [,] ( ( n  +  1 )  /  N ) ) )
154 uniretop 21559 . . . . . . . . . . . . . . . 16  |-  RR  =  U. ( topGen `  ran  (,) )
15583unieqi 4199 . . . . . . . . . . . . . . . 16  |-  U. L  =  U. ( topGen `  ran  (,) )
156154, 155eqtr4i 2434 . . . . . . . . . . . . . . 15  |-  RR  =  U. L
157156restcldi 19965 . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  e.  ( Clsd `  ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) ) ) )
159 icccld 21564 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  /  N
)  e.  RR  /\  ( ( n  + 
1 )  /  N
)  e.  RR )  ->  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
160130, 124, 159syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  e.  ( Clsd `  ( topGen `  ran  (,) )
) )
161160, 133syl6eleqr 2501 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  e.  ( Clsd `  L ) )
162 ssun2 3606 . . . . . . . . . . . . . . 15  |-  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) )  C_  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )
163162, 152syl5sseqr 3490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  C_  ( 0 [,] ( ( n  +  1 )  /  N ) ) )
164156restcldi 19965 . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) )  e.  ( Clsd `  ( Lt  ( 0 [,] ( ( n  + 
1 )  /  N
) ) ) ) )
166 retop 21558 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  e.  Top
16783, 166eqeltri 2486 . . . . . . . . . . . . . . 15  |-  L  e. 
Top
168156restuni 19954 . . . . . . . . . . . . . . 15  |-  ( ( L  e.  Top  /\  ( 0 [,] (
( n  +  1 )  /  N ) )  C_  RR )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  =  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
169167, 126, 168sylancr 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  =  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
170152, 169eqtr3d 2445 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
171114simprbi 462 . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
) )
174 eqid 2402 . . . . . . . . . . . . . . . . . . 19  |-  U. ( Lt  ( 0 [,] (
n  /  N ) ) )  =  U. ( Lt  ( 0 [,] ( n  /  N
) ) )
175174, 75cnf 20038 . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
n  /  N ) ) ) --> B )
177 iccssre 11658 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR  /\  ( n  /  N
)  e.  RR )  ->  ( 0 [,] ( n  /  N
) )  C_  RR )
178116, 130, 177sylancr 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  C_  RR )
179156restuni 19954 . . . . . . . . . . . . . . . . . . 19  |-  ( ( L  e.  Top  /\  ( 0 [,] (
n  /  N ) )  C_  RR )  ->  ( 0 [,] (
n  /  N ) )  =  U. ( Lt  ( 0 [,] (
n  /  N ) ) ) )
180167, 178, 179sylancr 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
n  /  N ) )  =  U. ( Lt  ( 0 [,] (
n  /  N ) ) ) )
181180feq2d 5700 . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
) : ( 0 [,] ( n  /  N ) ) --> B )
183 eqid 2402 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) )  =  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) )
184 simpr 459 . . . . . . . . . . . . . . . . . . . 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 29575 . . . . . . . . . . . . . . . . . . . 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 29574 . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) ) : ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) ) --> B )
189128nncnd 10591 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  n  e.  CC )
190 ax-1cn 9579 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
191 pncan 9861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  CC  /\  1  e.  CC )  ->  ( ( n  + 
1 )  -  1 )  =  n )
192189, 190, 191sylancl 660 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  ( ( n  + 
1 )  -  1 )  =  n )
193192oveq1d 6292 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( ( ( n  +  1 )  - 
1 )  /  N
)  =  ( n  /  N ) )
194193oveq1d 6292 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) )  =  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
195194feq2d 5700 . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) ) : ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) --> B )
197 ffun 5715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) : ( 0 [,] ( n  /  N
) ) --> B  ->  Fun  U_ k  e.  ( 1 ... n ) ( Q `  k
) )
198182, 197syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  Fun  U_ k  e.  ( 1 ... n ) ( Q `  k
) )
199128, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  n  e.  ( ZZ>= ` 
1 ) )
200 eluzfz2 11746 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  ( ZZ>= `  1
)  ->  n  e.  ( 1 ... n
) )
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ch )  ->  n  e.  ( 1 ... n ) )
202 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  n  ->  ( Q `  k )  =  ( Q `  n ) )
203202ssiun2s 4314 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... n )  ->  ( Q `  n )  C_ 
U_ k  e.  ( 1 ... n ) ( Q `  k
) )
204201, 203syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( Q `  n
)  C_  U_ k  e.  ( 1 ... n
) ( Q `  k ) )
205 peano2rem 9921 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  e.  RR  ->  (
n  -  1 )  e.  RR )
206129, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  ( n  -  1 )  e.  RR )
207206, 123nndivred 10624 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  e.  RR )
208207rexrd 9672 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  e.  RR* )
209130rexrd 9672 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  RR* )
210129ltm1d 10517 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  ( n  -  1 )  <  n )
211 ltdiv1 10446 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1234 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  <  n  <->  ( ( n  -  1 )  /  N )  <  ( n  /  N ) ) )
213210, 212mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  <  ( n  /  N ) )
214207, 130, 213ltled 9764 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( ( n  - 
1 )  /  N
)  <_  ( n  /  N ) )
215 ubicc2 11689 . . . . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) )
217199, 119, 110syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ch )  ->  n  e.  ( 1 ... N ) )
218 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) )  =  ( ( ( n  -  1 )  /  N ) [,] (
n  /  N ) )
219 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  ( 1 ... N
) )
22074, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218cvmliftlem7 29575 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29574 . . . . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ch )  ->  ( ( Q `  n ) : ( ( ( n  - 
1 )  /  N
) [,] ( n  /  N ) ) --> B  /\  ( F  o.  ( Q `  n ) )  =  ( G  |`  (
( ( n  - 
1 )  /  N
) [,] ( n  /  N ) ) ) ) )
223222simpld 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ch )  ->  ( Q `  n
) : ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) --> B )
224 fdm 5717 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Q `  n ) : ( ( ( n  -  1 )  /  N ) [,] ( n  /  N
) ) --> B  ->  dom  ( Q `  n
)  =  ( ( ( n  -  1 )  /  N ) [,] ( n  /  N ) ) )
225223, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ch )  ->  dom  ( Q `  n )  =  ( ( ( n  - 
1 )  /  N
) [,] ( n  /  N ) ) )
226216, 225eleqtrrd 2493 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  dom  ( Q `  n )
)
227 funssfv 5863 . . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k ) `  (
n  /  N ) )  =  ( ( Q `  n ) `
 ( n  /  N ) ) )
229192fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( Q `  (
( n  +  1 )  -  1 ) )  =  ( Q `
 n ) )
230229, 193fveq12d 5854 . . . . . . . . . . . . . . . . . . . . 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 29577 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  (
( Q `  (
n  +  1 ) ) `  ( ( ( n  +  1 )  -  1 )  /  N ) )  =  ( ( Q `
 ( ( n  +  1 )  - 
1 ) ) `  ( ( ( n  +  1 )  - 
1 )  /  N
) ) )
232119, 231syldan 468 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  ( ( n  +  1 )  -  1 ) ) `
 ( ( ( n  +  1 )  -  1 )  /  N ) ) )
233193fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) )
234232, 233eqtr3d 2445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( ( n  + 
1 )  -  1 ) ) `  (
( ( n  + 
1 )  -  1 )  /  N ) )  =  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) )
235228, 230, 2343eqtr2d 2449 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k ) `  (
n  /  N ) )  =  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) )
236235opeq2d 4165 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  -> 
<. ( n  /  N
) ,  ( U_ k  e.  ( 1 ... n ) ( Q `  k ) `
 ( n  /  N ) ) >.  =  <. ( n  /  N ) ,  ( ( Q `  (
n  +  1 ) ) `  ( n  /  N ) )
>. )
237236sneqd 3983 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  { <. ( n  /  N ) ,  (
U_ k  e.  ( 1 ... n ) ( Q `  k
) `  ( n  /  N ) ) >. }  =  { <. (
n  /  N ) ,  ( ( Q `
 ( n  + 
1 ) ) `  ( n  /  N
) ) >. } )
238 ffn 5713 . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... n ) ( Q `  k
)  Fn  ( 0 [,] ( n  /  N ) ) )
240 0xr 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  RR*
241240a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  0  e.  RR* )
242 ubicc2 11689 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  RR*  /\  (
n  /  N )  e.  RR*  /\  0  <_  ( n  /  N
) )  ->  (
n  /  N )  e.  ( 0 [,] ( n  /  N
) ) )
243241, 209, 142, 242syl3anc 1230 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( 0 [,] ( n  /  N ) ) )
244 fnressn 6062 . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Q `  ( n  +  1 ) ) : ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) --> B  -> 
( Q `  (
n  +  1 ) )  Fn  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
247196, 246syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) )  Fn  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
248124rexrd 9672 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  ( ( n  + 
1 )  /  N
)  e.  RR* )
249 lbicc2 11688 . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( n  /  N
)  e.  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )
251 fnressn 6062 . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) )  |`  { ( n  /  N ) } )  =  { <. ( n  /  N
) ,  ( ( Q `  ( n  +  1 ) ) `
 ( n  /  N ) ) >. } )
253237, 245, 2523eqtr4d 2453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  |`  { ( n  /  N ) } )  =  ( ( Q `  (
n  +  1 ) )  |`  { (
n  /  N ) } ) )
254 df-icc 11588 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  =  ( x  e.  RR* ,  y  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <_  y ) } )
255 xrmaxle 11436 . . . . . . . . . . . . . . . . . . . . 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 11437 . . . . . . . . . . . . . . . . . . . . 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 11598 . . . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
259142iftrued 3892 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  if ( 0  <_ 
( n  /  N
) ,  ( n  /  N ) ,  0 )  =  ( n  /  N ) )
260147iftrued 3892 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ch )  ->  if ( ( n  /  N )  <_ 
( ( n  + 
1 )  /  N
) ,  ( n  /  N ) ,  ( ( n  + 
1 )  /  N
) )  =  ( n  /  N ) )
261259, 260oveq12d 6295 . . . . . . . . . . . . . . . . . . 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 ) ) )
262 iccid 11626 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  /  N )  e.  RR*  ->  ( ( n  /  N ) [,] ( n  /  N ) )  =  { ( n  /  N ) } )
263209, 262syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ch )  ->  ( ( n  /  N ) [,] (
n  /  N ) )  =  { ( n  /  N ) } )
264258, 261, 2633eqtrd 2447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( ( 0 [,] ( n  /  N
) )  i^i  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  { ( n  /  N ) } )
265264reseq2d 5093 . . . . . . . . . . . . . . . . 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 ) } ) )
266264reseq2d 5093 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  ( ( Q `  ( n  +  1
) )  |`  (
( 0 [,] (
n  /  N ) )  i^i  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( Q `  ( n  +  1 ) )  |`  { ( n  /  N ) } ) )
267253, 265, 2663eqtr4d 2453 . . . . . . . . . . . . . . . 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 ) ) ) ) )
268 fresaun 5738 . . . . . . . . . . . . . . . 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 )
269182, 196, 267, 268syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) ) : ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) --> B )
270 fzsuc 11780 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( n  + 
1 ) )  =  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) )
271199, 270syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ch )  ->  ( 1 ... (
n  +  1 ) )  =  ( ( 1 ... n )  u.  { ( n  +  1 ) } ) )
272271iuneq1d 4295 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
)  =  U_ k  e.  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) ( Q `  k ) )
273 iunxun 4355 . . . . . . . . . . . . . . . . . 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 ) )
274 ovex 6305 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  +  1 )  e. 
_V
275 fveq2 5848 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  ( n  + 
1 )  ->  ( Q `  k )  =  ( Q `  ( n  +  1
) ) )
276274, 275iunxsn 4353 . . . . . . . . . . . . . . . . . . 19  |-  U_ k  e.  { ( n  + 
1 ) }  ( Q `  k )  =  ( Q `  ( n  +  1
) )
277276uneq2i 3593 . . . . . . . . . . . . . . . . . 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
) ) )
278273, 277eqtri 2431 . . . . . . . . . . . . . . . . 17  |-  U_ k  e.  ( ( 1 ... n )  u.  {
( n  +  1 ) } ) ( Q `  k )  =  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )
279272, 278syl6req 2460 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  =  U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k ) )
280279feq1d 5699 . . . . . . . . . . . . . . 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 ) )
281269, 280mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) : ( ( 0 [,] ( n  /  N ) )  u.  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) --> B )
282170feq2d 5700 . . . . . . . . . . . . . 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 ) )
283281, 282mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
) : U. ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) ) --> B )
284279reseq1d 5092 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
285 fresaunres1 5740 . . . . . . . . . . . . . . . 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_ k  e.  ( 1 ... n ) ( Q `  k ) )
286182, 196, 267, 285syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  |`  ( 0 [,] ( n  /  N ) ) )  =  U_ k  e.  ( 1 ... n
) ( Q `  k ) )
287284, 286eqtr3d 2445 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
0 [,] ( n  /  N ) ) )  =  U_ k  e.  ( 1 ... n
) ( Q `  k ) )
288167a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  L  e.  Top )
289 ovex 6305 . . . . . . . . . . . . . . . . 17  |-  ( 0 [,] ( ( n  +  1 )  /  N ) )  e. 
_V
290289a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( 0 [,] (
( n  +  1 )  /  N ) )  e.  _V )
291 restabs 19957 . . . . . . . . . . . . . . . 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 ) ) ) )
292288, 153, 290, 291syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( 0 [,] ( n  /  N ) ) )  =  ( Lt  ( 0 [,] ( n  /  N ) ) ) )
293292oveq1d 6292 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( 0 [,] (
n  /  N ) ) )  Cn  C
)  =  ( ( Lt  ( 0 [,] (
n  /  N ) ) )  Cn  C
) )
294173, 287, 2933eltr4d 2505 . . . . . . . . . . . . 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 ) )
29574, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183cvmliftlem8 29576 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( n  +  1 )  e.  ( 1 ... N
) )  ->  ( Q `  ( n  +  1 ) )  e.  ( ( Lt  ( ( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C ) )
296119, 295syldan 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) )  e.  ( ( Lt  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
297194oveq2d 6293 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( Lt  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] ( ( n  + 
1 )  /  N
) ) )  =  ( Lt  ( ( n  /  N ) [,] ( ( n  + 
1 )  /  N
) ) ) )
298297oveq1d 6292 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( Lt  ( ( ( ( n  + 
1 )  -  1 )  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C )  =  ( ( Lt  ( ( n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  Cn  C ) )
299296, 298eleqtrd 2492 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( Q `  (
n  +  1 ) )  e.  ( ( Lt  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
300279reseq1d 5092 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
301 fresaunres2 5739 . . . . . . . . . . . . . . . 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
) ) )  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  =  ( Q `  ( n  +  1 ) ) )
302182, 196, 267, 301syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( U_ k  e.  ( 1 ... n
) ( Q `  k )  u.  ( Q `  ( n  +  1 ) ) )  |`  ( (
n  /  N ) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Q `  ( n  +  1
) ) )
303300, 302eqtr3d 2445 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( U_ k  e.  ( 1 ... (
n  +  1 ) ) ( Q `  k )  |`  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Q `
 ( n  + 
1 ) ) )
304 restabs 19957 . . . . . . . . . . . . . . . 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 ) ) ) )
305288, 163, 290, 304syl3anc 1230 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( Lt  ( ( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )
306305oveq1d 6292 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ch )  ->  ( ( ( Lt  ( 0 [,] ( ( n  +  1 )  /  N ) ) )t  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
)  =  ( ( Lt  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
307299, 303, 3063eltr4d 2505 . . . . . . . . . . . . 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 ) )
308115, 75, 158, 165, 170, 283, 294, 307paste 20086 . . . . . . . . . . . 12  |-  ( (
ph  /\  ch )  ->  U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) )  Cn  C
) )
309152reseq2d 5093 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ch )  ->  ( G  |`  (
0 [,] ( ( n  +  1 )  /  N ) ) )  =  ( G  |`  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) ) )
310172simprd 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
n  /  N ) ) ) )
311187simprd 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( F  o.  ( Q `  ( n  +  1 ) ) )  =  ( G  |`  ( ( ( ( n  +  1 )  -  1 )  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
312194reseq2d 5093 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ch )  ->  ( G  |`  (
( ( ( n  +  1 )  - 
1 )  /  N
) [,] ( ( n  +  1 )  /  N ) ) )  =  ( G  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
313311, 312eqtrd 2443 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ch )  ->  ( F  o.  ( Q `  ( n  +  1 ) ) )  =  ( G  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
314310, 313uneq12d 3597 . . . . . . . . . . . . . 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
) ) ) ) )
315 coundi 5323 . . . . . . . . . . . . . 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
) ) ) )
316 resundi 5106 . . . . . . . . . . . . . 14  |-  ( G  |`  ( ( 0 [,] ( n  /  N
) )  u.  (
( n  /  N
) [,] ( ( n  +  1 )  /  N ) ) ) )  =  ( ( G  |`  (
0 [,] ( n  /  N ) ) )  u.  ( G  |`  ( ( n  /  N ) [,] (
( n  +  1 )  /  N ) ) ) )
317314, 315, 3163eqtr4g 2468 . . . . . . . . . . . . 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 ) ) ) ) )
318279coeq2d 4985 . . . . . . . . . . . . 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 ) ) )
319309, 317, 3183eqtr2rd 2450 . . . . . . . . . . . 12  |-  ( (
ph  /\  ch )  ->  ( F  o.  U_ k  e.  ( 1 ... ( n  + 
1 ) ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] (
( n  +  1 )  /  N ) ) ) )
320308, 319jca 530 . . . . . . . . . . 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 ) ) ) ) )
321114, 320sylan2br 474 . . . . . . . . . 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 ) ) ) ) )
322321expr 613 . . . . . . . . 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 ) ) ) ) ) )
323322expr 613 . . . . . . . 8  |-  ( (
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 ) ) ) ) ) ) )
324323a2d 26 . . . . . . 7  |-  ( (
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 ) ) ) ) )  ->  (
( n  +  1 )  e.  ( 1 ... N )  -> 
( U_ k  e.  ( 1 ... ( n  +  1 ) ) ( Q `  k
)  e.  ( ( Lt  ( 0 [,] (
( n  +  1 )  /  N ) ) )