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