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-addf 8001	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 8004 should be used. Note that uses of ax-addf 8001 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) 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 7935. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ + :(ℂ × ℂ)⟶ℂ
Axiom	ax-mulf 8002	Multiplication is an operation on the complex numbers. This axiom tells us that · is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf 8228 or eff 11828. 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 8006. Note that uses of ax-mulf 8002 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 8016. This axiom is justified by Theorem axmulf 7936. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ · :(ℂ × ℂ)⟶ℂ
4.2  Derive the basic properties from the field axioms
4.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 8003	Alias for ax-cnex 7970. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℂ ∈ V
Theorem	addcl 8004	Alias for ax-addcl 7975, for naming consistency with addcli 8030. Use this theorem instead of ax-addcl 7975 or axaddcl 7931. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	readdcl 8005	Alias for ax-addrcl 7976, for naming consistency with readdcli 8039. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	mulcl 8006	Alias for ax-mulcl 7977, for naming consistency with mulcli 8031. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	remulcl 8007	Alias for ax-mulrcl 7978, for naming consistency with remulcli 8040. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 8008	Alias for ax-mulcom 7980, for naming consistency with mulcomi 8032. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 8009	Alias for ax-addass 7981, for naming consistency with addassi 8034. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 8010	Alias for ax-mulass 7982, for naming consistency with mulassi 8035. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 8011	Alias for ax-distr 7983, for naming consistency with adddii 8036. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 8012	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 8013	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 8014	Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 8015	Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	mpomulf 8016*	Multiplication is an operation on complex numbers. Version of ax-mulf 8002 using maps-to notation, proved from the axioms of set theory and ax-mulcl 7977. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	adddir 8017	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 8018	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ
Theorem	0cnd 8019	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℂ)
Theorem	c0ex 8020	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ∈ V
Theorem	1ex 8021	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 1 ∈ V
Theorem	cnre 8022*	Alias for ax-cnre 7990, for naming consistency. (Contributed by NM, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	mulrid 8023	1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Theorem	mullid 8024	Identity law for multiplication. Note: see mulrid 8023 for commuted version. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	1re 8025	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
⊢ 1 ∈ ℝ
Theorem	0re 8026	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 0 ∈ ℝ
Theorem	0red 8027	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℝ)
Theorem	mulridi 8028	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 1) = 𝐴
Theorem	mullidi 8029	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (1 · 𝐴) = 𝐴
Theorem	addcli 8030	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℂ
Theorem	mulcli 8031	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℂ
Theorem	mulcomi 8032	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	mulcomli 8033	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (𝐵 · 𝐴) = 𝐶
Theorem	addassi 8034	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	mulassi 8035	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	adddii 8036	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Theorem	adddiri 8037	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
Theorem	recni 8038	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	readdcli 8039	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℝ
Theorem	remulcli 8040	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℝ
Theorem	1red 8041	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℝ)
Theorem	1cnd 8042	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℂ)
Theorem	mulridd 8043	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐴)
Theorem	mullidd 8044	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	mulid2d 8045	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	addcld 8046	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Theorem	mulcld 8047	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Theorem	mulcomd 8048	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addassd 8049	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulassd 8050	Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddid 8051	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	adddird 8052	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	adddirp1d 8053	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Theorem	joinlmuladdmuld 8054	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
Theorem	recnd 8055	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	readdcld 8056	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Theorem	remulcld 8057	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
4.2.2  Infinity and the extended real number system
Syntax	cpnf 8058	Plus infinity.
class +∞
Syntax	cmnf 8059	Minus infinity.
class -∞
Syntax	cxr 8060	The set of extended reals (includes plus and minus infinity).
class ℝ*
Syntax	clt 8061	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 8062	Extend wff notation to include the 'less than or equal to' relation.
class ≤
Definition	df-pnf 8063	Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in ℝ and different from -∞ (df-mnf 8064). We use 𝒫 ∪ ℂ to make it independent of the construction of ℂ, and Cantor's Theorem will show that it is different from any member of ℂ and therefore ℝ. See pnfnre 8068 and mnfnre 8069, and we'll also be able to prove +∞ ≠ -∞. A simpler possibility is to define +∞ as ℂ and -∞ as {ℂ}, but that approach requires the Axiom of Regularity to show that +∞ and -∞ are different from each other and from all members of ℝ. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ +∞ = 𝒫 ∪ ℂ
Definition	df-mnf 8064	Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -∞ be a set not in ℝ and different from +∞ (see mnfnre 8069). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ -∞ = 𝒫 +∞
Definition	df-xr 8065	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.)
⊢ ℝ* = (ℝ ∪ {+∞, -∞})
Definition	df-ltxr 8066*	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, <ℝ is primitive and not necessarily a relation on ℝ. (Contributed by NM, 13-Oct-2005.)
⊢ < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
Definition	df-le 8067	Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
Theorem	pnfnre 8068	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ +∞ ∉ ℝ
Theorem	mnfnre 8069	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ -∞ ∉ ℝ
Theorem	ressxr 8070	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ℝ ⊆ ℝ*
Theorem	rexpssxrxp 8071	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.)
⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
Theorem	rexr 8072	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Theorem	0xr 8073	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 0 ∈ ℝ*
Theorem	renepnf 8074	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Theorem	renemnf 8075	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
Theorem	rexrd 8076	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	renepnfd 8077	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ +∞)
Theorem	renemnfd 8078	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ -∞)
Theorem	pnfxr 8079	Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
⊢ +∞ ∈ ℝ*
Theorem	pnfex 8080	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ +∞ ∈ V
Theorem	pnfnemnf 8081	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 8082	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	mnfxr 8083	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.)
⊢ -∞ ∈ ℝ*
Theorem	rexri 8084	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℝ*
Theorem	1xr 8085	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 1 ∈ ℝ*
Theorem	renfdisj 8086	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (ℝ ∩ {+∞, -∞}) = ∅
Theorem	ltrelxr 8087	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ < ⊆ (ℝ* × ℝ*)
Theorem	ltrel 8088	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
⊢ Rel <
Theorem	lerelxr 8089	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ≤ ⊆ (ℝ* × ℝ*)
Theorem	lerel 8090	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ Rel ≤
Theorem	xrlenlt 8091	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	ltxrlt 8092	The standard less-than <ℝ and the extended real less-than < are identical when restricted to the non-extended reals ℝ. (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵))
4.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axltirr 8093	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7991 with ordering on the extended reals. New proofs should use ltnr 8103 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Theorem	axltwlin 8094	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7992 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶 ∨ 𝐶 < 𝐵)))
Theorem	axlttrn 8095	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7993 with ordering on the extended reals. New proofs should use lttr 8100 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	axltadd 8096	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7995 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	axapti 8097	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7994 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) → 𝐴 = 𝐵)
Theorem	axmulgt0 8098	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7996 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
Theorem	axsuploc 8099*	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 8000 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.)
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
4.2.4  Ordering on reals
Theorem	lttr 8100	Alias for axlttrn 8095, for naming consistency with lttri 8131. New proofs should generally use this instead of ax-pre-lttrn 7993. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))