Theorem List for Intuitionistic Logic Explorer - 8001-8100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | addsubeq4 8001 |
Relation between sums and differences. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pncan3oi 8002 |
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 8063 and pncan 7992, this order happens often when
applying
"operations to both sides" so create a theorem specifically
for it. A
deduction version of this is available as pncand 8098. (Contributed by
David A. Wheeler, 11-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif)
![A A](_ca.gif) |
|
Theorem | mvrraddi 8003 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![C C](_cc.gif)
![B B](_cb.gif) |
|
Theorem | mvlladdi 8004 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | subid 8005 |
Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.)
(Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | subid1 8006 |
Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | npncan 8007 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nppcan 8008 |
Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif)
![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnpcan 8009 |
Cancellation law for subtraction: ((a-b)-c)+b = a-c holds for complex
numbers a,b,c. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif)
![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nppcan3 8010 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subcan2 8011 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subeq0 8012 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16-Nov-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | npncan2 8013 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
21-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![0 0](0.gif) ![)
)](rp.gif) |
|
Theorem | subsub2 8014 |
Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nncan 8015 |
Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subsub 8016 |
Law for double subtraction. (Contributed by NM, 13-May-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nppcan2 8017 |
Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif)
![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsub3 8018 |
Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsub4 8019 |
Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sub32 8020 |
Swap the second and third terms in a double subtraction. (Contributed by
NM, 19-Aug-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnncan 8021 |
Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif)
![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnncan1 8022 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnncan2 8023 |
Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | npncan3 8024 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pnpcan 8025 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pnpcan2 8026 |
Cancellation law for mixed addition and subtraction. (Contributed by
Scott Fenton, 9-Jun-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pnncan 8027 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ppncan 8028 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsub4 8029 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 4-Mar-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subadd4 8030 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 24-Aug-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sub4 8031 |
Rearrangement of 4 terms in a subtraction. (Contributed by NM,
23-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | neg0 8032 |
Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|
![-u -u](shortminus.gif)
![0 0](0.gif) |
|
Theorem | negid 8033 |
Addition of a number and its negative. (Contributed by NM,
14-Mar-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | negsub 8034 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subneg 8035 |
Relationship between subtraction and negative. (Contributed by NM,
10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negneg 8036 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by NM,
12-Jan-2002.) (Revised by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | neg11 8037 |
Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negcon1 8038 |
Negative contraposition law. (Contributed by NM, 9-May-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negcon2 8039 |
Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negeq0 8040 |
A number is zero iff its negative is zero. (Contributed by NM,
12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subcan 8041 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negsubdi 8042 |
Distribution of negative over subtraction. (Contributed by NM,
15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negdi 8043 |
Distribution of negative over addition. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negdi2 8044 |
Distribution of negative over addition. (Contributed by NM,
1-Jan-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negsubdi2 8045 |
Distribution of negative over subtraction. (Contributed by NM,
4-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | neg2sub 8046 |
Relationship between subtraction and negative. (Contributed by Paul
Chapman, 8-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | renegcl 8047 |
Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|
![( (](lp.gif) ![-u
-u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | renegcli 8048 |
Closure law for negative of reals. (Note: this inference proof style
and the deduction theorem usage in renegcl 8047 is deprecated, but is
retained for its demonstration value.) (Contributed by NM,
17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
![-u -u](shortminus.gif) ![RR RR](bbr.gif) |
|
Theorem | resubcli 8049 |
Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.)
(Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![B B](_cb.gif)
![RR RR](bbr.gif) |
|
Theorem | resubcl 8050 |
Closure law for subtraction of reals. (Contributed by NM,
20-Jan-1997.)
|
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![B B](_cb.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | negreb 8051 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | peano2cnm 8052 |
"Reverse" second Peano postulate analog for complex numbers: A
complex
number minus 1 is a complex number. (Contributed by Alexander van der
Vekens, 18-Mar-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | peano2rem 8053 |
"Reverse" second Peano postulate analog for reals. (Contributed by
NM,
6-Feb-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | negcli 8054 |
Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|
![-u -u](shortminus.gif) ![CC CC](bbc.gif) |
|
Theorem | negidi 8055 |
Addition of a number and its negative. (Contributed by NM,
26-Nov-1994.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![0 0](0.gif) |
|
Theorem | negnegi 8056 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by NM,
8-Feb-1995.) (Proof shortened by
Andrew Salmon, 22-Oct-2011.)
|
![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) |
|
Theorem | subidi 8057 |
Subtraction of a number from itself. (Contributed by NM,
26-Nov-1994.)
|
![( (](lp.gif) ![A A](_ca.gif)
![0 0](0.gif) |
|
Theorem | subid1i 8058 |
Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|
![( (](lp.gif) ![0 0](0.gif)
![A A](_ca.gif) |
|
Theorem | negne0bi 8059 |
A number is nonzero iff its negative is nonzero. (Contributed by NM,
10-Aug-1999.)
|
![( (](lp.gif) ![-u -u](shortminus.gif)
![0 0](0.gif) ![)
)](rp.gif) |
|
Theorem | negrebi 8060 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|
![( (](lp.gif) ![-u -u](shortminus.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | negne0i 8061 |
The negative of a nonzero number is nonzero. (Contributed by NM,
30-Jul-2004.)
|
![-u -u](shortminus.gif)
![0 0](0.gif) |
|
Theorem | subcli 8062 |
Closure law for subtraction. (Contributed by NM, 26-Nov-1994.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
![( (](lp.gif) ![B B](_cb.gif)
![CC CC](bbc.gif) |
|
Theorem | pncan3i 8063 |
Subtraction and addition of equals. (Contributed by NM,
26-Nov-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![B B](_cb.gif) |
|
Theorem | negsubi 8064 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by NM, 26-Nov-1994.) (Proof shortened by Andrew
Salmon, 22-Oct-2011.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subnegi 8065 |
Relationship between subtraction and negative. (Contributed by NM,
1-Dec-2005.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subeq0i 8066 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8-May-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | neg11i 8067 |
Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | negcon1i 8068 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | negcon2i 8069 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | negdii 8070 |
Distribution of negative over addition. (Contributed by NM,
28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | negsubdii 8071 |
Distribution of negative over subtraction. (Contributed by NM,
6-Aug-1999.)
|
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | negsubdi2i 8072 |
Distribution of negative over subtraction. (Contributed by NM,
1-Oct-1999.)
|
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | subaddi 8073 |
Relationship between subtraction and addition. (Contributed by NM,
26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | subadd2i 8074 |
Relationship between subtraction and addition. (Contributed by NM,
15-Dec-2006.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | subaddrii 8075 |
Relationship between subtraction and addition. (Contributed by NM,
16-Dec-2006.)
|
![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) |
|
Theorem | subsub23i 8076 |
Swap subtrahend and result of subtraction. (Contributed by NM,
7-Oct-1999.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | addsubassi 8077 |
Associative-type law for subtraction and addition. (Contributed by NM,
16-Sep-1999.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsubi 8078 |
Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subcani 8079 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | subcan2i 8080 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | pnncani 8081 |
Cancellation law for mixed addition and subtraction. (Contributed by
NM, 14-Jan-2006.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | addsub4i 8082 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 17-Oct-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 0reALT 8083 |
Alternate proof of 0re 7790. (Contributed by NM, 19-Feb-2005.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
![RR RR](bbr.gif) |
|
Theorem | negcld 8084 |
Closure law for negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | subidd 8085 |
Subtraction of a number from itself. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | subid1d 8086 |
Identity law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | negidd 8087 |
Addition of a number and its negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | negnegd 8088 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | negeq0d 8089 |
A number is zero iff its negative is zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negne0bd 8090 |
A number is nonzero iff its negative is nonzero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | negcon1d 8091 |
Contraposition law for unary minus. Deduction form of negcon1 8038.
(Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif)
![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | negcon1ad 8092 |
Contraposition law for unary minus. One-way deduction form of
negcon1 8038. (Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![B B](_cb.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | neg11ad 8093 |
The negatives of two complex numbers are equal iff they are equal.
Deduction form of neg11 8037. Generalization of neg11d 8109.
(Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negned 8094 |
If two complex numbers are unequal, so are their negatives.
Contrapositive of neg11d 8109. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | negne0d 8095 |
The negative of a nonzero number is nonzero. See also negap0d 8417 which
is similar but for apart from zero rather than not equal to zero.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | negrebd 8096 |
The negative of a real is real. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | subcld 8097 |
Closure law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | pncand 8098 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | pncan2d 8099 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | pncan3d 8100 |
Subtraction and addition of equals. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |