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

Metamath Proof Explorer

Theorem remsqsqrt

Description: Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013)

		Ref	Expression
	Assertion	remsqsqrt	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \sqrt{A} = A$

Step	Hyp	Ref	Expression
1		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
2	1	recnd	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℂ$
3	2	sqvald	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = \sqrt{A} \sqrt{A}$
4		resqrtth	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = A$
5	3 4	eqtr3d	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \sqrt{A} = A$