Theorem znegcl

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

	Ref	Expression
Assertion	znegcl	|- ( N e. ZZ -> -u N e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		elz	|- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2		negeq	|- ( N = 0 -> -u N = -u 0 )
3		neg0	|- -u 0 = 0
4	2 3	eqtrdi	|- ( N = 0 -> -u N = 0 )
5		0z	|- 0 e. ZZ
6	4 5	eqeltrdi	|- ( N = 0 -> -u N e. ZZ )
7		nnnegz	|- ( N e. NN -> -u N e. ZZ )
8		nnz	|- ( -u N e. NN -> -u N e. ZZ )
9	6 7 8	3jaoi	|- ( ( N = 0 \/ N e. NN \/ -u N e. NN ) -> -u N e. ZZ )
10	1 9	simplbiim	|- ( N e. ZZ -> -u N e. ZZ )