heiborlem6

Description: Lemma for heibor . Since the sequence of balls connected by the function T ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (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	heiborlem6	$⊢ φ \to \forall k \in ℕ ball (D) (M (k + 1)) \subseteq ball (D) (M (k))$

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		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
13		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
14	5 13	syl	$⊢ φ \to D \in Met (X)$
15		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
16	14 15	syl	$⊢ φ \to D \in ∞Met (X)$
17	16	adantr	$⊢ (φ \land k \in ℕ_{0}) \to D \in ∞Met (X)$
18		inss1	$⊢ 𝒫 X \cap Fin \subseteq 𝒫 X$
19		fss	$⊢ (F : ℕ_{0} ⟶ 𝒫 X \cap Fin \land 𝒫 X \cap Fin \subseteq 𝒫 X) \to F : ℕ_{0} ⟶ 𝒫 X$
20	6 18 19	sylancl	$⊢ φ \to F : ℕ_{0} ⟶ 𝒫 X$
21		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
22		ffvelcdm	$⊢ (F : ℕ_{0} ⟶ 𝒫 X \land k + 1 \in ℕ_{0}) \to F (k + 1) \in 𝒫 X$
23	20 21 22	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) \in 𝒫 X$
24	23	elpwid	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) \subseteq X$
25	1 2 3 4 5 6 7 8 9 10	heiborlem4	$⊢ (φ \land k + 1 \in ℕ_{0}) \to S (k + 1) G (k + 1)$
26	21 25	sylan2	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) G (k + 1)$
27		fvex	$⊢ S (k + 1) \in V$
28		ovex	$⊢ k + 1 \in V$
29	1 2 3 27 28	heiborlem2	$⊢ S (k + 1) G (k + 1) \leftrightarrow (k + 1 \in ℕ_{0} \land S (k + 1) \in F (k + 1) \land S (k + 1) B (k + 1) \in K)$
30	29	simp2bi	$⊢ S (k + 1) G (k + 1) \to S (k + 1) \in F (k + 1)$
31	26 30	syl	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) \in F (k + 1)$
32	24 31	sseldd	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) \in X$
33	20	ffvelcdmda	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in 𝒫 X$
34	33	elpwid	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \subseteq X$
35	1 2 3 4 5 6 7 8 9 10	heiborlem4	$⊢ (φ \land k \in ℕ_{0}) \to S (k) G k$
36		fvex	$⊢ S (k) \in V$
37		vex	$⊢ k \in V$
38	1 2 3 36 37	heiborlem2	$⊢ S (k) G k \leftrightarrow (k \in ℕ_{0} \land S (k) \in F (k) \land S (k) B k \in K)$
39	38	simp2bi	$⊢ S (k) G k \to S (k) \in F (k)$
40	35 39	syl	$⊢ (φ \land k \in ℕ_{0}) \to S (k) \in F (k)$
41	34 40	sseldd	$⊢ (φ \land k \in ℕ_{0}) \to S (k) \in X$
42		3re	$⊢ 3 \in ℝ$
43		2nn	$⊢ 2 \in ℕ$
44		nnexpcl	$⊢ (2 \in ℕ \land k + 1 \in ℕ_{0}) \to 2^{k + 1} \in ℕ$
45	43 21 44	sylancr	$⊢ k \in ℕ_{0} \to 2^{k + 1} \in ℕ$
46	45	nnrpd	$⊢ k \in ℕ_{0} \to 2^{k + 1} \in ℝ^{+}$
47	46	adantl	$⊢ (φ \land k \in ℕ_{0}) \to 2^{k + 1} \in ℝ^{+}$
48		rerpdivcl	$⊢ (3 \in ℝ \land 2^{k + 1} \in ℝ^{+}) \to \frac{3}{2^{k + 1}} \in ℝ$
49	42 47 48	sylancr	$⊢ (φ \land k \in ℕ_{0}) \to \frac{3}{2^{k + 1}} \in ℝ$
50		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
51	43 50	mpan	$⊢ k \in ℕ_{0} \to 2^{k} \in ℕ$
52	51	nnrpd	$⊢ k \in ℕ_{0} \to 2^{k} \in ℝ^{+}$
53	52	adantl	$⊢ (φ \land k \in ℕ_{0}) \to 2^{k} \in ℝ^{+}$
54		rerpdivcl	$⊢ (3 \in ℝ \land 2^{k} \in ℝ^{+}) \to \frac{3}{2^{k}} \in ℝ$
55	42 53 54	sylancr	$⊢ (φ \land k \in ℕ_{0}) \to \frac{3}{2^{k}} \in ℝ$
56		oveq1	$⊢ z = S (k) \to z ball (D) (\frac{1}{2^{m}}) = S (k) ball (D) (\frac{1}{2^{m}})$
57		oveq2	$⊢ m = k \to 2^{m} = 2^{k}$
58	57	oveq2d	$⊢ m = k \to \frac{1}{2^{m}} = \frac{1}{2^{k}}$
59	58	oveq2d	$⊢ m = k \to S (k) ball (D) (\frac{1}{2^{m}}) = S (k) ball (D) (\frac{1}{2^{k}})$
60		ovex	$⊢ S (k) ball (D) (\frac{1}{2^{k}}) \in V$
61	56 59 4 60	ovmpo	$⊢ (S (k) \in X \land k \in ℕ_{0}) \to S (k) B k = S (k) ball (D) (\frac{1}{2^{k}})$
62	41 61	sylancom	$⊢ (φ \land k \in ℕ_{0}) \to S (k) B k = S (k) ball (D) (\frac{1}{2^{k}})$
63		df-br	$⊢ S (k) G k \leftrightarrow ⟨S (k), k⟩ \in G$
64		fveq2	$⊢ x = ⟨S (k), k⟩ \to T (x) = T (⟨S (k), k⟩)$
65		df-ov	$⊢ S (k) T k = T (⟨S (k), k⟩)$
66	64 65	eqtr4di	$⊢ x = ⟨S (k), k⟩ \to T (x) = S (k) T k$
67	36 37	op2ndd	$⊢ x = ⟨S (k), k⟩ \to 2^{nd} (x) = k$
68	67	oveq1d	$⊢ x = ⟨S (k), k⟩ \to 2^{nd} (x) + 1 = k + 1$
69	66 68	breq12d	$⊢ x = ⟨S (k), k⟩ \to (T (x) G (2^{nd} (x) + 1) \leftrightarrow (S (k) T k) G (k + 1))$
70		fveq2	$⊢ x = ⟨S (k), k⟩ \to B (x) = B (⟨S (k), k⟩)$
71		df-ov	$⊢ S (k) B k = B (⟨S (k), k⟩)$
72	70 71	eqtr4di	$⊢ x = ⟨S (k), k⟩ \to B (x) = S (k) B k$
73	66 68	oveq12d	$⊢ x = ⟨S (k), k⟩ \to T (x) B (2^{nd} (x) + 1) = (S (k) T k) B (k + 1)$
74	72 73	ineq12d	$⊢ x = ⟨S (k), k⟩ \to B (x) \cap (T (x) B (2^{nd} (x) + 1)) = (S (k) B k) \cap ((S (k) T k) B (k + 1))$
75	74	eleq1d	$⊢ x = ⟨S (k), k⟩ \to (B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K \leftrightarrow (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K)$
76	69 75	anbi12d	$⊢ x = ⟨S (k), k⟩ \to ((T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K) \leftrightarrow ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
77	76	rspccv	$⊢ \forall x \in G (T (x) G (2^{nd} (x) + 1) \land B (x) \cap (T (x) B (2^{nd} (x) + 1)) \in K) \to (⟨S (k), k⟩ \in G \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
78	8 77	syl	$⊢ φ \to (⟨S (k), k⟩ \in G \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
79	63 78	biimtrid	$⊢ φ \to (S (k) G k \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
80	79	adantr	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) G k \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K))$
81	35 80	mpd	$⊢ (φ \land k \in ℕ_{0}) \to ((S (k) T k) G (k + 1) \land (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K)$
82	81	simpld	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) T k) G (k + 1)$
83		ovex	$⊢ S (k) T k \in V$
84	1 2 3 83 28	heiborlem2	$⊢ (S (k) T k) G (k + 1) \leftrightarrow (k + 1 \in ℕ_{0} \land S (k) T k \in F (k + 1) \land (S (k) T k) B (k + 1) \in K)$
85	84	simp2bi	$⊢ (S (k) T k) G (k + 1) \to S (k) T k \in F (k + 1)$
86	82 85	syl	$⊢ (φ \land k \in ℕ_{0}) \to S (k) T k \in F (k + 1)$
87	24 86	sseldd	$⊢ (φ \land k \in ℕ_{0}) \to S (k) T k \in X$
88	21	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
89		oveq1	$⊢ z = S (k) T k \to z ball (D) (\frac{1}{2^{m}}) = (S (k) T k) ball (D) (\frac{1}{2^{m}})$
90		oveq2	$⊢ m = k + 1 \to 2^{m} = 2^{k + 1}$
91	90	oveq2d	$⊢ m = k + 1 \to \frac{1}{2^{m}} = \frac{1}{2^{k + 1}}$
92	91	oveq2d	$⊢ m = k + 1 \to (S (k) T k) ball (D) (\frac{1}{2^{m}}) = (S (k) T k) ball (D) (\frac{1}{2^{k + 1}})$
93		ovex	$⊢ (S (k) T k) ball (D) (\frac{1}{2^{k + 1}}) \in V$
94	89 92 4 93	ovmpo	$⊢ (S (k) T k \in X \land k + 1 \in ℕ_{0}) \to (S (k) T k) B (k + 1) = (S (k) T k) ball (D) (\frac{1}{2^{k + 1}})$
95	87 88 94	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) T k) B (k + 1) = (S (k) T k) ball (D) (\frac{1}{2^{k + 1}})$
96	62 95	ineq12d	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) B k) \cap ((S (k) T k) B (k + 1)) = (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}}))$
97	81	simprd	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K$
98		0elpw	$⊢ \emptyset \in 𝒫 U$
99		0fi	$⊢ \emptyset \in Fin$
100		elin	$⊢ \emptyset \in (𝒫 U \cap Fin) \leftrightarrow (\emptyset \in 𝒫 U \land \emptyset \in Fin)$
101	98 99 100	mpbir2an	$⊢ \emptyset \in (𝒫 U \cap Fin)$
102		0ss	$⊢ \emptyset \subseteq ⋃ \emptyset$
103		unieq	$⊢ v = \emptyset \to ⋃ v = ⋃ \emptyset$
104	103	sseq2d	$⊢ v = \emptyset \to (\emptyset \subseteq ⋃ v \leftrightarrow \emptyset \subseteq ⋃ \emptyset)$
105	104	rspcev	$⊢ (\emptyset \in (𝒫 U \cap Fin) \land \emptyset \subseteq ⋃ \emptyset) \to \exists v \in (𝒫 U \cap Fin) \emptyset \subseteq ⋃ v$
106	101 102 105	mp2an	$⊢ \exists v \in (𝒫 U \cap Fin) \emptyset \subseteq ⋃ v$
107		0ex	$⊢ \emptyset \in V$
108		sseq1	$⊢ u = \emptyset \to (u \subseteq ⋃ v \leftrightarrow \emptyset \subseteq ⋃ v)$
109	108	rexbidv	$⊢ u = \emptyset \to (\exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v \leftrightarrow \exists v \in (𝒫 U \cap Fin) \emptyset \subseteq ⋃ v)$
110	109	notbid	$⊢ u = \emptyset \to (\neg \exists v \in (𝒫 U \cap Fin) u \subseteq ⋃ v \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) \emptyset \subseteq ⋃ v)$
111	107 110 2	elab2	$⊢ \emptyset \in K \leftrightarrow \neg \exists v \in (𝒫 U \cap Fin) \emptyset \subseteq ⋃ v$
112	111	con2bii	$⊢ \exists v \in (𝒫 U \cap Fin) \emptyset \subseteq ⋃ v \leftrightarrow \neg \emptyset \in K$
113	106 112	mpbi	$⊢ \neg \emptyset \in K$
114		nelne2	$⊢ ((S (k) B k) \cap ((S (k) T k) B (k + 1)) \in K \land \neg \emptyset \in K) \to (S (k) B k) \cap ((S (k) T k) B (k + 1)) \neq \emptyset$
115	97 113 114	sylancl	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) B k) \cap ((S (k) T k) B (k + 1)) \neq \emptyset$
116	96 115	eqnetrrd	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) \neq \emptyset$
117	52	rpreccld	$⊢ k \in ℕ_{0} \to \frac{1}{2^{k}} \in ℝ^{+}$
118	117	adantl	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2^{k}} \in ℝ^{+}$
119	118	rpred	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2^{k}} \in ℝ$
120	46	rpreccld	$⊢ k \in ℕ_{0} \to \frac{1}{2^{k + 1}} \in ℝ^{+}$
121	120	adantl	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2^{k + 1}} \in ℝ^{+}$
122	121	rpred	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2^{k + 1}} \in ℝ$
123		rexadd	$⊢ (\frac{1}{2^{k}} \in ℝ \land \frac{1}{2^{k + 1}} \in ℝ) \to (\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) = (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}})$
124	119 122 123	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to (\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) = (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}})$
125	124	breq1d	$⊢ (φ \land k \in ℕ_{0}) \to ((\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \leftrightarrow (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k))$
126	118	rpxrd	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2^{k}} \in ℝ^{*}$
127	121	rpxrd	$⊢ (φ \land k \in ℕ_{0}) \to \frac{1}{2^{k + 1}} \in ℝ^{*}$
128		bldisj	$⊢ ((D \in ∞Met (X) \land S (k) \in X \land S (k) T k \in X) \land (\frac{1}{2^{k}} \in ℝ^{} \land \frac{1}{2^{k + 1}} \in ℝ^{} \land (\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k))) \to (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) = \emptyset$
129	128	3exp2	$⊢ (D \in ∞Met (X) \land S (k) \in X \land S (k) T k \in X) \to (\frac{1}{2^{k}} \in ℝ^{} \to (\frac{1}{2^{k + 1}} \in ℝ^{} \to ((\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \to (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) = \emptyset)))$
130	129	imp32	$⊢ ((D \in ∞Met (X) \land S (k) \in X \land S (k) T k \in X) \land (\frac{1}{2^{k}} \in ℝ^{} \land \frac{1}{2^{k + 1}} \in ℝ^{})) \to ((\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \to (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) = \emptyset)$
131	17 41 87 126 127 130	syl32anc	$⊢ (φ \land k \in ℕ_{0}) \to ((\frac{1}{2^{k}}) +_{𝑒} (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \to (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) = \emptyset)$
132	125 131	sylbird	$⊢ (φ \land k \in ℕ_{0}) \to ((\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \to (S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) = \emptyset)$
133	132	necon3ad	$⊢ (φ \land k \in ℕ_{0}) \to ((S (k) ball (D) (\frac{1}{2^{k}})) \cap ((S (k) T k) ball (D) (\frac{1}{2^{k + 1}})) \neq \emptyset \to \neg (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k))$
134	116 133	mpd	$⊢ (φ \land k \in ℕ_{0}) \to \neg (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k)$
135	118 121	rpaddcld	$⊢ (φ \land k \in ℕ_{0}) \to (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \in ℝ^{+}$
136	135	rpred	$⊢ (φ \land k \in ℕ_{0}) \to (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \in ℝ$
137	14	adantr	$⊢ (φ \land k \in ℕ_{0}) \to D \in Met (X)$
138		metcl	$⊢ (D \in Met (X) \land S (k) \in X \land S (k) T k \in X) \to S (k) D (S (k) T k) \in ℝ$
139	137 41 87 138	syl3anc	$⊢ (φ \land k \in ℕ_{0}) \to S (k) D (S (k) T k) \in ℝ$
140	136 139	letrid	$⊢ (φ \land k \in ℕ_{0}) \to ((\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \lor S (k) D (S (k) T k) \leq (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}))$
141	140	ord	$⊢ (φ \land k \in ℕ_{0}) \to (\neg (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) \leq S (k) D (S (k) T k) \to S (k) D (S (k) T k) \leq (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}))$
142	134 141	mpd	$⊢ (φ \land k \in ℕ_{0}) \to S (k) D (S (k) T k) \leq (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}})$
143		seqp1	$⊢ k \in ℤ_{\geq 0} \to seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
144		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
145	143 144	eleq2s	$⊢ k \in ℕ_{0} \to seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
146	10	fveq1i	$⊢ S (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k + 1)$
147	10	fveq1i	$⊢ S (k) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k)$
148	147	oveq1i	$⊢ S (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = seq 0 (T, (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))) (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
149	145 146 148	3eqtr4g	$⊢ k \in ℕ_{0} \to S (k + 1) = S (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1)$
150		eqid	$⊢ (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) = (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1))$
151		eqeq1	$⊢ m = k + 1 \to (m = 0 \leftrightarrow k + 1 = 0)$
152		oveq1	$⊢ m = k + 1 \to m - 1 = k + 1 - 1$
153	151 152	ifbieq2d	$⊢ m = k + 1 \to if (m = 0, C, m - 1) = if (k + 1 = 0, C, k + 1 - 1)$
154		nn0p1nn	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ$
155		nnne0	$⊢ k + 1 \in ℕ \to k + 1 \neq 0$
156	155	neneqd	$⊢ k + 1 \in ℕ \to \neg k + 1 = 0$
157	154 156	syl	$⊢ k \in ℕ_{0} \to \neg k + 1 = 0$
158	157	iffalsed	$⊢ k \in ℕ_{0} \to if (k + 1 = 0, C, k + 1 - 1) = k + 1 - 1$
159		ovex	$⊢ k + 1 - 1 \in V$
160	158 159	eqeltrdi	$⊢ k \in ℕ_{0} \to if (k + 1 = 0, C, k + 1 - 1) \in V$
161	150 153 21 160	fvmptd3	$⊢ k \in ℕ_{0} \to (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = if (k + 1 = 0, C, k + 1 - 1)$
162		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
163		ax-1cn	$⊢ 1 \in ℂ$
164		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
165	162 163 164	sylancl	$⊢ k \in ℕ_{0} \to k + 1 - 1 = k$
166	161 158 165	3eqtrd	$⊢ k \in ℕ_{0} \to (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = k$
167	166	oveq2d	$⊢ k \in ℕ_{0} \to S (k) T (m \in ℕ_{0} ⟼ if (m = 0, C, m - 1)) (k + 1) = S (k) T k$
168	149 167	eqtrd	$⊢ k \in ℕ_{0} \to S (k + 1) = S (k) T k$
169	168	adantl	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) = S (k) T k$
170	169	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) D S (k) = (S (k) T k) D S (k)$
171		metsym	$⊢ (D \in Met (X) \land S (k) T k \in X \land S (k) \in X) \to (S (k) T k) D S (k) = S (k) D (S (k) T k)$
172	137 87 41 171	syl3anc	$⊢ (φ \land k \in ℕ_{0}) \to (S (k) T k) D S (k) = S (k) D (S (k) T k)$
173	170 172	eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) D S (k) = S (k) D (S (k) T k)$
174		3cn	$⊢ 3 \in ℂ$
175	174	2timesi	$⊢ 2 \cdot 3 = 3 + 3$
176	175	oveq1i	$⊢ 2 \cdot 3 - 3 = 3 + 3 - 3$
177	174 174	pncan3oi	$⊢ 3 + 3 - 3 = 3$
178		df-3	$⊢ 3 = 2 + 1$
179	176 177 178	3eqtri	$⊢ 2 \cdot 3 - 3 = 2 + 1$
180	179	oveq1i	$⊢ \frac{2 \cdot 3 - 3}{2^{k + 1}} = \frac{2 + 1}{2^{k + 1}}$
181		rpcn	$⊢ 2^{k + 1} \in ℝ^{+} \to 2^{k + 1} \in ℂ$
182		rpne0	$⊢ 2^{k + 1} \in ℝ^{+} \to 2^{k + 1} \neq 0$
183		2cn	$⊢ 2 \in ℂ$
184	183 174	mulcli	$⊢ 2 \cdot 3 \in ℂ$
185		divsubdir	$⊢ (2 \cdot 3 \in ℂ \land 3 \in ℂ \land (2^{k + 1} \in ℂ \land 2^{k + 1} \neq 0)) \to \frac{2 \cdot 3 - 3}{2^{k + 1}} = (\frac{2 \cdot 3}{2^{k + 1}}) - (\frac{3}{2^{k + 1}})$
186	184 174 185	mp3an12	$⊢ (2^{k + 1} \in ℂ \land 2^{k + 1} \neq 0) \to \frac{2 \cdot 3 - 3}{2^{k + 1}} = (\frac{2 \cdot 3}{2^{k + 1}}) - (\frac{3}{2^{k + 1}})$
187	181 182 186	syl2anc	$⊢ 2^{k + 1} \in ℝ^{+} \to \frac{2 \cdot 3 - 3}{2^{k + 1}} = (\frac{2 \cdot 3}{2^{k + 1}}) - (\frac{3}{2^{k + 1}})$
188	46 187	syl	$⊢ k \in ℕ_{0} \to \frac{2 \cdot 3 - 3}{2^{k + 1}} = (\frac{2 \cdot 3}{2^{k + 1}}) - (\frac{3}{2^{k + 1}})$
189		divdir	$⊢ (2 \in ℂ \land 1 \in ℂ \land (2^{k + 1} \in ℂ \land 2^{k + 1} \neq 0)) \to \frac{2 + 1}{2^{k + 1}} = (\frac{2}{2^{k + 1}}) + (\frac{1}{2^{k + 1}})$
190	183 163 189	mp3an12	$⊢ (2^{k + 1} \in ℂ \land 2^{k + 1} \neq 0) \to \frac{2 + 1}{2^{k + 1}} = (\frac{2}{2^{k + 1}}) + (\frac{1}{2^{k + 1}})$
191	181 182 190	syl2anc	$⊢ 2^{k + 1} \in ℝ^{+} \to \frac{2 + 1}{2^{k + 1}} = (\frac{2}{2^{k + 1}}) + (\frac{1}{2^{k + 1}})$
192	46 191	syl	$⊢ k \in ℕ_{0} \to \frac{2 + 1}{2^{k + 1}} = (\frac{2}{2^{k + 1}}) + (\frac{1}{2^{k + 1}})$
193	180 188 192	3eqtr3a	$⊢ k \in ℕ_{0} \to (\frac{2 \cdot 3}{2^{k + 1}}) - (\frac{3}{2^{k + 1}}) = (\frac{2}{2^{k + 1}}) + (\frac{1}{2^{k + 1}})$
194		rpcn	$⊢ 2^{k} \in ℝ^{+} \to 2^{k} \in ℂ$
195		rpne0	$⊢ 2^{k} \in ℝ^{+} \to 2^{k} \neq 0$
196		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
197		divcan5	$⊢ (3 \in ℂ \land (2^{k} \in ℂ \land 2^{k} \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 \cdot 3}{2 2^{k}} = \frac{3}{2^{k}}$
198	174 196 197	mp3an13	$⊢ (2^{k} \in ℂ \land 2^{k} \neq 0) \to \frac{2 \cdot 3}{2 2^{k}} = \frac{3}{2^{k}}$
199	194 195 198	syl2anc	$⊢ 2^{k} \in ℝ^{+} \to \frac{2 \cdot 3}{2 2^{k}} = \frac{3}{2^{k}}$
200	52 199	syl	$⊢ k \in ℕ_{0} \to \frac{2 \cdot 3}{2 2^{k}} = \frac{3}{2^{k}}$
201	52 194	syl	$⊢ k \in ℕ_{0} \to 2^{k} \in ℂ$
202		mulcom	$⊢ (2 \in ℂ \land 2^{k} \in ℂ) \to 2 2^{k} = 2^{k} \cdot 2$
203	183 201 202	sylancr	$⊢ k \in ℕ_{0} \to 2 2^{k} = 2^{k} \cdot 2$
204		expp1	$⊢ (2 \in ℂ \land k \in ℕ_{0}) \to 2^{k + 1} = 2^{k} \cdot 2$
205	183 204	mpan	$⊢ k \in ℕ_{0} \to 2^{k + 1} = 2^{k} \cdot 2$
206	203 205	eqtr4d	$⊢ k \in ℕ_{0} \to 2 2^{k} = 2^{k + 1}$
207	206	oveq2d	$⊢ k \in ℕ_{0} \to \frac{2 \cdot 3}{2 2^{k}} = \frac{2 \cdot 3}{2^{k + 1}}$
208	200 207	eqtr3d	$⊢ k \in ℕ_{0} \to \frac{3}{2^{k}} = \frac{2 \cdot 3}{2^{k + 1}}$
209	208	oveq1d	$⊢ k \in ℕ_{0} \to (\frac{3}{2^{k}}) - (\frac{3}{2^{k + 1}}) = (\frac{2 \cdot 3}{2^{k + 1}}) - (\frac{3}{2^{k + 1}})$
210		divcan5	$⊢ (1 \in ℂ \land (2^{k} \in ℂ \land 2^{k} \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 \cdot 1}{2 2^{k}} = \frac{1}{2^{k}}$
211	163 196 210	mp3an13	$⊢ (2^{k} \in ℂ \land 2^{k} \neq 0) \to \frac{2 \cdot 1}{2 2^{k}} = \frac{1}{2^{k}}$
212	194 195 211	syl2anc	$⊢ 2^{k} \in ℝ^{+} \to \frac{2 \cdot 1}{2 2^{k}} = \frac{1}{2^{k}}$
213	52 212	syl	$⊢ k \in ℕ_{0} \to \frac{2 \cdot 1}{2 2^{k}} = \frac{1}{2^{k}}$
214		2t1e2	$⊢ 2 \cdot 1 = 2$
215	214	a1i	$⊢ k \in ℕ_{0} \to 2 \cdot 1 = 2$
216	215 206	oveq12d	$⊢ k \in ℕ_{0} \to \frac{2 \cdot 1}{2 2^{k}} = \frac{2}{2^{k + 1}}$
217	213 216	eqtr3d	$⊢ k \in ℕ_{0} \to \frac{1}{2^{k}} = \frac{2}{2^{k + 1}}$
218	217	oveq1d	$⊢ k \in ℕ_{0} \to (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}}) = (\frac{2}{2^{k + 1}}) + (\frac{1}{2^{k + 1}})$
219	193 209 218	3eqtr4d	$⊢ k \in ℕ_{0} \to (\frac{3}{2^{k}}) - (\frac{3}{2^{k + 1}}) = (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}})$
220	219	adantl	$⊢ (φ \land k \in ℕ_{0}) \to (\frac{3}{2^{k}}) - (\frac{3}{2^{k + 1}}) = (\frac{1}{2^{k}}) + (\frac{1}{2^{k + 1}})$
221	142 173 220	3brtr4d	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) D S (k) \leq (\frac{3}{2^{k}}) - (\frac{3}{2^{k + 1}})$
222		blss2	$⊢ ((D \in ∞Met (X) \land S (k + 1) \in X \land S (k) \in X) \land (\frac{3}{2^{k + 1}} \in ℝ \land \frac{3}{2^{k}} \in ℝ \land S (k + 1) D S (k) \leq (\frac{3}{2^{k}}) - (\frac{3}{2^{k + 1}}))) \to S (k + 1) ball (D) (\frac{3}{2^{k + 1}}) \subseteq S (k) ball (D) (\frac{3}{2^{k}})$
223	17 32 41 49 55 221 222	syl33anc	$⊢ (φ \land k \in ℕ_{0}) \to S (k + 1) ball (D) (\frac{3}{2^{k + 1}}) \subseteq S (k) ball (D) (\frac{3}{2^{k}})$
224	12 223	sylan2	$⊢ (φ \land k \in ℕ) \to S (k + 1) ball (D) (\frac{3}{2^{k + 1}}) \subseteq S (k) ball (D) (\frac{3}{2^{k}})$
225		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
226		fveq2	$⊢ n = k + 1 \to S (n) = S (k + 1)$
227		oveq2	$⊢ n = k + 1 \to 2^{n} = 2^{k + 1}$
228	227	oveq2d	$⊢ n = k + 1 \to \frac{3}{2^{n}} = \frac{3}{2^{k + 1}}$
229	226 228	opeq12d	$⊢ n = k + 1 \to ⟨S (n), \frac{3}{2^{n}}⟩ = ⟨S (k + 1), \frac{3}{2^{k + 1}}⟩$
230		opex	$⊢ ⟨S (k + 1), \frac{3}{2^{k + 1}}⟩ \in V$
231	229 11 230	fvmpt	$⊢ k + 1 \in ℕ \to M (k + 1) = ⟨S (k + 1), \frac{3}{2^{k + 1}}⟩$
232	225 231	syl	$⊢ k \in ℕ \to M (k + 1) = ⟨S (k + 1), \frac{3}{2^{k + 1}}⟩$
233	232	adantl	$⊢ (φ \land k \in ℕ) \to M (k + 1) = ⟨S (k + 1), \frac{3}{2^{k + 1}}⟩$
234	233	fveq2d	$⊢ (φ \land k \in ℕ) \to ball (D) (M (k + 1)) = ball (D) (⟨S (k + 1), \frac{3}{2^{k + 1}}⟩)$
235		df-ov	$⊢ S (k + 1) ball (D) (\frac{3}{2^{k + 1}}) = ball (D) (⟨S (k + 1), \frac{3}{2^{k + 1}}⟩)$
236	234 235	eqtr4di	$⊢ (φ \land k \in ℕ) \to ball (D) (M (k + 1)) = S (k + 1) ball (D) (\frac{3}{2^{k + 1}})$
237		fveq2	$⊢ n = k \to S (n) = S (k)$
238		oveq2	$⊢ n = k \to 2^{n} = 2^{k}$
239	238	oveq2d	$⊢ n = k \to \frac{3}{2^{n}} = \frac{3}{2^{k}}$
240	237 239	opeq12d	$⊢ n = k \to ⟨S (n), \frac{3}{2^{n}}⟩ = ⟨S (k), \frac{3}{2^{k}}⟩$
241		opex	$⊢ ⟨S (k), \frac{3}{2^{k}}⟩ \in V$
242	240 11 241	fvmpt	$⊢ k \in ℕ \to M (k) = ⟨S (k), \frac{3}{2^{k}}⟩$
243	242	fveq2d	$⊢ k \in ℕ \to ball (D) (M (k)) = ball (D) (⟨S (k), \frac{3}{2^{k}}⟩)$
244		df-ov	$⊢ S (k) ball (D) (\frac{3}{2^{k}}) = ball (D) (⟨S (k), \frac{3}{2^{k}}⟩)$
245	243 244	eqtr4di	$⊢ k \in ℕ \to ball (D) (M (k)) = S (k) ball (D) (\frac{3}{2^{k}})$
246	245	adantl	$⊢ (φ \land k \in ℕ) \to ball (D) (M (k)) = S (k) ball (D) (\frac{3}{2^{k}})$
247	224 236 246	3sstr4d	$⊢ (φ \land k \in ℕ) \to ball (D) (M (k + 1)) \subseteq ball (D) (M (k))$
248	247	ralrimiva	$⊢ φ \to \forall k \in ℕ ball (D) (M (k + 1)) \subseteq ball (D) (M (k))$

Metamath Proof Explorer

Theorem heiborlem6

Proof