Theorem negn0nposznnd

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

	Ref	Expression
Hypotheses	negn0nposznnd.1	$$⊢\phi \to A\ne 0$$
	negn0nposznnd.2	$$⊢\phi \to \neg 0<A$$
	negn0nposznnd.3	$$⊢\phi \to A\in \mathbb{Z}$$
Assertion	negn0nposznnd	$$⊢\phi \to -A\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		negn0nposznnd.1	$$⊢\phi \to A\ne 0$$
2		negn0nposznnd.2	$$⊢\phi \to \neg 0<A$$
3		negn0nposznnd.3	$$⊢\phi \to A\in \mathbb{Z}$$
4		nngt0	$$⊢A\in \mathbb{N}\to 0<A$$
5	2 4	nsyl	$$⊢\phi \to \neg A\in \mathbb{N}$$
6	1	neneqd	$$⊢\phi \to \neg A=0$$
7	5 6	jca	$$⊢\phi \to \left(\neg A\in \mathbb{N}\wedge \neg A=0\right)$$
8		pm4.56	$$⊢\left(\neg A\in \mathbb{N}\wedge \neg A=0\right)\leftrightarrow \neg \left(A\in \mathbb{N}\vee A=0\right)$$
9	7 8	sylib	$$⊢\phi \to \neg \left(A\in \mathbb{N}\vee A=0\right)$$
10		elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
11	9 10	sylnibr	$$⊢\phi \to \neg A\in {\mathbb{N}}_0$$
12		znnn0nn	$$⊢\left(A\in \mathbb{Z}\wedge \neg A\in {\mathbb{N}}_0\right)\to -A\in \mathbb{N}$$
13	3 11 12	syl2anc	$$⊢\phi \to -A\in \mathbb{N}$$