Metamath Proof Explorer

Theorem reclimc

Description: Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses reclimc.f 
|- F = ( x e. A |-> B )
reclimc.g 
|- G = ( x e. A |-> ( 1 / B ) )
reclimc.b 
|- ( ( ph /\ x e. A ) -> B e. ( CC \ { 0 } ) )
reclimc.c 
|- ( ph -> C e. ( F limCC D ) )
reclimc.cne0 
|- ( ph -> C =/= 0 )
Assertion reclimc 
|- ( ph -> ( 1 / C ) e. ( G limCC D ) )

Proof

Step Hyp Ref Expression
1 reclimc.f 
 |-  F = ( x e. A |-> B )
2 reclimc.g 
 |-  G = ( x e. A |-> ( 1 / B ) )
3 reclimc.b 
 |-  ( ( ph /\ x e. A ) -> B e. ( CC \ { 0 } ) )
4 reclimc.c 
 |-  ( ph -> C e. ( F limCC D ) )
5 reclimc.cne0 
 |-  ( ph -> C =/= 0 )
6 eqid 
 |-  ( x e. A |-> ( C - B ) ) = ( x e. A |-> ( C - B ) )
7 eqid 
 |-  ( x e. A |-> ( B x. C ) ) = ( x e. A |-> ( B x. C ) )
8 eqid 
 |-  ( x e. A |-> ( ( C - B ) / ( B x. C ) ) ) = ( x e. A |-> ( ( C - B ) / ( B x. C ) ) )
9 limccl 
 |-  ( F limCC D ) C_ CC
10 9 4 sselid 
 |-  ( ph -> C e. CC )
11 10 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
12 3 eldifad 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
13 11 12 subcld 
 |-  ( ( ph /\ x e. A ) -> ( C - B ) e. CC )
14 12 11 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) e. CC )
15 eldifsni 
 |-  ( B e. ( CC \ { 0 } ) -> B =/= 0 )
16 3 15 syl 
 |-  ( ( ph /\ x e. A ) -> B =/= 0 )
17 5 adantr 
 |-  ( ( ph /\ x e. A ) -> C =/= 0 )
18 12 11 16 17 mulne0d 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) =/= 0 )
19 18 neneqd 
 |-  ( ( ph /\ x e. A ) -> -. ( B x. C ) = 0 )
20 elsng 
 |-  ( ( B x. C ) e. CC -> ( ( B x. C ) e. { 0 } <-> ( B x. C ) = 0 ) )
21 14 20 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( B x. C ) e. { 0 } <-> ( B x. C ) = 0 ) )
22 19 21 mtbird 
 |-  ( ( ph /\ x e. A ) -> -. ( B x. C ) e. { 0 } )
23 14 22 eldifd 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) e. ( CC \ { 0 } ) )
24 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
25 eqid 
 |-  ( x e. A |-> -u B ) = ( x e. A |-> -u B )
26 eqid 
 |-  ( x e. A |-> ( C + -u B ) ) = ( x e. A |-> ( C + -u B ) )
27 12 negcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
28 1 12 4 limcmptdm 
 |-  ( ph -> A C_ CC )
29 limcrcl 
 |-  ( C e. ( F limCC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
30 4 29 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
31 30 simp3d 
 |-  ( ph -> D e. CC )
32 24 28 10 31 constlimc 
 |-  ( ph -> C e. ( ( x e. A |-> C ) limCC D ) )
33 1 25 12 4 neglimc 
 |-  ( ph -> -u C e. ( ( x e. A |-> -u B ) limCC D ) )
34 24 25 26 11 27 32 33 addlimc 
 |-  ( ph -> ( C + -u C ) e. ( ( x e. A |-> ( C + -u B ) ) limCC D ) )
35 10 negidd 
 |-  ( ph -> ( C + -u C ) = 0 )
36 11 12 negsubd 
 |-  ( ( ph /\ x e. A ) -> ( C + -u B ) = ( C - B ) )
37 36 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( C + -u B ) ) = ( x e. A |-> ( C - B ) ) )
38 37 oveq1d 
 |-  ( ph -> ( ( x e. A |-> ( C + -u B ) ) limCC D ) = ( ( x e. A |-> ( C - B ) ) limCC D ) )
39 34 35 38 3eltr3d 
 |-  ( ph -> 0 e. ( ( x e. A |-> ( C - B ) ) limCC D ) )
40 1 24 7 12 11 4 32 mullimc 
 |-  ( ph -> ( C x. C ) e. ( ( x e. A |-> ( B x. C ) ) limCC D ) )
41 10 10 5 5 mulne0d 
 |-  ( ph -> ( C x. C ) =/= 0 )
42 6 7 8 13 23 39 40 41 0ellimcdiv 
 |-  ( ph -> 0 e. ( ( x e. A |-> ( ( C - B ) / ( B x. C ) ) ) limCC D ) )
43 1cnd 
 |-  ( ( ph /\ x e. A ) -> 1 e. CC )
44 43 12 43 11 16 17 divsubdivd 
 |-  ( ( ph /\ x e. A ) -> ( ( 1 / B ) - ( 1 / C ) ) = ( ( ( 1 x. C ) - ( 1 x. B ) ) / ( B x. C ) ) )
45 11 mulid2d 
 |-  ( ( ph /\ x e. A ) -> ( 1 x. C ) = C )
46 12 mulid2d 
 |-  ( ( ph /\ x e. A ) -> ( 1 x. B ) = B )
47 45 46 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( 1 x. C ) - ( 1 x. B ) ) = ( C - B ) )
48 47 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( 1 x. C ) - ( 1 x. B ) ) / ( B x. C ) ) = ( ( C - B ) / ( B x. C ) ) )
49 44 48 eqtr2d 
 |-  ( ( ph /\ x e. A ) -> ( ( C - B ) / ( B x. C ) ) = ( ( 1 / B ) - ( 1 / C ) ) )
50 49 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( C - B ) / ( B x. C ) ) ) = ( x e. A |-> ( ( 1 / B ) - ( 1 / C ) ) ) )
51 50 oveq1d 
 |-  ( ph -> ( ( x e. A |-> ( ( C - B ) / ( B x. C ) ) ) limCC D ) = ( ( x e. A |-> ( ( 1 / B ) - ( 1 / C ) ) ) limCC D ) )
52 42 51 eleqtrd 
 |-  ( ph -> 0 e. ( ( x e. A |-> ( ( 1 / B ) - ( 1 / C ) ) ) limCC D ) )
53 eqid 
 |-  ( x e. A |-> ( ( 1 / B ) - ( 1 / C ) ) ) = ( x e. A |-> ( ( 1 / B ) - ( 1 / C ) ) )
54 12 16 reccld 
 |-  ( ( ph /\ x e. A ) -> ( 1 / B ) e. CC )
55 10 5 reccld 
 |-  ( ph -> ( 1 / C ) e. CC )
56 2 53 28 54 31 55 ellimcabssub0 
 |-  ( ph -> ( ( 1 / C ) e. ( G limCC D ) <-> 0 e. ( ( x e. A |-> ( ( 1 / B ) - ( 1 / C ) ) ) limCC D ) ) )
57 52 56 mpbird 
 |-  ( ph -> ( 1 / C ) e. ( G limCC D ) )