Theorem sqrt9

Description: The square root of 9 is 3. (Contributed by NM, 11-May-2004)

	Ref	Expression
Assertion	sqrt9	$$⊢\sqrt{9}=3$$

Proof

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