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 7902 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 7902 | . 2 |
3 | cc0 7588 | . . 3 | |
4 | cmin 7901 | . . 3 | |
5 | 3, 1, 4 | co 5742 | . 2 |
6 | 2, 5 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: negeq 7923 nfnegd 7926 csbnegg 7928 negcl 7930 neg0 7976 negid 7977 negsub 7978 subneg 7979 negneg 7980 negsubdi 7986 renegcl 7991 mulneg1 8125 ltneg 8192 leneg 8195 ixi 8313 0mnnnnn0 8977 fzshftral 9856 bernneq2 10381 cji 10642 bdtri 10979 sin0pilem1 12789 cospi 12808 coshalfpip 12830 ptolemy 12832 |
Copyright terms: Public domain | W3C validator |