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
Axiom	ax-1re 8001	1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7957. Proofs should use 1re 8053 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 8002	_i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7958. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 8003	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 7959. Proofs should normally use addcl 8032 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Axiom	ax-addrcl 8004	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 7960. Proofs should normally use readdcl 8033 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Axiom	ax-mulcl 8005	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 7961. Proofs should normally use mulcl 8034 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Axiom	ax-mulrcl 8006	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 7962. Proofs should normally use remulcl 8035 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Axiom	ax-addcom 8007	Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 7965. Proofs should normally use addcom 8191 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Axiom	ax-mulcom 8008	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 7966. Proofs should normally use mulcom 8036 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Axiom	ax-addass 8009	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 7967. Proofs should normally use addass 8037 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Axiom	ax-mulass 8010	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 7968. Proofs should normally use mulass 8038 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
Axiom	ax-distr 8011	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7969. Proofs should normally use adddi 8039 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
Axiom	ax-i2m1 8012	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 7970. (Contributed by NM, 29-Jan-1995.)
|- ( ( _i x. _i ) + 1 ) = 0
Axiom	ax-0lt1 8013	0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 7971. Proofs should normally use 0lt1 8181 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 8014	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7972. (Contributed by NM, 29-Jan-1995.)
|- ( A e. RR -> ( A x. 1 ) = A )
Axiom	ax-0id 8015	0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 7973. Proofs should normally use addrid 8192 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Axiom	ax-rnegex 8016*	Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7974. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Axiom	ax-precex 8017*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 7975. (Contributed by Jim Kingdon, 6-Feb-2020.)
|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
Axiom	ax-cnre 8018*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, justified by Theorem axcnre 7976. For naming consistency, use cnre 8050 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
Axiom	ax-pre-ltirr 8019	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 8019. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ( A e. RR -> -. A <RR A )
Axiom	ax-pre-ltwlin 8020	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 7978. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
Axiom	ax-pre-lttrn 8021	Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 7979. (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
Axiom	ax-pre-apti 8022	Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 7980. (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
Axiom	ax-pre-ltadd 8023	Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 7981. (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
Axiom	ax-pre-mulgt0 8024	The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 7982. (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
Axiom	ax-pre-mulext 8025	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by Theorem axpre-mulext 7983 (Contributed by Jim Kingdon, 18-Feb-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
Axiom	ax-arch 8026*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 7986. This axiom should not be used directly; instead use arch 9274 (which is the same, but stated in terms of NN and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)
|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
Axiom	ax-caucvg 8027*	Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7995. A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / n of the nth term. This axiom should not be used directly; instead use caucvgre 11211 (which is the same, but stated in terms of the NN and 1 / n notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   =>    |- ( ph -> E. y e. RR A. x e. RR ( 0 <RR x -> E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) ) ) )
Axiom	ax-pre-suploc 8028*	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound. Although this and ax-caucvg 8027 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8027. (Contributed by Jim Kingdon, 23-Jan-2024.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
Axiom	ax-addf 8029	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 https://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 8032 should be used. Note that uses of ax-addf 8029 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 7963. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 8030	Multiplication is an operation on the complex numbers. This axiom tells us that x. is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf 8256 or eff 11893. However, while Metamath can handle this axiom, if we wish to work with weaker complex number axioms, we can avoid it by using the less specific mulcl 8034. Note that uses of ax-mulf 8030 can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x x. y ) ) in place of x., as seen in mpomulf 8044. This axiom is justified by Theorem axmulf 7964. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- x. : ( CC X. CC ) --> CC
4.2  Derive the basic properties from the field axioms
4.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 8031	Alias for ax-cnex 7998. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 8032	Alias for ax-addcl 8003, for naming consistency with addcli 8058. Use this theorem instead of ax-addcl 8003 or axaddcl 7959. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 8033	Alias for ax-addrcl 8004, for naming consistency with readdcli 8067. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 8034	Alias for ax-mulcl 8005, for naming consistency with mulcli 8059. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 8035	Alias for ax-mulrcl 8006, for naming consistency with remulcli 8068. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 8036	Alias for ax-mulcom 8008, for naming consistency with mulcomi 8060. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 8037	Alias for ax-addass 8009, for naming consistency with addassi 8062. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 8038	Alias for ax-mulass 8010, for naming consistency with mulassi 8063. (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 8039	Alias for ax-distr 8011, for naming consistency with adddii 8064. (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 8040	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 8041	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 8042	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 8043	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 8044*	Multiplication is an operation on complex numbers. Version of ax-mulf 8030 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8005. (Contributed by GG, 16-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
Theorem	adddir 8045	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 8046	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 8047	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )
Theorem	c0ex 8048	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 8049	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 8050*	Alias for ax-cnre 8018, 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 8051	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 8052	Identity law for multiplication. Note: see mulrid 8051 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- ( A e. CC -> ( 1 x. A ) = A )
Theorem	1re 8053	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
Theorem	0re 8054	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 8055	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 0 e. RR )
Theorem	mulridi 8056	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( A x. 1 ) = A
Theorem	mullidi 8057	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( 1 x. A ) = A
Theorem	addcli 8058	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) e. CC
Theorem	mulcli 8059	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) e. CC
Theorem	mulcomi 8060	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) = ( B x. A )
Theorem	mulcomli 8061	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 8062	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 8063	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 8064	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 8065	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 8066	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>    |- A e. CC
Theorem	readdcli 8067	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A + B ) e. RR
Theorem	remulcli 8068	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 8069	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. RR )
Theorem	1cnd 8070	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. CC )
Theorem	mulridd 8071	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 1 ) = A )
Theorem	mullidd 8072	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	mulid2d 8073	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	addcld 8074	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 8075	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 8076	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 8077	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 8078	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 8079	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 8080	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 8081	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 8082	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 8083	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. CC )
Theorem	readdcld 8084	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 8085	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 8086	Plus infinity.
class +oo
Syntax	cmnf 8087	Minus infinity.
class -oo
Syntax	cxr 8088	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 8089	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 8090	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 8091	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 8092). 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 8096 and mnfnre 8097, 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 8092	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 8097). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 8093	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 8094*	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 8095	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 8096	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 8097	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR
Theorem	ressxr 8098	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
|- RR C_ RR*
Theorem	rexpssxrxp 8099	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 8100	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A e. RR* )