Metamath Proof Explorer
Description: A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018)
|
|
Ref |
Expression |
|
Assertion |
nn0p1gt0 |
⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nn0re |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ ) |
2 |
|
1red |
⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ ) |
3 |
|
nn0ge0 |
⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 ) |
4 |
|
0lt1 |
⊢ 0 < 1 |
5 |
4
|
a1i |
⊢ ( 𝑁 ∈ ℕ0 → 0 < 1 ) |
6 |
1 2 3 5
|
addgegt0d |
⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) ) |