Metamath Proof Explorer

Theorem reelznn0nn

Description: elznn0nn restated using df-resub . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion reelznn0nn ⊢ N ∈ ℤ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ 0 - ℝ N ∈ ℕ

Proof

Step Hyp Ref Expression
1 elznn0nn ⊢ N ∈ ℤ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ
2 df-neg ⊢ − N = 0 − N
3 0re ⊢ 0 ∈ ℝ
4 resubeqsub ⊢ 0 ∈ ℝ ∧ N ∈ ℝ → 0 - ℝ N = 0 − N
5 3 4 mpan ⊢ N ∈ ℝ → 0 - ℝ N = 0 − N
6 2 5 eqtr4id ⊢ N ∈ ℝ → − N = 0 - ℝ N
7 6 eleq1d ⊢ N ∈ ℝ → − N ∈ ℕ ↔ 0 - ℝ N ∈ ℕ
8 7 pm5.32i ⊢ N ∈ ℝ ∧ − N ∈ ℕ ↔ N ∈ ℝ ∧ 0 - ℝ N ∈ ℕ
9 8 orbi2i ⊢ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ 0 - ℝ N ∈ ℕ
10 1 9 bitri ⊢ N ∈ ℤ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ 0 - ℝ N ∈ ℕ