![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-neg | Unicode version |
Description: Define the negative of a
number (unary minus). We use different symbols
for unary minus (-u ) and subtraction
() to prevent syntax
ambiguity. See cneg 9829 for a discussion of this. (Contributed by
NM,
10-Feb-1995.) |
Ref | Expression |
---|---|
df-neg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | cneg 9829 | . 2 |
3 | cc0 9513 | . . 3 | |
4 | cmin 9828 | . . 3 | |
5 | 3, 1, 4 | co 6296 | . 2 |
6 | 2, 5 | wceq 1395 | 1 |
Copyright terms: Public domain | W3C validator |