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 \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
	heibor.4	$⊢ G = \{⟨y, n⟩ \| (n \in ℕ_{0} \land y \in F (n) \land y B n \in K)\}$
	heibor.5	$⊢ B = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
	heibor.6	$⊢ φ \to D \in CMet (X)$
	heibor.7	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
	heibor.8	$⊢ φ \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
	heibor.9	$⊢ φ \to \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K)$
	heibor.10	$⊢ φ \to C G 0$
	heibor.11	$⊢ S = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)))$
	heibor.12	$⊢ M = (n \in ℕ ⟼ ⟨S (n), \frac{3}{2^{n}}⟩)$
Assertion	heiborlem7	$⊢ \forall r \in ℝ^{+} \exists k \in ℕ 2^{nd} (M (k)) < r$

Proof

Step	Hyp	Ref	Expression
1		heibor.1	$⊢ J = MetOpen (D)$
2		heibor.3	$⊢ K = \{u \| \neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v\}$
3		heibor.4	$⊢ G = \{⟨y, n⟩ \| (n \in ℕ_{0} \land y \in F (n) \land y B n \in K)\}$
4		heibor.5	$⊢ B = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
5		heibor.6	$⊢ φ \to D \in CMet (X)$
6		heibor.7	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X \cap Fin$
7		heibor.8	$⊢ φ \to \forall n \in ℕ_{0} X = ⋃_{y \in F (n)} (y B n)$
8		heibor.9	$⊢ φ \to \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K)$
9		heibor.10	$⊢ φ \to C G 0$
10		heibor.11	$⊢ S = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)))$
11		heibor.12	$⊢ M = (n \in ℕ ⟼ ⟨S (n), \frac{3}{2^{n}}⟩)$
12		3re	$⊢ 3 \in ℝ$
13		3pos	$⊢ 0 < 3$
14	12 13	elrpii	$⊢ 3 \in ℝ^{+}$
15		rpdivcl	$⊢ (r \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{r}{3} \in ℝ^{+}$
16	14 15	mpan2	$⊢ r \in ℝ^{+} \to \frac{r}{3} \in ℝ^{+}$
17		2re	$⊢ 2 \in ℝ$
18		1lt2	$⊢ 1 < 2$
19		expnlbnd	$⊢ (\frac{r}{3} \in ℝ^{+} \land 2 \in ℝ \land 1 < 2) \to \exists k \in ℕ \frac{1}{2^{k}} < \frac{r}{3}$
20	17 18 19	mp3an23	$⊢ \frac{r}{3} \in ℝ^{+} \to \exists k \in ℕ \frac{1}{2^{k}} < \frac{r}{3}$
21	16 20	syl	$⊢ r \in ℝ^{+} \to \exists k \in ℕ \frac{1}{2^{k}} < \frac{r}{3}$
22		2nn	$⊢ 2 \in ℕ$
23		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
24		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
25	22 23 24	sylancr	$⊢ k \in ℕ \to 2^{k} \in ℕ$
26	25	nnrpd	$⊢ k \in ℕ \to 2^{k} \in ℝ^{+}$
27		rpcn	$⊢ 2^{k} \in ℝ^{+} \to 2^{k} \in ℂ$
28		rpne0	$⊢ 2^{k} \in ℝ^{+} \to 2^{k} \neq 0$
29		3cn	$⊢ 3 \in ℂ$
30		divrec	$⊢ (3 \in ℂ \land 2^{k} \in ℂ \land 2^{k} \neq 0) \to \frac{3}{2^{k}} = 3 (\frac{1}{2^{k}})$
31	29 30	mp3an1	$⊢ (2^{k} \in ℂ \land 2^{k} \neq 0) \to \frac{3}{2^{k}} = 3 (\frac{1}{2^{k}})$
32	27 28 31	syl2anc	$⊢ 2^{k} \in ℝ^{+} \to \frac{3}{2^{k}} = 3 (\frac{1}{2^{k}})$
33	26 32	syl	$⊢ k \in ℕ \to \frac{3}{2^{k}} = 3 (\frac{1}{2^{k}})$
34	33	adantl	$⊢ (r \in ℝ^{+} \land k \in ℕ) \to \frac{3}{2^{k}} = 3 (\frac{1}{2^{k}})$
35	34	breq1d	$⊢ (r \in ℝ^{+} \land k \in ℕ) \to (\frac{3}{2^{k}} < r \leftrightarrow 3 (\frac{1}{2^{k}}) < r)$
36	25	nnrecred	$⊢ k \in ℕ \to \frac{1}{2^{k}} \in ℝ$
37		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
38	12 13	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
39		ltmuldiv2	$⊢ (\frac{1}{2^{k}} \in ℝ \land r \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (3 (\frac{1}{2^{k}}) < r \leftrightarrow \frac{1}{2^{k}} < \frac{r}{3})$
40	38 39	mp3an3	$⊢ (\frac{1}{2^{k}} \in ℝ \land r \in ℝ) \to (3 (\frac{1}{2^{k}}) < r \leftrightarrow \frac{1}{2^{k}} < \frac{r}{3})$
41	36 37 40	syl2anr	$⊢ (r \in ℝ^{+} \land k \in ℕ) \to (3 (\frac{1}{2^{k}}) < r \leftrightarrow \frac{1}{2^{k}} < \frac{r}{3})$
42	35 41	bitrd	$⊢ (r \in ℝ^{+} \land k \in ℕ) \to (\frac{3}{2^{k}} < r \leftrightarrow \frac{1}{2^{k}} < \frac{r}{3})$
43	42	rexbidva	$⊢ r \in ℝ^{+} \to (\exists k \in ℕ \frac{3}{2^{k}} < r \leftrightarrow \exists k \in ℕ \frac{1}{2^{k}} < \frac{r}{3})$
44	21 43	mpbird	$⊢ r \in ℝ^{+} \to \exists k \in ℕ \frac{3}{2^{k}} < r$
45		fveq2	$⊢ n = k \to S (n) = S (k)$
46		oveq2	$⊢ n = k \to 2^{n} = 2^{k}$
47	46	oveq2d	$⊢ n = k \to \frac{3}{2^{n}} = \frac{3}{2^{k}}$
48	45 47	opeq12d	$⊢ n = k \to ⟨S (n), \frac{3}{2^{n}}⟩ = ⟨S (k), \frac{3}{2^{k}}⟩$
49		opex	$⊢ ⟨S (k), \frac{3}{2^{k}}⟩ \in V$
50	48 11 49	fvmpt	$⊢ k \in ℕ \to M (k) = ⟨S (k), \frac{3}{2^{k}}⟩$
51	50	fveq2d	$⊢ k \in ℕ \to 2^{nd} (M (k)) = 2^{nd} (⟨S (k), \frac{3}{2^{k}}⟩)$
52		fvex	$⊢ S (k) \in V$
53		ovex	$⊢ \frac{3}{2^{k}} \in V$
54	52 53	op2nd	$⊢ 2^{nd} (⟨S (k), \frac{3}{2^{k}}⟩) = \frac{3}{2^{k}}$
55	51 54	syl6eq	$⊢ k \in ℕ \to 2^{nd} (M (k)) = \frac{3}{2^{k}}$
56	55	breq1d	$⊢ k \in ℕ \to (2^{nd} (M (k)) < r \leftrightarrow \frac{3}{2^{k}} < r)$
57	56	rexbiia	$⊢ \exists k \in ℕ 2^{nd} (M (k)) < r \leftrightarrow \exists k \in ℕ \frac{3}{2^{k}} < r$
58	44 57	sylibr	$⊢ r \in ℝ^{+} \to \exists k \in ℕ 2^{nd} (M (k)) < r$
59	58	rgen	$⊢ \forall r \in ℝ^{+} \exists k \in ℕ 2^{nd} (M (k)) < r$

Metamath Proof Explorer

Theorem heiborlem7

Proof