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 ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
2 rpreccl ( 𝑁 ∈ ℝ+ → ( 1 / 𝑁 ) ∈ ℝ+ )
3 1 2 syl ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ+ )