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