Theorem caucvgrlem

Description: Lemma for caurcvgr . (Contributed by Mario Carneiro, 15-Feb-2014) (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)$$
	caucvgrlem.4	$$⊢\phi \to R\in {ℝ}^{+}$$
Assertion	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|<3R\right)\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		caucvgrlem.4	$$⊢\phi \to R\in {ℝ}^{+}$$
6		reex	$$⊢ℝ\in \mathrm{V}$$
7	6	ssex	$$⊢A\subseteq ℝ\to A\in \mathrm{V}$$
8	1 7	syl	$$⊢\phi \to A\in \mathrm{V}$$
9	6	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
10		fex2	$$⊢\left(F:A⟶ℝ\wedge A\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\to F\in \mathrm{V}$$
11	2 8 9 10	syl3anc	$$⊢\phi \to F\in \mathrm{V}$$
12		limsupcl	$$⊢F\in \mathrm{V}\to \mathrm{lim\; sup}\left(F\right)\in {ℝ}^{*}$$
13	11 12	syl	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\in {ℝ}^{*}$$
14	13	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in {ℝ}^{*}$$
15	2	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F:A⟶ℝ$$
16		simprl	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to j\in A$$
17	15 16	ffvelcdmd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F\left(j\right)\in ℝ$$
18	5	rpred	$$⊢\phi \to R\in ℝ$$
19	18	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to R\in ℝ$$
20	17 19	readdcld	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F\left(j\right)+R\in ℝ$$
21		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
22	21	a1i	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$$
23	17 19	resubcld	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F\left(j\right)-R\in ℝ$$
24	23	rexrd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F\left(j\right)-R\in {ℝ}^{*}$$
25	23	mnfltd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \mathrm{-\infty }<F\left(j\right)-R$$
26	1	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to A\subseteq ℝ$$
27		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
28		fss	$$⊢\left(F:A⟶ℝ\wedge ℝ\subseteq {ℝ}^{*}\right)\to F:A⟶{ℝ}^{*}$$
29	2 27 28	sylancl	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
30	29	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F:A⟶{ℝ}^{*}$$
31	3	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
32	26 16	sseldd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to j\in ℝ$$
33		simprr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)$$
34		breq2	$$⊢k=m\to \left(j\le k\leftrightarrow j\le m\right)$$
35	34	imbrov2fvoveq	$$⊢k=m\to \left(\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\leftrightarrow \left(j\le m\to \left|F\left(m\right)-F\left(j\right)\right|<R\right)\right)$$
36	35	cbvralvw	$$⊢\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\leftrightarrow \forall m\in A\left(j\le m\to \left|F\left(m\right)-F\left(j\right)\right|<R\right)$$
37	33 36	sylib	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \forall m\in A\left(j\le m\to \left|F\left(m\right)-F\left(j\right)\right|<R\right)$$
38	15	ffvelcdmda	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to F\left(m\right)\in ℝ$$
39	17	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to F\left(j\right)\in ℝ$$
40	38 39	resubcld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to F\left(m\right)-F\left(j\right)\in ℝ$$
41	40	recnd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to F\left(m\right)-F\left(j\right)\in ℂ$$
42	41	abscld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left|F\left(m\right)-F\left(j\right)\right|\in ℝ$$
43	19	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to R\in ℝ$$
44		ltle	$$⊢\left(\left|F\left(m\right)-F\left(j\right)\right|\in ℝ\wedge R\in ℝ\right)\to \left(\left|F\left(m\right)-F\left(j\right)\right|<R\to \left|F\left(m\right)-F\left(j\right)\right|\le R\right)$$
45	42 43 44	syl2anc	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(\left|F\left(m\right)-F\left(j\right)\right|<R\to \left|F\left(m\right)-F\left(j\right)\right|\le R\right)$$
46	38 39 43	absdifled	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(\left|F\left(m\right)-F\left(j\right)\right|\le R\leftrightarrow \left(F\left(j\right)-R\le F\left(m\right)\wedge F\left(m\right)\le F\left(j\right)+R\right)\right)$$
47	45 46	sylibd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(\left|F\left(m\right)-F\left(j\right)\right|<R\to \left(F\left(j\right)-R\le F\left(m\right)\wedge F\left(m\right)\le F\left(j\right)+R\right)\right)$$
48		simpl	$$⊢\left(F\left(j\right)-R\le F\left(m\right)\wedge F\left(m\right)\le F\left(j\right)+R\right)\to F\left(j\right)-R\le F\left(m\right)$$
49	47 48	syl6	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(\left|F\left(m\right)-F\left(j\right)\right|<R\to F\left(j\right)-R\le F\left(m\right)\right)$$
50	49	imim2d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(\left(j\le m\to \left|F\left(m\right)-F\left(j\right)\right|<R\right)\to \left(j\le m\to F\left(j\right)-R\le F\left(m\right)\right)\right)$$
51	50	ralimdva	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \left(\forall m\in A\left(j\le m\to \left|F\left(m\right)-F\left(j\right)\right|<R\right)\to \forall m\in A\left(j\le m\to F\left(j\right)-R\le F\left(m\right)\right)\right)$$
52	37 51	mpd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \forall m\in A\left(j\le m\to F\left(j\right)-R\le F\left(m\right)\right)$$
53		breq1	$$⊢n=j\to \left(n\le m\leftrightarrow j\le m\right)$$
54	53	rspceaimv	$$⊢\left(j\in ℝ\wedge \forall m\in A\left(j\le m\to F\left(j\right)-R\le F\left(m\right)\right)\right)\to \exists n\in ℝ\forall m\in A\left(n\le m\to F\left(j\right)-R\le F\left(m\right)\right)$$
55	32 52 54	syl2anc	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \exists n\in ℝ\forall m\in A\left(n\le m\to F\left(j\right)-R\le F\left(m\right)\right)$$
56	26 30 24 31 55	limsupbnd2	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F\left(j\right)-R\le \mathrm{lim\; sup}\left(F\right)$$
57	22 24 14 25 56	xrltletrd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \mathrm{-\infty }<\mathrm{lim\; sup}\left(F\right)$$
58	20	rexrd	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to F\left(j\right)+R\in {ℝ}^{*}$$
59	42	adantrr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-F\left(j\right)\right|\in ℝ$$
60	19	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to R\in ℝ$$
61		simprr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to j\le m$$
62		simplrr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)$$
63		simprl	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to m\in A$$
64	35 62 63	rspcdva	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(j\le m\to \left|F\left(m\right)-F\left(j\right)\right|<R\right)$$
65	61 64	mpd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-F\left(j\right)\right|<R$$
66	59 60 65	ltled	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-F\left(j\right)\right|\le R$$
67	38	adantrr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)\in ℝ$$
68	17	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)\in ℝ$$
69	67 68 60	absdifled	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(\left|F\left(m\right)-F\left(j\right)\right|\le R\leftrightarrow \left(F\left(j\right)-R\le F\left(m\right)\wedge F\left(m\right)\le F\left(j\right)+R\right)\right)$$
70	66 69	mpbid	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(F\left(j\right)-R\le F\left(m\right)\wedge F\left(m\right)\le F\left(j\right)+R\right)$$
71	70	simprd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)\le F\left(j\right)+R$$
72	71	expr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(j\le m\to F\left(m\right)\le F\left(j\right)+R\right)$$
73	72	ralrimiva	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \forall m\in A\left(j\le m\to F\left(m\right)\le F\left(j\right)+R\right)$$
74	53	rspceaimv	$$⊢\left(j\in ℝ\wedge \forall m\in A\left(j\le m\to F\left(m\right)\le F\left(j\right)+R\right)\right)\to \exists n\in ℝ\forall m\in A\left(n\le m\to F\left(m\right)\le F\left(j\right)+R\right)$$
75	32 73 74	syl2anc	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \exists n\in ℝ\forall m\in A\left(n\le m\to F\left(m\right)\le F\left(j\right)+R\right)$$
76	26 30 58 75	limsupbnd1	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \mathrm{lim\; sup}\left(F\right)\le F\left(j\right)+R$$
77		xrre	$$⊢\left(\left(\mathrm{lim\; sup}\left(F\right)\in {ℝ}^{*}\wedge F\left(j\right)+R\in ℝ\right)\wedge \left(\mathrm{-\infty }<\mathrm{lim\; sup}\left(F\right)\wedge \mathrm{lim\; sup}\left(F\right)\le F\left(j\right)+R\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in ℝ$$
78	14 20 57 76 77	syl22anc	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in ℝ$$
79	78	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in ℝ$$
80	67 79	resubcld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\in ℝ$$
81	80	recnd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\in ℂ$$
82	81	abscld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|\in ℝ$$
83		2re	$$⊢2\in ℝ$$
84		remulcl	$$⊢\left(2\in ℝ\wedge R\in ℝ\right)\to 2R\in ℝ$$
85	83 60 84	sylancr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to 2R\in ℝ$$
86		3re	$$⊢3\in ℝ$$
87		remulcl	$$⊢\left(3\in ℝ\wedge R\in ℝ\right)\to 3R\in ℝ$$
88	86 60 87	sylancr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to 3R\in ℝ$$
89	67	recnd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)\in ℂ$$
90	79	recnd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \mathrm{lim\; sup}\left(F\right)\in ℂ$$
91	89 90	abssubd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|=\left|\mathrm{lim\; sup}\left(F\right)-F\left(m\right)\right|$$
92	67 85	resubcld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-2R\in ℝ$$
93	23	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)-R\in ℝ$$
94	60	recnd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to R\in ℂ$$
95	94	2timesd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to 2R=R+R$$
96	95	oveq2d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-2R=F\left(m\right)-\left(R+R\right)$$
97	89 94 94	subsub4d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-R-R=F\left(m\right)-\left(R+R\right)$$
98	96 97	eqtr4d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-2R=F\left(m\right)-R-R$$
99	67 60	resubcld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-R\in ℝ$$
100	67 60 68	lesubaddd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(F\left(m\right)-R\le F\left(j\right)\leftrightarrow F\left(m\right)\le F\left(j\right)+R\right)$$
101	71 100	mpbird	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-R\le F\left(j\right)$$
102	99 68 60 101	lesub1dd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-R-R\le F\left(j\right)-R$$
103	98 102	eqbrtrd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-2R\le F\left(j\right)-R$$
104	56	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)-R\le \mathrm{lim\; sup}\left(F\right)$$
105	92 93 79 103 104	letrd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)-2R\le \mathrm{lim\; sup}\left(F\right)$$
106	20	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)+R\in ℝ$$
107	67 85	readdcld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)+2R\in ℝ$$
108	76	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \mathrm{lim\; sup}\left(F\right)\le F\left(j\right)+R$$
109	67 60	readdcld	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)+R\in ℝ$$
110	70 48	syl	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)-R\le F\left(m\right)$$
111	68 60 67	lesubaddd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(F\left(j\right)-R\le F\left(m\right)\leftrightarrow F\left(j\right)\le F\left(m\right)+R\right)$$
112	110 111	mpbid	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)\le F\left(m\right)+R$$
113	68 109 60 112	leadd1dd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)+R\le F\left(m\right)+R+R$$
114	89 94 94	addassd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)+R+R=F\left(m\right)+R+R$$
115	95	oveq2d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)+2R=F\left(m\right)+R+R$$
116	114 115	eqtr4d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(m\right)+R+R=F\left(m\right)+2R$$
117	113 116	breqtrd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to F\left(j\right)+R\le F\left(m\right)+2R$$
118	79 106 107 108 117	letrd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \mathrm{lim\; sup}\left(F\right)\le F\left(m\right)+2R$$
119	79 67 85	absdifled	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(\left|\mathrm{lim\; sup}\left(F\right)-F\left(m\right)\right|\le 2R\leftrightarrow \left(F\left(m\right)-2R\le \mathrm{lim\; sup}\left(F\right)\wedge \mathrm{lim\; sup}\left(F\right)\le F\left(m\right)+2R\right)\right)$$
120	105 118 119	mpbir2and	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|\mathrm{lim\; sup}\left(F\right)-F\left(m\right)\right|\le 2R$$
121	91 120	eqbrtrd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|\le 2R$$
122		2lt3	$$⊢2<3$$
123	83	a1i	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to 2\in ℝ$$
124	86	a1i	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to 3\in ℝ$$
125	5	adantr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to R\in {ℝ}^{+}$$
126	125	adantr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to R\in {ℝ}^{+}$$
127	123 124 126	ltmul1d	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left(2<3\leftrightarrow 2R<3R\right)$$
128	122 127	mpbii	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to 2R<3R$$
129	82 85 88 121 128	lelttrd	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge \left(m\in A\wedge j\le m\right)\right)\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R$$
130	129	expr	$$⊢\left(\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\wedge m\in A\right)\to \left(j\le m\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R\right)$$
131	130	ralrimiva	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \forall m\in A\left(j\le m\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R\right)$$
132	34	imbrov2fvoveq	$$⊢k=m\to \left(\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R\right)\leftrightarrow \left(j\le m\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R\right)\right)$$
133	132	cbvralvw	$$⊢\forall k\in A\left(j\le k\to \left|F\left(k\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R\right)\leftrightarrow \forall m\in A\left(j\le m\to \left|F\left(m\right)-\mathrm{lim\; sup}\left(F\right)\right|<3R\right)$$
134	131 133	sylibr	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\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|<3R\right)$$
135	78 134	jca	$$⊢\left(\phi \wedge \left(j\in A\wedge \forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)\right)\to \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|<3R\right)\right)$$
136		breq2	$$⊢x=R\to \left(\left|F\left(k\right)-F\left(j\right)\right|<x\leftrightarrow \left|F\left(k\right)-F\left(j\right)\right|<R\right)$$
137	136	imbi2d	$$⊢x=R\to \left(\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<x\right)\leftrightarrow \left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)$$
138	137	rexralbidv	$$⊢x=R\to \left(\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)\leftrightarrow \exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)\right)$$
139	138 4 5	rspcdva	$$⊢\phi \to \exists j\in A\forall k\in A\left(j\le k\to \left|F\left(k\right)-F\left(j\right)\right|<R\right)$$
140	135 139	reximddv	$$⊢\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|<3R\right)\right)$$