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

Proof

Step Hyp Ref Expression
1 sq2
 |-  ( 2 ^ 2 ) = 4
2 1 fveq2i
 |-  ( sqrt ` ( 2 ^ 2 ) ) = ( sqrt ` 4 )
3 2re
 |-  2 e. RR
4 0le2
 |-  0 <_ 2
5 sqrtsq
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( sqrt ` ( 2 ^ 2 ) ) = 2 )
6 3 4 5 mp2an
 |-  ( sqrt ` ( 2 ^ 2 ) ) = 2
7 2 6 eqtr3i
 |-  ( sqrt ` 4 ) = 2