P. 83 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulridd 8201	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐴)
Theorem	mullidd 8202	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	mulid2d 8203	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	addcld 8204	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Theorem	mulcld 8205	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Theorem	mulcomd 8206	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addassd 8207	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulassd 8208	Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddid 8209	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	adddird 8210	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	adddirp1d 8211	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Theorem	joinlmuladdmuld 8212	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
Theorem	recnd 8213	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	readdcld 8214	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Theorem	remulcld 8215	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 8216	Plus infinity.
class +∞
Syntax	cmnf 8217	Minus infinity.
class -∞
Syntax	cxr 8218	The set of extended reals (includes plus and minus infinity).
class ℝ*
Syntax	clt 8219	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 8220	Extend wff notation to include the 'less than or equal to' relation.
class ≤
Definition	df-pnf 8221	Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in ℝ and different from -∞ (df-mnf 8222). 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 8226 and mnfnre 8227, 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 8222	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 8227). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ -∞ = 𝒫 +∞
Definition	df-xr 8223	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 8224*	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 8225	Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
Theorem	pnfnre 8226	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ +∞ ∉ ℝ
Theorem	mnfnre 8227	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ -∞ ∉ ℝ
Theorem	ressxr 8228	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ℝ ⊆ ℝ*
Theorem	rexpssxrxp 8229	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 8230	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Theorem	0xr 8231	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 0 ∈ ℝ*
Theorem	renepnf 8232	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Theorem	renemnf 8233	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
Theorem	rexrd 8234	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	renepnfd 8235	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ +∞)
Theorem	renemnfd 8236	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ -∞)
Theorem	pnfxr 8237	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 8238	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ +∞ ∈ V
Theorem	pnfnemnf 8239	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 8240	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	mnfxr 8241	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 8242	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℝ*
Theorem	1xr 8243	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 1 ∈ ℝ*
Theorem	renfdisj 8244	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (ℝ ∩ {+∞, -∞}) = ∅
Theorem	ltrelxr 8245	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ < ⊆ (ℝ* × ℝ*)
Theorem	ltrel 8246	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
⊢ Rel <
Theorem	lerelxr 8247	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ≤ ⊆ (ℝ* × ℝ*)
Theorem	lerel 8248	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ Rel ≤
Theorem	xrlenlt 8249	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	ltxrlt 8250	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 8251	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 8149 with ordering on the extended reals. New proofs should use ltnr 8261 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Theorem	axltwlin 8252	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 8150 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶 ∨ 𝐶 < 𝐵)))
Theorem	axlttrn 8253	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 8151 with ordering on the extended reals. New proofs should use lttr 8258 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	axltadd 8254	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 8153 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	axapti 8255	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 8152 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) → 𝐴 = 𝐵)
Theorem	axmulgt0 8256	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 8154 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
Theorem	axsuploc 8257*	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 8158 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.)
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
4.2.4  Ordering on reals
Theorem	lttr 8258	Alias for axlttrn 8253, for naming consistency with lttri 8289. New proofs should generally use this instead of ax-pre-lttrn 8151. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	mulgt0 8259	The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵))
Theorem	lenlt 8260	'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 8261	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Theorem	ltso 8262	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
⊢ < Or ℝ
Theorem	gtso 8263	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
⊢ ◡ < Or ℝ
Theorem	lttri3 8264	Tightness of real apartness. (Contributed by NM, 5-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
Theorem	letri3 8265	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
Theorem	ltleletr 8266	Transitive law, weaker form of (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	letr 8267	Transitive law. (Contributed by NM, 12-Nov-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	leid 8268	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴)
Theorem	ltne 8269	'Less than' implies not equal. See also ltap 8818 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
Theorem	ltnsym 8270	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
Theorem	eqlelt 8271	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵)))
Theorem	ltle 8272	'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
Theorem	lelttr 8273	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	ltletr 8274	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
Theorem	ltnsym2 8275	'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴))
Theorem	eqle 8276	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵)
Theorem	ltnri 8277	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ ¬ 𝐴 < 𝐴
Theorem	eqlei 8278	Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵)
Theorem	eqlei2 8279	Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴)
Theorem	gtneii 8280	'Less than' implies not equal. See also gtapii 8819 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	ltneii 8281	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	lttri3i 8282	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))
Theorem	letri3i 8283	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))
Theorem	ltnsymi 8284	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)
Theorem	lenlti 8285	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)
Theorem	ltlei 8286	'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)
Theorem	ltleii 8287	'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐴 ≤ 𝐵
Theorem	ltnei 8288	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 → 𝐵 ≠ 𝐴)
Theorem	lttri 8289	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)
Theorem	lelttri 8290	'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)
Theorem	ltletri 8291	'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)
Theorem	letri 8292	'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)
Theorem	le2tri3i 8293	Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴))
Theorem	mulgt0i 8294	The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵))
Theorem	mulgt0ii 8295	The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 0 < 𝐴    &   ⊢ 0 < 𝐵    ⇒   ⊢ 0 < (𝐴 · 𝐵)
Theorem	ltnrd 8296	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ¬ 𝐴 < 𝐴)
Theorem	gtned 8297	'Less than' implies not equal. See also gtapd 8822 which is the same but for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	ltned 8298	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	lttri3d 8299	Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
Theorem	letri3d 8300	Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))