Metamath Proof Explorer

Theorem nnneneg

Description: No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023)

Ref Expression
Assertion nnneneg 
|- ( A e. NN -> A =/= -u A )

Proof

Step Hyp Ref Expression
1 nnne0 
 |-  ( A e. NN -> A =/= 0 )
2 1 neneqd 
 |-  ( A e. NN -> -. A = 0 )
3 nncn 
 |-  ( A e. NN -> A e. CC )
4 3 eqnegd 
 |-  ( A e. NN -> ( A = -u A <-> A = 0 ) )
5 2 4 mtbird 
 |-  ( A e. NN -> -. A = -u A )
6 5 neqned 
 |-  ( A e. NN -> A =/= -u A )