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