Metamath Proof Explorer


Theorem nn0p1gt0

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 ) )