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

Metamath Proof Explorer

Theorem divcnv

Description: The sequence of reciprocals of positive integers, multiplied by the factor A , converges to zero. (Contributed by NM, 6-Feb-2008) (Revised by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion divcnv 
|- ( A e. CC -> ( n e. NN |-> ( A / n ) ) ~~> 0 )

Proof

Step Hyp Ref Expression
1 nnrp 
 |-  ( n e. NN -> n e. RR+ )
2 1 ssriv 
 |-  NN C_ RR+
3 2 a1i 
 |-  ( A e. CC -> NN C_ RR+ )
4 divrcnv 
 |-  ( A e. CC -> ( n e. RR+ |-> ( A / n ) ) ~~>r 0 )
5 3 4 rlimres2 
 |-  ( A e. CC -> ( n e. NN |-> ( A / n ) ) ~~>r 0 )
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 1zzd 
 |-  ( A e. CC -> 1 e. ZZ )
8 simpl 
 |-  ( ( A e. CC /\ n e. NN ) -> A e. CC )
9 nncn 
 |-  ( n e. NN -> n e. CC )
10 9 adantl 
 |-  ( ( A e. CC /\ n e. NN ) -> n e. CC )
11 nnne0 
 |-  ( n e. NN -> n =/= 0 )
12 11 adantl 
 |-  ( ( A e. CC /\ n e. NN ) -> n =/= 0 )
13 8 10 12 divcld 
 |-  ( ( A e. CC /\ n e. NN ) -> ( A / n ) e. CC )
14 13 fmpttd 
 |-  ( A e. CC -> ( n e. NN |-> ( A / n ) ) : NN --> CC )
15 6 7 14 rlimclim 
 |-  ( A e. CC -> ( ( n e. NN |-> ( A / n ) ) ~~>r 0 <-> ( n e. NN |-> ( A / n ) ) ~~> 0 ) )
16 5 15 mpbid 
 |-  ( A e. CC -> ( n e. NN |-> ( A / n ) ) ~~> 0 )