Metamath Proof Explorer


Theorem negn0nposznnd

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

Ref Expression
Hypotheses negn0nposznnd.1 φA0
negn0nposznnd.2 φ¬0<A
negn0nposznnd.3 φA
Assertion negn0nposznnd φA

Proof

Step Hyp Ref Expression
1 negn0nposznnd.1 φA0
2 negn0nposznnd.2 φ¬0<A
3 negn0nposznnd.3 φA
4 nngt0 A0<A
5 2 4 nsyl φ¬A
6 1 neneqd φ¬A=0
7 5 6 jca φ¬A¬A=0
8 pm4.56 ¬A¬A=0¬AA=0
9 7 8 sylib φ¬AA=0
10 elnn0 A0AA=0
11 9 10 sylnibr φ¬A0
12 znnn0nn A¬A0A
13 3 11 12 syl2anc φA