Theorem List for Intuitionistic Logic Explorer - 7901-8000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
4.3.2 Subtraction
|
|
Syntax | cmin 7901 |
Extend class notation to include subtraction.
|
|
|
Syntax | cneg 7902 |
Extend class notation to include unary minus. The symbol is not a
class by itself but part of a compound class definition. We do this
rather than making it a formal function since it is so commonly used.
Note: We use different symbols for unary minus () and subtraction
cmin 7901 () to prevent syntax ambiguity. For example, looking at the
syntax definition co 5742, if we used the same symbol
then " " could
mean either "
" minus
"", or
it could represent the (meaningless) operation of
classes "
" and "
" connected with
"operation" "".
On the other hand, "
" is unambiguous.
|
|
|
Definition | df-sub 7903* |
Define subtraction. Theorem subval 7922 shows its value (and describes how
this definition works), theorem subaddi 8017 relates it to addition, and
theorems subcli 8006 and resubcli 7993 prove its closure laws. (Contributed
by NM, 26-Nov-1994.)
|
|
|
Definition | df-neg 7904 |
Define the negative of a number (unary minus). We use different symbols
for unary minus () and subtraction () to prevent syntax
ambiguity. See cneg 7902 for a discussion of this. (Contributed by
NM,
10-Feb-1995.)
|
|
|
Theorem | cnegexlem1 7905 |
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 7908. (Contributed by Eric Schmidt, 22-May-2007.)
|
|
|
Theorem | cnegexlem2 7906 |
Existence of a real number which produces a real number when multiplied
by . (Hint:
zero is such a number, although we don't need to
prove that yet). Lemma for cnegex 7908. (Contributed by Eric Schmidt,
22-May-2007.)
|
|
|
Theorem | cnegexlem3 7907* |
Existence of real number difference. Lemma for cnegex 7908. (Contributed
by Eric Schmidt, 22-May-2007.)
|
|
|
Theorem | cnegex 7908* |
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21-May-2007.)
|
|
|
Theorem | cnegex2 7909* |
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | addcan 7910 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addcan2 7911 |
Cancellation law for addition. (Contributed by NM, 30-Jul-2004.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | addcani 7912 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | addcan2i 7913 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 14-May-2003.) (Revised by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | addcand 7914 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addcan2d 7915 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addcanad 7916 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 7914. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | addcan2ad 7917 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 7915. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | addneintrd 7918 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 7916. Consequence of addcand 7914.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | addneintr2d 7919 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 7917. Consequence of
addcan2d 7915. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | 0cnALT 7920 |
Alternate proof of 0cn 7726. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | negeu 7921* |
Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subval 7922* |
Value of subtraction, which is the (unique) element such that
.
(Contributed by NM, 4-Aug-2007.) (Revised by Mario
Carneiro, 2-Nov-2013.)
|
|
|
Theorem | negeq 7923 |
Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|
|
|
Theorem | negeqi 7924 |
Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|
|
|
Theorem | negeqd 7925 |
Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|
|
|
Theorem | nfnegd 7926 |
Deduction version of nfneg 7927. (Contributed by NM, 29-Feb-2008.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | nfneg 7927 |
Bound-variable hypothesis builder for the negative of a complex number.
(Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
|
|
Theorem | csbnegg 7928 |
Move class substitution in and out of the negative of a number.
(Contributed by NM, 1-Mar-2008.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
|
|
Theorem | subcl 7929 |
Closure law for subtraction. (Contributed by NM, 10-May-1999.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | negcl 7930 |
Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|
|
|
Theorem | negicn 7931 |
is a complex number
(common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
|
|
Theorem | subf 7932 |
Subtraction is an operation on the complex numbers. (Contributed by NM,
4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
|
|
Theorem | subadd 7933 |
Relationship between subtraction and addition. (Contributed by NM,
20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | subadd2 7934 |
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subsub23 7935 |
Swap subtrahend and result of subtraction. (Contributed by NM,
14-Dec-2007.)
|
|
|
Theorem | pncan 7936 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pncan2 7937 |
Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|
|
|
Theorem | pncan3 7938 |
Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|
|
|
Theorem | npcan 7939 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsubass 7940 |
Associative-type law for addition and subtraction. (Contributed by NM,
6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsub 7941 |
Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | subadd23 7942 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 1-Feb-2007.)
|
|
|
Theorem | addsub12 7943 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 8-Feb-2005.)
|
|
|
Theorem | 2addsub 7944 |
Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|
|
|
Theorem | addsubeq4 7945 |
Relation between sums and differences. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
|
|
Theorem | pncan3oi 7946 |
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 8007 and pncan 7936, 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 8042. (Contributed by
David A. Wheeler, 11-Oct-2018.)
|
|
|
Theorem | mvrraddi 7947 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
|
|
Theorem | mvlladdi 7948 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
|
|
Theorem | subid 7949 |
Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subid1 7950 |
Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | npncan 7951 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | nppcan 7952 |
Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|
|
|
Theorem | nnpcan 7953 |
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.)
|
|
|
Theorem | nppcan3 7954 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
|
|
Theorem | subcan2 7955 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | subeq0 7956 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16-Nov-1999.)
|
|
|
Theorem | npncan2 7957 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
21-Jun-2013.)
|
|
|
Theorem | subsub2 7958 |
Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nncan 7959 |
Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | subsub 7960 |
Law for double subtraction. (Contributed by NM, 13-May-2004.)
|
|
|
Theorem | nppcan2 7961 |
Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|
|
|
Theorem | subsub3 7962 |
Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | subsub4 7963 |
Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | sub32 7964 |
Swap the second and third terms in a double subtraction. (Contributed by
NM, 19-Aug-2005.)
|
|
|
Theorem | nnncan 7965 |
Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|
|
|
Theorem | nnncan1 7966 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | nnncan2 7967 |
Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
|
|
|
Theorem | npncan3 7968 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pnpcan 7969 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pnpcan2 7970 |
Cancellation law for mixed addition and subtraction. (Contributed by
Scott Fenton, 9-Jun-2006.)
|
|
|
Theorem | pnncan 7971 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ppncan 7972 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.)
|
|
|
Theorem | addsub4 7973 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 4-Mar-2005.)
|
|
|
Theorem | subadd4 7974 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 24-Aug-2006.)
|
|
|
Theorem | sub4 7975 |
Rearrangement of 4 terms in a subtraction. (Contributed by NM,
23-Nov-2007.)
|
|
|
Theorem | neg0 7976 |
Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|
|
|
Theorem | negid 7977 |
Addition of a number and its negative. (Contributed by NM,
14-Mar-2005.)
|
|
|
Theorem | negsub 7978 |
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.)
|
|
|
Theorem | subneg 7979 |
Relationship between subtraction and negative. (Contributed by NM,
10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negneg 7980 |
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.)
|
|
|
Theorem | neg11 7981 |
Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negcon1 7982 |
Negative contraposition law. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | negcon2 7983 |
Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|
|
|
Theorem | negeq0 7984 |
A number is zero iff its negative is zero. (Contributed by NM,
12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subcan 7985 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negsubdi 7986 |
Distribution of negative over subtraction. (Contributed by NM,
15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negdi 7987 |
Distribution of negative over addition. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negdi2 7988 |
Distribution of negative over addition. (Contributed by NM,
1-Jan-2006.)
|
|
|
Theorem | negsubdi2 7989 |
Distribution of negative over subtraction. (Contributed by NM,
4-Oct-1999.)
|
|
|
Theorem | neg2sub 7990 |
Relationship between subtraction and negative. (Contributed by Paul
Chapman, 8-Oct-2007.)
|
|
|
Theorem | renegcl 7991 |
Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|
|
|
Theorem | renegcli 7992 |
Closure law for negative of reals. (Note: this inference proof style
and the deduction theorem usage in renegcl 7991 is deprecated, but is
retained for its demonstration value.) (Contributed by NM,
17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | resubcli 7993 |
Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | resubcl 7994 |
Closure law for subtraction of reals. (Contributed by NM,
20-Jan-1997.)
|
|
|
Theorem | negreb 7995 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
|
|
Theorem | peano2cnm 7996 |
"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.)
|
|
|
Theorem | peano2rem 7997 |
"Reverse" second Peano postulate analog for reals. (Contributed by
NM,
6-Feb-2007.)
|
|
|
Theorem | negcli 7998 |
Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|
|
|
Theorem | negidi 7999 |
Addition of a number and its negative. (Contributed by NM,
26-Nov-1994.)
|
|
|
Theorem | negnegi 8000 |
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.)
|
|