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

Metamath Proof Explorer

Theorem resqrtth

Description: Square root theorem over the reals. Theorem I.35 of Apostol p. 29. (Contributed by Mario Carneiro, 9-Jul-2013)

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

Step	Hyp	Ref	Expression
1		resqrtthlem	$⊢ (A \in ℝ \land 0 \leq A) \to ({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+})$
2	1	simp1d	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = A$