P. 76 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gtso 7501	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri3 7502	Tightness of real apartness. (Contributed by NM, 5-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	letri3 7503	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	ltleletr 7504	Transitive law, weaker form of ( A < B /\ B <_ C ) -> A < C. (Contributed by AV, 14-Oct-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A <_ C ) )
Theorem	letr 7505	Transitive law. (Contributed by NM, 12-Nov-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
Theorem	leid 7506	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 7507	'Less than' implies not equal. See also ltap 8042 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( ( A e. RR /\ A < B ) -> B =/= A )
Theorem	ltnsym 7508	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	ltle 7509	'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
Theorem	lelttr 7510	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
Theorem	ltletr 7511	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
Theorem	ltnsym2 7512	'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> -. ( A < B /\ B < A ) )
Theorem	eqle 7513	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	ltnri 7514	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 7515	Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|- A e. RR   =>    |- ( A = B -> A <_ B )
Theorem	eqlei2 7516	Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- A e. RR   =>    |- ( B = A -> B <_ A )
Theorem	gtneii 7517	'Less than' implies not equal. See also gtapii 8043 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 7518	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri3i 7519	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 7520	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	ltnsymi 7521	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 7522	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B <-> -. B < A )
Theorem	ltlei 7523	'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> A <_ B )
Theorem	ltleii 7524	'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- A < B   =>    |- A <_ B
Theorem	ltnei 7525	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	lttri 7526	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A < B /\ B < C ) -> A < C )
Theorem	lelttri 7527	'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B < C ) -> A < C )
Theorem	ltletri 7528	'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A < B /\ B <_ C ) -> A < C )
Theorem	letri 7529	'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B <_ C ) -> A <_ C )
Theorem	le2tri3i 7530	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 7531	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 7532	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 7533	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 7534	'Less than' implies not equal. See also gtapd 8046 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 7535	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	lttri3d 7536	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 7537	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	lenltd 7538	'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 7539	'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 7540	'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 7541	'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 7542	'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 7543	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 7544	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 7545	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 7546	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 7547	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
3.2.5  Initial properties of the complex numbers
Theorem	mul12 7548	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 7549	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 7550	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 7551	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 7552	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 7553	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 7554	A theorem for complex numbers analogous the second Peano postulate peano2 4382. (Contributed by NM, 17-Aug-2005.)
|- ( A e. CC -> ( A + 1 ) e. CC )
Theorem	peano2re 7555	A theorem for reals analogous the second Peano postulate peano2 4382. (Contributed by NM, 5-Jul-2005.)
|- ( A e. RR -> ( A + 1 ) e. RR )
Theorem	addcom 7556	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	addid1 7557	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Theorem	addid2 7558	0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( 0 + A ) = A )
Theorem	readdcan 7559	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 7560	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0 ) = 0
Theorem	addid1i 7561	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	addid2i 7562	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
|- A e. CC   =>    |- ( 0 + A ) = A
Theorem	addcomi 7563	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 7564	Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = C   =>    |- ( B + A ) = C
Theorem	mul12i 7565	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 7566	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 7567	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	addid1d 7568	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + 0 ) = A )
Theorem	addid2d 7569	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 + A ) = A )
Theorem	addcomd 7570	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 7571	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 7572	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 7573	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 7574	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 7575	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 7576	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 ) )
3.3  Real and complex numbers - basic operations
3.3.1  Addition
Theorem	add12 7577	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 7578	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 7579	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 7580	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 7581	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 7582	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 7583	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 7584	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 7585	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 7586	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 7587	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 7588	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 7589	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 ) ) )
3.3.2  Subtraction
Syntax	cmin 7590	Extend class notation to include subtraction.
class -
Syntax	cneg 7591	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 7590 ( -) to prevent syntax ambiguity. For example, looking at the syntax definition co 5607, 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 7592*	Define subtraction. Theorem subval 7611 shows its value (and describes how this definition works), theorem subaddi 7706 relates it to addition, and theorems subcli 7695 and resubcli 7682 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 7593	Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 7591 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
|- -u A = ( 0 - A )
Theorem	cnegexlem1 7594	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 7597. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( A e. RR /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
Theorem	cnegexlem2 7595	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 7597. (Contributed by Eric Schmidt, 22-May-2007.)
|- E. y e. RR ( _i x. y ) e. RR
Theorem	cnegexlem3 7596*	Existence of real number difference. Lemma for cnegex 7597. (Contributed by Eric Schmidt, 22-May-2007.)
|- ( ( b e. RR /\ y e. RR ) -> E. c e. RR ( b + c ) = y )
Theorem	cnegex 7597*	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 7598*	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 7599	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 7600	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 ) )