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+ )