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