Theorem negn0nposznnd

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

	Ref	Expression
Hypotheses	negn0nposznnd.1	|- ( ph -> A =/= 0 )
	negn0nposznnd.2	|- ( ph -> -. 0 < A )
	negn0nposznnd.3	|- ( ph -> A e. ZZ )
Assertion	negn0nposznnd	|- ( ph -> -u A e. NN )

Proof

Step	Hyp	Ref	Expression
1		negn0nposznnd.1	|- ( ph -> A =/= 0 )
2		negn0nposznnd.2	|- ( ph -> -. 0 < A )
3		negn0nposznnd.3	|- ( ph -> A e. ZZ )
4		nngt0	|- ( A e. NN -> 0 < A )
5	2 4	nsyl	|- ( ph -> -. A e. NN )
6	1	neneqd	|- ( ph -> -. A = 0 )
7	5 6	jca	|- ( ph -> ( -. A e. NN /\ -. A = 0 ) )
8		pm4.56	|- ( ( -. A e. NN /\ -. A = 0 ) <-> -. ( A e. NN \/ A = 0 ) )
9	7 8	sylib	|- ( ph -> -. ( A e. NN \/ A = 0 ) )
10		elnn0	|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
11	9 10	sylnibr	|- ( ph -> -. A e. NN0 )
12		znnn0nn	|- ( ( A e. ZZ /\ -. A e. NN0 ) -> -u A e. NN )
13	3 11 12	syl2anc	|- ( ph -> -u A e. NN )