Metamath Proof Explorer

Theorem divlimc

Description: Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses divlimc.f 
|- F = ( x e. A |-> B )
divlimc.g 
|- G = ( x e. A |-> C )
divlimc.h 
|- H = ( x e. A |-> ( B / C ) )
divlimc.b 
|- ( ( ph /\ x e. A ) -> B e. CC )
divlimc.c 
|- ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )
divlimc.x 
|- ( ph -> X e. ( F limCC D ) )
divlimc.y 
|- ( ph -> Y e. ( G limCC D ) )
divlimc.yne0 
|- ( ph -> Y =/= 0 )
divlimc.cne0 
|- ( ( ph /\ x e. A ) -> C =/= 0 )
Assertion divlimc 
|- ( ph -> ( X / Y ) e. ( H limCC D ) )

Proof

Step Hyp Ref Expression
1 divlimc.f 
 |-  F = ( x e. A |-> B )
2 divlimc.g 
 |-  G = ( x e. A |-> C )
3 divlimc.h 
 |-  H = ( x e. A |-> ( B / C ) )
4 divlimc.b 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 divlimc.c 
 |-  ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )
6 divlimc.x 
 |-  ( ph -> X e. ( F limCC D ) )
7 divlimc.y 
 |-  ( ph -> Y e. ( G limCC D ) )
8 divlimc.yne0 
 |-  ( ph -> Y =/= 0 )
9 divlimc.cne0 
 |-  ( ( ph /\ x e. A ) -> C =/= 0 )
10 eqid 
 |-  ( x e. A |-> ( 1 / C ) ) = ( x e. A |-> ( 1 / C ) )
11 eqid 
 |-  ( x e. A |-> ( B x. ( 1 / C ) ) ) = ( x e. A |-> ( B x. ( 1 / C ) ) )
12 5 eldifad 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
13 12 9 reccld 
 |-  ( ( ph /\ x e. A ) -> ( 1 / C ) e. CC )
14 2 10 5 7 8 reclimc 
 |-  ( ph -> ( 1 / Y ) e. ( ( x e. A |-> ( 1 / C ) ) limCC D ) )
15 1 10 11 4 13 6 14 mullimc 
 |-  ( ph -> ( X x. ( 1 / Y ) ) e. ( ( x e. A |-> ( B x. ( 1 / C ) ) ) limCC D ) )
16 limccl 
 |-  ( F limCC D ) C_ CC
17 16 6 sselid 
 |-  ( ph -> X e. CC )
18 limccl 
 |-  ( G limCC D ) C_ CC
19 18 7 sselid 
 |-  ( ph -> Y e. CC )
20 17 19 8 divrecd 
 |-  ( ph -> ( X / Y ) = ( X x. ( 1 / Y ) ) )
21 4 12 9 divrecd 
 |-  ( ( ph /\ x e. A ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
22 21 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( B / C ) ) = ( x e. A |-> ( B x. ( 1 / C ) ) ) )
23 3 22 syl5eq 
 |-  ( ph -> H = ( x e. A |-> ( B x. ( 1 / C ) ) ) )
24 23 oveq1d 
 |-  ( ph -> ( H limCC D ) = ( ( x e. A |-> ( B x. ( 1 / C ) ) ) limCC D ) )
25 15 20 24 3eltr4d 
 |-  ( ph -> ( X / Y ) e. ( H limCC D ) )