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 e. RR
4		0re	|- 0 e. RR
5		3pos	|- 0 < 3
6	4 3 5	ltleii	|- 0 <_ 3
7		sqrtsq	|- ( ( 3 e. RR /\ 0 <_ 3 ) -> ( sqrt ` ( 3 ^ 2 ) ) = 3 )
8	3 6 7	mp2an	|- ( sqrt ` ( 3 ^ 2 ) ) = 3
9	2 8	eqtr3i	|- ( sqrt ` 9 ) = 3