Description: Lemma for dffltz . (Contributed by Steven Nguyen, 27-Feb-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | negn0nposznnd.1 | |
|
negn0nposznnd.2 | |
||
negn0nposznnd.3 | |
||
Assertion | negn0nposznnd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negn0nposznnd.1 | |
|
2 | negn0nposznnd.2 | |
|
3 | negn0nposznnd.3 | |
|
4 | nngt0 | |
|
5 | 2 4 | nsyl | |
6 | 1 | neneqd | |
7 | 5 6 | jca | |
8 | pm4.56 | |
|
9 | 7 8 | sylib | |
10 | elnn0 | |
|
11 | 9 10 | sylnibr | |
12 | znnn0nn | |
|
13 | 3 11 12 | syl2anc | |