Theorem caubnd

Description: A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005) (Revised by Mario Carneiro, 14-Feb-2014)

	Ref	Expression
Hypothesis	cau3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	caubnd	$$⊢\left(\forall k\in ZF\left(k\right)\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y$$

Proof

Step	Hyp	Ref	Expression
1		cau3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		abscl	$$⊢F\left(k\right)\in ℂ\to \left|F\left(k\right)\right|\in ℝ$$
3	2	ralimi	$$⊢\forall k\in ZF\left(k\right)\in ℂ\to \forall k\in Z\left|F\left(k\right)\right|\in ℝ$$
4	1	r19.29uz	$$⊢\left(\forall k\in ZF\left(k\right)\in ℂ\wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
5	4	ex	$$⊢\forall k\in ZF\left(k\right)\in ℂ\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\right)$$
6	5	ralimdv	$$⊢\forall k\in ZF\left(k\right)\in ℂ\to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\to \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\right)$$
7	1	caubnd2	$$⊢\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\to \exists z\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z$$
8	6 7	syl6	$$⊢\forall k\in ZF\left(k\right)\in ℂ\to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\to \exists z\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\right)$$
9		fzssuz	$$⊢\left(M\dots j\right)\subseteq {\mathbb{Z}}_{\ge M}$$
10	9 1	sseqtrri	$$⊢\left(M\dots j\right)\subseteq Z$$
11		ssralv	$$⊢\left(M\dots j\right)\subseteq Z\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\right)$$
12	10 11	ax-mp	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ$$
13		fzfi	$$⊢\left(M\dots j\right)\in \mathrm{Fin}$$
14		fimaxre3	$$⊢\left(\left(M\dots j\right)\in \mathrm{Fin}\wedge \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\right)\to \exists x\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\le x$$
15	13 14	mpan	$$⊢\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\to \exists x\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\le x$$
16		peano2re	$$⊢x\in ℝ\to x+1\in ℝ$$
17	16	adantl	$$⊢\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to x+1\in ℝ$$
18		ltp1	$$⊢x\in ℝ\to x<x+1$$
19	18	adantl	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to x<x+1$$
20	16	adantl	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to x+1\in ℝ$$
21		lelttr	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\wedge x+1\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|\le x\wedge x<x+1\right)\to \left|F\left(k\right)\right|<x+1\right)$$
22	20 21	mpd3an3	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|\le x\wedge x<x+1\right)\to \left|F\left(k\right)\right|<x+1\right)$$
23	19 22	mpan2d	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to \left(\left|F\left(k\right)\right|\le x\to \left|F\left(k\right)\right|<x+1\right)$$
24	23	expcom	$$⊢x\in ℝ\to \left(\left|F\left(k\right)\right|\in ℝ\to \left(\left|F\left(k\right)\right|\le x\to \left|F\left(k\right)\right|<x+1\right)\right)$$
25	24	ralimdv	$$⊢x\in ℝ\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\to \forall k\in \left(M\dots j\right)\left(\left|F\left(k\right)\right|\le x\to \left|F\left(k\right)\right|<x+1\right)\right)$$
26	25	impcom	$$⊢\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to \forall k\in \left(M\dots j\right)\left(\left|F\left(k\right)\right|\le x\to \left|F\left(k\right)\right|<x+1\right)$$
27		ralim	$$⊢\forall k\in \left(M\dots j\right)\left(\left|F\left(k\right)\right|\le x\to \left|F\left(k\right)\right|<x+1\right)\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\le x\to \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<x+1\right)$$
28	26 27	syl	$$⊢\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\le x\to \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<x+1\right)$$
29		brralrspcev	$$⊢\left(x+1\in ℝ\wedge \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<x+1\right)\to \exists w\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w$$
30	17 28 29	syl6an	$$⊢\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\wedge x\in ℝ\right)\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\le x\to \exists w\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\right)$$
31	30	rexlimdva	$$⊢\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\to \left(\exists x\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\le x\to \exists w\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\right)$$
32	15 31	mpd	$$⊢\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|\in ℝ\to \exists w\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w$$
33	12 32	syl	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \exists w\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w$$
34		max1	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to w\le if\left(w\le z,z,w\right)$$
35	34	3adant3	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to w\le if\left(w\le z,z,w\right)$$
36		simp3	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to \left|F\left(k\right)\right|\in ℝ$$
37		simp1	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to w\in ℝ$$
38		ifcl	$$⊢\left(z\in ℝ\wedge w\in ℝ\right)\to if\left(w\le z,z,w\right)\in ℝ$$
39	38	ancoms	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to if\left(w\le z,z,w\right)\in ℝ$$
40	39	3adant3	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to if\left(w\le z,z,w\right)\in ℝ$$
41		ltletr	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge w\in ℝ\wedge if\left(w\le z,z,w\right)\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|<w\wedge w\le if\left(w\le z,z,w\right)\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
42	36 37 40 41	syl3anc	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|<w\wedge w\le if\left(w\le z,z,w\right)\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
43	35 42	mpan2d	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to \left(\left|F\left(k\right)\right|<w\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
44		max2	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to z\le if\left(w\le z,z,w\right)$$
45	44	3adant3	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to z\le if\left(w\le z,z,w\right)$$
46		simp2	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to z\in ℝ$$
47		ltletr	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge z\in ℝ\wedge if\left(w\le z,z,w\right)\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|<z\wedge z\le if\left(w\le z,z,w\right)\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
48	36 46 40 47	syl3anc	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|<z\wedge z\le if\left(w\le z,z,w\right)\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
49	45 48	mpan2d	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to \left(\left|F\left(k\right)\right|<z\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
50	43 49	jaod	$$⊢\left(w\in ℝ\wedge z\in ℝ\wedge \left|F\left(k\right)\right|\in ℝ\right)\to \left(\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
51	50	3expia	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(\left|F\left(k\right)\right|\in ℝ\to \left(\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)\right)$$
52	51	ralimdv	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \forall k\in Z\left(\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)\right)$$
53		ralim	$$⊢\forall k\in Z\left(\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)\to \left(\forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \forall k\in Z\left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)$$
54	52 53	syl6	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \forall k\in Z\left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)\right)$$
55		brralrspcev	$$⊢\left(if\left(w\le z,z,w\right)\in ℝ\wedge \forall k\in Z\left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y$$
56	55	ex	$$⊢if\left(w\le z,z,w\right)\in ℝ\to \left(\forall k\in Z\left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)$$
57	39 56	syl	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(\forall k\in Z\left|F\left(k\right)\right|<if\left(w\le z,z,w\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)$$
58	54 57	syl6d	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)$$
59		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
60	1 59	eqsstri	$$⊢Z\subseteq \mathbb{Z}$$
61	60	sseli	$$⊢k\in Z\to k\in \mathbb{Z}$$
62	60	sseli	$$⊢j\in Z\to j\in \mathbb{Z}$$
63		uztric	$$⊢\left(k\in \mathbb{Z}\wedge j\in \mathbb{Z}\right)\to \left(j\in {\mathbb{Z}}_{\ge k}\vee k\in {\mathbb{Z}}_{\ge j}\right)$$
64	61 62 63	syl2anr	$$⊢\left(j\in Z\wedge k\in Z\right)\to \left(j\in {\mathbb{Z}}_{\ge k}\vee k\in {\mathbb{Z}}_{\ge j}\right)$$
65		simpr	$$⊢\left(j\in Z\wedge k\in Z\right)\to k\in Z$$
66	65 1	eleqtrdi	$$⊢\left(j\in Z\wedge k\in Z\right)\to k\in {\mathbb{Z}}_{\ge M}$$
67		elfzuzb	$$⊢k\in \left(M\dots j\right)\leftrightarrow \left(k\in {\mathbb{Z}}_{\ge M}\wedge j\in {\mathbb{Z}}_{\ge k}\right)$$
68	67	baib	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left(k\in \left(M\dots j\right)\leftrightarrow j\in {\mathbb{Z}}_{\ge k}\right)$$
69	66 68	syl	$$⊢\left(j\in Z\wedge k\in Z\right)\to \left(k\in \left(M\dots j\right)\leftrightarrow j\in {\mathbb{Z}}_{\ge k}\right)$$
70	69	orbi1d	$$⊢\left(j\in Z\wedge k\in Z\right)\to \left(\left(k\in \left(M\dots j\right)\vee k\in {\mathbb{Z}}_{\ge j}\right)\leftrightarrow \left(j\in {\mathbb{Z}}_{\ge k}\vee k\in {\mathbb{Z}}_{\ge j}\right)\right)$$
71	64 70	mpbird	$$⊢\left(j\in Z\wedge k\in Z\right)\to \left(k\in \left(M\dots j\right)\vee k\in {\mathbb{Z}}_{\ge j}\right)$$
72	71	ex	$$⊢j\in Z\to \left(k\in Z\to \left(k\in \left(M\dots j\right)\vee k\in {\mathbb{Z}}_{\ge j}\right)\right)$$
73		pm3.48	$$⊢\left(\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)\to \left(\left(k\in \left(M\dots j\right)\vee k\in {\mathbb{Z}}_{\ge j}\right)\to \left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\right)$$
74	72 73	syl9	$$⊢j\in Z\to \left(\left(\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)\to \left(k\in Z\to \left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\right)\right)$$
75	74	alimdv	$$⊢j\in Z\to \left(\forall k\left(\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)\to \forall k\left(k\in Z\to \left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\right)\right)$$
76		df-ral	$$⊢\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\leftrightarrow \forall k\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)$$
77		df-ral	$$⊢\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\leftrightarrow \forall k\left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)$$
78	76 77	anbi12i	$$⊢\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\wedge \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\right)\leftrightarrow \left(\forall k\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \forall k\left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)$$
79		19.26	$$⊢\forall k\left(\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)\leftrightarrow \left(\forall k\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \forall k\left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)$$
80	78 79	bitr4i	$$⊢\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\wedge \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\right)\leftrightarrow \forall k\left(\left(k\in \left(M\dots j\right)\to \left|F\left(k\right)\right|<w\right)\wedge \left(k\in {\mathbb{Z}}_{\ge j}\to \left|F\left(k\right)\right|<z\right)\right)$$
81		df-ral	$$⊢\forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\leftrightarrow \forall k\left(k\in Z\to \left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\right)$$
82	75 80 81	3imtr4g	$$⊢j\in Z\to \left(\left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\wedge \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\right)\to \forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\right)$$
83	82	3impib	$$⊢\left(j\in Z\wedge \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\wedge \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\right)\to \forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)$$
84	83	imim1i	$$⊢\left(\forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\to \left(\left(j\in Z\wedge \forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\wedge \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)$$
85	84	3expd	$$⊢\left(\forall k\in Z\left(\left|F\left(k\right)\right|<w\vee \left|F\left(k\right)\right|<z\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\to \left(j\in Z\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)$$
86	58 85	syl6	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(j\in Z\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)\right)$$
87	86	com23	$$⊢\left(w\in ℝ\wedge z\in ℝ\right)\to \left(j\in Z\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)\right)$$
88	87	expimpd	$$⊢w\in ℝ\to \left(\left(z\in ℝ\wedge j\in Z\right)\to \left(\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)\right)$$
89	88	com3r	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(w\in ℝ\to \left(\left(z\in ℝ\wedge j\in Z\right)\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)\right)$$
90	89	com34	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(w\in ℝ\to \left(\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\left(z\in ℝ\wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)\right)$$
91	90	rexlimdv	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\exists w\in ℝ\forall k\in \left(M\dots j\right)\left|F\left(k\right)\right|<w\to \left(\left(z\in ℝ\wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)\right)$$
92	33 91	mpd	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\left(z\in ℝ\wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)\right)$$
93	92	rexlimdvv	$$⊢\forall k\in Z\left|F\left(k\right)\right|\in ℝ\to \left(\exists z\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\right|<z\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)$$
94	3 8 93	sylsyld	$$⊢\forall k\in ZF\left(k\right)\in ℂ\to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y\right)$$
95	94	imp	$$⊢\left(\forall k\in ZF\left(k\right)\in ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-F\left(j\right)\right|<x\right)\to \exists y\in ℝ\forall k\in Z\left|F\left(k\right)\right|<y$$