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 7902 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 7902 | . 2 class -𝐴 |
3 | cc0 7588 | . . 3 class 0 | |
4 | cmin 7901 | . . 3 class − | |
5 | 3, 1, 4 | co 5742 | . 2 class (0 − 𝐴) |
6 | 2, 5 | wceq 1316 | 1 wff -𝐴 = (0 − 𝐴) |
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 8312 0mnnnnn0 8967 fzshftral 9843 bernneq2 10368 cji 10629 bdtri 10966 sin0pilem1 12773 cospi 12792 coshalfpip 12814 ptolemy 12816 |
Copyright terms: Public domain | W3C validator |