Theorem nnrecre

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

	Ref	Expression
Assertion	nnrecre	⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		nndivre	⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 1 / 𝑁 ) ∈ ℝ )
3	1 2	mpan	⊢ ( 𝑁 ∈ ℕ → ( 1 / 𝑁 ) ∈ ℝ )