This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0* )
xnn0nnd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
Assertion xnn0nn0d ( 𝜑 → 𝑁 ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 xnn0nnd.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0* )
2 xnn0nnd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
3 elxnn0 ⊢ ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
4 1 3 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
5 2 renepnfd ⊢ ( 𝜑 → 𝑁 ≠ +∞ )
6 5 neneqd ⊢ ( 𝜑 → ¬ 𝑁 = +∞ )
7 4 6 olcnd ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )