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

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