Theorem caurcvgr

Description: A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	caurcvgr.1	$$⊢\phi \to A\subseteq ℝ$$
	caurcvgr.2	$$⊢\phi \to F:A⟶ℝ$$
	caurcvgr.3	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
	caurcvgr.4	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
Assertion	caurcvgr	$$⊢\phi \to F\underset{ℝ}{⇝}\mathrm{lim\; sup}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		caurcvgr.1	$$⊢\phi \to A\subseteq ℝ$$
2		caurcvgr.2	$$⊢\phi \to F:A⟶ℝ$$
3		caurcvgr.3	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
4		caurcvgr.4	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
5		1rp	$$⊢1\in {ℝ}^{+}$$
6	5	a1i	$$⊢\phi \to 1\in {ℝ}^{+}$$
7	1 2 3 4 6	caucvgrlem	$$⊢\phi \to \exists j\in A\left(\mathrm{lim\; sup}\left(F\right)\in ℝ\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\cdot 1\right)\right)$$
8		simpl	$$⊢\left(\mathrm{lim\; sup}\left(F\right)\in ℝ\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\cdot 1\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in ℝ$$
9	8	rexlimivw	$$⊢\exists j\in A\left(\mathrm{lim\; sup}\left(F\right)\in ℝ\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\cdot 1\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in ℝ$$
10	7 9	syl	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\in ℝ$$
11	10	recnd	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\in ℂ$$
12	1	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to A\subseteq ℝ$$
13	2	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to F:A⟶ℝ$$
14	3	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
15	4	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \forall x\in {ℝ}^{+}\exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
16		simpr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y\in {ℝ}^{+}$$
17		3rp	$$⊢3\in {ℝ}^{+}$$
18		rpdivcl	$$⊢\left(y\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to \frac{y}{3}\in {ℝ}^{+}$$
19	16 17 18	sylancl	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \frac{y}{3}\in {ℝ}^{+}$$
20	12 13 14 15 19	caucvgrlem	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists j\in A\left(\mathrm{lim\; sup}\left(F\right)\in ℝ\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\right)$$
21		simpr	$$⊢\left(\mathrm{lim\; sup}\left(F\right)\in ℝ\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\right)\to \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)$$
22	21	reximi	$$⊢\exists j\in A\left(\mathrm{lim\; sup}\left(F\right)\in ℝ\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\right)\to \exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)$$
23	20 22	syl	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)$$
24		ssrexv	$$⊢A\subseteq ℝ\to \left(\exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\to \exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\right)$$
25	12 23 24	sylc	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)$$
26		rpcn	$$⊢y\in {ℝ}^{+}\to y\in ℂ$$
27	26	adantl	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y\in ℂ$$
28		3cn	$$⊢3\in ℂ$$
29	28	a1i	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to 3\in ℂ$$
30		3ne0	$$⊢3\ne 0$$
31	30	a1i	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to 3\ne 0$$
32	27 29 31	divcan2d	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to 3\left(\frac{y}{3}\right)=y$$
33	32	breq2d	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\leftrightarrow \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<y\right)$$
34	33	imbi2d	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\leftrightarrow \left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<y\right)\right)$$
35	34	rexralbidv	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3\left(\frac{y}{3}\right)\right)\leftrightarrow \exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<y\right)\right)$$
36	25 35	mpbid	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<y\right)$$
37	36	ralrimiva	$$⊢\phi \to \forall y\in {ℝ}^{+}\exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<y\right)$$
38		ax-resscn	$$⊢ℝ\subseteq ℂ$$
39		fss	$$⊢\left(F:A⟶ℝ\wedge ℝ\subseteq ℂ\right)\to F:A⟶ℂ$$
40	2 38 39	sylancl	$$⊢\phi \to F:A⟶ℂ$$
41		eqidd	$$⊢\left(\phi \wedge k\in A\right)\to F\left(k\right)=F\left(k\right)$$
42	40 1 41	rlim	$$⊢\phi \to \left(F\underset{ℝ}{⇝}\mathrm{lim\; sup}\left(F\right)\leftrightarrow \left(\mathrm{lim\; sup}\left(F\right)\in ℂ\wedge \forall y\in {ℝ}^{+}\exists j\in ℝ\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<y\right)\right)\right)$$
43	11 37 42	mpbir2and	$$⊢\phi \to F\underset{ℝ}{⇝}\mathrm{lim\; sup}\left(F\right)$$