Description: Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xnegcli.1 | |- A e. RR* |
|
Assertion | xnegcli | |- -e A e. RR* |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xnegcli.1 | |- A e. RR* |
|
2 | xnegcl | |- ( A e. RR* -> -e A e. RR* ) |
|
3 | 1 2 | ax-mp | |- -e A e. RR* |