Theorem xnn0nn0d

Description: Conditions for an extended nonnegative integer to be a nonnegative integer. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	xnn0nnd.1	$$⊢\phi \to N\in {\mathbb{N}}_0^{*}$$
	xnn0nnd.2	$$⊢\phi \to N\in ℝ$$
Assertion	xnn0nn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		xnn0nnd.1	$$⊢\phi \to N\in {\mathbb{N}}_0^{*}$$
2		xnn0nnd.2	$$⊢\phi \to N\in ℝ$$
3		elxnn0	$$⊢N\in {\mathbb{N}}_0^{*}\leftrightarrow \left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)$$
4	1 3	sylib	$$⊢\phi \to \left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)$$
5	2	renepnfd	$$⊢\phi \to N\ne \mathrm{+\infty }$$
6	5	neneqd	$$⊢\phi \to \neg N=\mathrm{+\infty }$$
7	4 6	olcnd	$$⊢\phi \to N\in {\mathbb{N}}_0$$