Theorem sqrtmsq

Description: Square root of square. (Contributed by NM, 2-Aug-1999) (Revised by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	sqrtmsq	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{AA}=A$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A\in ℝ$$
2	1	recnd	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A\in ℂ$$
3	2	sqvald	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A^2=AA$$
4	3	fveq2d	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{A^2}=\sqrt{AA}$$
5		sqrtsq	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{A^2}=A$$
6	4 5	eqtr3d	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{AA}=A$$