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 −ℝ 𝑁 ) ∈ ℕ ) ) )