Step |
Hyp |
Ref |
Expression |
1 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
2 |
|
rpge0 |
|- ( A e. RR+ -> 0 <_ A ) |
3 |
|
remsqsqrt |
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) x. ( sqrt ` A ) ) = A ) |
4 |
1 2 3
|
syl2anc |
|- ( A e. RR+ -> ( ( sqrt ` A ) x. ( sqrt ` A ) ) = A ) |
5 |
4
|
oveq1d |
|- ( A e. RR+ -> ( ( ( sqrt ` A ) x. ( sqrt ` A ) ) / ( sqrt ` A ) ) = ( A / ( sqrt ` A ) ) ) |
6 |
1
|
recnd |
|- ( A e. RR+ -> A e. CC ) |
7 |
6
|
sqrtcld |
|- ( A e. RR+ -> ( sqrt ` A ) e. CC ) |
8 |
|
rpsqrtcl |
|- ( A e. RR+ -> ( sqrt ` A ) e. RR+ ) |
9 |
8
|
rpne0d |
|- ( A e. RR+ -> ( sqrt ` A ) =/= 0 ) |
10 |
7 7 9
|
divcan4d |
|- ( A e. RR+ -> ( ( ( sqrt ` A ) x. ( sqrt ` A ) ) / ( sqrt ` A ) ) = ( sqrt ` A ) ) |
11 |
5 10
|
eqtr3d |
|- ( A e. RR+ -> ( A / ( sqrt ` A ) ) = ( sqrt ` A ) ) |