# Metamath Proof Explorer

## Theorem climcn2

Description: Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climcn2.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
climcn2.2 ${⊢}{\phi }\to {M}\in ℤ$
climcn2.3a ${⊢}{\phi }\to {A}\in {C}$
climcn2.3b ${⊢}{\phi }\to {B}\in {D}$
climcn2.4 ${⊢}\left({\phi }\wedge \left({u}\in {C}\wedge {v}\in {D}\right)\right)\to {u}{F}{v}\in ℂ$
climcn2.5a ${⊢}{\phi }\to {G}⇝{A}$
climcn2.5b ${⊢}{\phi }\to {H}⇝{B}$
climcn2.6 ${⊢}{\phi }\to {K}\in {W}$
climcn2.7 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
climcn2.8a ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in {C}$
climcn2.8b ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)\in {D}$
climcn2.9 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {K}\left({k}\right)={G}\left({k}\right){F}{H}\left({k}\right)$
Assertion climcn2 ${⊢}{\phi }\to {K}⇝\left({A}{F}{B}\right)$

### Proof

Step Hyp Ref Expression
1 climcn2.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 climcn2.2 ${⊢}{\phi }\to {M}\in ℤ$
3 climcn2.3a ${⊢}{\phi }\to {A}\in {C}$
4 climcn2.3b ${⊢}{\phi }\to {B}\in {D}$
5 climcn2.4 ${⊢}\left({\phi }\wedge \left({u}\in {C}\wedge {v}\in {D}\right)\right)\to {u}{F}{v}\in ℂ$
6 climcn2.5a ${⊢}{\phi }\to {G}⇝{A}$
7 climcn2.5b ${⊢}{\phi }\to {H}⇝{B}$
8 climcn2.6 ${⊢}{\phi }\to {K}\in {W}$
9 climcn2.7 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
10 climcn2.8a ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in {C}$
11 climcn2.8b ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)\in {D}$
12 climcn2.9 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {K}\left({k}\right)={G}\left({k}\right){F}{H}\left({k}\right)$
13 2 adantr ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to {M}\in ℤ$
14 simprl ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to {y}\in {ℝ}^{+}$
15 eqidd ${⊢}\left(\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\wedge {k}\in {Z}\right)\to {G}\left({k}\right)={G}\left({k}\right)$
16 6 adantr ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to {G}⇝{A}$
17 1 13 14 15 16 climi2 ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{G}\left({k}\right)-{A}\right|<{y}$
18 simprr ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to {z}\in {ℝ}^{+}$
19 eqidd ${⊢}\left(\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={H}\left({k}\right)$
20 7 adantr ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to {H}⇝{B}$
21 1 13 18 19 20 climi2 ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{H}\left({k}\right)-{B}\right|<{z}$
22 1 rexanuz2 ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)↔\left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{H}\left({k}\right)-{B}\right|<{z}\right)$
23 17 21 22 sylanbrc ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)$
24 1 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
25 fvoveq1 ${⊢}{u}={G}\left({k}\right)\to \left|{u}-{A}\right|=\left|{G}\left({k}\right)-{A}\right|$
26 25 breq1d ${⊢}{u}={G}\left({k}\right)\to \left(\left|{u}-{A}\right|<{y}↔\left|{G}\left({k}\right)-{A}\right|<{y}\right)$
27 26 anbi1d ${⊢}{u}={G}\left({k}\right)\to \left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)↔\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\right)$
28 oveq1 ${⊢}{u}={G}\left({k}\right)\to {u}{F}{v}={G}\left({k}\right){F}{v}$
29 28 fvoveq1d ${⊢}{u}={G}\left({k}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|=\left|\left({G}\left({k}\right){F}{v}\right)-\left({A}{F}{B}\right)\right|$
30 29 breq1d ${⊢}{u}={G}\left({k}\right)\to \left(\left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}↔\left|\left({G}\left({k}\right){F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
31 27 30 imbi12d ${⊢}{u}={G}\left({k}\right)\to \left(\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)↔\left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)$
32 fvoveq1 ${⊢}{v}={H}\left({k}\right)\to \left|{v}-{B}\right|=\left|{H}\left({k}\right)-{B}\right|$
33 32 breq1d ${⊢}{v}={H}\left({k}\right)\to \left(\left|{v}-{B}\right|<{z}↔\left|{H}\left({k}\right)-{B}\right|<{z}\right)$
34 33 anbi2d ${⊢}{v}={H}\left({k}\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)↔\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\right)$
35 oveq2 ${⊢}{v}={H}\left({k}\right)\to {G}\left({k}\right){F}{v}={G}\left({k}\right){F}{H}\left({k}\right)$
36 35 fvoveq1d ${⊢}{v}={H}\left({k}\right)\to \left|\left({G}\left({k}\right){F}{v}\right)-\left({A}{F}{B}\right)\right|=\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|$
37 36 breq1d ${⊢}{v}={H}\left({k}\right)\to \left(\left|\left({G}\left({k}\right){F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}↔\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
38 34 37 imbi12d ${⊢}{v}={H}\left({k}\right)\to \left(\left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)↔\left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)$
39 31 38 rspc2v ${⊢}\left({G}\left({k}\right)\in {C}\wedge {H}\left({k}\right)\in {D}\right)\to \left(\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)$
40 10 11 39 syl2anc ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)$
41 40 imp ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
42 41 an32s ${⊢}\left(\left({\phi }\wedge \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)\wedge {k}\in {Z}\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
43 24 42 sylan2 ${⊢}\left(\left({\phi }\wedge \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)\wedge \left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
44 43 anassrs ${⊢}\left(\left(\left({\phi }\wedge \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
45 44 ralimdva ${⊢}\left(\left({\phi }\wedge \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
46 45 reximdva ${⊢}\left({\phi }\wedge \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
47 46 ex ${⊢}{\phi }\to \left(\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)$
48 47 adantr ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to \left(\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left(\left|{G}\left({k}\right)-{A}\right|<{y}\wedge \left|{H}\left({k}\right)-{B}\right|<{z}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)\right)$
49 23 48 mpid ${⊢}\left({\phi }\wedge \left({y}\in {ℝ}^{+}\wedge {z}\in {ℝ}^{+}\right)\right)\to \left(\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
50 49 rexlimdvva ${⊢}{\phi }\to \left(\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
51 50 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|\left({u}{F}{v}\right)-\left({A}{F}{B}\right)\right|<{x}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
52 9 51 mpd ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}$
53 52 ralrimiva ${⊢}{\phi }\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}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}$
54 5 3 4 caovcld ${⊢}{\phi }\to {A}{F}{B}\in ℂ$
55 10 11 jca ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({G}\left({k}\right)\in {C}\wedge {H}\left({k}\right)\in {D}\right)$
56 5 ralrimivva ${⊢}{\phi }\to \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}{u}{F}{v}\in ℂ$
57 56 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}{u}{F}{v}\in ℂ$
58 28 eleq1d ${⊢}{u}={G}\left({k}\right)\to \left({u}{F}{v}\in ℂ↔{G}\left({k}\right){F}{v}\in ℂ\right)$
59 35 eleq1d ${⊢}{v}={H}\left({k}\right)\to \left({G}\left({k}\right){F}{v}\in ℂ↔{G}\left({k}\right){F}{H}\left({k}\right)\in ℂ\right)$
60 58 59 rspc2v ${⊢}\left({G}\left({k}\right)\in {C}\wedge {H}\left({k}\right)\in {D}\right)\to \left(\forall {u}\in {C}\phantom{\rule{.4em}{0ex}}\forall {v}\in {D}\phantom{\rule{.4em}{0ex}}{u}{F}{v}\in ℂ\to {G}\left({k}\right){F}{H}\left({k}\right)\in ℂ\right)$
61 55 57 60 sylc ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right){F}{H}\left({k}\right)\in ℂ$
62 1 2 8 12 54 61 clim2c ${⊢}{\phi }\to \left({K}⇝\left({A}{F}{B}\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({G}\left({k}\right){F}{H}\left({k}\right)\right)-\left({A}{F}{B}\right)\right|<{x}\right)$
63 53 62 mpbird ${⊢}{\phi }\to {K}⇝\left({A}{F}{B}\right)$