Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  mvrraddi 7228 
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11Oct2018.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  sub32 7245 
Swap the second and third terms in a double subtraction. (Contributed by
NM, 19Aug2005.)



Theorem  nnncan 7246 
Cancellation law for subtraction. (Contributed by NM, 4Sep2005.)



Theorem  nnncan1 7247 
Cancellation law for subtraction. (Contributed by NM, 8Feb2005.)
(Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  nnncan2 7248 
Cancellation law for subtraction. (Contributed by NM, 1Oct2005.)



Theorem  npncan3 7249 
Cancellation law for subtraction. (Contributed by Scott Fenton,
23Jun2013.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  pnpcan 7250 
Cancellation law for mixed addition and subtraction. (Contributed by NM,
4Mar2005.) (Revised by Mario Carneiro, 27May2016.)



Theorem  pnpcan2 7251 
Cancellation law for mixed addition and subtraction. (Contributed by
Scott Fenton, 9Jun2006.)



Theorem  pnncan 7252 
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30Jun2005.) (Revised by Mario Carneiro, 27May2016.)



Theorem  ppncan 7253 
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30Jun2005.)



Theorem  addsub4 7254 
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 4Mar2005.)



Theorem  subadd4 7255 
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 24Aug2006.)



Theorem  sub4 7256 
Rearrangement of 4 terms in a subtraction. (Contributed by NM,
23Nov2007.)



Theorem  neg0 7257 
Minus 0 equals 0. (Contributed by NM, 17Jan1997.)



Theorem  negid 7258 
Addition of a number and its negative. (Contributed by NM,
14Mar2005.)



Theorem  negsub 7259 
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by NM, 21Jan1997.) (Proof shortened by Mario
Carneiro, 27May2016.)



Theorem  subneg 7260 
Relationship between subtraction and negative. (Contributed by NM,
10May2004.) (Revised by Mario Carneiro, 27May2016.)



Theorem  negneg 7261 
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by NM,
12Jan2002.) (Revised by Mario
Carneiro, 27May2016.)



Theorem  neg11 7262 
Negative is onetoone. (Contributed by NM, 8Feb2005.) (Revised by
Mario Carneiro, 27May2016.)



Theorem  negcon1 7263 
Negative contraposition law. (Contributed by NM, 9May2004.)



Theorem  negcon2 7264 
Negative contraposition law. (Contributed by NM, 14Nov2004.)



Theorem  negeq0 7265 
A number is zero iff its negative is zero. (Contributed by NM,
12Jul2005.) (Revised by Mario Carneiro, 27May2016.)



Theorem  subcan 7266 
Cancellation law for subtraction. (Contributed by NM, 8Feb2005.)
(Revised by Mario Carneiro, 27May2016.)



Theorem  negsubdi 7267 
Distribution of negative over subtraction. (Contributed by NM,
15Nov2004.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  negdi 7268 
Distribution of negative over addition. (Contributed by NM, 10May2004.)
(Proof shortened by Mario Carneiro, 27May2016.)



Theorem  negdi2 7269 
Distribution of negative over addition. (Contributed by NM,
1Jan2006.)



Theorem  negsubdi2 7270 
Distribution of negative over subtraction. (Contributed by NM,
4Oct1999.)



Theorem  neg2sub 7271 
Relationship between subtraction and negative. (Contributed by Paul
Chapman, 8Oct2007.)



Theorem  renegcl 7272 
Closure law for negative of reals. (Contributed by NM, 20Jan1997.)



Theorem  renegcli 7273 
Closure law for negative of reals. (Note: this inference proof style
and the deduction theorem usage in renegcl 7272 is deprecated, but is
retained for its demonstration value.) (Contributed by NM,
17Jan1997.) (Proof shortened by Andrew Salmon, 22Oct2011.)



Theorem  resubcli 7274 
Closure law for subtraction of reals. (Contributed by NM, 17Jan1997.)
(Revised by Mario Carneiro, 27May2016.)



Theorem  resubcl 7275 
Closure law for subtraction of reals. (Contributed by NM,
20Jan1997.)



Theorem  negreb 7276 
The negative of a real is real. (Contributed by NM, 11Aug1999.)
(Revised by Mario Carneiro, 14Jul2014.)



Theorem  peano2cnm 7277 
"Reverse" second Peano postulate analog for complex numbers: A
complex
number minus 1 is a complex number. (Contributed by Alexander van der
Vekens, 18Mar2018.)



Theorem  peano2rem 7278 
"Reverse" second Peano postulate analog for reals. (Contributed by
NM,
6Feb2007.)



Theorem  negcli 7279 
Closure law for negative. (Contributed by NM, 26Nov1994.)



Theorem  negidi 7280 
Addition of a number and its negative. (Contributed by NM,
26Nov1994.)



Theorem  negnegi 7281 
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by NM,
8Feb1995.) (Proof shortened by
Andrew Salmon, 22Oct2011.)



Theorem  subidi 7282 
Subtraction of a number from itself. (Contributed by NM,
26Nov1994.)



Theorem  subid1i 7283 
Identity law for subtraction. (Contributed by NM, 29May1999.)



Theorem  negne0bi 7284 
A number is nonzero iff its negative is nonzero. (Contributed by NM,
10Aug1999.)



Theorem  negrebi 7285 
The negative of a real is real. (Contributed by NM, 11Aug1999.)



Theorem  negne0i 7286 
The negative of a nonzero number is nonzero. (Contributed by NM,
30Jul2004.)



Theorem  subcli 7287 
Closure law for subtraction. (Contributed by NM, 26Nov1994.)
(Revised by Mario Carneiro, 21Dec2013.)



Theorem  pncan3i 7288 
Subtraction and addition of equals. (Contributed by NM,
26Nov1994.)



Theorem  negsubi 7289 
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by NM, 26Nov1994.) (Proof shortened by Andrew
Salmon, 22Oct2011.)



Theorem  subnegi 7290 
Relationship between subtraction and negative. (Contributed by NM,
1Dec2005.)



Theorem  subeq0i 7291 
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8May1999.)



Theorem  neg11i 7292 
Negative is onetoone. (Contributed by NM, 1Aug1999.)



Theorem  negcon1i 7293 
Negative contraposition law. (Contributed by NM, 25Aug1999.)



Theorem  negcon2i 7294 
Negative contraposition law. (Contributed by NM, 25Aug1999.)



Theorem  negdii 7295 
Distribution of negative over addition. (Contributed by NM,
28Jul1999.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  negsubdii 7296 
Distribution of negative over subtraction. (Contributed by NM,
6Aug1999.)



Theorem  negsubdi2i 7297 
Distribution of negative over subtraction. (Contributed by NM,
1Oct1999.)



Theorem  subaddi 7298 
Relationship between subtraction and addition. (Contributed by NM,
26Nov1994.) (Revised by Mario Carneiro, 21Dec2013.)



Theorem  subadd2i 7299 
Relationship between subtraction and addition. (Contributed by NM,
15Dec2006.)



Theorem  subaddrii 7300 
Relationship between subtraction and addition. (Contributed by NM,
16Dec2006.)

