Metamath Proof Explorer

Theorem sqrt2re

Description: The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004)

Ref Expression
Assertion sqrt2re 
|- ( sqrt ` 2 ) e. RR

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 2pos 
 |-  0 < 2
3 1 2 sqrtpclii 
 |-  ( sqrt ` 2 ) e. RR