# Metamath Proof Explorer

## Theorem climmul

Description: Limit of the product of two converging sequences. Proposition 12-2.1(c) of Gleason p. 168. (Contributed by NM, 27-Dec-2005) (Proof shortened by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses climadd.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
climadd.2 ${⊢}{\phi }\to {M}\in ℤ$
climadd.4 ${⊢}{\phi }\to {F}⇝{A}$
climadd.6 ${⊢}{\phi }\to {H}\in {X}$
climadd.7 ${⊢}{\phi }\to {G}⇝{B}$
climadd.8 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
climadd.9 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
climmul.h ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
Assertion climmul ${⊢}{\phi }\to {H}⇝{A}{B}$

### Proof

Step Hyp Ref Expression
1 climadd.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 climadd.2 ${⊢}{\phi }\to {M}\in ℤ$
3 climadd.4 ${⊢}{\phi }\to {F}⇝{A}$
4 climadd.6 ${⊢}{\phi }\to {H}\in {X}$
5 climadd.7 ${⊢}{\phi }\to {G}⇝{B}$
6 climadd.8 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
7 climadd.9 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)\in ℂ$
8 climmul.h ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({k}\right){G}\left({k}\right)$
9 climcl ${⊢}{F}⇝{A}\to {A}\in ℂ$
10 3 9 syl ${⊢}{\phi }\to {A}\in ℂ$
11 climcl ${⊢}{G}⇝{B}\to {B}\in ℂ$
12 5 11 syl ${⊢}{\phi }\to {B}\in ℂ$
13 mulcl ${⊢}\left({u}\in ℂ\wedge {v}\in ℂ\right)\to {u}{v}\in ℂ$
14 13 adantl ${⊢}\left({\phi }\wedge \left({u}\in ℂ\wedge {v}\in ℂ\right)\right)\to {u}{v}\in ℂ$
15 simpr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
16 10 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {A}\in ℂ$
17 12 adantr ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to {B}\in ℂ$
18 mulcn2 ${⊢}\left({x}\in {ℝ}^{+}\wedge {A}\in ℂ\wedge {B}\in ℂ\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|{u}{v}-{A}{B}\right|<{x}\right)$
19 15 16 17 18 syl3anc ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left(\left|{u}-{A}\right|<{y}\wedge \left|{v}-{B}\right|<{z}\right)\to \left|{u}{v}-{A}{B}\right|<{x}\right)$
20 1 2 10 12 14 3 5 4 19 6 7 8 climcn2 ${⊢}{\phi }\to {H}⇝{A}{B}$