P. 72 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	remulcl 7101	Alias for ax-mulrcl 7075, for naming consistency with remulcli 7133. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 7102	Alias for ax-mulcom 7077, for naming consistency with mulcomi 7125. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 7103	Alias for ax-addass 7078, for naming consistency with addassi 7127. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 7104	Alias for ax-mulass 7079, for naming consistency with mulassi 7128. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 7105	Alias for ax-distr 7080, for naming consistency with adddii 7129. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 7106	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 7107	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 7108	Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 7109	Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	adddir 7110	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 7111	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ
Theorem	0cnd 7112	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℂ)
Theorem	c0ex 7113	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ∈ V
Theorem	1ex 7114	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 1 ∈ V
Theorem	cnre 7115*	Alias for ax-cnre 7087, for naming consistency. (Contributed by NM, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	mulid1 7116	1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Theorem	mulid2 7117	Identity law for multiplication. Note: see mulid1 7116 for commuted version. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	1re 7118	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
⊢ 1 ∈ ℝ
Theorem	0re 7119	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 0 ∈ ℝ
Theorem	0red 7120	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℝ)
Theorem	mulid1i 7121	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 1) = 𝐴
Theorem	mulid2i 7122	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (1 · 𝐴) = 𝐴
Theorem	addcli 7123	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℂ
Theorem	mulcli 7124	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℂ
Theorem	mulcomi 7125	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	mulcomli 7126	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (𝐵 · 𝐴) = 𝐶
Theorem	addassi 7127	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	mulassi 7128	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	adddii 7129	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Theorem	adddiri 7130	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
Theorem	recni 7131	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	readdcli 7132	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℝ
Theorem	remulcli 7133	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℝ
Theorem	1red 7134	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℝ)
Theorem	1cnd 7135	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℂ)
Theorem	mulid1d 7136	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐴)
Theorem	mulid2d 7137	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	addcld 7138	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Theorem	mulcld 7139	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Theorem	mulcomd 7140	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addassd 7141	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulassd 7142	Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddid 7143	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	adddird 7144	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	adddirp1d 7145	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Theorem	joinlmuladdmuld 7146	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
Theorem	recnd 7147	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	readdcld 7148	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Theorem	remulcld 7149	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
3.2.2  Infinity and the extended real number system
Syntax	cpnf 7150	Plus infinity.
class +∞
Syntax	cmnf 7151	Minus infinity.
class -∞
Syntax	cxr 7152	The set of extended reals (includes plus and minus infinity).
class ℝ*
Syntax	clt 7153	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 7154	Extend wff notation to include the 'less than or equal to' relation.
class ≤
Definition	df-pnf 7155	Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in ℝ and different from -∞ (df-mnf 7156). 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 7160 and mnfnre 7161, 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 7156	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 7161). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ -∞ = 𝒫 +∞
Definition	df-xr 7157	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 7158*	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 7159	Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
Theorem	pnfnre 7160	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ +∞ ∉ ℝ
Theorem	mnfnre 7161	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ -∞ ∉ ℝ
Theorem	ressxr 7162	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ℝ ⊆ ℝ*
Theorem	rexpssxrxp 7163	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 7164	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Theorem	0xr 7165	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 0 ∈ ℝ*
Theorem	renepnf 7166	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Theorem	renemnf 7167	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
Theorem	rexrd 7168	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	renepnfd 7169	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ +∞)
Theorem	renemnfd 7170	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ -∞)
Theorem	rexri 7171	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℝ*
Theorem	renfdisj 7172	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (ℝ ∩ {+∞, -∞}) = ∅
Theorem	ltrelxr 7173	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ < ⊆ (ℝ* × ℝ*)
Theorem	ltrel 7174	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
⊢ Rel <
Theorem	lerelxr 7175	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ≤ ⊆ (ℝ* × ℝ*)
Theorem	lerel 7176	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ Rel ≤
Theorem	xrlenlt 7177	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	ltxrlt 7178	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.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵))
3.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axltirr 7179	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7088 with ordering on the extended reals. New proofs should use ltnr 7188 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Theorem	axltwlin 7180	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7089 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶 ∨ 𝐶 < 𝐵)))
Theorem	axlttrn 7181	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7090 with ordering on the extended reals. New proofs should use lttr 7185 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	axltadd 7182	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7092 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	axapti 7183	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7091 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) → 𝐴 = 𝐵)
Theorem	axmulgt0 7184	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7093 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
3.2.4  Ordering on reals
Theorem	lttr 7185	Alias for axlttrn 7181, for naming consistency with lttri 7215. New proofs should generally use this instead of ax-pre-lttrn 7090. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	mulgt0 7186	The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵))
Theorem	lenlt 7187	'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.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	ltnr 7188	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Theorem	ltso 7189	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
⊢ < Or ℝ
Theorem	gtso 7190	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
⊢ ◡ < Or ℝ
Theorem	lttri3 7191	Tightness of real apartness. (Contributed by NM, 5-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
Theorem	letri3 7192	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
Theorem	ltleletr 7193	Transitive law, weaker form of (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	letr 7194	Transitive law. (Contributed by NM, 12-Nov-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	leid 7195	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴)
Theorem	ltne 7196	'Less than' implies not equal. See also ltap 7731 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
Theorem	ltnsym 7197	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
Theorem	ltle 7198	'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
Theorem	lelttr 7199	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	ltletr 7200	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))