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

Metamath Proof Explorer

Theorem nn0p1nn

Description: A nonnegative integer plus 1 is a positive integer. Strengthening of peano2nn . (Contributed by Raph Levien, 30-Jun-2006) (Revised by Mario Carneiro, 16-May-2014)

		Ref	Expression
	Assertion	nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		nn0nnaddcl	$⊢ (N \in ℕ_{0} \land 1 \in ℕ) \to N + 1 \in ℕ$
3	1 2	mpan2	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$