caurcvg

Description: A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	caurcvg.1	$⊢ Z = ℤ_{\geq M}$
	caurcvg.3	$⊢ φ \to F : Z ⟶ ℝ$
	caurcvg.4	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x$
Assertion	caurcvg	$⊢ φ \to F ⇝ lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		caurcvg.1	$⊢ Z = ℤ_{\geq M}$
2		caurcvg.3	$⊢ φ \to F : Z ⟶ ℝ$
3		caurcvg.4	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x$
4		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
5	1 4	eqsstri	$⊢ Z \subseteq ℤ$
6		zssre	$⊢ ℤ \subseteq ℝ$
7	5 6	sstri	$⊢ Z \subseteq ℝ$
8	7	a1i	$⊢ φ \to Z \subseteq ℝ$
9		1rp	$⊢ 1 \in ℝ^{+}$
10	9	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
11		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x) \to \exists x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x$
12	10 3 11	sylancr	$⊢ φ \to \exists x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x$
13		eluzel2	$⊢ m \in ℤ_{\geq M} \to M \in ℤ$
14	13 1	eleq2s	$⊢ m \in Z \to M \in ℤ$
15	1	uzsup	$⊢ M \in ℤ \to sup (Z ℝ^{*} <) = +∞$
16	14 15	syl	$⊢ m \in Z \to sup (Z ℝ^{*} <) = +∞$
17	16	a1d	$⊢ m \in Z \to (\forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to sup (Z ℝ^{*} <) = +∞)$
18	17	rexlimiv	$⊢ \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to sup (Z ℝ^{*} <) = +∞$
19	18	rexlimivw	$⊢ \exists x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to sup (Z ℝ^{*} <) = +∞$
20	12 19	syl	$⊢ φ \to sup (Z ℝ^{*} <) = +∞$
21	5	sseli	$⊢ m \in Z \to m \in ℤ$
22	5	sseli	$⊢ k \in Z \to k \in ℤ$
23		eluz	$⊢ (m \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq m} \leftrightarrow m \leq k)$
24	21 22 23	syl2an	$⊢ (m \in Z \land k \in Z) \to (k \in ℤ_{\geq m} \leftrightarrow m \leq k)$
25	24	biimprd	$⊢ (m \in Z \land k \in Z) \to (m \leq k \to k \in ℤ_{\geq m})$
26	25	expimpd	$⊢ m \in Z \to ((k \in Z \land m \leq k) \to k \in ℤ_{\geq m})$
27	26	imim1d	$⊢ m \in Z \to ((k \in ℤ_{\geq m} \to \|F (k) - F (m)\| < x) \to ((k \in Z \land m \leq k) \to \|F (k) - F (m)\| < x))$
28	27	exp4a	$⊢ m \in Z \to ((k \in ℤ_{\geq m} \to \|F (k) - F (m)\| < x) \to (k \in Z \to (m \leq k \to \|F (k) - F (m)\| < x)))$
29	28	ralimdv2	$⊢ m \in Z \to (\forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to \forall k \in Z (m \leq k \to \|F (k) - F (m)\| < x))$
30	29	reximia	$⊢ \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to \exists m \in Z \forall k \in Z (m \leq k \to \|F (k) - F (m)\| < x)$
31	30	ralimi	$⊢ \forall x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to \forall x \in ℝ^{+} \exists m \in Z \forall k \in Z (m \leq k \to \|F (k) - F (m)\| < x)$
32	3 31	syl	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall k \in Z (m \leq k \to \|F (k) - F (m)\| < x)$
33	8 2 20 32	caurcvgr	$⊢ φ \to F \underset{ℝ}{⇝} lim sup (F)$
34	14	a1d	$⊢ m \in Z \to (\forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to M \in ℤ)$
35	34	rexlimiv	$⊢ \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to M \in ℤ$
36	35	rexlimivw	$⊢ \exists x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x \to M \in ℤ$
37	12 36	syl	$⊢ φ \to M \in ℤ$
38		ax-resscn	$⊢ ℝ \subseteq ℂ$
39		fss	$⊢ (F : Z ⟶ ℝ \land ℝ \subseteq ℂ) \to F : Z ⟶ ℂ$
40	2 38 39	sylancl	$⊢ φ \to F : Z ⟶ ℂ$
41	1 37 40	rlimclim	$⊢ φ \to (F \underset{ℝ}{⇝} lim sup (F) \leftrightarrow F ⇝ lim sup (F))$
42	33 41	mpbid	$⊢ φ \to F ⇝ lim sup (F)$

Metamath Proof Explorer

Theorem caurcvg

Proof