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

Metamath Proof Explorer

Theorem znnn0nn

Description: The negative of a negative integer, is a natural number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion znnn0nn 
|- ( ( N e. ZZ /\ -. N e. NN0 ) -> -u N e. NN )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> N e. ZZ )
2 1 znegcld 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> -u N e. ZZ )
3 elznn 
 |-  ( -u N e. ZZ <-> ( -u N e. RR /\ ( -u N e. NN \/ -u -u N e. NN0 ) ) )
4 2 3 sylib 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> ( -u N e. RR /\ ( -u N e. NN \/ -u -u N e. NN0 ) ) )
5 4 simprd 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> ( -u N e. NN \/ -u -u N e. NN0 ) )
6 zcn 
 |-  ( N e. ZZ -> N e. CC )
7 6 adantr 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> N e. CC )
8 7 negnegd 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> -u -u N = N )
9 simpr 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> -. N e. NN0 )
10 8 9 eqneltrd 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> -. -u -u N e. NN0 )
11 pm2.24 
 |-  ( -u -u N e. NN0 -> ( -. -u -u N e. NN0 -> -u N e. NN ) )
12 11 jao1i 
 |-  ( ( -u N e. NN \/ -u -u N e. NN0 ) -> ( -. -u -u N e. NN0 -> -u N e. NN ) )
13 5 10 12 sylc 
 |-  ( ( N e. ZZ /\ -. N e. NN0 ) -> -u N e. NN )