Metamath Proof Explorer

Theorem 2re

Description: The number 2 is real. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion 2re 
|- 2 e. RR

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1re 
 |-  1 e. RR
3 2 2 readdcli 
 |-  ( 1 + 1 ) e. RR
4 1 3 eqeltri 
 |-  2 e. RR