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 |