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	subnegi 8501	Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.)
|- A e. CC   &    |- B e. CC   =>    |- ( A - -u B ) = ( A + B )
Theorem	subeq0i 8502	If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( ( A - B ) = 0 <-> A = B )
Theorem	neg11i 8503	Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A = -u B <-> A = B )
Theorem	negcon1i 8504	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A = B <-> -u B = A )
Theorem	negcon2i 8505	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( A = -u B <-> B = -u A )
Theorem	negdii 8506	Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. CC   &    |- B e. CC   =>    |- -u ( A + B ) = ( -u A + -u B )
Theorem	negsubdii 8507	Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.)
|- A e. CC   &    |- B e. CC   =>    |- -u ( A - B ) = ( -u A + B )
Theorem	negsubdi2i 8508	Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- -u ( A - B ) = ( B - A )
Theorem	subaddi 8509	Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( B + C ) = A )
Theorem	subadd2i 8510	Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( C + B ) = A )
Theorem	subaddrii 8511	Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- ( B + C ) = A   =>    |- ( A - B ) = C
Theorem	subsub23i 8512	Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = C <-> ( A - C ) = B )
Theorem	addsubassi 8513	Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - C ) = ( A + ( B - C ) )
Theorem	addsubi 8514	Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - C ) = ( ( A - C ) + B )
Theorem	subcani 8515	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) = ( A - C ) <-> B = C )
Theorem	subcan2i 8516	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	pnncani 8517	Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) - ( A - C ) ) = ( B + C )
Theorem	addsub4i 8518	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) )
Theorem	0reALT 8519	Alternate proof of 0re 8222. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- 0 e. RR
Theorem	negcld 8520	Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> -u A e. CC )
Theorem	subidd 8521	Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A - A ) = 0 )
Theorem	subid1d 8522	Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A - 0 ) = A )
Theorem	negidd 8523	Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + -u A ) = 0 )
Theorem	negnegd 8524	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> -u -u A = A )
Theorem	negeq0d 8525	A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A = 0 <-> -u A = 0 ) )
Theorem	negne0bd 8526	A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A =/= 0 <-> -u A =/= 0 ) )
Theorem	negcon1d 8527	Contraposition law for unary minus. Deduction form of negcon1 8474. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A = B <-> -u B = A ) )
Theorem	negcon1ad 8528	Contraposition law for unary minus. One-way deduction form of negcon1 8474. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> -u A = B )   =>    |- ( ph -> -u B = A )
Theorem	neg11ad 8529	The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 8473. Generalization of neg11d 8545. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A = -u B <-> A = B ) )
Theorem	negned 8530	If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 8545. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> -u A =/= -u B )
Theorem	negne0d 8531	The negative of a nonzero number is nonzero. See also negap0d 8854 which is similar but for apart from zero rather than not equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> -u A =/= 0 )
Theorem	negrebd 8532	The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> -u A e. RR )   =>    |- ( ph -> A e. RR )
Theorem	subcld 8533	Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - B ) e. CC )
Theorem	pncand 8534	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + B ) - B ) = A )
Theorem	pncan2d 8535	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + B ) - A ) = B )
Theorem	pncan3d 8536	Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + ( B - A ) ) = B )
Theorem	npcand 8537	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A - B ) + B ) = A )
Theorem	nncand 8538	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - ( A - B ) ) = B )
Theorem	negsubd 8539	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + -u B ) = ( A - B ) )
Theorem	subnegd 8540	Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A - -u B ) = ( A + B ) )
Theorem	subeq0d 8541	If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A - B ) = 0 )   =>    |- ( ph -> A = B )
Theorem	subne0d 8542	Two unequal numbers have nonzero difference. See also subap0d 8867 which is the same thing for apartness rather than negated equality. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A - B ) =/= 0 )
Theorem	subeq0ad 8543	The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 8448. Generalization of subeq0d 8541. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A - B ) = 0 <-> A = B ) )
Theorem	subne0ad 8544	If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 8542. Contrapositive of subeq0bd 8601. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A - B ) =/= 0 )   =>    |- ( ph -> A =/= B )
Theorem	neg11d 8545	If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> -u A = -u B )   =>    |- ( ph -> A = B )
Theorem	negdid 8546	Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A + B ) = ( -u A + -u B ) )
Theorem	negdi2d 8547	Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A + B ) = ( -u A - B ) )
Theorem	negsubdid 8548	Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( -u A + B ) )
Theorem	negsubdi2d 8549	Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( B - A ) )
Theorem	neg2subd 8550	Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A - -u B ) = ( B - A ) )
Theorem	subaddd 8551	Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( B + C ) = A ) )
Theorem	subadd2d 8552	Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( C + B ) = A ) )
Theorem	addsubassd 8553	Associative-type law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )
Theorem	addsubd 8554	Law for subtraction and addition. (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	subadd23d 8555	Commutative/associative law for addition and subtraction. (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	addsub12d 8556	Commutative/associative law for addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A + ( B - C ) ) = ( B + ( A - C ) ) )
Theorem	npncand 8557	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )
Theorem	nppcand 8558	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( ( A - B ) + C ) + B ) = ( A + C ) )
Theorem	nppcan2d 8559	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )
Theorem	nppcan3d 8560	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) + ( C + B ) ) = ( A + C ) )
Theorem	subsubd 8561	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A - ( B - C ) ) = ( ( A - B ) + C ) )
Theorem	subsub2d 8562	Law for double subtraction. (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	subsub3d 8563	Law for double subtraction. (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	subsub4d 8564	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) - C ) = ( A - ( B + C ) ) )
Theorem	sub32d 8565	Swap the second and third terms in a double subtraction. (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	nnncand 8566	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - ( B - C ) ) - C ) = ( A - B ) )
Theorem	nnncan1d 8567	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) - ( A - C ) ) = ( C - B ) )
Theorem	nnncan2d 8568	Cancellation law for subtraction. (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	npncan3d 8569	Cancellation law for subtraction. (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	pnpcand 8570	Cancellation law for mixed addition and subtraction. (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	pnpcan2d 8571	Cancellation law for mixed addition and subtraction. (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	pnncand 8572	Cancellation law for mixed addition and subtraction. (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	ppncand 8573	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) + ( C - B ) ) = ( A + C ) )
Theorem	subcand 8574	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A - B ) = ( A - C ) )   =>    |- ( ph -> B = C )
Theorem	subcan2d 8575	Cancellation law for subtraction. (Contributed by Mario Carneiro, 22-Sep-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( A - C ) = ( B - C ) )   =>    |- ( ph -> A = B )
Theorem	subcanad 8576	Cancellation law for subtraction. Deduction form of subcan 8477. Generalization of subcand 8574. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = ( A - C ) <-> B = C ) )
Theorem	subneintrd 8577	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcand 8574. (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	subcan2ad 8578	Cancellation law for subtraction. Deduction form of subcan2 8447. Generalization of subcan2d 8575. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - C ) = ( B - C ) <-> A = B ) )
Theorem	subneintr2d 8579	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 8575. (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	addsub4d 8580	Rearrangement of 4 terms in a mixed addition and subtraction. (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	subadd4d 8581	Rearrangement of 4 terms in a mixed addition and subtraction. (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 + D ) - ( B + C ) ) )
Theorem	sub4d 8582	Rearrangement of 4 terms in a subtraction. (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	2addsubd 8583	Law for subtraction and addition. (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 ) )
Theorem	addsubeq4d 8584	Relation between sums and differences. (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 ) <-> ( C - A ) = ( B - D ) ) )
Theorem	subeqxfrd 8585	Transfer two terms of a subtraction in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( A - B ) = ( C - D ) )   =>    |- ( ph -> ( A - C ) = ( B - D ) )
Theorem	mvlraddd 8586	Move LHS right addition to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A + B ) = C )   =>    |- ( ph -> A = ( C - B ) )
Theorem	mvlladdd 8587	Move LHS left addition to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A + B ) = C )   =>    |- ( ph -> B = ( C - A ) )
Theorem	mvrraddd 8588	Move RHS right addition to LHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> ( A - C ) = B )
Theorem	mvrladdd 8589	Move RHS left addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> ( A - B ) = C )
Theorem	assraddsubd 8590	Associate RHS addition-subtraction. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> A = ( ( B + C ) - D ) )   =>    |- ( ph -> A = ( B + ( C - D ) ) )
Theorem	subaddeqd 8591	Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( A + B ) = ( C + D ) )   =>    |- ( ph -> ( A - D ) = ( C - B ) )
Theorem	addlsub 8592	Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )
Theorem	addrsub 8593	Right-subtraction: Subtraction of the right summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) = C <-> B = ( C - A ) ) )
Theorem	subexsub 8594	A subtraction law: Exchanging the subtrahend and the result of the subtraction. (Contributed by BJ, 6-Jun-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )
Theorem	addid0 8595	If adding a number to a another number yields the other number, the added number must be 0. This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
|- ( ( X e. CC /\ Y e. CC ) -> ( ( X + Y ) = X <-> Y = 0 ) )
Theorem	addn0nid 8596	Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021.)
|- ( ( X e. CC /\ Y e. CC /\ Y =/= 0 ) -> ( X + Y ) =/= X )
Theorem	pnpncand 8597	Addition/subtraction cancellation law. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + ( B - C ) ) + ( C - B ) ) = A )
Theorem	subeqrev 8598	Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) = ( C - D ) <-> ( B - A ) = ( D - C ) ) )
Theorem	pncan1 8599	Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( A e. CC -> ( ( A + 1 ) - 1 ) = A )
Theorem	npcan1 8600	Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.)
|- ( A e. CC -> ( ( A - 1 ) + 1 ) = A )