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 ⊢ φ → N ∈ ℕ 0 *
xnn0nnd.2 ⊢ φ → N ∈ ℝ
Assertion xnn0nn0d ⊢ φ → N ∈ ℕ 0

Proof

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