Metamath Proof Explorer

Theorem nnrecrp

Description: The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion nnrecrp 
|- ( N e. NN -> ( 1 / N ) e. RR+ )

Proof

Step Hyp Ref Expression
1 nnrp 
 |-  ( N e. NN -> N e. RR+ )
2 rpreccl 
 |-  ( N e. RR+ -> ( 1 / N ) e. RR+ )
3 1 2 syl 
 |-  ( N e. NN -> ( 1 / N ) e. RR+ )