This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )