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
Axiom	ax-addf 9601	Addition is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see http://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific addcl 9604 should be used. Note that uses of ax-addf 9601 can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x + y ) ) in place of +, from which this axiom (with the defined operation in place of +) follows as a theorem. This axiom is justified by theorem axaddf 9552. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 9602	Multiplication is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see http://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific ax-mulcl 9584 should be used. Note that uses of ax-mulf 9602 can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x x. y ) ) in place of x., from which this axiom (with the defined operation in place of x.) follows as a theorem. This axiom is justified by theorem axmulf 9553. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- x. : ( CC X. CC ) --> CC
5.2  Derive the basic properties from the field axioms
5.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 9603	Alias for ax-cnex 9578. See also cnexALT 11261. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 9604	Alias for ax-addcl 9582, for naming consistency with addcli 9630. Use this theorem instead of ax-addcl 9582 or axaddcl 9558. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 9605	Alias for ax-addrcl 9583, for naming consistency with readdcli 9639. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 9606	Alias for ax-mulcl 9584, for naming consistency with mulcli 9631. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 9607	Alias for ax-mulrcl 9585, for naming consistency with remulcli 9640. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 9608	Alias for ax-mulcom 9586, for naming consistency with mulcomi 9632. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 9609	Alias for ax-addass 9587, for naming consistency with addassi 9634. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 9610	Alias for ax-mulass 9588, for naming consistency with mulassi 9635. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
Theorem	adddi 9611	Alias for ax-distr 9589, for naming consistency with adddii 9636. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
Theorem	recn 9612	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 9613	The real numbers form a set. See also reexALT 11259. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 9614	Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- RR e. { RR , CC }
Theorem	cnelprrecn 9615	Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- CC e. { RR , CC }
Theorem	elimne0 9616	Hypothesis for weak deduction theorem to eliminate A =/= 0. (Contributed by NM, 15-May-1999.)
|- if ( A =/= 0 , A , 1 ) =/= 0
Theorem	adddir 9617	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
Theorem	0cn 9618	0 is a complex number. See also 0cnALT 9845. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 9619	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )
Theorem	c0ex 9620	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 9621	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 9622*	Alias for ax-cnre 9595, for naming consistency. (Contributed by NM, 3-Jan-2013.)
|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
Theorem	mulid1 9623	1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( A x. 1 ) = A )
Theorem	mulid2 9624	Identity law for multiplication. Note: see mulid1 9623 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- ( A e. CC -> ( 1 x. A ) = A )
Theorem	1re 9625	1 is a real number. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 9580, by exploiting properties of the imaginary unit _i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 1 e. RR
Theorem	0re 9626	0 is a real number. See also 0reALT 9953. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 9627	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 0 e. RR )
Theorem	mulid1i 9628	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( A x. 1 ) = A
Theorem	mulid2i 9629	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( 1 x. A ) = A
Theorem	addcli 9630	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) e. CC
Theorem	mulcli 9631	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) e. CC
Theorem	mulcomi 9632	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) = ( B x. A )
Theorem	mulcomli 9633	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   &    |- ( A x. B ) = C   =>    |- ( B x. A ) = C
Theorem	addassi 9634	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A + B ) + C ) = ( A + ( B + C ) )
Theorem	mulassi 9635	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 9636	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 9637	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 9638	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>    |- A e. CC
Theorem	readdcli 9639	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A + B ) e. RR
Theorem	remulcli 9640	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 9641	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. RR )
Theorem	1cnd 9642	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. CC )
Theorem	mulid1d 9643	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 1 ) = A )
Theorem	mulid2d 9644	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	addcld 9645	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 9646	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 9647	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 9648	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 9649	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 9650	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 9651	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 9652	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. CC )
Theorem	readdcld 9653	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 9654	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 9655	Plus infinity.
class +oo
Syntax	cmnf 9656	Minus infinity.
class -oo
Syntax	cxr 9657	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 9658	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 9659	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 9660	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 9661). 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 9665, mnfnre 9666, and pnfnemnf 11379. 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 9661	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 9666 and pnfnemnf 11379). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 9662	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 9663*	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 9664	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 9702 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)
|- <_ = ( ( RR* X. RR* ) \ `' < )
Theorem	pnfnre 9665	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 9666	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR
Theorem	ressxr 9667	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 9668	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 9669	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )
Theorem	0xr 9670	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- 0 e. RR*
Theorem	renepnf 9671	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 9672	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 9673	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. RR* )
Theorem	renepnfd 9674	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= +oo )
Theorem	renemnfd 9675	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= -oo )
Theorem	rexri 9676	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	renfdisj 9677	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 9678	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 9679	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 9680	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 9681	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 9682	'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 9683	'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	xrnltled 9684	'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	ssxr 9685	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 9686	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 9687	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 9596 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 9688	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 9597 with ordering on the extended reals. New proofs should use lttr 9692 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 9689	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 9598 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 9690	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 9599 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 9691*	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 9600 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 9692	Alias for axlttrn 9688, for naming consistency with lttri 9742. New proofs should generally use this instead of ax-pre-lttrn 9597. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 9693	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 9694	'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 9695	'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 9696	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 9697	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri2 9698	Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
Theorem	lttri3 9699	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 9700	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 ) )