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	letri3 9701	Trichotomy law. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	leloe 9702	'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
Theorem	eqlelt 9703	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
Theorem	ltle 9704	'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	leltne 9705	'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( A < B <-> B =/= A ) )
Theorem	lelttr 9706	Transitive law. (Contributed by NM, 23-May-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
Theorem	ltletr 9707	Transitive law. (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
Theorem	ltleletr 9708	Transitive law, weaker form of ltletr 9707. (Contributed by AV, 14-Oct-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A <_ C ) )
Theorem	letr 9709	Transitive law. (Contributed by NM, 12-Nov-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
Theorem	ltnr 9710	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	leid 9711	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 9712	'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( ( A e. RR /\ A < B ) -> B =/= A )
Theorem	ltneOLD 9713	'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B =/= A )
Theorem	ltnsym 9714	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	ltnsym2 9715	'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 9716	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 9717	'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 9718	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	eqled 9719	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> A <_ B )
Theorem	ltadd2 9720	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 9721	A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> 0 < A ) )
Theorem	lecasei 9722	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 9723	Trichotomy law. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B < A ) )
Theorem	ltlecasei 9724	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 9725	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 9726	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 9727	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 9728	'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 9729	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri2i 9730	Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A =/= B <-> ( A < B \/ B < A ) )
Theorem	lttri3i 9731	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 9732	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	leloei 9733	'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 9734	'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 9735	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 9736	'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 9737	'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 9738	'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 9739	'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 9740	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	letrii 9741	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 9742	'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 9743	'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 9744	'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 9745	'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 9746	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 9747	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 9748	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 9747 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 9749	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 9750	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 9751	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 9752	'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B =/= A )
Theorem	ltned 9753	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	ne0gt0d 9754	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 9755	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 9756	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 9757	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 9758	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 9759	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 9760	'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 9761	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 9762	'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 9763	'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 9764	'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 9765	'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 9766	'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 9767	'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 9768	'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	letrid 9769	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 9770	'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 9771	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 9772	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 9773	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 9774	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 9775	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 9776	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 9777	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 9778*	The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 9600 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 9779*	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 9780	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 9781	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 9782	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 9783	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 9784	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 9785	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 9786	A theorem for complex numbers analogous the second Peano postulate peano2nn 10588. (Contributed by NM, 17-Aug-2005.)
|- ( A e. CC -> ( A + 1 ) e. CC )
Theorem	peano2re 9787	A theorem for reals analogous the second Peano postulate peano2nn 10588. (Contributed by NM, 5-Jul-2005.)
|- ( A e. RR -> ( A + 1 ) e. RR )
Theorem	readdcan 9788	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 9789	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0 ) = 0
Theorem	mul02lem1 9790	Lemma for mul02 9792. 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 9791	Lemma for mul02 9792. Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. RR -> ( 0 x. A ) = 0 )
Theorem	mul02 9792	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 9793	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 9794	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 9795*	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 9796*	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 9797	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 9798	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 9799	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 9800	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 ) )