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 = M
climadd.2 φ M
climadd.4 φ F A
climadd.6 φ H X
climadd.7 φ G B
climadd.8 φ k Z F k
climadd.9 φ k Z G k
climmul.h φ k Z H k = F k G k
Assertion climmul φ H A B

Proof

Step Hyp Ref Expression
1 climadd.1 Z = M
2 climadd.2 φ M
3 climadd.4 φ F A
4 climadd.6 φ H X
5 climadd.7 φ G B
6 climadd.8 φ k Z F k
7 climadd.9 φ k Z G k
8 climmul.h φ k Z H k = F k G k
9 climcl F A A
10 3 9 syl φ A
11 climcl G B B
12 5 11 syl φ B
13 mulcl u v u v
14 13 adantl φ u v u v
15 simpr φ x + x +
16 10 adantr φ x + A
17 12 adantr φ x + B
18 mulcn2 x + A B y + z + u v u A < y v B < z u v A B < x
19 15 16 17 18 syl3anc φ x + y + z + u v u A < y v B < z u v A B < x
20 1 2 10 12 14 3 5 4 19 6 7 8 climcn2 φ H A B