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

Proof

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