Theorem elnnnn0b

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005)

	Ref	Expression
Assertion	elnnnn0b	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 0<N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
2		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
3	1 2	jca	$$⊢N\in \mathbb{N}\to \left(N\in {\mathbb{N}}_0\wedge 0<N\right)$$
4		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
5		breq2	$$⊢N=0\to \left(0<N\leftrightarrow 0<0\right)$$
6		0re	$$⊢0\in ℝ$$
7	6	ltnri	$$⊢\neg 0<0$$
8	7	pm2.21i	$$⊢0<0\to N\in \mathbb{N}$$
9	5 8	biimtrdi	$$⊢N=0\to \left(0<N\to N\in \mathbb{N}\right)$$
10	9	jao1i	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \left(0<N\to N\in \mathbb{N}\right)$$
11	4 10	sylbi	$$⊢N\in {\mathbb{N}}_0\to \left(0<N\to N\in \mathbb{N}\right)$$
12	11	imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge 0<N\right)\to N\in \mathbb{N}$$
13	3 12	impbii	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 0<N\right)$$