Theorem List for Intuitionistic Logic Explorer - 7901-8000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mul4 7901 |
Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|
|
|
Theorem | muladd11 7902 |
A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | 1p1times 7903 |
Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | peano2cn 7904 |
A theorem for complex numbers analogous the second Peano postulate
peano2 4509. (Contributed by NM, 17-Aug-2005.)
|
|
|
Theorem | peano2re 7905 |
A theorem for reals analogous the second Peano postulate peano2 4509.
(Contributed by NM, 5-Jul-2005.)
|
|
|
Theorem | addcom 7906 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
|
|
Theorem | addid1 7907 |
is an additive identity.
(Contributed by Jim Kingdon,
16-Jan-2020.)
|
|
|
Theorem | addid2 7908 |
is a left identity for
addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | readdcan 7909 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
|
|
Theorem | 00id 7910 |
is its own additive
identity. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | addid1i 7911 |
is an additive identity.
(Contributed by NM, 23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | addid2i 7912 |
is a left identity for
addition. (Contributed by NM,
3-Jan-2013.)
|
|
|
Theorem | addcomi 7913 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | addcomli 7914 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
|
|
Theorem | mul12i 7915 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew
Salmon, 19-Nov-2011.)
|
|
|
Theorem | mul32i 7916 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
|
|
Theorem | mul4i 7917 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
|
|
Theorem | addid1d 7918 |
is an additive identity.
(Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addid2d 7919 |
is a left identity for
addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addcomd 7920 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul12d 7921 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul32d 7922 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul31d 7923 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mul4d 7924 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | muladd11r 7925 |
A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|
|
|
Theorem | comraddd 7926 |
Commute RHS addition, in deduction form. (Contributed by David A.
Wheeler, 11-Oct-2018.)
|
|
|
4.3 Real and complex numbers - basic
operations
|
|
4.3.1 Addition
|
|
Theorem | add12 7927 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
|
|
Theorem | add32 7928 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
|
|
Theorem | add32r 7929 |
Commutative/associative law that swaps the last two terms in a triple sum,
rearranging the parentheses. (Contributed by Paul Chapman,
18-May-2007.)
|
|
|
Theorem | add4 7930 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | add42 7931 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
|
|
Theorem | add12i 7932 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | add32i 7933 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | add4i 7934 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
|
|
Theorem | add42i 7935 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
|
|
Theorem | add12d 7936 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | add32d 7937 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | add4d 7938 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | add42d 7939 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
4.3.2 Subtraction
|
|
Syntax | cmin 7940 |
Extend class notation to include subtraction.
|
|
|
Syntax | cneg 7941 |
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 7940 () to prevent syntax ambiguity. For example, looking at the
syntax definition co 5774, 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 7942* |
Define subtraction. Theorem subval 7961 shows its value (and describes how
this definition works), theorem subaddi 8056 relates it to addition, and
theorems subcli 8045 and resubcli 8032 prove its closure laws. (Contributed
by NM, 26-Nov-1994.)
|
|
|
Definition | df-neg 7943 |
Define the negative of a number (unary minus). We use different symbols
for unary minus () and subtraction () to prevent syntax
ambiguity. See cneg 7941 for a discussion of this. (Contributed by
NM,
10-Feb-1995.)
|
|
|
Theorem | cnegexlem1 7944 |
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 7947. (Contributed by Eric Schmidt, 22-May-2007.)
|
|
|
Theorem | cnegexlem2 7945 |
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 7947. (Contributed by Eric Schmidt,
22-May-2007.)
|
|
|
Theorem | cnegexlem3 7946* |
Existence of real number difference. Lemma for cnegex 7947. (Contributed
by Eric Schmidt, 22-May-2007.)
|
|
|
Theorem | cnegex 7947* |
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21-May-2007.)
|
|
|
Theorem | cnegex2 7948* |
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | addcan 7949 |
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 7950 |
Cancellation law for addition. (Contributed by NM, 30-Jul-2004.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | addcani 7951 |
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 7952 |
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 7953 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addcan2d 7954 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addcanad 7955 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 7953. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | addcan2ad 7956 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 7954. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | addneintrd 7957 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 7955. Consequence of addcand 7953.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | addneintr2d 7958 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 7956. Consequence of
addcan2d 7954. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | 0cnALT 7959 |
Alternate proof of 0cn 7765. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
|
Theorem | negeu 7960* |
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 7961* |
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 7962 |
Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|
|
|
Theorem | negeqi 7963 |
Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|
|
|
Theorem | negeqd 7964 |
Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|
|
|
Theorem | nfnegd 7965 |
Deduction version of nfneg 7966. (Contributed by NM, 29-Feb-2008.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | nfneg 7966 |
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 7967 |
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 7968 |
Closure law for subtraction. (Contributed by NM, 10-May-1999.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | negcl 7969 |
Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|
|
|
Theorem | negicn 7970 |
is a complex number
(common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
|
|
Theorem | subf 7971 |
Subtraction is an operation on the complex numbers. (Contributed by NM,
4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
|
|
Theorem | subadd 7972 |
Relationship between subtraction and addition. (Contributed by NM,
20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | subadd2 7973 |
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subsub23 7974 |
Swap subtrahend and result of subtraction. (Contributed by NM,
14-Dec-2007.)
|
|
|
Theorem | pncan 7975 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pncan2 7976 |
Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|
|
|
Theorem | pncan3 7977 |
Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|
|
|
Theorem | npcan 7978 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsubass 7979 |
Associative-type law for addition and subtraction. (Contributed by NM,
6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsub 7980 |
Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
|
|
Theorem | subadd23 7981 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 1-Feb-2007.)
|
|
|
Theorem | addsub12 7982 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 8-Feb-2005.)
|
|
|
Theorem | 2addsub 7983 |
Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|
|
|
Theorem | addsubeq4 7984 |
Relation between sums and differences. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
|
|
Theorem | pncan3oi 7985 |
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 8046 and pncan 7975, 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 8081. (Contributed by
David A. Wheeler, 11-Oct-2018.)
|
|
|
Theorem | mvrraddi 7986 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
|
|
Theorem | mvlladdi 7987 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
|
|
Theorem | subid 7988 |
Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.)
(Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subid1 7989 |
Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | npncan 7990 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | nppcan 7991 |
Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|
|
|
Theorem | nnpcan 7992 |
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 7993 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
|
|
Theorem | subcan2 7994 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | subeq0 7995 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16-Nov-1999.)
|
|
|
Theorem | npncan2 7996 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
21-Jun-2013.)
|
|
|
Theorem | subsub2 7997 |
Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nncan 7998 |
Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | subsub 7999 |
Law for double subtraction. (Contributed by NM, 13-May-2004.)
|
|
|
Theorem | nppcan2 8000 |
Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|
|