Metamath Proof Explorer

Theorem rlimmul

Description: Limit of the product of two converging functions. Proposition 12-2.1(c) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses rlimadd.3 
|- ( ( ph /\ x e. A ) -> B e. V )
rlimadd.4 
|- ( ( ph /\ x e. A ) -> C e. V )
rlimadd.5 
|- ( ph -> ( x e. A |-> B ) ~~>r D )
rlimadd.6 
|- ( ph -> ( x e. A |-> C ) ~~>r E )
Assertion rlimmul 
|- ( ph -> ( x e. A |-> ( B x. C ) ) ~~>r ( D x. E ) )

Proof

Step Hyp Ref Expression
1 rlimadd.3 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 rlimadd.4 
 |-  ( ( ph /\ x e. A ) -> C e. V )
3 rlimadd.5 
 |-  ( ph -> ( x e. A |-> B ) ~~>r D )
4 rlimadd.6 
 |-  ( ph -> ( x e. A |-> C ) ~~>r E )
5 1 3 rlimmptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 2 4 rlimmptrcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
7 5 6 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) e. CC )
8 rlimcl 
 |-  ( ( x e. A |-> B ) ~~>r D -> D e. CC )
9 3 8 syl 
 |-  ( ph -> D e. CC )
10 rlimcl 
 |-  ( ( x e. A |-> C ) ~~>r E -> E e. CC )
11 4 10 syl 
 |-  ( ph -> E e. CC )
12 9 11 mulcld 
 |-  ( ph -> ( D x. E ) e. CC )
13 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
14 9 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> D e. CC )
15 11 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> E e. CC )
16 mulcn2 
 |-  ( ( y e. RR+ /\ D e. CC /\ E e. CC ) -> E. z e. RR+ E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - D ) ) < z /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( u x. v ) - ( D x. E ) ) ) < y ) )
17 13 14 15 16 syl3anc 
 |-  ( ( ph /\ y e. RR+ ) -> E. z e. RR+ E. w e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - D ) ) < z /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( u x. v ) - ( D x. E ) ) ) < y ) )
18 5 6 7 12 3 4 17 rlimcn3 
 |-  ( ph -> ( x e. A |-> ( B x. C ) ) ~~>r ( D x. E ) )