Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-neg | Unicode version |
Description: Define the negative of a number (unary minus). We use different symbols for unary minus () and subtraction () to prevent syntax ambiguity. See cneg 8078 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 8078 | . 2 |
3 | cc0 7761 | . . 3 | |
4 | cmin 8077 | . . 3 | |
5 | 3, 1, 4 | co 5850 | . 2 |
6 | 2, 5 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: negeq 8099 nfnegd 8102 csbnegg 8104 negcl 8106 neg0 8152 negid 8153 negsub 8154 subneg 8155 negneg 8156 negsubdi 8162 renegcl 8167 mulneg1 8301 ltneg 8368 leneg 8371 ixi 8489 0mnnnnn0 9154 fzshftral 10051 bernneq2 10584 cji 10853 bdtri 11190 prmdiv 12176 pcrec 12249 pcid 12264 4sqlem6 12322 4sqlem10 12326 sin0pilem1 13455 cospi 13474 coshalfpip 13496 ptolemy 13498 logbrec 13631 lgslem4 13657 |
Copyright terms: Public domain | W3C validator |