Type  Label  Description 
Statement 

Theorem  mul31 6901 
Commutative/associative law. (Contributed by Scott Fenton,
3Jan2013.)



Theorem  mul4 6902 
Rearrangement of 4 factors. (Contributed by NM, 8Oct1999.)



Theorem  muladd11 6903 
A simple product of sums expansion. (Contributed by NM, 21Feb2005.)



Theorem  1p1times 6904 
Two times a number. (Contributed by NM, 18May1999.) (Revised by Mario
Carneiro, 27May2016.)



Theorem  peano2cn 6905 
A theorem for complex numbers analogous the second Peano postulate
peano2 4261. (Contributed by NM, 17Aug2005.)



Theorem  peano2re 6906 
A theorem for reals analogous the second Peano postulate peano2 4261.
(Contributed by NM, 5Jul2005.)



Theorem  addcom 6907 
Addition commutes. (Contributed by Jim Kingdon, 17Jan2020.)



Theorem  addid1 6908 
is an additive identity.
(Contributed by Jim Kingdon,
16Jan2020.)



Theorem  addid2 6909 
is a left identity for
addition. (Contributed by Scott Fenton,
3Jan2013.)



Theorem  readdcan 6910 
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3Jan2013.)



Theorem  00id 6911 
is its own additive
identity. (Contributed by Scott Fenton,
3Jan2013.)



Theorem  addid1i 6912 
is an additive identity.
(Contributed by NM, 23Nov1994.)
(Revised by Scott Fenton, 3Jan2013.)



Theorem  addid2i 6913 
is a left identity for
addition. (Contributed by NM,
3Jan2013.)



Theorem  addcomi 6914 
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3Jan2013.)



Theorem  addcomli 6915 
Addition commutes. (Contributed by Mario Carneiro, 19Apr2015.)



Theorem  mul12i 6916 
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM, 11May1999.) (Proof shortened by Andrew
Salmon, 19Nov2011.)



Theorem  mul32i 6917 
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11May1999.)



Theorem  mul4i 6918 
Rearrangement of 4 factors. (Contributed by NM, 16Feb1995.)



Theorem  addid1d 6919 
is an additive identity.
(Contributed by Mario Carneiro,
27May2016.)



Theorem  addid2d 6920 
is a left identity for
addition. (Contributed by Mario Carneiro,
27May2016.)



Theorem  addcomd 6921 
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3Jan2013.) (Revised by Mario Carneiro, 27May2016.)



Theorem  mul12d 6922 
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27May2016.)



Theorem  mul32d 6923 
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27May2016.)



Theorem  mul31d 6924 
Commutative/associative law. (Contributed by Mario Carneiro,
27May2016.)



Theorem  mul4d 6925 
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27May2016.)



3.3 Real and complex numbers  basic
operations


3.3.1 Addition


Theorem  add12 6926 
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11May2004.)



Theorem  add32 6927 
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 13Nov1999.)



Theorem  add32r 6928 
Commutative/associative law that swaps the last two terms in a triple sum,
rearranging the parentheses. (Contributed by Paul Chapman,
18May2007.)



Theorem  add4 6929 
Rearrangement of 4 terms in a sum. (Contributed by NM, 13Nov1999.)
(Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  add42 6930 
Rearrangement of 4 terms in a sum. (Contributed by NM, 12May2005.)



Theorem  add12i 6931 
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21Jan1997.)



Theorem  add32i 6932 
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21Jan1997.)



Theorem  add4i 6933 
Rearrangement of 4 terms in a sum. (Contributed by NM, 9May1999.)



Theorem  add42i 6934 
Rearrangement of 4 terms in a sum. (Contributed by NM, 22Aug1999.)



Theorem  add12d 6935 
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27May2016.)



Theorem  add32d 6936 
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27May2016.)



Theorem  add4d 6937 
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27May2016.)



Theorem  add42d 6938 
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27May2016.)



3.3.2 Subtraction


Syntax  cmin 6939 
Extend class notation to include subtraction.



