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 ∈ ℤ ∧ ¬ N ∈ ℕ 0 → − N ∈ ℕ

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → N ∈ ℤ
2 1 znegcld ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → − N ∈ ℤ
3 elznn ⊢ − N ∈ ℤ ↔ − N ∈ ℝ ∧ − N ∈ ℕ ∨ − -N ∈ ℕ 0
4 2 3 sylib ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → − N ∈ ℝ ∧ − N ∈ ℕ ∨ − -N ∈ ℕ 0
5 4 simprd ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → − N ∈ ℕ ∨ − -N ∈ ℕ 0
6 zcn ⊢ N ∈ ℤ → N ∈ ℂ
7 6 adantr ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → N ∈ ℂ
8 7 negnegd ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → − -N = N
9 simpr ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → ¬ N ∈ ℕ 0
10 8 9 eqneltrd ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → ¬ − -N ∈ ℕ 0
11 pm2.24 ⊢ − -N ∈ ℕ 0 → ¬ − -N ∈ ℕ 0 → − N ∈ ℕ
12 11 jao1i ⊢ − N ∈ ℕ ∨ − -N ∈ ℕ 0 → ¬ − -N ∈ ℕ 0 → − N ∈ ℕ
13 5 10 12 sylc ⊢ N ∈ ℤ ∧ ¬ N ∈ ℕ 0 → − N ∈ ℕ