![]() |
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 (![]() ![]() |
Ref | Expression |
---|---|
df-neg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | 1 | cneg 8160 |
. 2
![]() ![]() ![]() |
3 | cc0 7842 |
. . 3
![]() ![]() | |
4 | cmin 8159 |
. . 3
![]() ![]() | |
5 | 3, 1, 4 | co 5897 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: negeq 8181 nfnegd 8184 csbnegg 8186 negcl 8188 neg0 8234 negid 8235 negsub 8236 subneg 8237 negneg 8238 negsubdi 8244 renegcl 8249 mulneg1 8383 ltneg 8450 leneg 8453 ixi 8571 0mnnnnn0 9239 fzshftral 10140 bernneq2 10676 cji 10946 bdtri 11283 prmdiv 12270 pcrec 12343 pcid 12359 4sqlem6 12418 4sqlem10 12422 sin0pilem1 14679 cospi 14698 coshalfpip 14720 ptolemy 14722 logbrec 14855 lgslem4 14882 |
Copyright terms: Public domain | W3C validator |