Metamath Proof Explorer

Theorem cvmliftlem2

Description: Lemma for cvmlift . W = [ ( k - 1 ) / N , k / N ] is a subset of [ 0 , 1 ] for each M e. ( 1 ... N ) . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses 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. ( ( C |`t u ) Homeo ( J |`t 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 (,) )
cvmliftlem1.m 
|- ( ( ph /\ ps ) -> M e. ( 1 ... N ) )
cvmliftlem3.3 
|- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
Assertion cvmliftlem2 
|- ( ( ph /\ ps ) -> W C_ ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 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. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmliftlem.b 
 |-  B = U. C
3 cvmliftlem.x 
 |-  X = U. J
4 cvmliftlem.f 
 |-  ( ph -> F e. ( C CovMap J ) )
5 cvmliftlem.g 
 |-  ( ph -> G e. ( II Cn J ) )
6 cvmliftlem.p 
 |-  ( ph -> P e. B )
7 cvmliftlem.e 
 |-  ( ph -> ( F ` P ) = ( G ` 0 ) )
8 cvmliftlem.n 
 |-  ( ph -> N e. NN )
9 cvmliftlem.t 
 |-  ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
10 cvmliftlem.a 
 |-  ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
11 cvmliftlem.l 
 |-  L = ( topGen ` ran (,) )
12 cvmliftlem1.m 
 |-  ( ( ph /\ ps ) -> M e. ( 1 ... N ) )
13 cvmliftlem3.3 
 |-  W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
14 0red 
 |-  ( ( ph /\ ps ) -> 0 e. RR )
15 1red 
 |-  ( ( ph /\ ps ) -> 1 e. RR )
16 elfznn 
 |-  ( M e. ( 1 ... N ) -> M e. NN )
17 12 16 syl 
 |-  ( ( ph /\ ps ) -> M e. NN )
18 17 nnred 
 |-  ( ( ph /\ ps ) -> M e. RR )
19 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
20 18 19 syl 
 |-  ( ( ph /\ ps ) -> ( M - 1 ) e. RR )
21 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
22 17 21 syl 
 |-  ( ( ph /\ ps ) -> ( M - 1 ) e. NN0 )
23 22 nn0ge0d 
 |-  ( ( ph /\ ps ) -> 0 <_ ( M - 1 ) )
24 8 adantr 
 |-  ( ( ph /\ ps ) -> N e. NN )
25 24 nnred 
 |-  ( ( ph /\ ps ) -> N e. RR )
26 24 nngt0d 
 |-  ( ( ph /\ ps ) -> 0 < N )
27 divge0 
 |-  ( ( ( ( M - 1 ) e. RR /\ 0 <_ ( M - 1 ) ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( ( M - 1 ) / N ) )
28 20 23 25 26 27 syl22anc 
 |-  ( ( ph /\ ps ) -> 0 <_ ( ( M - 1 ) / N ) )
29 elfzle2 
 |-  ( M e. ( 1 ... N ) -> M <_ N )
30 12 29 syl 
 |-  ( ( ph /\ ps ) -> M <_ N )
31 24 nncnd 
 |-  ( ( ph /\ ps ) -> N e. CC )
32 31 mulid1d 
 |-  ( ( ph /\ ps ) -> ( N x. 1 ) = N )
33 30 32 breqtrrd 
 |-  ( ( ph /\ ps ) -> M <_ ( N x. 1 ) )
34 ledivmul 
 |-  ( ( M e. RR /\ 1 e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( M / N ) <_ 1 <-> M <_ ( N x. 1 ) ) )
35 18 15 25 26 34 syl112anc 
 |-  ( ( ph /\ ps ) -> ( ( M / N ) <_ 1 <-> M <_ ( N x. 1 ) ) )
36 33 35 mpbird 
 |-  ( ( ph /\ ps ) -> ( M / N ) <_ 1 )
37 iccss 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ ( ( M - 1 ) / N ) /\ ( M / N ) <_ 1 ) ) -> ( ( ( M - 1 ) / N ) [,] ( M / N ) ) C_ ( 0 [,] 1 ) )
38 14 15 28 36 37 syl22anc 
 |-  ( ( ph /\ ps ) -> ( ( ( M - 1 ) / N ) [,] ( M / N ) ) C_ ( 0 [,] 1 ) )
39 13 38 eqsstrid 
 |-  ( ( ph /\ ps ) -> W C_ ( 0 [,] 1 ) )