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