P. 98 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltnsym2 9701	'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	letric 9702	Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B <_ A ) )
Theorem	ltlen 9703	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )
Theorem	eqle 9704	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	ltadd2 9705	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C + A ) < ( C + B ) ) )
Theorem	ne0gt0 9706	A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> 0 < A ) )
Theorem	lecasei 9707	Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ( ph /\ A <_ B ) -> ps )   &    |- ( ( ph /\ B <_ A ) -> ps )   =>    |- ( ph -> ps )
Theorem	lelttric 9708	Trichotomy law. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B < A ) )
Theorem	ltlecasei 9709	Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ph /\ A < B ) -> ps )   &    |- ( ( ph /\ B <_ A ) -> ps )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ps )
Theorem	ltnri 9710	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 9711	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 9712	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 9713	'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 9714	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri2i 9715	Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A =/= B <-> ( A < B \/ B < A ) )
Theorem	lttri3i 9716	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 9717	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	leloei 9718	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B <-> ( A < B \/ A = B ) )
Theorem	ltleni 9719	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B <-> ( A <_ B /\ B =/= A ) )
Theorem	ltnsymi 9720	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 9721	'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	ltnlei 9722	'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B <-> -. B <_ A )
Theorem	ltlei 9723	'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 9724	'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 9725	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	letrii 9726	Trichotomy law for 'less than or equal to'. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B \/ B <_ A )
Theorem	lttri 9727	'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 9728	'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 9729	'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 9730	'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 9731	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	ltadd2i 9732	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( C + A ) < ( C + B ) )
Theorem	ltadd2iOLD 9733	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Paul Chapman, 27-Jan-2008.) Obsolete version of ltadd2i 9732 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( C + A ) < ( C + B ) )
Theorem	mulgt0i 9734	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 9735	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 9736	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 9737	'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B =/= A )
Theorem	ltned 9738	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	ne0gt0d 9739	A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> 0 < A )
Theorem	lttrid 9740	Ordering on reals satisfies strict trichotomy. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> -. ( A = B \/ B < A ) ) )
Theorem	lttri2d 9741	Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A =/= B <-> ( A < B \/ B < A ) ) )
Theorem	lttri3d 9742	Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	lttri4d 9743	Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B \/ A = B \/ B < A ) )
Theorem	letri3d 9744	Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	leloed 9745	'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 <-> ( A < B \/ A = B ) ) )
Theorem	eqleltd 9746	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	ltlend 9747	'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )
Theorem	lenltd 9748	'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	ltnled 9749	'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> -. B <_ A ) )
Theorem	ltled 9750	'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 9751	'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	letrid 9752	Trichotomy law for 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ B \/ B <_ A ) )
Theorem	leltned 9753	'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A < B <-> B =/= A ) )
Theorem	mulgt0d 9754	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	ltadd2d 9755	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( C + A ) < ( C + B ) ) )
Theorem	letrd 9756	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 9757	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	ltadd2dd 9758	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( C + A ) < ( C + B ) )
Theorem	ltletrd 9759	Transitive law deduction for 'less than', 'less than or equal to'. (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	lttrd 9760	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	dedekind 9761*	The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 9587 with appropriate adjustments, states that, if A completely preceeds B, then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013.)
|- ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
Theorem	dedekindle 9762*	The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013.)
|- ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x <_ y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
5.2.5  Initial properties of the complex numbers
Theorem	mul12 9763	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 9764	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 9765	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 9766	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 9767	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 9768	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 9769	A theorem for complex numbers analogous the second Peano postulate peano2nn 10568. (Contributed by NM, 17-Aug-2005.)
|- ( A e. CC -> ( A + 1 ) e. CC )
Theorem	peano2re 9770	A theorem for reals analogous the second Peano postulate peano2nn 10568. (Contributed by NM, 5-Jul-2005.)
|- ( A e. RR -> ( A + 1 ) e. RR )
Theorem	readdcan 9771	Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) = ( C + B ) <-> A = B ) )
Theorem	00id 9772	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0 ) = 0
Theorem	mul02lem1 9773	Lemma for mul02 9775. If any real does not produce 0 when multiplied by 0, then any complex is equal to double itself. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ B e. CC ) -> B = ( B + B ) )
Theorem	mul02lem2 9774	Lemma for mul02 9775. Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. RR -> ( 0 x. A ) = 0 )
Theorem	mul02 9775	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. Based on ideas by Eric Schmidt. (Contributed by NM, 10-Aug-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( 0 x. A ) = 0 )
Theorem	mul01 9776	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( A x. 0 ) = 0 )
Theorem	addid1 9777	0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( A + 0 ) = A )
Theorem	cnegex 9778*	Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> E. x e. CC ( A + x ) = 0 )
Theorem	cnegex2 9779*	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	addid2 9780	0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( 0 + A ) = A )
Theorem	addcan 9781	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 9782	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	addcom 9783	Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	addid1i 9784	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 9785	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
|- A e. CC   =>    |- ( 0 + A ) = A
Theorem	mul02i 9786	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   =>    |- ( 0 x. A ) = 0
Theorem	mul01i 9787	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   =>    |- ( A x. 0 ) = 0
Theorem	addcomi 9788	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 9789	Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = C   =>    |- ( B + A ) = C
Theorem	addcani 9790	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 9791	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	mul12i 9792	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 9793	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 9794	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	mul02d 9795	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 x. A ) = 0 )
Theorem	mul01d 9796	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 0 ) = 0 )
Theorem	addid1d 9797	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + 0 ) = A )
Theorem	addid2d 9798	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 + A ) = A )
Theorem	addcomd 9799	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	addcand 9800	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 ) )