Theorem elnnnn0

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004)

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

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
2		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
3	2	eleq1d	$$⊢N\in ℂ\to \left(N-1+1\in \mathbb{N}\leftrightarrow N\in \mathbb{N}\right)$$
4		peano2cnm	$$⊢N\in ℂ\to N-1\in ℂ$$
5	4	biantrurd	$$⊢N\in ℂ\to \left(N-1+1\in \mathbb{N}\leftrightarrow \left(N-1\in ℂ\wedge N-1+1\in \mathbb{N}\right)\right)$$
6	3 5	bitr3d	$$⊢N\in ℂ\to \left(N\in \mathbb{N}\leftrightarrow \left(N-1\in ℂ\wedge N-1+1\in \mathbb{N}\right)\right)$$
7		elnn0nn	$$⊢N-1\in {\mathbb{N}}_0\leftrightarrow \left(N-1\in ℂ\wedge N-1+1\in \mathbb{N}\right)$$
8	6 7	bitr4di	$$⊢N\in ℂ\to \left(N\in \mathbb{N}\leftrightarrow N-1\in {\mathbb{N}}_0\right)$$
9	1 8	biadanii	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)$$