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 )