Description: The number 2 is positive. (Contributed by NM, 27May1999)
Ref  Expression  

Assertion  2pos   0 < 2 
Step  Hyp  Ref  Expression 

1  1re   1 e. RR 

2  0lt1   0 < 1 

3  1 1 2 2  addgt0ii   0 < ( 1 + 1 ) 
4  df2   2 = ( 1 + 1 ) 

5  3 4  breqtrri   0 < 2 