![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-neg | GIF 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 7958 for a discussion of this. (Contributed by NM, 10-Feb-1995.) |
Ref | Expression |
---|---|
df-neg | ⊢ -𝐴 = (0 − 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cneg 7958 | . 2 class -𝐴 |
3 | cc0 7644 | . . 3 class 0 | |
4 | cmin 7957 | . . 3 class − | |
5 | 3, 1, 4 | co 5782 | . 2 class (0 − 𝐴) |
6 | 2, 5 | wceq 1332 | 1 wff -𝐴 = (0 − 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: negeq 7979 nfnegd 7982 csbnegg 7984 negcl 7986 neg0 8032 negid 8033 negsub 8034 subneg 8035 negneg 8036 negsubdi 8042 renegcl 8047 mulneg1 8181 ltneg 8248 leneg 8251 ixi 8369 0mnnnnn0 9033 fzshftral 9919 bernneq2 10444 cji 10706 bdtri 11043 sin0pilem1 12910 cospi 12929 coshalfpip 12951 ptolemy 12953 logbrec 13085 |
Copyright terms: Public domain | W3C validator |