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

Metamath Proof Explorer

Theorem reelznn0nn

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

Ref Expression
Assertion reelznn0nn ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ ( 0 −ℝ 𝑁 ) ∈ ℕ ) ) )

Proof

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