Theorem sqrt1

Description: The square root of 1 is 1. (Contributed by NM, 31-Jul-1999)

	Ref	Expression
Assertion	sqrt1	$$⊢\sqrt{1}=1$$

Proof

Step	Hyp	Ref	Expression
1		sq1	$$⊢1^2=1$$
2	1	fveq2i	$$⊢\sqrt{1^2}=\sqrt{1}$$
3		1re	$$⊢1\in ℝ$$
4		0le1	$$⊢0\le 1$$
5		sqrtsq	$$⊢\left(1\in ℝ\wedge 0\le 1\right)\to \sqrt{1^2}=1$$
6	3 4 5	mp2an	$$⊢\sqrt{1^2}=1$$
7	2 6	eqtr3i	$$⊢\sqrt{1}=1$$