Syntax  cneg 6940 
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 6939 () to prevent syntax ambiguity. For example, looking at the
syntax definition co 5455, 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  dfsub 6941* 
Define subtraction. Theorem subval 6960 shows its value (and describes how
this definition works), theorem subaddi 7054 relates it to addition, and
theorems subcli 7043 and resubcli 7030 prove its closure laws. (Contributed
by NM, 26Nov1994.)



Definition  dfneg 6942 
Define the negative of a number (unary minus). We use different symbols
for unary minus () and subtraction () to prevent syntax
ambiguity. See cneg 6940 for a discussion of this. (Contributed by
NM,
10Feb1995.)



Theorem  cnegexlem1 6943 
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 6946. (Contributed by Eric Schmidt, 22May2007.)



Theorem  cnegexlem2 6944 
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 6946. (Contributed by Eric Schmidt,
22May2007.)



Theorem  cnegexlem3 6945* 
Existence of real number difference. Lemma for cnegex 6946. (Contributed
by Eric Schmidt, 22May2007.)



Theorem  cnegex 6946* 
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21May2007.)



Theorem  cnegex2 6947* 
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3Jan2013.)



Theorem  addcan 6948 
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 22Nov1994.) (Proof shortened by Mario Carneiro,
27May2016.)



Theorem  addcan2 6949 
Cancellation law for addition. (Contributed by NM, 30Jul2004.)
(Revised by Scott Fenton, 3Jan2013.)



Theorem  addcani 6950 
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 27Oct1999.) (Revised by Scott Fenton,
3Jan2013.)



Theorem  addcan2i 6951 
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 14May2003.) (Revised by Scott Fenton,
3Jan2013.)



Theorem  addcand 6952 
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  addcan2d 6953 
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  addcanad 6954 
Cancelling a term on the lefthand side of a sum in an equality.
Consequence of addcand 6952. (Contributed by David Moews,
28Feb2017.)



Theorem  addcan2ad 6955 
Cancelling a term on the righthand side of a sum in an equality.
Consequence of addcan2d 6953. (Contributed by David Moews,
28Feb2017.)



Theorem  addneintrd 6956 
Introducing a term on the lefthand side of a sum in a negated
equality. Contrapositive of addcanad 6954. Consequence of addcand 6952.
(Contributed by David Moews, 28Feb2017.)



Theorem  addneintr2d 6957 
Introducing a term on the righthand side of a sum in a negated
equality. Contrapositive of addcan2ad 6955. Consequence of
addcan2d 6953. (Contributed by David Moews, 28Feb2017.)



