Metamath Proof Explorer

Theorem nnrpd

Description: A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypothesis nnrpd.1 
|- ( ph -> A e. NN )
Assertion nnrpd 
|- ( ph -> A e. RR+ )

Proof

Step Hyp Ref Expression
1 nnrpd.1 
 |-  ( ph -> A e. NN )
2 nnrp 
 |-  ( A e. NN -> A e. RR+ )
3 1 2 syl 
 |-  ( ph -> A e. RR+ )