Theorem nnrecre

Description: The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008)

	Ref	Expression
Assertion	nnrecre	$$⊢N\in \mathbb{N}\to \frac{1}{N}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		nndivre	$$⊢\left(1\in ℝ\wedge N\in \mathbb{N}\right)\to \frac{1}{N}\in ℝ$$
3	1 2	mpan	$$⊢N\in \mathbb{N}\to \frac{1}{N}\in ℝ$$