Metamath Proof Explorer

Theorem heiborlem7

Description: Lemma for heibor . Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014)

Ref Expression
Hypotheses heibor.1 
|- J = ( MetOpen ` D )
heibor.3 
|- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
heibor.4 
|- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
heibor.5 
|- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
heibor.6 
|- ( ph -> D e. ( CMet ` X ) )
heibor.7 
|- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
heibor.8 
|- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
heibor.9 
|- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
heibor.10 
|- ( ph -> C G 0 )
heibor.11 
|- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )
heibor.12 
|- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )
Assertion heiborlem7 
|- A. r e. RR+ E. k e. NN ( 2nd ` ( M ` k ) ) < r

Proof

Step Hyp Ref Expression
1 heibor.1 
 |-  J = ( MetOpen ` D )
2 heibor.3 
 |-  K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
3 heibor.4 
 |-  G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
4 heibor.5 
 |-  B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
5 heibor.6 
 |-  ( ph -> D e. ( CMet ` X ) )
6 heibor.7 
 |-  ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
7 heibor.8 
 |-  ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
8 heibor.9 
 |-  ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
9 heibor.10 
 |-  ( ph -> C G 0 )
10 heibor.11 
 |-  S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )
11 heibor.12 
 |-  M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )
12 3re 
 |-  3 e. RR
13 3pos 
 |-  0 < 3
14 12 13 elrpii 
 |-  3 e. RR+
15 rpdivcl 
 |-  ( ( r e. RR+ /\ 3 e. RR+ ) -> ( r / 3 ) e. RR+ )
16 14 15 mpan2 
 |-  ( r e. RR+ -> ( r / 3 ) e. RR+ )
17 2re 
 |-  2 e. RR
18 1lt2 
 |-  1 < 2
19 expnlbnd 
 |-  ( ( ( r / 3 ) e. RR+ /\ 2 e. RR /\ 1 < 2 ) -> E. k e. NN ( 1 / ( 2 ^ k ) ) < ( r / 3 ) )
20 17 18 19 mp3an23 
 |-  ( ( r / 3 ) e. RR+ -> E. k e. NN ( 1 / ( 2 ^ k ) ) < ( r / 3 ) )
21 16 20 syl 
 |-  ( r e. RR+ -> E. k e. NN ( 1 / ( 2 ^ k ) ) < ( r / 3 ) )
22 2nn 
 |-  2 e. NN
23 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
24 nnexpcl 
 |-  ( ( 2 e. NN /\ k e. NN0 ) -> ( 2 ^ k ) e. NN )
25 22 23 24 sylancr 
 |-  ( k e. NN -> ( 2 ^ k ) e. NN )
26 25 nnrpd 
 |-  ( k e. NN -> ( 2 ^ k ) e. RR+ )
27 rpcn 
 |-  ( ( 2 ^ k ) e. RR+ -> ( 2 ^ k ) e. CC )
28 rpne0 
 |-  ( ( 2 ^ k ) e. RR+ -> ( 2 ^ k ) =/= 0 )
29 3cn 
 |-  3 e. CC
30 divrec 
 |-  ( ( 3 e. CC /\ ( 2 ^ k ) e. CC /\ ( 2 ^ k ) =/= 0 ) -> ( 3 / ( 2 ^ k ) ) = ( 3 x. ( 1 / ( 2 ^ k ) ) ) )
31 29 30 mp3an1 
 |-  ( ( ( 2 ^ k ) e. CC /\ ( 2 ^ k ) =/= 0 ) -> ( 3 / ( 2 ^ k ) ) = ( 3 x. ( 1 / ( 2 ^ k ) ) ) )
32 27 28 31 syl2anc 
 |-  ( ( 2 ^ k ) e. RR+ -> ( 3 / ( 2 ^ k ) ) = ( 3 x. ( 1 / ( 2 ^ k ) ) ) )
33 26 32 syl 
 |-  ( k e. NN -> ( 3 / ( 2 ^ k ) ) = ( 3 x. ( 1 / ( 2 ^ k ) ) ) )
