Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

Hypothesis  nn0red.1   ( ph > A e. NN0 ) 

Assertion  nn0red   ( ph > A e. RR ) 
Step  Hyp  Ref  Expression 

1  nn0red.1   ( ph > A e. NN0 ) 

2  nn0ssre   NN0 C_ RR 

3  2 1  sseldi   ( ph > A e. RR ) 