This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 |