Theorem sqrtlim

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

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

Proof

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	$$⊢\left(n\in {ℝ}^{+}⟼\frac{1}{n^{\frac{1}{2}}}\right)=\left(n\in {ℝ}^{+}⟼\frac{1}{\sqrt{n}}\right)$$
6		1rp	$$⊢1\in {ℝ}^{+}$$
7		rphalfcl	$$⊢1\in {ℝ}^{+}\to \frac{1}{2}\in {ℝ}^{+}$$
8		cxplim	$$⊢\frac{1}{2}\in {ℝ}^{+}\to \left(n\in {ℝ}^{+}⟼\frac{1}{n^{\frac{1}{2}}}\right)\underset{ℝ}{⇝}0$$
9	6 7 8	mp2b	$$⊢\left(n\in {ℝ}^{+}⟼\frac{1}{n^{\frac{1}{2}}}\right)\underset{ℝ}{⇝}0$$
10	5 9	eqbrtrri	$$⊢\left(n\in {ℝ}^{+}⟼\frac{1}{\sqrt{n}}\right)\underset{ℝ}{⇝}0$$