sqrtlim

Description: The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016)

		Ref	Expression
	Assertion	sqrtlim	$⊢ (n \in ℝ^{+} ⟼ \frac{1}{\sqrt{n}}) \underset{ℝ}{⇝} 0$

Step	Hyp	Ref	Expression
1		rpcn	$⊢ n \in ℝ^{+} \to n \in ℂ$
2		cxpsqrt	$⊢ n \in ℂ \to n^{\frac{1}{2}} = \sqrt{n}$
3	1 2	syl	$⊢ n \in ℝ^{+} \to n^{\frac{1}{2}} = \sqrt{n}$
4	3	oveq2d	$⊢ n \in ℝ^{+} \to \frac{1}{n^{\frac{1}{2}}} = \frac{1}{\sqrt{n}}$
5	4	mpteq2ia	$⊢ (n \in ℝ^{+} ⟼ \frac{1}{n^{\frac{1}{2}}}) = (n \in ℝ^{+} ⟼ \frac{1}{\sqrt{n}})$
6		1rp	$⊢ 1 \in ℝ^{+}$
7		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
8		cxplim	$⊢ \frac{1}{2} \in ℝ^{+} \to (n \in ℝ^{+} ⟼ \frac{1}{n^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0$
9	6 7 8	mp2b	$⊢ (n \in ℝ^{+} ⟼ \frac{1}{n^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0$
10	5 9	eqbrtrri	$⊢ (n \in ℝ^{+} ⟼ \frac{1}{\sqrt{n}}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer