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	$$⊢N\in {\mathbb{N}}_0\to 0<N+1$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
2		1red	$$⊢N\in {\mathbb{N}}_0\to 1\in ℝ$$
3		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
4		0lt1	$$⊢0<1$$
5	4	a1i	$$⊢N\in {\mathbb{N}}_0\to 0<1$$
6	1 2 3 5	addgegt0d	$$⊢N\in {\mathbb{N}}_0\to 0<N+1$$