Theorem xnn0nemnf

Description: No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	xnn0nemnf	$$⊢A\in {\mathbb{N}}_0^{*}\to A\ne \mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		elxnn0	$$⊢A\in {\mathbb{N}}_0^{*}\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)$$
2		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
3	2	renemnfd	$$⊢A\in {\mathbb{N}}_0\to A\ne \mathrm{-\infty }$$
4		pnfnemnf	$$⊢\mathrm{+\infty }\ne \mathrm{-\infty }$$
5		neeq1	$$⊢A=\mathrm{+\infty }\to \left(A\ne \mathrm{-\infty }\leftrightarrow \mathrm{+\infty }\ne \mathrm{-\infty }\right)$$
6	4 5	mpbiri	$$⊢A=\mathrm{+\infty }\to A\ne \mathrm{-\infty }$$
7	3 6	jaoi	$$⊢\left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)\to A\ne \mathrm{-\infty }$$
8	1 7	sylbi	$$⊢A\in {\mathbb{N}}_0^{*}\to A\ne \mathrm{-\infty }$$