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

Metamath Proof Explorer

Theorem sqrt1

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

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

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