Metamath Proof Explorer

Theorem climrec

Description: Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climrec.1 
|- Z = ( ZZ>= ` M )
climrec.2 
|- ( ph -> M e. ZZ )
climrec.3 
|- ( ph -> G ~~> A )
climrec.4 
|- ( ph -> A =/= 0 )
climrec.5 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )
climrec.6 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) )
climrec.7 
|- ( ph -> H e. W )
Assertion climrec 
|- ( ph -> H ~~> ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 climrec.1 
 |-  Z = ( ZZ>= ` M )
2 climrec.2 
 |-  ( ph -> M e. ZZ )
3 climrec.3 
 |-  ( ph -> G ~~> A )
4 climrec.4 
 |-  ( ph -> A =/= 0 )
5 climrec.5 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )
6 climrec.6 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) )
7 climrec.7 
 |-  ( ph -> H e. W )
8 climcl 
 |-  ( G ~~> A -> A e. CC )
9 3 8 syl 
 |-  ( ph -> A e. CC )
10 4 neneqd 
 |-  ( ph -> -. A = 0 )
11 c0ex 
 |-  0 e. _V
12 11 elsn2 
 |-  ( A e. { 0 } <-> A = 0 )
13 10 12 sylnibr 
 |-  ( ph -> -. A e. { 0 } )
14 9 13 eldifd 
 |-  ( ph -> A e. ( CC \ { 0 } ) )
15 eqidd 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) = ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) )
16 simpr 
 |-  ( ( ( ph /\ z e. ( CC \ { 0 } ) ) /\ w = z ) -> w = z )
17 16 oveq2d 
 |-  ( ( ( ph /\ z e. ( CC \ { 0 } ) ) /\ w = z ) -> ( 1 / w ) = ( 1 / z ) )
18 simpr 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> z e. ( CC \ { 0 } ) )
19 18 eldifad 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> z e. CC )
20 eldifsni 
 |-  ( z e. ( CC \ { 0 } ) -> z =/= 0 )
21 20 adantl 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> z =/= 0 )
22 19 21 reccld 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> ( 1 / z ) e. CC )
23 15 17 18 22 fvmptd 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) = ( 1 / z ) )
24 23 22 eqeltrd 
 |-  ( ( ph /\ z e. ( CC \ { 0 } ) ) -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) e. CC )
25 eqid 
 |-  ( if ( 1 <_ ( ( abs ` A ) x. x ) , 1 , ( ( abs ` A ) x. x ) ) x. ( ( abs ` A ) / 2 ) ) = ( if ( 1 <_ ( ( abs ` A ) x. x ) , 1 , ( ( abs ` A ) x. x ) ) x. ( ( abs ` A ) / 2 ) )
26 25 reccn2 
 |-  ( ( A e. ( CC \ { 0 } ) /\ x e. RR+ ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) )
27 14 26 sylan 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) )
28 eqidd 
 |-  ( z e. ( CC \ { 0 } ) -> ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) = ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) )
29 simpr 
 |-  ( ( z e. ( CC \ { 0 } ) /\ w = z ) -> w = z )
30 29 oveq2d 
 |-  ( ( z e. ( CC \ { 0 } ) /\ w = z ) -> ( 1 / w ) = ( 1 / z ) )
31 id 
 |-  ( z e. ( CC \ { 0 } ) -> z e. ( CC \ { 0 } ) )
32 eldifi 
 |-  ( z e. ( CC \ { 0 } ) -> z e. CC )
33 32 20 reccld 
 |-  ( z e. ( CC \ { 0 } ) -> ( 1 / z ) e. CC )
34 28 30 31 33 fvmptd 
 |-  ( z e. ( CC \ { 0 } ) -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) = ( 1 / z ) )
35 34 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) = ( 1 / z ) )
36 eqidd 
 |-  ( ph -> ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) = ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) )
37 simpr 
 |-  ( ( ph /\ w = A ) -> w = A )
38 37 oveq2d 
 |-  ( ( ph /\ w = A ) -> ( 1 / w ) = ( 1 / A ) )
39 9 4 reccld 
 |-  ( ph -> ( 1 / A ) e. CC )
40 36 38 14 39 fvmptd 
 |-  ( ph -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) = ( 1 / A ) )
41 40 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) = ( 1 / A ) )
42 35 41 oveq12d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) = ( ( 1 / z ) - ( 1 / A ) ) )
43 42 fveq2d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) ) = ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) )
44 31 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> z e. ( CC \ { 0 } ) )
45 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( z - A ) ) < y )
46 simpllr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) )
47 44 45 46 mp2d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x )
48 43 47 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) ) /\ z e. ( CC \ { 0 } ) ) /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) ) < x )
49 48 exp41 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) ) -> ( z e. ( CC \ { 0 } ) -> ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) ) < x ) ) ) )
50 49 ralimdv2 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) -> A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) ) < x ) ) )
51 50 reximdv 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < x ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) ) < x ) ) )
52 27 51 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` z ) - ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) ) ) < x ) )
53 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) = ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) )
54 oveq2 
 |-  ( w = ( G ` k ) -> ( 1 / w ) = ( 1 / ( G ` k ) ) )
55 54 adantl 
 |-  ( ( ( ph /\ k e. Z ) /\ w = ( G ` k ) ) -> ( 1 / w ) = ( 1 / ( G ` k ) ) )
56 5 eldifad 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
57 eldifsni 
 |-  ( ( G ` k ) e. ( CC \ { 0 } ) -> ( G ` k ) =/= 0 )
58 5 57 syl 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) =/= 0 )
59 56 58 reccld 
 |-  ( ( ph /\ k e. Z ) -> ( 1 / ( G ` k ) ) e. CC )
60 53 55 5 59 fvmptd 
 |-  ( ( ph /\ k e. Z ) -> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` ( G ` k ) ) = ( 1 / ( G ` k ) ) )
61 6 60 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` ( G ` k ) ) )
62 1 2 14 24 3 7 52 5 61 climcn1 
 |-  ( ph -> H ~~> ( ( w e. ( CC \ { 0 } ) |-> ( 1 / w ) ) ` A ) )
63 62 40 breqtrd 
 |-  ( ph -> H ~~> ( 1 / A ) )