Theorem xnn0gt0

Description: Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	xnn0gt0	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge N\ne 0\right)\to 0<N$$

Proof

Step	Hyp	Ref	Expression
1		elxnn0	$$⊢N\in {\mathbb{N}}_0^{*}\leftrightarrow \left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)$$
2		elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
3		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
4	2 3	sylbir	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)\to 0<N$$
5	4	ancoms	$$⊢\left(N\ne 0\wedge N\in {\mathbb{N}}_0\right)\to 0<N$$
6	5	adantll	$$⊢\left(\left(\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\wedge N\ne 0\right)\wedge N\in {\mathbb{N}}_0\right)\to 0<N$$
7		0ltpnf	$$⊢0<\mathrm{+\infty }$$
8		breq2	$$⊢N=\mathrm{+\infty }\to \left(0<N\leftrightarrow 0<\mathrm{+\infty }\right)$$
9	7 8	mpbiri	$$⊢N=\mathrm{+\infty }\to 0<N$$
10	9	adantl	$$⊢\left(\left(\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\wedge N\ne 0\right)\wedge N=\mathrm{+\infty }\right)\to 0<N$$
11		simpl	$$⊢\left(\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\wedge N\ne 0\right)\to \left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)$$
12	6 10 11	mpjaodan	$$⊢\left(\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\wedge N\ne 0\right)\to 0<N$$
13	1 12	sylanb	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge N\ne 0\right)\to 0<N$$