Metamath Proof Explorer
Description: A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3Oct2018)


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