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	|- ( ph -> N e. NN0* )
	xnn0nnd.2	|- ( ph -> N e. RR )
Assertion	xnn0nn0d	|- ( ph -> N e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		xnn0nnd.1	|- ( ph -> N e. NN0* )
2		xnn0nnd.2	|- ( ph -> N e. RR )
3		elxnn0	|- ( N e. NN0* <-> ( N e. NN0 \/ N = +oo ) )
4	1 3	sylib	|- ( ph -> ( N e. NN0 \/ N = +oo ) )
5	2	renepnfd	|- ( ph -> N =/= +oo )
6	5	neneqd	|- ( ph -> -. N = +oo )
7	4 6	olcnd	|- ( ph -> N e. NN0 )