Theorem nnnegz

Description: The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002)

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

Proof

Step	Hyp	Ref	Expression
1		nnre	|- ( N e. NN -> N e. RR )
2	1	renegcld	|- ( N e. NN -> -u N e. RR )
3		nncn	|- ( N e. NN -> N e. CC )
4		negneg	|- ( N e. CC -> -u -u N = N )
5	4	eleq1d	|- ( N e. CC -> ( -u -u N e. NN <-> N e. NN ) )
6	5	biimprd	|- ( N e. CC -> ( N e. NN -> -u -u N e. NN ) )
7	3 6	mpcom	|- ( N e. NN -> -u -u N e. NN )
8	7	3mix3d	|- ( N e. NN -> ( -u N = 0 \/ -u N e. NN \/ -u -u N e. NN ) )
9		elz	|- ( -u N e. ZZ <-> ( -u N e. RR /\ ( -u N = 0 \/ -u N e. NN \/ -u -u N e. NN ) ) )
10	2 8 9	sylanbrc	|- ( N e. NN -> -u N e. ZZ )