# Metamath Proof Explorer

## Theorem fnlimabslt

Description: A sequence of function values, approximates the corresponding limit function value, all but finitely many times. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimabslt.p ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
fnlimabslt.f ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}$
fnlimabslt.n ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
fnlimabslt.m ${⊢}{\phi }\to {M}\in ℤ$
fnlimabslt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
fnlimabslt.b ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
fnlimabslt.d ${⊢}{D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
fnlimabslt.g ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
fnlimabslt.x ${⊢}{\phi }\to {X}\in {D}$
fnlimabslt.y ${⊢}{\phi }\to {Y}\in {ℝ}^{+}$
Assertion fnlimabslt ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℝ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$

### Proof

Step Hyp Ref Expression
1 fnlimabslt.p ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fnlimabslt.f ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}$
3 fnlimabslt.n ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
4 fnlimabslt.m ${⊢}{\phi }\to {M}\in ℤ$
5 fnlimabslt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
6 fnlimabslt.b ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
7 fnlimabslt.d ${⊢}{D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
8 fnlimabslt.g ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
9 fnlimabslt.x ${⊢}{\phi }\to {X}\in {D}$
10 fnlimabslt.y ${⊢}{\phi }\to {Y}\in {ℝ}^{+}$
11 eqid ${⊢}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
12 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Z}$
13 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{ℤ}_{\ge {n}}$
14 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{m}$
15 3 14 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)$
16 15 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({m}\right)$
17 13 16 nfiin ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
18 12 17 nfiun ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
19 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
20 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
21 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
22 15 21 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({y}\right)$
23 12 22 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)$
24 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}⇝$
25 23 24 nfel ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝$
26 fveq2 ${⊢}{x}={y}\to {F}\left({m}\right)\left({x}\right)={F}\left({m}\right)\left({y}\right)$
27 26 mpteq2dv ${⊢}{x}={y}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)$
28 27 eleq1d ${⊢}{x}={y}\to \left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right)$
29 18 19 20 25 28 cbvrabw ${⊢}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{y}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right\}$
30 ssrab2 ${⊢}\left\{{y}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right\}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
31 29 30 eqsstri ${⊢}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
32 7 31 eqsstri ${⊢}{D}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
33 32 9 sseldi ${⊢}{\phi }\to {X}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
34 1 5 6 11 33 allbutfifvre ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ$
35 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
36 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({X}\right)\right)$
37 3 7 8 9 fnlimcnv ${⊢}{\phi }\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({X}\right)\right)⇝{G}\left({X}\right)$
38 nfcv ${⊢}\underset{_}{Ⅎ}{l}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)$
39 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{l}$
40 2 39 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)$
41 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{X}$
42 40 41 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({X}\right)$
43 fveq2 ${⊢}{m}={l}\to {F}\left({m}\right)={F}\left({l}\right)$
44 43 fveq1d ${⊢}{m}={l}\to {F}\left({m}\right)\left({X}\right)={F}\left({l}\right)\left({X}\right)$
45 38 42 44 cbvmpt ${⊢}\left({m}\in {Z}⟼{F}\left({m}\right)\left({X}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({X}\right)\right)$
46 fveq2 ${⊢}{l}={j}\to {F}\left({l}\right)={F}\left({j}\right)$
47 46 fveq1d ${⊢}{l}={j}\to {F}\left({l}\right)\left({X}\right)={F}\left({j}\right)\left({X}\right)$
48 simpr ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {j}\in {Z}$
49 fvexd ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\left({X}\right)\in \mathrm{V}$
50 45 47 48 49 fvmptd3 ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({X}\right)\right)\left({j}\right)={F}\left({j}\right)\left({X}\right)$
51 35 36 5 4 37 50 10 climd ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {j}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({j}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
52 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
53 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{j}$
54 2 53 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)$
55 54 41 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\left({X}\right)$
56 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}ℂ$
57 55 56 nfel ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\left({X}\right)\in ℂ$
58 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\mathrm{abs}$
59 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}-$
60 nfmpt1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)$
61 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\mathrm{dom}⇝$
62 60 61 nfel ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
63 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{Z}$
64 nfii1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
65 63 64 nfiun ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
66 62 65 nfrabw ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
67 7 66 nfcxfr ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{D}$
68 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}⇝$
69 68 60 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
70 67 69 nfmpt ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
71 8 70 nfcxfr ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{G}$
72 71 41 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{G}\left({X}\right)$
73 55 59 72 nfov ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right)$
74 58 73 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|$
75 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}<$
76 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{Y}$
77 74 75 76 nfbr ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}$
78 57 77 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({F}\left({j}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
79 fveq2 ${⊢}{m}={j}\to {F}\left({m}\right)={F}\left({j}\right)$
80 79 fveq1d ${⊢}{m}={j}\to {F}\left({m}\right)\left({X}\right)={F}\left({j}\right)\left({X}\right)$
81 80 eleq1d ${⊢}{m}={j}\to \left({F}\left({m}\right)\left({X}\right)\in ℂ↔{F}\left({j}\right)\left({X}\right)\in ℂ\right)$
82 80 fvoveq1d ${⊢}{m}={j}\to \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|=\left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|$
83 82 breq1d ${⊢}{m}={j}\to \left(\left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}↔\left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
84 81 83 anbi12d ${⊢}{m}={j}\to \left(\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)↔\left({F}\left({j}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)\right)$
85 52 78 84 cbvralw ${⊢}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)↔\forall {j}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({j}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
86 85 rexbii ${⊢}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)↔\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {j}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({j}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({j}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
87 51 86 sylibr ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
88 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{n}\in {Z}$
89 1 88 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\right)$
90 simpr ${⊢}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)\to \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}$
91 90 a1i ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left(\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)\to \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
92 89 91 ralimdaa ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
93 92 reximdva ${⊢}{\phi }\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℂ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
94 87 93 mpd ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}$
95 34 94 jca ${⊢}{\phi }\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ\wedge \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
96 5 rexanuz2 ${⊢}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℝ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)↔\left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ\wedge \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$
97 95 96 sylibr ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left({F}\left({m}\right)\left({X}\right)\in ℝ\wedge \left|{F}\left({m}\right)\left({X}\right)-{G}\left({X}\right)\right|<{Y}\right)$