Metamath Proof Explorer


Theorem divsqrtid

Description: A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022)

Ref Expression
Assertion divsqrtid
|- ( A e. RR+ -> ( A / ( sqrt ` A ) ) = ( sqrt ` A ) )

Proof

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 ) )