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 | ¬ v 𝒫 U Fin u v
heibor.4 G = y n | n 0 y F n y B n K
heibor.5 B = z X , m 0 z ball D 1 2 m
heibor.6 φ D CMet X
heibor.7 φ F : 0 𝒫 X Fin
heibor.8 φ n 0 X = y F n y B n
heibor.9 φ x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K
heibor.10 φ C G 0
heibor.11 S = seq 0 T m 0 if m = 0 C m 1
heibor.12 M = n S n 3 2 n
Assertion heiborlem7 r + k 2 nd M k < r

Proof

Step Hyp Ref Expression
1 heibor.1 J = MetOpen D
2 heibor.3 K = u | ¬ v 𝒫 U Fin u v
3 heibor.4 G = y n | n 0 y F n y B n K
4 heibor.5 B = z X , m 0 z ball D 1 2 m
5 heibor.6 φ D CMet X
6 heibor.7 φ F : 0 𝒫 X Fin
7 heibor.8 φ n 0 X = y F n y B n
8 heibor.9 φ x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K
9 heibor.10 φ C G 0
10 heibor.11 S = seq 0 T m 0 if m = 0 C m 1
11 heibor.12 M = n S n 3 2 n
12 3re 3
13 3pos 0 < 3
14 12 13 elrpii 3 +
15 rpdivcl r + 3 + r 3 +
16 14 15 mpan2 r + r 3 +
17 2re 2
18 1lt2 1 < 2
19 expnlbnd r 3 + 2 1 < 2 k 1 2 k < r 3
20 17 18 19 mp3an23 r 3 + k 1 2 k < r 3
21 16 20 syl r + k 1 2 k < r 3
22 2nn 2
23 nnnn0 k k 0
24 nnexpcl 2 k 0 2 k
25 22 23 24 sylancr k 2 k
26 25 nnrpd k 2 k +
27 rpcn 2 k + 2 k
28 rpne0 2 k + 2 k 0
29 3cn 3
30 divrec 3 2 k 2 k 0 3 2 k = 3 1 2 k
31 29 30 mp3an1 2 k 2 k 0 3 2 k = 3 1 2 k
32 27 28 31 syl2anc 2 k + 3 2 k = 3 1 2 k
33 26 32 syl k 3 2 k = 3 1 2 k
34 33 adantl r + k 3 2 k = 3 1 2 k
35 34 breq1d r + k 3 2 k < r 3 1 2 k < r
36 25 nnrecred k 1 2 k
37 rpre r + r
38 12 13 pm3.2i 3 0 < 3
39 ltmuldiv2 1 2 k r 3 0 < 3 3 1 2 k < r 1 2 k < r 3
40 38 39 mp3an3 1 2 k r 3 1 2 k < r 1 2 k < r 3
41 36 37 40 syl2anr r + k 3 1 2 k < r 1 2 k < r 3
42 35 41 bitrd r + k 3 2 k < r 1 2 k < r 3
43 42 rexbidva r + k 3 2 k < r k 1 2 k < r 3
44 21 43 mpbird r + k 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 V
50 48 11 49 fvmpt k M k = S k 3 2 k
51 50 fveq2d k 2 nd M k = 2 nd S k 3 2 k
52 fvex S k V
53 ovex 3 2 k V
54 52 53 op2nd 2 nd S k 3 2 k = 3 2 k
55 51 54 eqtrdi k 2 nd M k = 3 2 k
56 55 breq1d k 2 nd M k < r 3 2 k < r
57 56 rexbiia k 2 nd M k < r k 3 2 k < r
58 44 57 sylibr r + k 2 nd M k < r
59 58 rgen r + k 2 nd M k < r