# Metamath Proof Explorer

## Theorem ulmcaulem

Description: Lemma for ulmcau and ulmcau2 : show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 . (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses ulmcau.z ${⊢}{Z}={ℤ}_{\ge {M}}$
ulmcau.m ${⊢}{\phi }\to {M}\in ℤ$
ulmcau.s ${⊢}{\phi }\to {S}\in {V}$
ulmcau.f ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
Assertion ulmcaulem ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$

### Proof

Step Hyp Ref Expression
1 ulmcau.z ${⊢}{Z}={ℤ}_{\ge {M}}$
2 ulmcau.m ${⊢}{\phi }\to {M}\in ℤ$
3 ulmcau.s ${⊢}{\phi }\to {S}\in {V}$
4 ulmcau.f ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
5 breq2 ${⊢}{x}={w}\to \left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}↔\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\right)$
6 5 ralbidv ${⊢}{x}={w}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\right)$
7 6 rexralbidv ${⊢}{x}={w}\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\right)$
8 7 cbvralvw ${⊢}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}↔\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}$
9 rphalfcl ${⊢}{x}\in {ℝ}^{+}\to \frac{{x}}{2}\in {ℝ}^{+}$
10 breq2 ${⊢}{w}=\frac{{x}}{2}\to \left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}↔\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
11 10 ralbidv ${⊢}{w}=\frac{{x}}{2}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
12 11 rexralbidv ${⊢}{w}=\frac{{x}}{2}\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
13 12 rspcv ${⊢}\frac{{x}}{2}\in {ℝ}^{+}\to \left(\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
14 9 13 syl ${⊢}{x}\in {ℝ}^{+}\to \left(\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
15 14 adantl ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
16 fveq2 ${⊢}{k}={m}\to {F}\left({k}\right)={F}\left({m}\right)$
17 16 fveq1d ${⊢}{k}={m}\to {F}\left({k}\right)\left({z}\right)={F}\left({m}\right)\left({z}\right)$
18 17 fvoveq1d ${⊢}{k}={m}\to \left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|=\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|$
19 18 breq1d ${⊢}{k}={m}\to \left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}↔\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
20 19 ralbidv ${⊢}{k}={m}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
21 20 cbvralvw ${⊢}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}↔\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}$
22 21 biimpi ${⊢}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}$
23 uzss ${⊢}{k}\in {ℤ}_{\ge {j}}\to {ℤ}_{\ge {k}}\subseteq {ℤ}_{\ge {j}}$
24 23 ad2antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to {ℤ}_{\ge {k}}\subseteq {ℤ}_{\ge {j}}$
25 ssralv ${⊢}{ℤ}_{\ge {k}}\subseteq {ℤ}_{\ge {j}}\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
26 24 25 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
27 r19.26 ${⊢}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)↔\left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
28 4 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {F}:{Z}⟶{ℂ}^{{S}}$
29 28 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}:{Z}⟶{ℂ}^{{S}}$
30 1 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
31 30 adantll ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
32 1 uztrn2 ${⊢}\left({k}\in {Z}\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {m}\in {Z}$
33 31 32 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {m}\in {Z}$
34 29 33 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}\left({m}\right)\in \left({ℂ}^{{S}}\right)$
35 elmapi ${⊢}{F}\left({m}\right)\in \left({ℂ}^{{S}}\right)\to {F}\left({m}\right):{S}⟶ℂ$
36 34 35 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}\left({m}\right):{S}⟶ℂ$
37 36 ffvelrnda ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to {F}\left({m}\right)\left({z}\right)\in ℂ$
38 28 ffvelrnda ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in \left({ℂ}^{{S}}\right)$
39 38 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}\left({j}\right)\in \left({ℂ}^{{S}}\right)$
40 elmapi ${⊢}{F}\left({j}\right)\in \left({ℂ}^{{S}}\right)\to {F}\left({j}\right):{S}⟶ℂ$
41 39 40 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}\left({j}\right):{S}⟶ℂ$
42 41 ffvelrnda ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to {F}\left({j}\right)\left({z}\right)\in ℂ$
43 37 42 abssubd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to \left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|=\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|$
44 43 breq1d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to \left(\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}↔\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
45 44 biimpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to \left(\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)$
46 ffvelrn ${⊢}\left({F}:{Z}⟶{ℂ}^{{S}}\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
47 28 30 46 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge \left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
48 47 anassrs ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
49 48 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
50 elmapi ${⊢}{F}\left({k}\right)\in \left({ℂ}^{{S}}\right)\to {F}\left({k}\right):{S}⟶ℂ$
51 49 50 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to {F}\left({k}\right):{S}⟶ℂ$
52 51 ffvelrnda ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to {F}\left({k}\right)\left({z}\right)\in ℂ$
53 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
54 53 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\to {x}\in ℝ$
55 54 ad3antrrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to {x}\in ℝ$
56 abs3lem ${⊢}\left(\left({F}\left({k}\right)\left({z}\right)\in ℂ\wedge {F}\left({m}\right)\left({z}\right)\in ℂ\right)\wedge \left({F}\left({j}\right)\left({z}\right)\in ℂ\wedge {x}\in ℝ\right)\right)\to \left(\left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
57 52 37 42 55 56 syl22anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to \left(\left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
58 45 57 sylan2d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge {z}\in {S}\right)\to \left(\left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
59 58 ralimdva ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
60 27 59 syl5bir ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to \left(\left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
61 60 expdimp ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
62 61 an32s ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\wedge {m}\in {ℤ}_{\ge {k}}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
63 62 ralimdva ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left(\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
64 26 63 syld ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
65 64 impancom ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
66 65 an32s ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
67 66 ralimdva ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
68 67 ex ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)\right)$
69 68 com23 ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)\right)$
70 22 69 mpdi ${⊢}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
71 70 reximdva ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<\frac{{x}}{2}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
72 15 71 syld ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
73 72 ralrimdva ${⊢}{\phi }\to \left(\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{w}\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
74 8 73 syl5bi ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
75 eluzelz ${⊢}{j}\in {ℤ}_{\ge {M}}\to {j}\in ℤ$
76 75 1 eleq2s ${⊢}{j}\in {Z}\to {j}\in ℤ$
77 uzid ${⊢}{j}\in ℤ\to {j}\in {ℤ}_{\ge {j}}$
78 76 77 syl ${⊢}{j}\in {Z}\to {j}\in {ℤ}_{\ge {j}}$
79 78 adantl ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {j}\in {ℤ}_{\ge {j}}$
80 fveq2 ${⊢}{k}={j}\to {ℤ}_{\ge {k}}={ℤ}_{\ge {j}}$
81 fveq2 ${⊢}{k}={j}\to {F}\left({k}\right)={F}\left({j}\right)$
82 81 fveq1d ${⊢}{k}={j}\to {F}\left({k}\right)\left({z}\right)={F}\left({j}\right)\left({z}\right)$
83 82 fvoveq1d ${⊢}{k}={j}\to \left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|=\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|$
84 83 breq1d ${⊢}{k}={j}\to \left(\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
85 84 ralbidv ${⊢}{k}={j}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
86 80 85 raleqbidv ${⊢}{k}={j}\to \left(\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
87 86 rspcv ${⊢}{j}\in {ℤ}_{\ge {j}}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
88 79 87 syl ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$
89 fveq2 ${⊢}{m}={k}\to {F}\left({m}\right)={F}\left({k}\right)$
90 89 fveq1d ${⊢}{m}={k}\to {F}\left({m}\right)\left({z}\right)={F}\left({k}\right)\left({z}\right)$
91 90 oveq2d ${⊢}{m}={k}\to {F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)={F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)$
92 91 fveq2d ${⊢}{m}={k}\to \left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|=\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|$
93 92 breq1d ${⊢}{m}={k}\to \left(\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|<{x}\right)$
94 93 ralbidv ${⊢}{m}={k}\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|<{x}\right)$
95 94 cbvralvw ${⊢}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|<{x}$
96 4 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in \left({ℂ}^{{S}}\right)$
97 96 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({j}\right)\in \left({ℂ}^{{S}}\right)$
98 97 40 syl ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({j}\right):{S}⟶ℂ$
99 98 ffvelrnda ${⊢}\left(\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {z}\in {S}\right)\to {F}\left({j}\right)\left({z}\right)\in ℂ$
100 4 30 46 syl2an ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
101 100 anassrs ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
102 101 50 syl ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({k}\right):{S}⟶ℂ$
103 102 ffvelrnda ${⊢}\left(\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {z}\in {S}\right)\to {F}\left({k}\right)\left({z}\right)\in ℂ$
104 99 103 abssubd ${⊢}\left(\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {z}\in {S}\right)\to \left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|=\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|$
105 104 breq1d ${⊢}\left(\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {z}\in {S}\right)\to \left(\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|<{x}↔\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
106 105 ralbidva ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|<{x}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
107 106 ralbidva ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({k}\right)\left({z}\right)\right|<{x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
108 95 107 syl5bb ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
109 88 108 sylibd ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
110 109 reximdva ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
111 110 ralimdv ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}\right)$
112 74 111 impbid ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({j}\right)\left({z}\right)\right|<{x}↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {k}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({z}\right)-{F}\left({m}\right)\left({z}\right)\right|<{x}\right)$