Theorem negn0nposznnd

Description: Lemma for dffltz . (Contributed by Steven Nguyen, 27-Feb-2023)

	Ref	Expression
Hypotheses	negn0nposznnd.1	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	negn0nposznnd.2	⊢ ( 𝜑 → ¬ 0 < 𝐴 )
	negn0nposznnd.3	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
Assertion	negn0nposznnd	⊢ ( 𝜑 → - 𝐴 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		negn0nposznnd.1	⊢ ( 𝜑 → 𝐴 ≠ 0 )
2		negn0nposznnd.2	⊢ ( 𝜑 → ¬ 0 < 𝐴 )
3		negn0nposznnd.3	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
4		nngt0	⊢ ( 𝐴 ∈ ℕ → 0 < 𝐴 )
5	2 4	nsyl	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℕ )
6	1	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
7	5 6	jca	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℕ ∧ ¬ 𝐴 = 0 ) )
8		pm4.56	⊢ ( ( ¬ 𝐴 ∈ ℕ ∧ ¬ 𝐴 = 0 ) ↔ ¬ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
9	7 8	sylib	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
10		elnn0	⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
11	9 10	sylnibr	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℕ0 )
12		znnn0nn	⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈ ℕ0 ) → - 𝐴 ∈ ℕ )
13	3 11 12	syl2anc	⊢ ( 𝜑 → - 𝐴 ∈ ℕ )