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 8048 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 8048 | . 2 class -𝐴 |
3 | cc0 7733 | . . 3 class 0 | |
4 | cmin 8047 | . . 3 class − | |
5 | 3, 1, 4 | co 5825 | . 2 class (0 − 𝐴) |
6 | 2, 5 | wceq 1335 | 1 wff -𝐴 = (0 − 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: negeq 8069 nfnegd 8072 csbnegg 8074 negcl 8076 neg0 8122 negid 8123 negsub 8124 subneg 8125 negneg 8126 negsubdi 8132 renegcl 8137 mulneg1 8271 ltneg 8338 leneg 8341 ixi 8459 0mnnnnn0 9123 fzshftral 10011 bernneq2 10543 cji 10806 bdtri 11143 prmdiv 12114 sin0pilem1 13144 cospi 13163 coshalfpip 13185 ptolemy 13187 logbrec 13319 |
Copyright terms: Public domain | W3C validator |