Theorem sqrtlim

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

	Ref	Expression
Assertion	sqrtlim	⊢ ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑛 ) ) ) ⇝𝑟 0

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℂ )
2		cxpsqrt	⊢ ( 𝑛 ∈ ℂ → ( 𝑛 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑛 ) )
3	1 2	syl	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑛 ) )
4	3	oveq2d	⊢ ( 𝑛 ∈ ℝ+ → ( 1 / ( 𝑛 ↑𝑐 ( 1 / 2 ) ) ) = ( 1 / ( √ ‘ 𝑛 ) ) )
5	4	mpteq2ia	⊢ ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( 𝑛 ↑𝑐 ( 1 / 2 ) ) ) ) = ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑛 ) ) )
6		1rp	⊢ 1 ∈ ℝ+
7		rphalfcl	⊢ ( 1 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
8		cxplim	⊢ ( ( 1 / 2 ) ∈ ℝ+ → ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( 𝑛 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0 )
9	6 7 8	mp2b	⊢ ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( 𝑛 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0
10	5 9	eqbrtrri	⊢ ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑛 ) ) ) ⇝𝑟 0