Theorem sqrt9

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

	Ref	Expression
Assertion	sqrt9	⊢ ( √ ‘ 9 ) = 3

Proof

Step	Hyp	Ref	Expression
1		sq3	⊢ ( 3 ↑ 2 ) = 9
2	1	fveq2i	⊢ ( √ ‘ ( 3 ↑ 2 ) ) = ( √ ‘ 9 )
3		3re	⊢ 3 ∈ ℝ
4		0re	⊢ 0 ∈ ℝ
5		3pos	⊢ 0 < 3
6	4 3 5	ltleii	⊢ 0 ≤ 3
7		sqrtsq	⊢ ( ( 3 ∈ ℝ ∧ 0 ≤ 3 ) → ( √ ‘ ( 3 ↑ 2 ) ) = 3 )
8	3 6 7	mp2an	⊢ ( √ ‘ ( 3 ↑ 2 ) ) = 3
9	2 8	eqtr3i	⊢ ( √ ‘ 9 ) = 3