# 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 ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to -{N}\in ℕ$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to {N}\in ℤ$
2 1 znegcld ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to -{N}\in ℤ$
3 elznn ${⊢}-{N}\in ℤ↔\left(-{N}\in ℝ\wedge \left(-{N}\in ℕ\vee --{N}\in {ℕ}_{0}\right)\right)$
4 2 3 sylib ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to \left(-{N}\in ℝ\wedge \left(-{N}\in ℕ\vee --{N}\in {ℕ}_{0}\right)\right)$
5 4 simprd ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to \left(-{N}\in ℕ\vee --{N}\in {ℕ}_{0}\right)$
6 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
7 6 adantr ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to {N}\in ℂ$
8 7 negnegd ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to --{N}={N}$
9 simpr ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to ¬{N}\in {ℕ}_{0}$
10 8 9 eqneltrd ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to ¬--{N}\in {ℕ}_{0}$
11 pm2.24 ${⊢}--{N}\in {ℕ}_{0}\to \left(¬--{N}\in {ℕ}_{0}\to -{N}\in ℕ\right)$
12 11 jao1i ${⊢}\left(-{N}\in ℕ\vee --{N}\in {ℕ}_{0}\right)\to \left(¬--{N}\in {ℕ}_{0}\to -{N}\in ℕ\right)$
13 5 10 12 sylc ${⊢}\left({N}\in ℤ\wedge ¬{N}\in {ℕ}_{0}\right)\to -{N}\in ℕ$