P. 86 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8501-8600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	add32d 8501	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) + C ) = ( ( A + C ) + B ) )
Theorem	add4d 8502	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) ) )
Theorem	add42d 8503	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) ) )
4.3.2  Subtraction
Syntax	cmin 8504	Extend class notation to include subtraction.
class -
Syntax	cneg 8505	Extend class notation to include unary minus. The symbol -u 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 ( -u) and subtraction cmin 8504 ( -) to prevent syntax ambiguity. For example, looking at the syntax definition co 6088, if we used the same symbol then " ( - A - B ) " could mean either " - A " minus " B", or it could represent the (meaningless) operation of classes " - " and " - B " connected with "operation" " A". On the other hand, " ( -u A - B ) " is unambiguous.
class -u A
Definition	df-sub 8506*	Define subtraction. Theorem subval 8525 shows its value (and describes how this definition works), Theorem subaddi 8620 relates it to addition, and Theorems subcli 8609 and resubcli 8596 prove its closure laws. (Contributed by NM, 26-Nov-1994.)
|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
Definition	df-neg 8507	Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 8505 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
|- -u A = ( 0 - A )
Theorem	cnegexlem1 8508	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 8511. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( A e. RR /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	cnegexlem2 8509	Existence of a real number which produces a real number when multiplied by _i. (Hint: zero is such a number, although we don't need to prove that yet). Lemma for cnegex 8511. (Contributed by Eric Schmidt, 22-May-2007.)
|- E. y e. RR ( _i x. y ) e. RR
Theorem	cnegexlem3 8510*	Existence of real number difference. Lemma for cnegex 8511. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( b e. RR /\ y e. RR ) -> E. c e. RR ( b + c ) = y )
Theorem	cnegex 8511*	Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. CC -> E. x e. CC ( A + x ) = 0 )
Theorem	cnegex2 8512*	Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> E. x e. CC ( x + A ) = 0 )
Theorem	addcan 8513	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.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	addcan2 8514	Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) = ( B + C ) <-> A = B ) )
Theorem	addcani 8515	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) = ( A + C ) <-> B = C )
Theorem	addcan2i 8516	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 14-May-2003.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + C ) = ( B + C ) <-> A = B )
Theorem	addcand 8517	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	addcan2d 8518	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + C ) = ( B + C ) <-> A = B ) )
Theorem	addcanad 8519	Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8517. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A + B ) = ( A + C ) )   =>    |- ( ph -> B = C )
Theorem	addcan2ad 8520	Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8518. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A + C ) = ( B + C ) )   =>    |- ( ph -> A = B )
Theorem	addneintrd 8521	Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8519. Consequence of addcand 8517. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( A + B ) =/= ( A + C ) )
Theorem	addneintr2d 8522	Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8520. Consequence of addcan2d 8518. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A + C ) =/= ( B + C ) )
Theorem	0cnALT 8523	Alternate proof of 0cn 8324. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- 0 e. CC
Theorem	negeu 8524*	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.)
|- ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( A + x ) = B )
Theorem	subval 8525*	Value of subtraction, which is the (unique) element x such that B + x = A. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 2-Nov-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
Theorem	negeq 8526	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|- ( A = B -> -u A = -u B )
Theorem	negeqi 8527	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|- A = B   =>    |- -u A = -u B
Theorem	negeqd 8528	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> -u A = -u B )
Theorem	nfnegd 8529	Deduction version of nfneg 8530. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x -u A )
Theorem	nfneg 8530	Bound-variable hypothesis builder for the negative of a complex number. (Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   =>    |- F/_ x -u A
Theorem	csbnegg 8531	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.)
|- ( A e. V -> [_ A / x ]_ -u B = -u [_ A / x ]_ B )
Theorem	subcl 8532	Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
Theorem	negcl 8533	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|- ( A e. CC -> -u A e. CC )
Theorem	negicn 8534	-u _i is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- -u _i e. CC
Theorem	subf 8535	Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- - : ( CC X. CC ) --> CC
Theorem	subadd 8536	Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( B + C ) = A ) )
Theorem	subadd2 8537	Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( C + B ) = A ) )
Theorem	subsub23 8538	Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( A - C ) = B ) )
Theorem	pncan 8539	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )
Theorem	pncan2 8540	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )
Theorem	pncan3 8541	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )
Theorem	npcan 8542	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + B ) = A )
Theorem	addsubass 8543	Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )
Theorem	addsub 8544	Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) )
Theorem	subadd23 8545	Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + C ) = ( A + ( C - B ) ) )
Theorem	addsub12 8546	Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B - C ) ) = ( B + ( A - C ) ) )
Theorem	2addsub 8547	Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) + C ) - D ) = ( ( ( A + C ) - D ) + B ) )
Theorem	addsubeq4 8548	Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) = ( C + D ) <-> ( C - A ) = ( B - D ) ) )
Theorem	pncan3oi 8549	Subtraction and addition of equals. Almost but not exactly the same as pncan3i 8610 and pncan 8539, 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 8645. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A + B ) - B ) = A
Theorem	mvrraddi 8550	Move RHS right addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- B e. CC   &    |- C e. CC   &    |- A = ( B + C )   =>    |- ( A - C ) = B
Theorem	mvlladdi 8551	Move LHS left addition to RHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = C   =>    |- B = ( C - A )
Theorem	subid 8552	Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A - A ) = 0 )
Theorem	subid1 8553	Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A - 0 ) = A )
Theorem	npncan 8554	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )
Theorem	nppcan 8555	Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) + B ) = ( A + C ) )
Theorem	nnpcan 8556	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.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) - C ) + B ) = ( A - C ) )
Theorem	nppcan3 8557	Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C + B ) ) = ( A + C ) )
Theorem	subcan2 8558	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) = ( B - C ) <-> A = B ) )
Theorem	subeq0 8559	If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) = 0 <-> A = B ) )
Theorem	npncan2 8560	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + ( B - A ) ) = 0 )
Theorem	subsub2 8561	Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( A + ( C - B ) ) )
Theorem	nncan 8562	Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - ( A - B ) ) = B )
Theorem	subsub 8563	Law for double subtraction. (Contributed by NM, 13-May-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( ( A - B ) + C ) )
Theorem	nppcan2 8564	Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )
Theorem	subsub3 8565	Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( ( A + C ) - B ) )
Theorem	subsub4 8566	Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - C ) = ( A - ( B + C ) ) )
Theorem	sub32 8567	Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - C ) = ( ( A - C ) - B ) )
Theorem	nnncan 8568	Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B - C ) ) - C ) = ( A - B ) )
Theorem	nnncan1 8569	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - ( A - C ) ) = ( C - B ) )
Theorem	nnncan2 8570	Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) - ( B - C ) ) = ( A - B ) )
Theorem	npncan3 8571	Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C - A ) ) = ( C - B ) )
Theorem	pnpcan 8572	Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A + C ) ) = ( B - C ) )
Theorem	pnpcan2 8573	Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) - ( B + C ) ) = ( A - B ) )
Theorem	pnncan 8574	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A - C ) ) = ( B + C ) )
Theorem	ppncan 8575	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + ( C - B ) ) = ( A + C ) )
Theorem	addsub4 8576	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) ) )
Theorem	subadd4 8577	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A + D ) - ( B + C ) ) )
Theorem	sub4 8578	Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A - C ) - ( B - D ) ) )
Theorem	neg0 8579	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|- -u 0 = 0
Theorem	negid 8580	Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.)
|- ( A e. CC -> ( A + -u A ) = 0 )
Theorem	negsub 8581	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.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
Theorem	subneg 8582	Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( A - -u B ) = ( A + B ) )
Theorem	negneg 8583	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.)
|- ( A e. CC -> -u -u A = A )
Theorem	neg11 8584	Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = -u B <-> A = B ) )
Theorem	negcon1 8585	Negative contraposition law. (Contributed by NM, 9-May-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = B <-> -u B = A ) )
Theorem	negcon2 8586	Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( A = -u B <-> B = -u A ) )
Theorem	negeq0 8587	A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A = 0 <-> -u A = 0 ) )
Theorem	subcan 8588	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = ( A - C ) <-> B = C ) )
Theorem	negsubdi 8589	Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( -u A + B ) )
Theorem	negdi 8590	Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A + -u B ) )
Theorem	negdi2 8591	Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A - B ) )
Theorem	negsubdi2 8592	Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
Theorem	neg2sub 8593	Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A - -u B ) = ( B - A ) )
Theorem	renegcl 8594	Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|- ( A e. RR -> -u A e. RR )
Theorem	renegcli 8595	Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 8594 is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A e. RR   =>    |- -u A e. RR
Theorem	resubcli 8596	Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. RR   &    |- B e. RR   =>    |- ( A - B ) e. RR
Theorem	resubcl 8597	Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
Theorem	negreb 8598	The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
|- ( A e. CC -> ( -u A e. RR <-> A e. RR ) )
Theorem	peano2cnm 8599	"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.)
|- ( N e. CC -> ( N - 1 ) e. CC )
Theorem	peano2rem 8600	"Reverse" second Peano postulate analog for reals. (Contributed by NM, 6-Feb-2007.)
|- ( N e. RR -> ( N - 1 ) e. RR )