P. 80 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axpre-suploc 7901*	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. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7932. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)
|- ( ( ( 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 ) ) )
4.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 7902	The complex numbers form a set. Proofs should normally use cnex 7935 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 7903	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7859. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 7904	1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7860. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-1re 7905	1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7861. Proofs should use 1re 7956 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 7906	_i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7862. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 7907	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 7863. Proofs should normally use addcl 7936 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 7908	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 7864. Proofs should normally use readdcl 7937 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Axiom	ax-mulcl 7909	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 7865. Proofs should normally use mulcl 7938 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 7910	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 7866. Proofs should normally use remulcl 7939 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 7911	Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 7869. Proofs should normally use addcom 8094 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 7912	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 7870. Proofs should normally use mulcom 7940 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 7913	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 7871. Proofs should normally use addass 7941 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 7914	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 7872. Proofs should normally use mulass 7942 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 7915	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7873. Proofs should normally use adddi 7943 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 7916	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 7874. (Contributed by NM, 29-Jan-1995.)
|- ( ( _i x. _i ) + 1 ) = 0
Axiom	ax-0lt1 7917	0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 7875. Proofs should normally use 0lt1 8084 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 7918	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7876. (Contributed by NM, 29-Jan-1995.)
|- ( A e. RR -> ( A x. 1 ) = A )
Axiom	ax-0id 7919	0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 7877. Proofs should normally use addid1 8095 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Axiom	ax-rnegex 7920*	Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7878. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Axiom	ax-precex 7921*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 7879. (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 7922*	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 7880. For naming consistency, use cnre 7953 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 7923	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7923. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ( A e. RR -> -. A <RR A )
Axiom	ax-pre-ltwlin 7924	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 7882. (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 7925	Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 7883. (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 7926	Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 7884. (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 7927	Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 7885. (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 7928	The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 7886. (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 7929	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by Theorem axpre-mulext 7887 (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 7930*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 7890. This axiom should not be used directly; instead use arch 9173 (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 7931*	Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7899. 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 10990 (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 7932*	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 7931 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7931. (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 7933	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 7936 should be used. Note that uses of ax-addf 7933 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 7867. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 7934	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 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 ax-mulcl 7909 should be used. Note that uses of ax-mulf 7934 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 7868. (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 7935	Alias for ax-cnex 7902. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 7936	Alias for ax-addcl 7907, for naming consistency with addcli 7961. Use this theorem instead of ax-addcl 7907 or axaddcl 7863. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 7937	Alias for ax-addrcl 7908, for naming consistency with readdcli 7970. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 7938	Alias for ax-mulcl 7909, for naming consistency with mulcli 7962. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 7939	Alias for ax-mulrcl 7910, for naming consistency with remulcli 7971. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 7940	Alias for ax-mulcom 7912, for naming consistency with mulcomi 7963. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 7941	Alias for ax-addass 7913, for naming consistency with addassi 7965. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 7942	Alias for ax-mulass 7914, for naming consistency with mulassi 7966. (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 7943	Alias for ax-distr 7915, for naming consistency with adddii 7967. (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 7944	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 7945	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 7946	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 7947	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	adddir 7948	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 7949	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 7950	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )
Theorem	c0ex 7951	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 7952	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 7953*	Alias for ax-cnre 7922, 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 7954	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 7955	Identity law for multiplication. Note: see mulrid 7954 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- ( A e. CC -> ( 1 x. A ) = A )
Theorem	1re 7956	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
Theorem	0re 7957	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 7958	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 0 e. RR )
Theorem	mulid1i 7959	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( A x. 1 ) = A
Theorem	mullidi 7960	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( 1 x. A ) = A
Theorem	addcli 7961	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) e. CC
Theorem	mulcli 7962	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) e. CC
Theorem	mulcomi 7963	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) = ( B x. A )
Theorem	mulcomli 7964	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 7965	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 7966	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 7967	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 7968	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 7969	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>    |- A e. CC
Theorem	readdcli 7970	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A + B ) e. RR
Theorem	remulcli 7971	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 7972	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. RR )
Theorem	1cnd 7973	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 1 e. CC )
Theorem	mulridd 7974	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 1 ) = A )
Theorem	mullidd 7975	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	mulid2d 7976	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 x. A ) = A )
Theorem	addcld 7977	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 7978	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 7979	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 7980	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 7981	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 7982	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 7983	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 7984	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 7985	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 7986	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A e. CC )
Theorem	readdcld 7987	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 7988	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 7989	Plus infinity.
class +oo
Syntax	cmnf 7990	Minus infinity.
class -oo
Syntax	cxr 7991	The set of extended reals (includes plus and minus infinity).
class RR*
Syntax	clt 7992	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 7993	Extend wff notation to include the 'less than or equal to' relation.
class <_
Definition	df-pnf 7994	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 7995). 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 7999 and mnfnre 8000, 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 7995	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 8000). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
|- -oo = ~P +oo
Definition	df-xr 7996	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 7997*	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 7998	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 7999	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- +oo e/ RR
Theorem	mnfnre 8000	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
|- -oo e/ RR