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}$

Step	Hyp	Ref	Expression
1		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
2		rpge0	$⊢ A \in ℝ^{+} \to 0 \leq A$
3		remsqsqrt	$⊢ (A \in ℝ \land 0 \leq A) \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} \neq 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}$

Metamath Proof Explorer