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 = ( ZZ>= ` M )
climadd.2 
|- ( ph -> M e. ZZ )
climadd.4 
|- ( ph -> F ~~> A )
climadd.6 
|- ( ph -> H e. X )
climadd.7 
|- ( ph -> G ~~> B )
climadd.8 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climadd.9 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
climmul.h 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
Assertion climmul 
|- ( ph -> H ~~> ( A x. B ) )

Proof

Step Hyp Ref Expression
1 climadd.1 
 |-  Z = ( ZZ>= ` M )
2 climadd.2 
 |-  ( ph -> M e. ZZ )
3 climadd.4 
 |-  ( ph -> F ~~> A )
4 climadd.6 
 |-  ( ph -> H e. X )
5 climadd.7 
 |-  ( ph -> G ~~> B )
6 climadd.8 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 climadd.9 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
8 climmul.h 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
9 climcl 
 |-  ( F ~~> A -> A e. CC )
10 3 9 syl 
 |-  ( ph -> A e. CC )
11 climcl 
 |-  ( G ~~> B -> B e. CC )
12 5 11 syl 
 |-  ( ph -> B e. CC )
13 mulcl 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u x. v ) e. CC )
14 13 adantl 
 |-  ( ( ph /\ ( u e. CC /\ v e. CC ) ) -> ( u x. v ) e. CC )
15 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
16 10 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> A e. CC )
17 12 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> B e. CC )
18 mulcn2 
 |-  ( ( x e. RR+ /\ A e. CC /\ B e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u x. v ) - ( A x. B ) ) ) < x ) )
19 15 16 17 18 syl3anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u x. v ) - ( A x. B ) ) ) < x ) )
20 1 2 10 12 14 3 5 4 19 6 7 8 climcn2 
 |-  ( ph -> H ~~> ( A x. B ) )