caubl

Description: Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	caubl.2	$⊢ φ \to D \in ∞Met (X)$
	caubl.3	$⊢ φ \to F : ℕ ⟶ X \times ℝ^{+}$
	caubl.4	$⊢ φ \to \forall n \in ℕ ball (D) (F (n + 1)) \subseteq ball (D) (F (n))$
	caubl.5	$⊢ φ \to \forall r \in ℝ^{+} \exists n \in ℕ 2^{nd} (F (n)) < r$
Assertion	caubl	$⊢ φ \to 1^{st} \circ F \in Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		caubl.2	$⊢ φ \to D \in ∞Met (X)$
2		caubl.3	$⊢ φ \to F : ℕ ⟶ X \times ℝ^{+}$
3		caubl.4	$⊢ φ \to \forall n \in ℕ ball (D) (F (n + 1)) \subseteq ball (D) (F (n))$
4		caubl.5	$⊢ φ \to \forall r \in ℝ^{+} \exists n \in ℕ 2^{nd} (F (n)) < r$
5		2fveq3	$⊢ r = n \to ball (D) (F (r)) = ball (D) (F (n))$
6	5	sseq1d	$⊢ r = n \to (ball (D) (F (r)) \subseteq ball (D) (F (n)) \leftrightarrow ball (D) (F (n)) \subseteq ball (D) (F (n)))$
7	6	imbi2d	$⊢ r = n \to (((φ \land n \in ℕ) \to ball (D) (F (r)) \subseteq ball (D) (F (n))) \leftrightarrow ((φ \land n \in ℕ) \to ball (D) (F (n)) \subseteq ball (D) (F (n))))$
8		2fveq3	$⊢ r = k \to ball (D) (F (r)) = ball (D) (F (k))$
9	8	sseq1d	$⊢ r = k \to (ball (D) (F (r)) \subseteq ball (D) (F (n)) \leftrightarrow ball (D) (F (k)) \subseteq ball (D) (F (n)))$
10	9	imbi2d	$⊢ r = k \to (((φ \land n \in ℕ) \to ball (D) (F (r)) \subseteq ball (D) (F (n))) \leftrightarrow ((φ \land n \in ℕ) \to ball (D) (F (k)) \subseteq ball (D) (F (n))))$
11		2fveq3	$⊢ r = k + 1 \to ball (D) (F (r)) = ball (D) (F (k + 1))$
12	11	sseq1d	$⊢ r = k + 1 \to (ball (D) (F (r)) \subseteq ball (D) (F (n)) \leftrightarrow ball (D) (F (k + 1)) \subseteq ball (D) (F (n)))$
13	12	imbi2d	$⊢ r = k + 1 \to (((φ \land n \in ℕ) \to ball (D) (F (r)) \subseteq ball (D) (F (n))) \leftrightarrow ((φ \land n \in ℕ) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (n))))$
14		ssid	$⊢ ball (D) (F (n)) \subseteq ball (D) (F (n))$
15	14	2a1i	$⊢ n \in ℤ \to ((φ \land n \in ℕ) \to ball (D) (F (n)) \subseteq ball (D) (F (n)))$
16		eluznn	$⊢ (n \in ℕ \land k \in ℤ_{\geq n}) \to k \in ℕ$
17		fvoveq1	$⊢ n = k \to F (n + 1) = F (k + 1)$
18	17	fveq2d	$⊢ n = k \to ball (D) (F (n + 1)) = ball (D) (F (k + 1))$
19		2fveq3	$⊢ n = k \to ball (D) (F (n)) = ball (D) (F (k))$
20	18 19	sseq12d	$⊢ n = k \to (ball (D) (F (n + 1)) \subseteq ball (D) (F (n)) \leftrightarrow ball (D) (F (k + 1)) \subseteq ball (D) (F (k)))$
21	20	rspccva	$⊢ (\forall n \in ℕ ball (D) (F (n + 1)) \subseteq ball (D) (F (n)) \land k \in ℕ) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (k))$
22	3 16 21	syl2an	$⊢ (φ \land (n \in ℕ \land k \in ℤ_{\geq n})) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (k))$
23	22	anassrs	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (k))$
24		sstr2	$⊢ ball (D) (F (k + 1)) \subseteq ball (D) (F (k)) \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (n)))$
25	23 24	syl	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (n)))$
26	25	expcom	$⊢ k \in ℤ_{\geq n} \to ((φ \land n \in ℕ) \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (n))))$
27	26	a2d	$⊢ k \in ℤ_{\geq n} \to (((φ \land n \in ℕ) \to ball (D) (F (k)) \subseteq ball (D) (F (n))) \to ((φ \land n \in ℕ) \to ball (D) (F (k + 1)) \subseteq ball (D) (F (n))))$
28	7 10 13 10 15 27	uzind4	$⊢ k \in ℤ_{\geq n} \to ((φ \land n \in ℕ) \to ball (D) (F (k)) \subseteq ball (D) (F (n)))$
29	28	com12	$⊢ (φ \land n \in ℕ) \to (k \in ℤ_{\geq n} \to ball (D) (F (k)) \subseteq ball (D) (F (n)))$
30	29	ad2ant2r	$⊢ ((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \to (k \in ℤ_{\geq n} \to ball (D) (F (k)) \subseteq ball (D) (F (n)))$
31		relxp	$⊢ Rel (X \times ℝ^{+})$
32	2	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to F : ℕ ⟶ X \times ℝ^{+}$
33		simplrl	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to n \in ℕ$
34	32 33	ffvelrnd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to F (n) \in (X \times ℝ^{+})$
35		1st2nd	$⊢ (Rel (X \times ℝ^{+}) \land F (n) \in (X \times ℝ^{+})) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
36	31 34 35	sylancr	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
37	36	fveq2d	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to ball (D) (F (n)) = ball (D) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
38		df-ov	$⊢ 1^{st} (F (n)) ball (D) 2^{nd} (F (n)) = ball (D) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
39	37 38	eqtr4di	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to ball (D) (F (n)) = 1^{st} (F (n)) ball (D) 2^{nd} (F (n))$
40	1	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to D \in ∞Met (X)$
41		xp1st	$⊢ F (n) \in (X \times ℝ^{+}) \to 1^{st} (F (n)) \in X$
42	34 41	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 1^{st} (F (n)) \in X$
43		xp2nd	$⊢ F (n) \in (X \times ℝ^{+}) \to 2^{nd} (F (n)) \in ℝ^{+}$
44	34 43	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 2^{nd} (F (n)) \in ℝ^{+}$
45	44	rpxrd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 2^{nd} (F (n)) \in ℝ^{*}$
46		simpllr	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to r \in ℝ^{+}$
47	46	rpxrd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to r \in ℝ^{*}$
48		simplrr	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 2^{nd} (F (n)) < r$
49		rpre	$⊢ 2^{nd} (F (n)) \in ℝ^{+} \to 2^{nd} (F (n)) \in ℝ$
50		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
51		ltle	$⊢ (2^{nd} (F (n)) \in ℝ \land r \in ℝ) \to (2^{nd} (F (n)) < r \to 2^{nd} (F (n)) \leq r)$
52	49 50 51	syl2an	$⊢ (2^{nd} (F (n)) \in ℝ^{+} \land r \in ℝ^{+}) \to (2^{nd} (F (n)) < r \to 2^{nd} (F (n)) \leq r)$
53	44 46 52	syl2anc	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to (2^{nd} (F (n)) < r \to 2^{nd} (F (n)) \leq r)$
54	48 53	mpd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 2^{nd} (F (n)) \leq r$
55		ssbl	$⊢ ((D \in ∞Met (X) \land 1^{st} (F (n)) \in X) \land (2^{nd} (F (n)) \in ℝ^{} \land r \in ℝ^{}) \land 2^{nd} (F (n)) \leq r) \to 1^{st} (F (n)) ball (D) 2^{nd} (F (n)) \subseteq 1^{st} (F (n)) ball (D) r$
56	40 42 45 47 54 55	syl221anc	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 1^{st} (F (n)) ball (D) 2^{nd} (F (n)) \subseteq 1^{st} (F (n)) ball (D) r$
57	39 56	eqsstrd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to ball (D) (F (n)) \subseteq 1^{st} (F (n)) ball (D) r$
58		sstr2	$⊢ ball (D) (F (k)) \subseteq ball (D) (F (n)) \to (ball (D) (F (n)) \subseteq 1^{st} (F (n)) ball (D) r \to ball (D) (F (k)) \subseteq 1^{st} (F (n)) ball (D) r)$
59	57 58	syl5com	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to ball (D) (F (k)) \subseteq 1^{st} (F (n)) ball (D) r)$
60		simprl	$⊢ ((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \to n \in ℕ$
61	60 16	sylan	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to k \in ℕ$
62	32 61	ffvelrnd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to F (k) \in (X \times ℝ^{+})$
63		xp1st	$⊢ F (k) \in (X \times ℝ^{+}) \to 1^{st} (F (k)) \in X$
64	62 63	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 1^{st} (F (k)) \in X$
65		xp2nd	$⊢ F (k) \in (X \times ℝ^{+}) \to 2^{nd} (F (k)) \in ℝ^{+}$
66	62 65	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 2^{nd} (F (k)) \in ℝ^{+}$
67		blcntr	$⊢ (D \in ∞Met (X) \land 1^{st} (F (k)) \in X \land 2^{nd} (F (k)) \in ℝ^{+}) \to 1^{st} (F (k)) \in (1^{st} (F (k)) ball (D) 2^{nd} (F (k)))$
68	40 64 66 67	syl3anc	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 1^{st} (F (k)) \in (1^{st} (F (k)) ball (D) 2^{nd} (F (k)))$
69		1st2nd	$⊢ (Rel (X \times ℝ^{+}) \land F (k) \in (X \times ℝ^{+})) \to F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
70	31 62 69	sylancr	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
71	70	fveq2d	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to ball (D) (F (k)) = ball (D) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩)$
72		df-ov	$⊢ 1^{st} (F (k)) ball (D) 2^{nd} (F (k)) = ball (D) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩)$
73	71 72	eqtr4di	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to ball (D) (F (k)) = 1^{st} (F (k)) ball (D) 2^{nd} (F (k))$
74	68 73	eleqtrrd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to 1^{st} (F (k)) \in ball (D) (F (k))$
75		ssel	$⊢ ball (D) (F (k)) \subseteq 1^{st} (F (n)) ball (D) r \to (1^{st} (F (k)) \in ball (D) (F (k)) \to 1^{st} (F (k)) \in (1^{st} (F (n)) ball (D) r))$
76	59 74 75	syl6ci	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to 1^{st} (F (k)) \in (1^{st} (F (n)) ball (D) r))$
77		elbl2	$⊢ ((D \in ∞Met (X) \land r \in ℝ^{*}) \land (1^{st} (F (n)) \in X \land 1^{st} (F (k)) \in X)) \to (1^{st} (F (k)) \in (1^{st} (F (n)) ball (D) r) \leftrightarrow 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
78	40 47 42 64 77	syl22anc	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to (1^{st} (F (k)) \in (1^{st} (F (n)) ball (D) r) \leftrightarrow 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
79	76 78	sylibd	$⊢ (((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \land k \in ℤ_{\geq n}) \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
80	79	ex	$⊢ ((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \to (k \in ℤ_{\geq n} \to (ball (D) (F (k)) \subseteq ball (D) (F (n)) \to 1^{st} (F (n)) D 1^{st} (F (k)) < r))$
81	30 80	mpdd	$⊢ ((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \to (k \in ℤ_{\geq n} \to 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
82	81	ralrimiv	$⊢ ((φ \land r \in ℝ^{+}) \land (n \in ℕ \land 2^{nd} (F (n)) < r)) \to \forall k \in ℤ_{\geq n} 1^{st} (F (n)) D 1^{st} (F (k)) < r$
83	82	expr	$⊢ ((φ \land r \in ℝ^{+}) \land n \in ℕ) \to (2^{nd} (F (n)) < r \to \forall k \in ℤ_{\geq n} 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
84	83	reximdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists n \in ℕ 2^{nd} (F (n)) < r \to \exists n \in ℕ \forall k \in ℤ_{\geq n} 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
85	84	ralimdva	$⊢ φ \to (\forall r \in ℝ^{+} \exists n \in ℕ 2^{nd} (F (n)) < r \to \forall r \in ℝ^{+} \exists n \in ℕ \forall k \in ℤ_{\geq n} 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
86	4 85	mpd	$⊢ φ \to \forall r \in ℝ^{+} \exists n \in ℕ \forall k \in ℤ_{\geq n} 1^{st} (F (n)) D 1^{st} (F (k)) < r$
87		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
88		1zzd	$⊢ φ \to 1 \in ℤ$
89		fvco3	$⊢ (F : ℕ ⟶ X \times ℝ^{+} \land k \in ℕ) \to (1^{st} \circ F) (k) = 1^{st} (F (k))$
90	2 89	sylan	$⊢ (φ \land k \in ℕ) \to (1^{st} \circ F) (k) = 1^{st} (F (k))$
91		fvco3	$⊢ (F : ℕ ⟶ X \times ℝ^{+} \land n \in ℕ) \to (1^{st} \circ F) (n) = 1^{st} (F (n))$
92	2 91	sylan	$⊢ (φ \land n \in ℕ) \to (1^{st} \circ F) (n) = 1^{st} (F (n))$
93		1stcof	$⊢ F : ℕ ⟶ X \times ℝ^{+} \to (1^{st} \circ F) : ℕ ⟶ X$
94	2 93	syl	$⊢ φ \to (1^{st} \circ F) : ℕ ⟶ X$
95	87 1 88 90 92 94	iscauf	$⊢ φ \to (1^{st} \circ F \in Cau (D) \leftrightarrow \forall r \in ℝ^{+} \exists n \in ℕ \forall k \in ℤ_{\geq n} 1^{st} (F (n)) D 1^{st} (F (k)) < r)$
96	86 95	mpbird	$⊢ φ \to 1^{st} \circ F \in Cau (D)$

Metamath Proof Explorer

Theorem caubl

Proof