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	$$⊢\phi \to N\in {\mathbb{N}}_0^{*}$$
	xnn0nnd.2	$$⊢\phi \to N\in ℝ$$
	xnn0nnd.3	$$⊢\phi \to 0<N$$
Assertion	xnn0nnd	$$⊢\phi \to N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		xnn0nnd.1	$$⊢\phi \to N\in {\mathbb{N}}_0^{*}$$
2		xnn0nnd.2	$$⊢\phi \to N\in ℝ$$
3		xnn0nnd.3	$$⊢\phi \to 0<N$$
4	1 2	xnn0nn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		elnnnn0b	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 0<N\right)$$
6	4 3 5	sylanbrc	$$⊢\phi \to N\in \mathbb{N}$$