This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimdiv

Description: Limit of the quotient of two converging functions. Proposition 12-2.1(a) 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 )
rlimdiv.7 
|- ( ph -> E =/= 0 )
rlimdiv.8 
|- ( ( ph /\ x e. A ) -> C =/= 0 )
Assertion rlimdiv 
|- ( ph -> ( x e. A |-> ( B / C ) ) ~~>r ( D / 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 rlimdiv.7 
 |-  ( ph -> E =/= 0 )
6 rlimdiv.8 
 |-  ( ( ph /\ x e. A ) -> C =/= 0 )
7 1 3 rlimmptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
8 2 4 rlimmptrcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
9 8 6 reccld 
 |-  ( ( ph /\ x e. A ) -> ( 1 / C ) e. CC )
10 eldifsn 
 |-  ( C e. ( CC \ { 0 } ) <-> ( C e. CC /\ C =/= 0 ) )
11 8 6 10 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )
12 11 fmpttd 
 |-  ( ph -> ( x e. A |-> C ) : A --> ( CC \ { 0 } ) )
13 rlimcl 
 |-  ( ( x e. A |-> C ) ~~>r E -> E e. CC )
14 4 13 syl 
 |-  ( ph -> E e. CC )
15 eldifsn 
 |-  ( E e. ( CC \ { 0 } ) <-> ( E e. CC /\ E =/= 0 ) )
16 14 5 15 sylanbrc 
 |-  ( ph -> E e. ( CC \ { 0 } ) )
17 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
18 reccl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( 1 / y ) e. CC )
19 17 18 sylbi 
 |-  ( y e. ( CC \ { 0 } ) -> ( 1 / y ) e. CC )
20 19 adantl 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> ( 1 / y ) e. CC )
21 20 fmpttd 
 |-  ( ph -> ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) : ( CC \ { 0 } ) --> CC )
22 eqid 
 |-  ( if ( 1 <_ ( ( abs ` E ) x. z ) , 1 , ( ( abs ` E ) x. z ) ) x. ( ( abs ` E ) / 2 ) ) = ( if ( 1 <_ ( ( abs ` E ) x. z ) , 1 , ( ( abs ` E ) x. z ) ) x. ( ( abs ` E ) / 2 ) )
23 22 reccn2 
 |-  ( ( E e. ( CC \ { 0 } ) /\ z e. RR+ ) -> E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) )
24 16 23 sylan 
 |-  ( ( ph /\ z e. RR+ ) -> E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) )
25 oveq2 
 |-  ( y = v -> ( 1 / y ) = ( 1 / v ) )
26 eqid 
 |-  ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) = ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) )
27 ovex 
 |-  ( 1 / v ) e. _V
28 25 26 27 fvmpt 
 |-  ( v e. ( CC \ { 0 } ) -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) = ( 1 / v ) )
29 oveq2 
 |-  ( y = E -> ( 1 / y ) = ( 1 / E ) )
30 ovex 
 |-  ( 1 / E ) e. _V
31 29 26 30 fvmpt 
 |-  ( E e. ( CC \ { 0 } ) -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) = ( 1 / E ) )
32 16 31 syl 
 |-  ( ph -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) = ( 1 / E ) )
33 28 32 oveqan12rd 
 |-  ( ( ph /\ v e. ( CC \ { 0 } ) ) -> ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) = ( ( 1 / v ) - ( 1 / E ) ) )
34 33 fveq2d 
 |-  ( ( ph /\ v e. ( CC \ { 0 } ) ) -> ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) = ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) )
35 34 breq1d 
 |-  ( ( ph /\ v e. ( CC \ { 0 } ) ) -> ( ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) < z <-> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) )
36 35 imbi2d 
 |-  ( ( ph /\ v e. ( CC \ { 0 } ) ) -> ( ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) < z ) <-> ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) ) )
37 36 ralbidva 
 |-  ( ph -> ( A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) < z ) <-> A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) ) )
38 37 rexbidv 
 |-  ( ph -> ( E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) < z ) <-> E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) ) )
39 38 biimpar 
 |-  ( ( ph /\ E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( 1 / v ) - ( 1 / E ) ) ) < z ) ) -> E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) < z ) )
40 24 39 syldan 
 |-  ( ( ph /\ z e. RR+ ) -> E. w e. RR+ A. v e. ( CC \ { 0 } ) ( ( abs ` ( v - E ) ) < w -> ( abs ` ( ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` v ) - ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) ) ) < z ) )
41 12 16 4 21 40 rlimcn1 
 |-  ( ph -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) o. ( x e. A |-> C ) ) ~~>r ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ` E ) )
42 eqidd 
 |-  ( ph -> ( x e. A |-> C ) = ( x e. A |-> C ) )
43 eqidd 
 |-  ( ph -> ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) = ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) )
44 oveq2 
 |-  ( y = C -> ( 1 / y ) = ( 1 / C ) )
45 11 42 43 44 fmptco 
 |-  ( ph -> ( ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) o. ( x e. A |-> C ) ) = ( x e. A |-> ( 1 / C ) ) )
46 41 45 32 3brtr3d 
 |-  ( ph -> ( x e. A |-> ( 1 / C ) ) ~~>r ( 1 / E ) )
47 7 9 3 46 rlimmul 
 |-  ( ph -> ( x e. A |-> ( B x. ( 1 / C ) ) ) ~~>r ( D x. ( 1 / E ) ) )
48 7 8 6 divrecd 
 |-  ( ( ph /\ x e. A ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
49 48 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( B / C ) ) = ( x e. A |-> ( B x. ( 1 / C ) ) ) )
50 rlimcl 
 |-  ( ( x e. A |-> B ) ~~>r D -> D e. CC )
51 3 50 syl 
 |-  ( ph -> D e. CC )
52 51 14 5 divrecd 
 |-  ( ph -> ( D / E ) = ( D x. ( 1 / E ) ) )
53 47 49 52 3brtr4d 
 |-  ( ph -> ( x e. A |-> ( B / C ) ) ~~>r ( D / E ) )