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 )