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\in \mathbb{N}\to \frac{1}{N}\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
2		rpreccl	$$⊢N\in {ℝ}^{+}\to \frac{1}{N}\in {ℝ}^{+}$$
3	1 2	syl	$$⊢N\in \mathbb{N}\to \frac{1}{N}\in {ℝ}^{+}$$