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

Metamath Proof Explorer

Theorem sqrt4

Description: The square root of 4 is 2. (Contributed by NM, 3-Aug-1999)

		Ref	Expression
	Assertion	sqrt4	$⊢ \sqrt{4} = 2$

Step	Hyp	Ref	Expression
1		sq2	$⊢ 2^{2} = 4$
2	1	fveq2i	$⊢ \sqrt{2^{2}} = \sqrt{4}$
3		2re	$⊢ 2 \in ℝ$
4		0le2	$⊢ 0 \leq 2$
5		sqrtsq	$⊢ (2 \in ℝ \land 0 \leq 2) \to \sqrt{2^{2}} = 2$
6	3 4 5	mp2an	$⊢ \sqrt{2^{2}} = 2$
7	2 6	eqtr3i	$⊢ \sqrt{4} = 2$