P. 83 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	le2tri3i 8201	Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B <_ C /\ C <_ A ) <-> ( A = B /\ B = C /\ C = A ) )
Theorem	mulgt0i 8202	The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) )
Theorem	mulgt0ii 8203	The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- 0 < ( A x. B )
Theorem	ltnrd 8204	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 8205	'Less than' implies not equal. See also gtapd 8730 which is the same but for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B =/= A )
Theorem	ltned 8206	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	lttri3d 8207	Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	letri3d 8208	Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	eqleltd 8209	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
Theorem	lenltd 8210	'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ B <-> -. B < A ) )
Theorem	ltled 8211	'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A <_ B )
Theorem	ltnsymd 8212	'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> -. B < A )
Theorem	nltled 8213	'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A <_ B )
Theorem	lensymd 8214	'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> -. B < A )
Theorem	mulgt0d 8215	The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A x. B ) )
Theorem	letrd 8216	Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A <_ C )
Theorem	lelttrd 8217	Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	lttrd 8218	Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	0lt1 8219	0 is less than 1. Theorem I.21 of [Apostol] p. 20. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 17-Jan-1997.)
|- 0 < 1
Theorem	ltntri 8220	Negative trichotomy property for real numbers. It is well known that we cannot prove real number trichotomy, A < B \/ A = B \/ B < A. Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no, as shown here. This is another example of distinguishing between being unable to prove something, or being able to refute it. (Contributed by Jim Kingdon, 13-Aug-2023.)
|- ( ( A e. RR /\ B e. RR ) -> -. ( -. A < B /\ -. A = B /\ -. B < A ) )
4.2.5  Initial properties of the complex numbers
Theorem	mul12 8221	Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
Theorem	mul32 8222	Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
Theorem	mul31 8223	Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( C x. B ) x. A ) )
Theorem	mul4 8224	Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) ) )
Theorem	muladd11 8225	A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( 1 + A ) + ( B + ( A x. B ) ) ) )
Theorem	1p1times 8226	Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
Theorem	peano2cn 8227	A theorem for complex numbers analogous the second Peano postulate peano2 4651. (Contributed by NM, 17-Aug-2005.)
|- ( A e. CC -> ( A + 1 ) e. CC )
Theorem	peano2re 8228	A theorem for reals analogous the second Peano postulate peano2 4651. (Contributed by NM, 5-Jul-2005.)
|- ( A e. RR -> ( A + 1 ) e. RR )
Theorem	addcom 8229	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	addrid 8230	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Theorem	addlid 8231	0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( 0 + A ) = A )
Theorem	readdcan 8232	Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) = ( C + B ) <-> A = B ) )
Theorem	00id 8233	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0 ) = 0
Theorem	addridi 8234	0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   =>    |- ( A + 0 ) = A
Theorem	addlidi 8235	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
|- A e. CC   =>    |- ( 0 + A ) = A
Theorem	addcomi 8236	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) = ( B + A )
Theorem	addcomli 8237	Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = C   =>    |- ( B + A ) = C
Theorem	mul12i 8238	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A x. ( B x. C ) ) = ( B x. ( A x. C ) )
Theorem	mul32i 8239	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A x. B ) x. C ) = ( ( A x. C ) x. B )
Theorem	mul4i 8240	Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) )
Theorem	addridd 8241	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + 0 ) = A )
Theorem	addlidd 8242	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 + A ) = A )
Theorem	addcomd 8243	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + B ) = ( B + A ) )
Theorem	mul12d 8244	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
Theorem	mul32d 8245	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
Theorem	mul31d 8246	Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) x. C ) = ( ( C x. B ) x. A ) )
Theorem	mul4d 8247	Rearrangement of 4 factors. (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 x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) ) )
Theorem	muladd11r 8248	A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + 1 ) x. ( B + 1 ) ) = ( ( ( A x. B ) + ( A + B ) ) + 1 ) )
Theorem	comraddd 8249	Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> A = ( C + B ) )
4.3  Real and complex numbers - basic operations
4.3.1  Addition
Theorem	add12 8250	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B + C ) ) = ( B + ( A + C ) ) )
Theorem	add32 8251	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( ( A + C ) + B ) )
Theorem	add32r 8252	Commutative/associative law that swaps the last two terms in a triple sum, rearranging the parentheses. (Contributed by Paul Chapman, 18-May-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B + C ) ) = ( ( A + C ) + B ) )
Theorem	add4 8253	Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) ) )
Theorem	add42 8254	Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) ) )
Theorem	add12i 8255	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A + ( B + C ) ) = ( B + ( A + C ) )
Theorem	add32i 8256	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 21-Jan-1997.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) + C ) = ( ( A + C ) + B )
Theorem	add4i 8257	Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) )
Theorem	add42i 8258	Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) )
Theorem	add12d 8259	Commutative/associative law that swaps the first 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 ) ) = ( B + ( A + C ) ) )
Theorem	add32d 8260	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 8261	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 8262	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 8263	Extend class notation to include subtraction.
class -
Syntax	cneg 8264	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 8263 ( -) to prevent syntax ambiguity. For example, looking at the syntax definition co 5957, 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 8265*	Define subtraction. Theorem subval 8284 shows its value (and describes how this definition works), Theorem subaddi 8379 relates it to addition, and Theorems subcli 8368 and resubcli 8355 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 8266	Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 8264 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
|- -u A = ( 0 - A )
Theorem	cnegexlem1 8267	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 8270. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( A e. RR /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	cnegexlem2 8268	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 8270. (Contributed by Eric Schmidt, 22-May-2007.)
|- E. y e. RR ( _i x. y ) e. RR
Theorem	cnegexlem3 8269*	Existence of real number difference. Lemma for cnegex 8270. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( b e. RR /\ y e. RR ) -> E. c e. RR ( b + c ) = y )
Theorem	cnegex 8270*	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 8271*	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 8272	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 8273	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 8274	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 8275	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 8276	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 8277	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 8278	Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8276. (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 8279	Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8277. (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 8280	Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8278. Consequence of addcand 8276. (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 8281	Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8279. Consequence of addcan2d 8277. (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 8282	Alternate proof of 0cn 8084. (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 8283*	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 8284*	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 8285	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|- ( A = B -> -u A = -u B )
Theorem	negeqi 8286	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|- A = B   =>    |- -u A = -u B
Theorem	negeqd 8287	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> -u A = -u B )
Theorem	nfnegd 8288	Deduction version of nfneg 8289. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x -u A )
Theorem	nfneg 8289	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 8290	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 8291	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 8292	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|- ( A e. CC -> -u A e. CC )
Theorem	negicn 8293	-u _i is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
|- -u _i e. CC
Theorem	subf 8294	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 8295	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 8296	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 8297	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 8298	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 8299	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )
Theorem	pncan3 8300	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )