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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 xnn0nnd.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0* )
2 xnn0nnd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
3 xnn0nnd.3 ⊢ ( 𝜑 → 0 < 𝑁 )
4 1 2 xnn0nn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 elnnnn0b ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 0 < 𝑁 ) )
6 4 3 5 sylanbrc ⊢ ( 𝜑 → 𝑁 ∈ ℕ )