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 ) → - 𝑁 ∈ ℕ )