![]() |
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 7805 |
. 2
![]() ![]() ![]() |
3 | cc0 7500 |
. . 3
![]() ![]() | |
4 | cmin 7804 |
. . 3
![]() ![]() | |
5 | 3, 1, 4 | co 5706 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: negeq 7826 nfnegd 7829 csbnegg 7831 negcl 7833 neg0 7879 negid 7880 negsub 7881 subneg 7882 negneg 7883 negsubdi 7889 renegcl 7894 mulneg1 8024 ltneg 8091 leneg 8094 ixi 8211 0mnnnnn0 8861 fzshftral 9729 bernneq2 10254 cji 10515 bdtri 10850 |
Copyright terms: Public domain | W3C validator |