P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	readdcld 8101	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 8102	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 )
4.2.2  Infinity and the extended real number system
Syntax	cpnf 8103	Plus infinity.
class +oo
Syntax	cmnf 8104	Minus infinity.
class -oo
Syntax	cxr 8105	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 8106	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 8107	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 8108	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 8109). 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 8113 and mnfnre 8114, and we'll also be able to prove +oo =/= -oo. 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 8109	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 8114). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 8110	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 8111*	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 8112	Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
|- <_ = ( ( RR* X. RR* ) \ `' < )
Theorem	pnfnre 8113	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 8114	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR
Theorem	ressxr 8115	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 8116	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 8117	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )
Theorem	0xr 8118	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- 0 e. RR*
Theorem	renepnf 8119	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 8120	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 8121	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. RR* )
Theorem	renepnfd 8122	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= +oo )
Theorem	renemnfd 8123	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= -oo )
Theorem	pnfxr 8124	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 8125	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- +oo e. _V
Theorem	pnfnemnf 8126	Plus and minus infinity are different elements of RR*. (Contributed by NM, 14-Oct-2005.)
|- +oo =/= -oo
Theorem	mnfnepnf 8127	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -oo =/= +oo
Theorem	mnfxr 8128	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 8129	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	1xr 8130	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- 1 e. RR*
Theorem	renfdisj 8131	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 8132	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 8133	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 8134	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 8135	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 8136	'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 8137	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 8138	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 8036 with ordering on the extended reals. New proofs should use ltnr 8148 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ( A e. RR -> -. A < A )
Theorem	axltwlin 8139	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 8037 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 8140	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 8038 with ordering on the extended reals. New proofs should use lttr 8145 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 8141	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 8040 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 8142	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 8039 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 8143	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 8041 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 8144*	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 8045 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 8145	Alias for axlttrn 8140, for naming consistency with lttri 8176. New proofs should generally use this instead of ax-pre-lttrn 8038. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 8146	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 8147	'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 8148	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	ltso 8149	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 8150	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri3 8151	Tightness of real apartness. (Contributed by NM, 5-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	letri3 8152	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	ltleletr 8153	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 8154	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 8155	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 8156	'Less than' implies not equal. See also ltap 8705 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 8157	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	eqlelt 8158	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 8159	'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 8160	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 8161	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 8162	'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 8163	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	ltnri 8164	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 8165	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 8166	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 8167	'Less than' implies not equal. See also gtapii 8706 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 8168	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri3i 8169	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 8170	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	ltnsymi 8171	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 8172	'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 8173	'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 8174	'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 8175	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	lttri 8176	'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 8177	'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 8178	'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 8179	'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 8180	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 8181	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 8182	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 8183	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 8184	'Less than' implies not equal. See also gtapd 8709 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 8185	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	lttri3d 8186	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 8187	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 8188	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 8189	'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 8190	'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 8191	'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 8192	'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 8193	'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 8194	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 8195	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 8196	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 8197	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 8198	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 8199	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 8200	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 ) ) )