This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 / 𝑁 ) ∈ ℝ+ )