34 33 adantl 
 |-  ( ( r e. RR+ /\ k e. NN ) -> ( 3 / ( 2 ^ k ) ) = ( 3 x. ( 1 / ( 2 ^ k ) ) ) )
35 34 breq1d 
 |-  ( ( r e. RR+ /\ k e. NN ) -> ( ( 3 / ( 2 ^ k ) ) < r <-> ( 3 x. ( 1 / ( 2 ^ k ) ) ) < r ) )
36 25 nnrecred 
 |-  ( k e. NN -> ( 1 / ( 2 ^ k ) ) e. RR )
37 rpre 
 |-  ( r e. RR+ -> r e. RR )
38 12 13 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
39 ltmuldiv2 
 |-  ( ( ( 1 / ( 2 ^ k ) ) e. RR /\ r e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( 3 x. ( 1 / ( 2 ^ k ) ) ) < r <-> ( 1 / ( 2 ^ k ) ) < ( r / 3 ) ) )
40 38 39 mp3an3 
 |-  ( ( ( 1 / ( 2 ^ k ) ) e. RR /\ r e. RR ) -> ( ( 3 x. ( 1 / ( 2 ^ k ) ) ) < r <-> ( 1 / ( 2 ^ k ) ) < ( r / 3 ) ) )
41 36 37 40 syl2anr 
 |-  ( ( r e. RR+ /\ k e. NN ) -> ( ( 3 x. ( 1 / ( 2 ^ k ) ) ) < r <-> ( 1 / ( 2 ^ k ) ) < ( r / 3 ) ) )
42 35 41 bitrd 
 |-  ( ( r e. RR+ /\ k e. NN ) -> ( ( 3 / ( 2 ^ k ) ) < r <-> ( 1 / ( 2 ^ k ) ) < ( r / 3 ) ) )
43 42 rexbidva 
 |-  ( r e. RR+ -> ( E. k e. NN ( 3 / ( 2 ^ k ) ) < r <-> E. k e. NN ( 1 / ( 2 ^ k ) ) < ( r / 3 ) ) )
44 21 43 mpbird 
 |-  ( r e. RR+ -> E. k e. NN ( 3 / ( 2 ^ k ) ) < r )
45 fveq2 
 |-  ( n = k -> ( S ` n ) = ( S ` k ) )
46 oveq2 
 |-  ( n = k -> ( 2 ^ n ) = ( 2 ^ k ) )
47 46 oveq2d 
 |-  ( n = k -> ( 3 / ( 2 ^ n ) ) = ( 3 / ( 2 ^ k ) ) )
48 45 47 opeq12d 
 |-  ( n = k -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. = <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. )
49 opex 
 |-  <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. e. _V
50 48 11 49 fvmpt 
 |-  ( k e. NN -> ( M ` k ) = <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. )
51 50 fveq2d 
 |-  ( k e. NN -> ( 2nd ` ( M ` k ) ) = ( 2nd ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) )
52 fvex 
 |-  ( S ` k ) e. _V
53 ovex 
 |-  ( 3 / ( 2 ^ k ) ) e. _V
54 52 53 op2nd 
 |-  ( 2nd ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) = ( 3 / ( 2 ^ k ) )
55 51 54 eqtrdi 
 |-  ( k e. NN -> ( 2nd ` ( M ` k ) ) = ( 3 / ( 2 ^ k ) ) )
56 55 breq1d 
 |-  ( k e. NN -> ( ( 2nd ` ( M ` k ) ) < r <-> ( 3 / ( 2 ^ k ) ) < r ) )
57 56 rexbiia 
 |-  ( E. k e. NN ( 2nd ` ( M ` k ) ) < r <-> E. k e. NN ( 3 / ( 2 ^ k ) ) < r )
58 44 57 sylibr 
 |-  ( r e. RR+ -> E. k e. NN ( 2nd ` ( M ` k ) ) < r )
59 58 rgen 
 |-  A. r e. RR+ E. k e. NN ( 2nd ` ( M ` k ) ) < r