caucvg

Description: A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of Gleason p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006) (Proof shortened by Mario Carneiro, 15-Feb-2014) (Revised by Mario Carneiro, 8-May-2016)

	Ref	Expression
Hypotheses	caucvg.1	$⊢ Z = ℤ_{\geq M}$
	caucvg.2	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	caucvg.3	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
	caucvg.4	$⊢ φ \to F \in V$
Assertion	caucvg	$⊢ φ \to F \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		caucvg.1	$⊢ Z = ℤ_{\geq M}$
2		caucvg.2	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
3		caucvg.3	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
4		caucvg.4	$⊢ φ \to F \in V$
5		fveq2	$⊢ k = n \to F (k) = F (n)$
6	5	cbvmptv	$⊢ (k \in Z ⟼ F (k)) = (n \in Z ⟼ F (n))$
7		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
8	1 7	eqsstri	$⊢ Z \subseteq ℤ$
9		zssre	$⊢ ℤ \subseteq ℝ$
10	8 9	sstri	$⊢ Z \subseteq ℝ$
11	10	a1i	$⊢ φ \to Z \subseteq ℝ$
12	6	eqcomi	$⊢ (n \in Z ⟼ F (n)) = (k \in Z ⟼ F (k))$
13	2 12	fmptd	$⊢ φ \to (n \in Z ⟼ F (n)) : Z ⟶ ℂ$
14		1rp	$⊢ 1 \in ℝ^{+}$
15	14	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
16		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x) \to \exists x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
17	15 3 16	sylancr	$⊢ φ \to \exists x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
18		eluzel2	$⊢ j \in ℤ_{\geq M} \to M \in ℤ$
19	18 1	eleq2s	$⊢ j \in Z \to M \in ℤ$
20	19	a1d	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to M \in ℤ)$
21	20	rexlimiv	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to M \in ℤ$
22	21	rexlimivw	$⊢ \exists x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to M \in ℤ$
23	17 22	syl	$⊢ φ \to M \in ℤ$
24	1	uzsup	$⊢ M \in ℤ \to sup (Z ℝ^{*} <) = +∞$
25	23 24	syl	$⊢ φ \to sup (Z ℝ^{*} <) = +∞$
26	8	sseli	$⊢ j \in Z \to j \in ℤ$
27	8	sseli	$⊢ k \in Z \to k \in ℤ$
28		eluz	$⊢ (j \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq j} \leftrightarrow j \leq k)$
29	26 27 28	syl2an	$⊢ (j \in Z \land k \in Z) \to (k \in ℤ_{\geq j} \leftrightarrow j \leq k)$
30	29	biimprd	$⊢ (j \in Z \land k \in Z) \to (j \leq k \to k \in ℤ_{\geq j})$
31		fveq2	$⊢ n = k \to F (n) = F (k)$
32		eqid	$⊢ (n \in Z ⟼ F (n)) = (n \in Z ⟼ F (n))$
33		fvex	$⊢ F (n) \in V$
34	31 32 33	fvmpt3i	$⊢ k \in Z \to (n \in Z ⟼ F (n)) (k) = F (k)$
35		fveq2	$⊢ n = j \to F (n) = F (j)$
36	35 32 33	fvmpt3i	$⊢ j \in Z \to (n \in Z ⟼ F (n)) (j) = F (j)$
37	34 36	oveqan12rd	$⊢ (j \in Z \land k \in Z) \to (n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j) = F (k) - F (j)$
38	37	fveq2d	$⊢ (j \in Z \land k \in Z) \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| = \|F (k) - F (j)\|$
39	38	breq1d	$⊢ (j \in Z \land k \in Z) \to (\|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x \leftrightarrow \|F (k) - F (j)\| < x)$
40	39	biimprd	$⊢ (j \in Z \land k \in Z) \to (\|F (k) - F (j)\| < x \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x)$
41	30 40	imim12d	$⊢ (j \in Z \land k \in Z) \to ((k \in ℤ_{\geq j} \to \|F (k) - F (j)\| < x) \to (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x))$
42	41	ex	$⊢ j \in Z \to (k \in Z \to ((k \in ℤ_{\geq j} \to \|F (k) - F (j)\| < x) \to (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x)))$
43	42	com23	$⊢ j \in Z \to ((k \in ℤ_{\geq j} \to \|F (k) - F (j)\| < x) \to (k \in Z \to (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x)))$
44	43	ralimdv2	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to \forall k \in Z (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x))$
45	44	reximia	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to \exists j \in Z \forall k \in Z (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x)$
46	45	ralimi	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in Z (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x)$
47	3 46	syl	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in Z (j \leq k \to \|(n \in Z ⟼ F (n)) (k) - (n \in Z ⟼ F (n)) (j)\| < x)$
48	11 13 25 47	caucvgr	$⊢ φ \to (n \in Z ⟼ F (n)) \in dom \underset{ℝ}{⇝}$
49	13 25	rlimdm	$⊢ φ \to ((n \in Z ⟼ F (n)) \in dom \underset{ℝ}{⇝} \leftrightarrow (n \in Z ⟼ F (n)) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))))$
50	48 49	mpbid	$⊢ φ \to (n \in Z ⟼ F (n)) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((n \in Z ⟼ F (n)))$
51	6 50	eqbrtrid	$⊢ φ \to (k \in Z ⟼ F (k)) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((n \in Z ⟼ F (n)))$
52		eqid	$⊢ (k \in Z ⟼ F (k)) = (k \in Z ⟼ F (k))$
53	2 52	fmptd	$⊢ φ \to (k \in Z ⟼ F (k)) : Z ⟶ ℂ$
54	1 23 53	rlimclim	$⊢ φ \to ((k \in Z ⟼ F (k)) \underset{ℝ}{⇝} \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))) \leftrightarrow (k \in Z ⟼ F (k)) ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))))$
55	51 54	mpbid	$⊢ φ \to (k \in Z ⟼ F (k)) ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n)))$
56	1 52	climmpt	$⊢ (M \in ℤ \land F \in V) \to (F ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))) \leftrightarrow (k \in Z ⟼ F (k)) ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))))$
57	23 4 56	syl2anc	$⊢ φ \to (F ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))) \leftrightarrow (k \in Z ⟼ F (k)) ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))))$
58	55 57	mpbird	$⊢ φ \to F ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n)))$
59		climrel	$⊢ Rel ⇝$
60	59	releldmi	$⊢ F ⇝ \underset{ℝ}{⇝} ((n \in Z ⟼ F (n))) \to F \in dom ⇝$
61	58 60	syl	$⊢ φ \to F \in dom ⇝$

Metamath Proof Explorer

Theorem caucvg

Proof