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	cnegexlem1 8501	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 8504. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( A e. RR /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	cnegexlem2 8502	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 8504. (Contributed by Eric Schmidt, 22-May-2007.)
|- E. y e. RR ( _i x. y ) e. RR
Theorem	cnegexlem3 8503*	Existence of real number difference. Lemma for cnegex 8504. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( b e. RR /\ y e. RR ) -> E. c e. RR ( b + c ) = y )
Theorem	cnegex 8504*	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 8505*	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 8506	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 8507	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 8508	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 8509	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 8510	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 8511	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 8512	Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8510. (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 8513	Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8511. (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 8514	Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8512. Consequence of addcand 8510. (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 8515	Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8513. Consequence of addcan2d 8511. (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 8516	Alternate proof of 0cn 8318. (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 8517*	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 8518*	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 8519	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|- ( A = B -> -u A = -u B )
Theorem	negeqi 8520	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|- A = B   =>    |- -u A = -u B
Theorem	negeqd 8521	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> -u A = -u B )
Theorem	nfnegd 8522	Deduction version of nfneg 8523. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x -u A )
Theorem	nfneg 8523	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 8524	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 8525	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 8526	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|- ( A e. CC -> -u A e. CC )
Theorem	negicn 8527	-u _i is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- -u _i e. CC
Theorem	subf 8528	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 8529	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 8530	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 8531	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 8532	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 8533	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )
Theorem	pncan3 8534	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )
Theorem	npcan 8535	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 8536	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 8537	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 8538	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 8539	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 8540	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 8541	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 8542	Subtraction and addition of equals. Almost but not exactly the same as pncan3i 8603 and pncan 8532, 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 8638. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A + B ) - B ) = A
Theorem	mvrraddi 8543	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 8544	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 8545	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 8546	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 8547	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 8548	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 8549	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 8550	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 8551	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 8552	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 8553	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + ( B - A ) ) = 0 )
Theorem	subsub2 8554	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 8555	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 8556	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 8557	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 8558	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 8559	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 8560	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 8561	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 8562	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 8563	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 8564	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 8565	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 8566	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 8567	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 8568	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 8569	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 8570	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 8571	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 8572	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|- -u 0 = 0
Theorem	negid 8573	Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.)
|- ( A e. CC -> ( A + -u A ) = 0 )
Theorem	negsub 8574	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 8575	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 8576	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 8577	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 8578	Negative contraposition law. (Contributed by NM, 9-May-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = B <-> -u B = A ) )
Theorem	negcon2 8579	Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( A = -u B <-> B = -u A ) )
Theorem	negeq0 8580	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 8581	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 8582	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 8583	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 8584	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 8585	Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.)
|- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
Theorem	neg2sub 8586	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 8587	Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|- ( A e. RR -> -u A e. RR )
Theorem	renegcli 8588	Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 8587 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 8589	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 8590	Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
Theorem	negreb 8591	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 8592	"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 8593	"Reverse" second Peano postulate analog for reals. (Contributed by NM, 6-Feb-2007.)
|- ( N e. RR -> ( N - 1 ) e. RR )
Theorem	negcli 8594	Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   =>    |- -u A e. CC
Theorem	negidi 8595	Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   =>    |- ( A + -u A ) = 0
Theorem	negnegi 8596	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.)
|- A e. CC   =>    |- -u -u A = A
Theorem	subidi 8597	Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   =>    |- ( A - A ) = 0
Theorem	subid1i 8598	Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A - 0 ) = A
Theorem	negne0bi 8599	A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.)
|- A e. CC   =>    |- ( A =/= 0 <-> -u A =/= 0 )
Theorem	negrebi 8600	The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|- A e. CC   =>    |- ( -u A e. RR <-> A e. RR )