Metamath Proof Explorer


Theorem znegcl

Description: Closure law for negative integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion znegcl N N

Proof

Step Hyp Ref Expression
1 elz N N N = 0 N N
2 negeq N = 0 N = 0
3 neg0 0 = 0
4 2 3 syl6eq N = 0 N = 0
5 0z 0
6 4 5 eqeltrdi N = 0 N
7 nnnegz N N
8 nnz N N
9 6 7 8 3jaoi N = 0 N N N
10 1 9 simplbiim N N