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	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 𝐴 / 𝑛 ) ) ⇝ 0 )

Proof

Step	Hyp	Ref	Expression
1		nnrp	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
2	1	ssriv	⊢ ℕ ⊆ ℝ+
3	2	a1i	⊢ ( 𝐴 ∈ ℂ → ℕ ⊆ ℝ+ )
4		divrcnv	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℝ+ ↦ ( 𝐴 / 𝑛 ) ) ⇝𝑟 0 )
5	3 4	rlimres2	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 𝐴 / 𝑛 ) ) ⇝𝑟 0 )
6		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
7		1zzd	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℤ )
8		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℂ )
9		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
11		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
12	11	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
13	8 10 12	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( 𝐴 / 𝑛 ) ∈ ℂ )
14	13	fmpttd	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 𝐴 / 𝑛 ) ) : ℕ ⟶ ℂ )
15	6 7 14	rlimclim	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ ↦ ( 𝐴 / 𝑛 ) ) ⇝𝑟 0 ↔ ( 𝑛 ∈ ℕ ↦ ( 𝐴 / 𝑛 ) ) ⇝ 0 ) )
16	5 15	mpbid	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 𝐴 / 𝑛 ) ) ⇝ 0 )