Theorem elnnnn0c

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

	Ref	Expression
Assertion	elnnnn0c	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 1\le N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
2		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
3	1 2	jca	$$⊢N\in \mathbb{N}\to \left(N\in {\mathbb{N}}_0\wedge 1\le N\right)$$
4		0lt1	$$⊢0<1$$
5		0re	$$⊢0\in ℝ$$
6		1re	$$⊢1\in ℝ$$
7		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
8		ltletr	$$⊢\left(0\in ℝ\wedge 1\in ℝ\wedge N\in ℝ\right)\to \left(\left(0<1\wedge 1\le N\right)\to 0<N\right)$$
9	5 6 7 8	mp3an12i	$$⊢N\in {\mathbb{N}}_0\to \left(\left(0<1\wedge 1\le N\right)\to 0<N\right)$$
10	4 9	mpani	$$⊢N\in {\mathbb{N}}_0\to \left(1\le N\to 0<N\right)$$
11	10	imdistani	$$⊢\left(N\in {\mathbb{N}}_0\wedge 1\le N\right)\to \left(N\in {\mathbb{N}}_0\wedge 0<N\right)$$
12		elnnnn0b	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 0<N\right)$$
13	11 12	sylibr	$$⊢\left(N\in {\mathbb{N}}_0\wedge 1\le N\right)\to N\in \mathbb{N}$$
14	3 13	impbii	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 1\le N\right)$$