Theorem xnn0ge0

Description: An extended nonnegative integer is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018) (Revised by AV, 10-Dec-2020)

	Ref	Expression
Assertion	xnn0ge0	$$⊢N\in {\mathbb{N}}_0^{*}\to 0\le 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		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
3		0lepnf	$$⊢0\le \mathrm{+\infty }$$
4		breq2	$$⊢N=\mathrm{+\infty }\to \left(0\le N\leftrightarrow 0\le \mathrm{+\infty }\right)$$
5	3 4	mpbiri	$$⊢N=\mathrm{+\infty }\to 0\le N$$
6	2 5	jaoi	$$⊢\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\to 0\le N$$
7	1 6	sylbi	$$⊢N\in {\mathbb{N}}_0^{*}\to 0\le N$$