Theorem elnn0nn

Description: The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	elnn0nn	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in ℂ\wedge N+1\in \mathbb{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
2		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
3	1 2	jca	$$⊢N\in {\mathbb{N}}_0\to \left(N\in ℂ\wedge N+1\in \mathbb{N}\right)$$
4		simpl	$$⊢\left(N\in ℂ\wedge N+1\in \mathbb{N}\right)\to N\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6		pncan	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N+1-1=N$$
7	4 5 6	sylancl	$$⊢\left(N\in ℂ\wedge N+1\in \mathbb{N}\right)\to N+1-1=N$$
8		nnm1nn0	$$⊢N+1\in \mathbb{N}\to N+1-1\in {\mathbb{N}}_0$$
9	8	adantl	$$⊢\left(N\in ℂ\wedge N+1\in \mathbb{N}\right)\to N+1-1\in {\mathbb{N}}_0$$
10	7 9	eqeltrrd	$$⊢\left(N\in ℂ\wedge N+1\in \mathbb{N}\right)\to N\in {\mathbb{N}}_0$$
11	3 10	impbii	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in ℂ\wedge N+1\in \mathbb{N}\right)$$