Theorem divsqrtid

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

	Ref	Expression
Assertion	divsqrtid	$$⊢A\in {ℝ}^{+}\to \frac{A}{\sqrt{A}}=\sqrt{A}$$

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
2		rpge0	$$⊢A\in {ℝ}^{+}\to 0\le A$$
3		remsqsqrt	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{A}\sqrt{A}=A$$
4	1 2 3	syl2anc	$$⊢A\in {ℝ}^{+}\to \sqrt{A}\sqrt{A}=A$$
5	4	oveq1d	$$⊢A\in {ℝ}^{+}\to \frac{\sqrt{A}\sqrt{A}}{\sqrt{A}}=\frac{A}{\sqrt{A}}$$
6	1	recnd	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
7	6	sqrtcld	$$⊢A\in {ℝ}^{+}\to \sqrt{A}\in ℂ$$
8		rpsqrtcl	$$⊢A\in {ℝ}^{+}\to \sqrt{A}\in {ℝ}^{+}$$
9	8	rpne0d	$$⊢A\in {ℝ}^{+}\to \sqrt{A}\ne 0$$
10	7 7 9	divcan4d	$$⊢A\in {ℝ}^{+}\to \frac{\sqrt{A}\sqrt{A}}{\sqrt{A}}=\sqrt{A}$$
11	5 10	eqtr3d	$$⊢A\in {ℝ}^{+}\to \frac{A}{\sqrt{A}}=\sqrt{A}$$