P. 97 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9601-9700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulassi 9601	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A x. B ) x. C ) = ( A x. ( B x. C ) )
Theorem	adddii 9602	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) )
Theorem	adddiri 9603	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) )
Theorem	recni 9604	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>    |- A e. CC
Theorem	readdcli 9605	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A + B ) e. RR
Theorem	remulcli 9606	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A x. B ) e. RR
Theorem	1red 9607	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. RR )
Theorem	1cnd 9608	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. CC )
Theorem	mulid1d 9609	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 1 ) = A )
Theorem	mulid2d 9610	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	addcld 9611	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + B ) e. CC )
Theorem	mulcld 9612	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A x. B ) e. CC )
Theorem	mulcomd 9613	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A x. B ) = ( B x. A ) )
Theorem	addassd 9614	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulassd 9615	Associative law for multiplication. (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. ( B x. C ) ) )
Theorem	adddid 9616	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
Theorem	adddird 9617	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
Theorem	recnd 9618	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. CC )
Theorem	readdcld 9619	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A + B ) e. RR )
Theorem	remulcld 9620	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A x. B ) e. RR )
5.2.2  Infinity and the extended real number system
Syntax	cpnf 9621	Plus infinity.
class +oo
Syntax	cmnf 9622	Minus infinity.
class -oo
Syntax	cxr 9623	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 9624	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 9625	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 9626	Define plus infinity. Note that the definition is arbitrary, requiring only that +oo be a set not in RR and different from -oo (df-mnf 9627). We use ~P U. CC to make it independent of the construction of CC, and Cantor's Theorem will show that it is different from any member of CC and therefore RR. See pnfnre 9631, mnfnre 9632, and pnfnemnf 11322. A simpler possibility is to define +oo as CC and -oo as { CC }, but that approach requires the Axiom of Regularity to show that +oo and -oo are different from each other and from all members of RR. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- +oo = ~P U. CC
Definition	df-mnf 9627	Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -oo be a set not in RR and different from +oo (see mnfnre 9632 and pnfnemnf 11322). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 9628	Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.)
|- RR* = ( RR u. { +oo , -oo } )
Definition	df-ltxr 9629*	Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, <RR is primitive and not necessarily a relation on RR. (Contributed by NM, 13-Oct-2005.)
|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
Definition	df-le 9630	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9667 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)
|- <_ = ( ( RR* X. RR* ) \ `' < )
Theorem	pnfnre 9631	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 9632	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR
Theorem	ressxr 9633	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 9634	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 9635	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )
Theorem	0xr 9636	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- 0 e. RR*
Theorem	renepnf 9637	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 9638	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 9639	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. RR* )
Theorem	renepnfd 9640	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= +oo )
Theorem	renemnfd 9641	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= -oo )
Theorem	rexri 9642	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	renfdisj 9643	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 9644	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 9645	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 9646	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 9647	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 9648	'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	xrltnle 9649	'Less than' expressed in terms of 'less than or equal to', for extended reals. (Contributed by NM, 6-Feb-2007.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )
Theorem	ssxr 9650	The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( A C_ RR* -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) )
Theorem	ltxrlt 9651	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 ) )
5.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axlttri 9652	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-lttri 9562 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. ( A = B \/ B < A ) ) )
Theorem	axlttrn 9653	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 9563 with ordering on the extended reals. New proofs should use lttr 9657 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 9654	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd 9564 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	axmulgt0 9655	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 9565 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	axsup 9656*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup 9566 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
5.2.4  Ordering on reals
Theorem	lttr 9657	Alias for axlttrn 9653, for naming consistency with lttri 9706. New proofs should generally use this instead of ax-pre-lttrn 9563. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 9658	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 9659	'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
Theorem	ltnle 9660	'Less than' expressed 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	ltso 9661	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 9662	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri2 9663	Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
Theorem	lttri3 9664	Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	lttri4 9665	Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B \/ A = B \/ B < A ) )
Theorem	letri3 9666	Trichotomy law. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	leloe 9667	'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 9668	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 9669	'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 9670	'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 9671	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 9672	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 9673	Transitive law, weaker form of ltletr 9672. (Contributed by AV, 14-Oct-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A <_ C ) )
Theorem	letr 9674	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 9675	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	leid 9676	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 9677	'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 9678	'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 9679	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	ltnsym2 9680	'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 9681	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 9682	'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 9683	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	ltadd2 9684	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 9685	A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A =/= 0 <-> 0 < A ) )
Theorem	lecasei 9686	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 9687	Trichotomy law. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B < A ) )
Theorem	ltlecasei 9688	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 9689	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 9690	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 9691	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 9692	'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 9693	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri2i 9694	Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A =/= B <-> ( A < B \/ B < A ) )
Theorem	lttri3i 9695	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 9696	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	leloei 9697	'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 9698	'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 9699	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 9700	'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 )