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 7934 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 7934 | . 2 class -𝐴 |
3 | cc0 7620 | . . 3 class 0 | |
4 | cmin 7933 | . . 3 class − | |
5 | 3, 1, 4 | co 5774 | . 2 class (0 − 𝐴) |
6 | 2, 5 | wceq 1331 | 1 wff -𝐴 = (0 − 𝐴) |
Colors of variables: wff set class |
This definition is referenced by: negeq 7955 nfnegd 7958 csbnegg 7960 negcl 7962 neg0 8008 negid 8009 negsub 8010 subneg 8011 negneg 8012 negsubdi 8018 renegcl 8023 mulneg1 8157 ltneg 8224 leneg 8227 ixi 8345 0mnnnnn0 9009 fzshftral 9888 bernneq2 10413 cji 10674 bdtri 11011 sin0pilem1 12862 cospi 12881 coshalfpip 12903 ptolemy 12905 |
Copyright terms: Public domain | W3C validator |