This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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