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	ressxr 8201	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 8202	The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( RR X. RR ) C_ ( RR* X. RR* )
Theorem	rexr 8203	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )
Theorem	0xr 8204	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- 0 e. RR*
Theorem	renepnf 8205	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( A e. RR -> A =/= +oo )
Theorem	renemnf 8206	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( A e. RR -> A =/= -oo )
Theorem	rexrd 8207	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. RR* )
Theorem	renepnfd 8208	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= +oo )
Theorem	renemnfd 8209	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= -oo )
Theorem	pnfxr 8210	Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
|- +oo e. RR*
Theorem	pnfex 8211	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- +oo e. _V
Theorem	pnfnemnf 8212	Plus and minus infinity are different elements of RR*. (Contributed by NM, 14-Oct-2005.)
|- +oo =/= -oo
Theorem	mnfnepnf 8213	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -oo =/= +oo
Theorem	mnfxr 8214	Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- -oo e. RR*
Theorem	rexri 8215	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	1xr 8216	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- 1 e. RR*
Theorem	renfdisj 8217	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( RR i^i { +oo , -oo } ) = (/)
Theorem	ltrelxr 8218	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 8219	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 8220	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 8221	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 8222	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
Theorem	ltxrlt 8223	The standard less-than <RR and the extended real less-than < are identical when restricted to the non-extended reals RR. (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A <RR B ) )
4.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axltirr 8224	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 8122 with ordering on the extended reals. New proofs should use ltnr 8234 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ( A e. RR -> -. A < A )
Theorem	axltwlin 8225	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 8123 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( A < C \/ C < B ) ) )
Theorem	axlttrn 8226	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 8124 with ordering on the extended reals. New proofs should use lttr 8231 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	axltadd 8227	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 8126 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( C + A ) < ( C + B ) ) )
Theorem	axapti 8228	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 8125 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ -. ( A < B \/ B < A ) ) -> A = B )
Theorem	axmulgt0 8229	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 8127 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) ) )
Theorem	axsuploc 8230*	An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 8131 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
4.2.4  Ordering on reals
Theorem	lttr 8231	Alias for axlttrn 8226, for naming consistency with lttri 8262. New proofs should generally use this instead of ax-pre-lttrn 8124. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 8232	The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )
Theorem	lenlt 8233	'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
Theorem	ltnr 8234	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	ltso 8235	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 8236	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri3 8237	Tightness of real apartness. (Contributed by NM, 5-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	letri3 8238	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	ltleletr 8239	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 8240	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 8241	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 8242	'Less than' implies not equal. See also ltap 8791 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 8243	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	eqlelt 8244	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 8245	'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 8246	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 8247	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 8248	'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 8249	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	ltnri 8250	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 8251	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 8252	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 8253	'Less than' implies not equal. See also gtapii 8792 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 8254	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri3i 8255	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 8256	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	ltnsymi 8257	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 8258	'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 8259	'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 8260	'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 8261	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	lttri 8262	'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 8263	'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 8264	'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 8265	'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 8266	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 8267	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 8268	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 8269	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 8270	'Less than' implies not equal. See also gtapd 8795 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 8271	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	lttri3d 8272	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 8273	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 8274	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 8275	'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 8276	'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 8277	'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 8278	'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 8279	'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 8280	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 8281	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 8282	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 8283	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 8284	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 8285	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 8286	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 8287	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 8288	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 8289	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 8290	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 8291	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 8292	A theorem for complex numbers analogous the second Peano postulate peano2 4687. (Contributed by NM, 17-Aug-2005.)
|- ( A e. CC -> ( A + 1 ) e. CC )
Theorem	peano2re 8293	A theorem for reals analogous the second Peano postulate peano2 4687. (Contributed by NM, 5-Jul-2005.)
|- ( A e. RR -> ( A + 1 ) e. RR )
Theorem	addcom 8294	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	addrid 8295	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Theorem	addlid 8296	0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( 0 + A ) = A )
Theorem	readdcan 8297	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 8298	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0 ) = 0
Theorem	addridi 8299	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 8300	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
|- A e. CC   =>    |- ( 0 + A ) = A