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 ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℕ )

Proof

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