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\in ℂ\to \left(n\in \mathbb{N}⟼\frac{A}{n}\right)⇝0$$

Proof

Step	Hyp	Ref	Expression
1		nnrp	$$⊢n\in \mathbb{N}\to n\in {ℝ}^{+}$$
2	1	ssriv	$$⊢\mathbb{N}\subseteq {ℝ}^{+}$$
3	2	a1i	$$⊢A\in ℂ\to \mathbb{N}\subseteq {ℝ}^{+}$$
4		divrcnv	$$⊢A\in ℂ\to \left(n\in {ℝ}^{+}⟼\frac{A}{n}\right)\underset{ℝ}{⇝}0$$
5	3 4	rlimres2	$$⊢A\in ℂ\to \left(n\in \mathbb{N}⟼\frac{A}{n}\right)\underset{ℝ}{⇝}0$$
6		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
7		1zzd	$$⊢A\in ℂ\to 1\in \mathbb{Z}$$
8		simpl	$$⊢\left(A\in ℂ\wedge n\in \mathbb{N}\right)\to A\in ℂ$$
9		nncn	$$⊢n\in \mathbb{N}\to n\in ℂ$$
10	9	adantl	$$⊢\left(A\in ℂ\wedge n\in \mathbb{N}\right)\to n\in ℂ$$
11		nnne0	$$⊢n\in \mathbb{N}\to n\ne 0$$
12	11	adantl	$$⊢\left(A\in ℂ\wedge n\in \mathbb{N}\right)\to n\ne 0$$
13	8 10 12	divcld	$$⊢\left(A\in ℂ\wedge n\in \mathbb{N}\right)\to \frac{A}{n}\in ℂ$$
14	13	fmpttd	$$⊢A\in ℂ\to \left(n\in \mathbb{N}⟼\frac{A}{n}\right):\mathbb{N}⟶ℂ$$
15	6 7 14	rlimclim	$$⊢A\in ℂ\to \left(\left(n\in \mathbb{N}⟼\frac{A}{n}\right)\underset{ℝ}{⇝}0\leftrightarrow \left(n\in \mathbb{N}⟼\frac{A}{n}\right)⇝0\right)$$
16	5 15	mpbid	$$⊢A\in ℂ\to \left(n\in \mathbb{N}⟼\frac{A}{n}\right)⇝0$$