Metamath Proof Explorer
Description: Closure law for negative integers. (Contributed by NM, 9May2004)


Ref 
Expression 

Assertion 
znegcl 
⊢ ( 𝑁 ∈ ℤ →  𝑁 ∈ ℤ ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

elz 
⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨  𝑁 ∈ ℕ ) ) ) 
2 

negeq 
⊢ ( 𝑁 = 0 →  𝑁 =  0 ) 
3 

neg0 
⊢  0 = 0 
4 
2 3

eqtrdi 
⊢ ( 𝑁 = 0 →  𝑁 = 0 ) 
5 

0z 
⊢ 0 ∈ ℤ 
6 
4 5

eqeltrdi 
⊢ ( 𝑁 = 0 →  𝑁 ∈ ℤ ) 
7 

nnnegz 
⊢ ( 𝑁 ∈ ℕ →  𝑁 ∈ ℤ ) 
8 

nnz 
⊢ (  𝑁 ∈ ℕ →  𝑁 ∈ ℤ ) 
9 
6 7 8

3jaoi 
⊢ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨  𝑁 ∈ ℕ ) →  𝑁 ∈ ℤ ) 
10 
1 9

simplbiim 
⊢ ( 𝑁 ∈ ℤ →  𝑁 ∈ ℤ ) 