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 
|- ( n e. RR+ |-> ( 1 / ( sqrt ` n ) ) ) ~~>r 0

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( n e. RR+ -> n e. CC )
2 cxpsqrt 
 |-  ( n e. CC -> ( n ^c ( 1 / 2 ) ) = ( sqrt ` n ) )
3 1 2 syl 
 |-  ( n e. RR+ -> ( n ^c ( 1 / 2 ) ) = ( sqrt ` n ) )
4 3 oveq2d 
 |-  ( n e. RR+ -> ( 1 / ( n ^c ( 1 / 2 ) ) ) = ( 1 / ( sqrt ` n ) ) )
5 4 mpteq2ia 
 |-  ( n e. RR+ |-> ( 1 / ( n ^c ( 1 / 2 ) ) ) ) = ( n e. RR+ |-> ( 1 / ( sqrt ` n ) ) )
6 1rp 
 |-  1 e. RR+
7 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
8 cxplim 
 |-  ( ( 1 / 2 ) e. RR+ -> ( n e. RR+ |-> ( 1 / ( n ^c ( 1 / 2 ) ) ) ) ~~>r 0 )
9 6 7 8 mp2b 
 |-  ( n e. RR+ |-> ( 1 / ( n ^c ( 1 / 2 ) ) ) ) ~~>r 0
10 5 9 eqbrtrri 
 |-  ( n e. RR+ |-> ( 1 / ( sqrt ` n ) ) ) ~~>r 0