Metamath Proof Explorer

Theorem nn0negzi

Description: The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypothesis nn0negzi.1 
|- N e. NN0
Assertion nn0negzi 
|- -u N e. ZZ

Proof

Step Hyp Ref Expression
1 nn0negzi.1 
 |-  N e. NN0
2 nn0negz 
 |-  ( N e. NN0 -> -u N e. ZZ )
3 1 2 ax-mp 
 |-  -u N e. ZZ