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

Metamath Proof Explorer

Theorem sqrt9

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

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

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 \leq 3$
7		sqrtsq	$⊢ (3 \in ℝ \land 0 \leq 3) \to \sqrt{3^{2}} = 3$
8	3 6 7	mp2an	$⊢ \sqrt{3^{2}} = 3$
9	2 8	eqtr3i	$⊢ \sqrt{9} = 3$