This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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