Theorem  0cnALT 6958 
Alternate proof of 0cn 6777. (Contributed by NM, 19Feb2005.) (Revised
by
Mario Carneiro, 27May2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  negeu 6959* 
Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.
(Contributed by NM, 22Nov1994.) (Proof shortened by Mario Carneiro,
27May2016.)



Theorem  subval 6960* 
Value of subtraction, which is the (unique) element such that
. (Contributed by NM, 4Aug2007.) (Revised by Mario
Carneiro, 2Nov2013.)



Theorem  negeq 6961 
Equality theorem for negatives. (Contributed by NM, 10Feb1995.)



Theorem  negeqi 6962 
Equality inference for negatives. (Contributed by NM, 14Feb1995.)



Theorem  negeqd 6963 
Equality deduction for negatives. (Contributed by NM, 14May1999.)



Theorem  nfnegd 6964 
Deduction version of nfneg 6965. (Contributed by NM, 29Feb2008.)
(Revised by Mario Carneiro, 15Oct2016.)



Theorem  nfneg 6965 
Boundvariable hypothesis builder for the negative of a complex number.
(Contributed by NM, 12Jun2005.) (Revised by Mario Carneiro,
15Oct2016.)



Theorem  csbnegg 6966 
Move class substitution in and out of the negative of a number.
(Contributed by NM, 1Mar2008.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  subcl 6967 
Closure law for subtraction. (Contributed by NM, 10May1999.)
(Revised by Mario Carneiro, 21Dec2013.)



Theorem  negcl 6968 
Closure law for negative. (Contributed by NM, 6Aug2003.)



Theorem  negicn 6969 
is a complex number
(common case). (Contributed by David A.
Wheeler, 7Dec2018.)



Theorem  subf 6970 
Subtraction is an operation on the complex numbers. (Contributed by NM,
4Aug2007.) (Revised by Mario Carneiro, 16Nov2013.)



Theorem  subadd 6971 
Relationship between subtraction and addition. (Contributed by NM,
20Jan1997.) (Revised by Mario Carneiro, 21Dec2013.)



Theorem  subadd2 6972 
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5Jul2013.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  subsub23 6973 
Swap subtrahend and result of subtraction. (Contributed by NM,
14Dec2007.)



Theorem  pncan 6974 
Cancellation law for subtraction. (Contributed by NM, 10May2004.)
(Revised by Mario Carneiro, 27May2016.)



Theorem  pncan2 6975 
Cancellation law for subtraction. (Contributed by NM, 17Apr2005.)



Theorem  pncan3 6976 
Subtraction and addition of equals. (Contributed by NM, 14Mar2005.)



Theorem  npcan 6977 
Cancellation law for subtraction. (Contributed by NM, 10May2004.)
(Revised by Mario Carneiro, 27May2016.)



Theorem  addsubass 6978 
Associativetype law for addition and subtraction. (Contributed by NM,
6Aug2003.) (Revised by Mario Carneiro, 27May2016.)



Theorem  addsub 6979 
Law for addition and subtraction. (Contributed by NM, 19Aug2001.)
(Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  subadd23 6980 
Commutative/associative law for addition and subtraction. (Contributed by
NM, 1Feb2007.)



Theorem  addsub12 6981 
Commutative/associative law for addition and subtraction. (Contributed by
NM, 8Feb2005.)



Theorem  2addsub 6982 
Law for subtraction and addition. (Contributed by NM, 20Nov2005.)



Theorem  addsubeq4 6983 
Relation between sums and differences. (Contributed by Jeff Madsen,
17Jun2010.)



Theorem  pncan3oi 6984 
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 7044 and pncan 6974, 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 7079. (Contributed by
David A. Wheeler, 11Oct2018.)



Theorem  mvlladdi 6985 
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11Oct2018.)



Theorem  subid 6986 
Subtraction of a number from itself. (Contributed by NM, 8Oct1999.)
(Revised by Mario Carneiro, 27May2016.)



Theorem  subid1 6987 
Identity law for subtraction. (Contributed by NM, 9May2004.) (Revised
by Mario Carneiro, 27May2016.)



Theorem  npncan 6988 
Cancellation law for subtraction. (Contributed by NM, 8Feb2005.)



Theorem  nppcan 6989 
Cancellation law for subtraction. (Contributed by NM, 1Sep2005.)



Theorem  nnpcan 6990 
Cancellation law for subtraction: ((ab)c)+b = ac holds for complex
numbers a,b,c. (Contributed by Alexander van der Vekens, 24Mar2018.)



Theorem  nppcan3 6991 
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14Sep2015.)



Theorem  subcan2 6992 
Cancellation law for subtraction. (Contributed by NM, 8Feb2005.)



Theorem  subeq0 6993 
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16Nov1999.)



Theorem  npncan2 6994 
Cancellation law for subtraction. (Contributed by Scott Fenton,
21Jun2013.)



Theorem  subsub2 6995 
Law for double subtraction. (Contributed by NM, 30Jun2005.) (Revised
by Mario Carneiro, 27May2016.)



Theorem  nncan 6996 
Cancellation law for subtraction. (Contributed by NM, 21Jun2005.)
(Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  subsub 6997 
Law for double subtraction. (Contributed by NM, 13May2004.)



Theorem  nppcan2 6998 
Cancellation law for subtraction. (Contributed by NM, 29Sep2005.)



Theorem  subsub3 6999 
Law for double subtraction. (Contributed by NM, 27Jul2005.)



Theorem  subsub4 7000 
Law for double subtraction. (Contributed by NM, 19Aug2005.) (Revised
by Mario Carneiro, 27May2016.)

