Theorem xnn0nnd

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

	Ref	Expression
Hypotheses	xnn0nnd.1	|- ( ph -> N e. NN0* )
	xnn0nnd.2	|- ( ph -> N e. RR )
	xnn0nnd.3	|- ( ph -> 0 < N )
Assertion	xnn0nnd	|- ( ph -> N e. NN )

Proof

Step	Hyp	Ref	Expression
1		xnn0nnd.1	|- ( ph -> N e. NN0* )
2		xnn0nnd.2	|- ( ph -> N e. RR )
3		xnn0nnd.3	|- ( ph -> 0 < N )
4	1 2	xnn0nn0d	|- ( ph -> N e. NN0 )
5		elnnnn0b	|- ( N e. NN <-> ( N e. NN0 /\ 0 < N ) )
6	4 3 5	sylanbrc	|- ( ph -> N e. NN )