P. 81 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulcl 8001	Alias for ax-mulcl 7972, for naming consistency with mulcli 8026. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 8002	Alias for ax-mulrcl 7973, for naming consistency with remulcli 8035. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 8003	Alias for ax-mulcom 7975, for naming consistency with mulcomi 8027. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 8004	Alias for ax-addass 7976, for naming consistency with addassi 8029. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 8005	Alias for ax-mulass 7977, for naming consistency with mulassi 8030. (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 8006	Alias for ax-distr 7978, for naming consistency with adddii 8031. (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 8007	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 8008	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 8009	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 8010	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	mpomulf 8011*	Multiplication is an operation on complex numbers. Version of ax-mulf 7997 using maps-to notation, proved from the axioms of set theory and ax-mulcl 7972. (Contributed by GG, 16-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
Theorem	adddir 8012	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 8013	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 8014	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )
Theorem	c0ex 8015	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 8016	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 8017*	Alias for ax-cnre 7985, 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	mulrid 8018	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	mullid 8019	Identity law for multiplication. Note: see mulrid 8018 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- ( A e. CC -> ( 1 x. A ) = A )
Theorem	1re 8020	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
Theorem	0re 8021	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 8022	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 0 e. RR )
Theorem	mulid1i 8023	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( A x. 1 ) = A
Theorem	mullidi 8024	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( 1 x. A ) = A
Theorem	addcli 8025	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) e. CC
Theorem	mulcli 8026	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) e. CC
Theorem	mulcomi 8027	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) = ( B x. A )
Theorem	mulcomli 8028	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 8029	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 8030	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 8031	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 8032	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 8033	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>    |- A e. CC
Theorem	readdcli 8034	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A + B ) e. RR
Theorem	remulcli 8035	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 8036	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. RR )
Theorem	1cnd 8037	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. CC )
Theorem	mulridd 8038	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 1 ) = A )
Theorem	mullidd 8039	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	mulid2d 8040	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	addcld 8041	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 8042	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 8043	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 8044	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 8045	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 8046	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 8047	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	adddirp1d 8048	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + B ) )
Theorem	joinlmuladdmuld 8049	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> ( ( A x. B ) + ( C x. B ) ) = D )   =>    |- ( ph -> ( ( A + C ) x. B ) = D )
Theorem	recnd 8050	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. CC )
Theorem	readdcld 8051	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 8052	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 8053	Plus infinity.
class +oo
Syntax	cmnf 8054	Minus infinity.
class -oo
Syntax	cxr 8055	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 8056	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 8057	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 8058	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 8059). 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 8063 and mnfnre 8064, 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 8059	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 8064). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 8060	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 8061*	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 8062	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 8063	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 8064	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR
Theorem	ressxr 8065	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 8066	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 8067	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )
Theorem	0xr 8068	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
|- 0 e. RR*
Theorem	renepnf 8069	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 8070	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 8071	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. RR* )
Theorem	renepnfd 8072	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= +oo )
Theorem	renemnfd 8073	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A =/= -oo )
Theorem	pnfxr 8074	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 8075	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- +oo e. _V
Theorem	pnfnemnf 8076	Plus and minus infinity are different elements of RR*. (Contributed by NM, 14-Oct-2005.)
|- +oo =/= -oo
Theorem	mnfnepnf 8077	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -oo =/= +oo
Theorem	mnfxr 8078	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 8079	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	1xr 8080	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- 1 e. RR*
Theorem	renfdisj 8081	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 8082	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 8083	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 8084	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 8085	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 8086	'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 8087	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 8088	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7986 with ordering on the extended reals. New proofs should use ltnr 8098 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ( A e. RR -> -. A < A )
Theorem	axltwlin 8089	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7987 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 8090	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7988 with ordering on the extended reals. New proofs should use lttr 8095 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 8091	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7990 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 8092	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7989 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 8093	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7991 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 8094*	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 7995 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 8095	Alias for axlttrn 8090, for naming consistency with lttri 8126. New proofs should generally use this instead of ax-pre-lttrn 7988. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 8096	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 8097	'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 8098	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	ltso 8099	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 8100	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR