Theorem xnn0nnn0pnf

Description: An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	xnn0nnn0pnf	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge \neg N\in {\mathbb{N}}_0\right)\to N=\mathrm{+\infty }$$

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		pm2.53	$$⊢\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\to \left(\neg N\in {\mathbb{N}}_0\to N=\mathrm{+\infty }\right)$$
3	1 2	sylbi	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\neg N\in {\mathbb{N}}_0\to N=\mathrm{+\infty }\right)$$
4	3	imp	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge \neg N\in {\mathbb{N}}_0\right)\to N=\mathrm{+\infty }$$