P. 113 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulcld 11201	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Theorem	mulcomd 11202	Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addassd 11203	Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulassd 11204	Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddid 11205	Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	adddird 11206	Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	adddirp1d 11207	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
Theorem	joinlmuladdmuld 11208	Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
Theorem	recnd 11209	Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	readdcld 11210	Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Theorem	remulcld 11211	Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
5.2.2  Infinity and the extended real number system
Syntax	cpnf 11212	Plus infinity.
class +∞
Syntax	cmnf 11213	Minus infinity.
class -∞
Syntax	cxr 11214	The set of extended reals (includes plus and minus infinity).
class ℝ*
Syntax	clt 11215	'Less than' predicate (extended to include the extended reals).
class <
Syntax	cle 11216	Extend wff notation to include the 'less than or equal to' relation.
class ≤
Definition	df-pnf 11217	Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in ℝ and different from -∞ (df-mnf 11218). 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 11222, mnfnre 11224, and pnfnemnf 11236. 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 11218	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 11224 and pnfnemnf 11236). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
⊢ -∞ = 𝒫 +∞
Definition	df-xr 11219	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 11220*	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 11221	Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 11267 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.)
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
Theorem	pnfnre 11222	Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ +∞ ∉ ℝ
Theorem	pnfnre2 11223	Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ¬ +∞ ∈ ℝ
Theorem	mnfnre 11224	Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
⊢ -∞ ∉ ℝ
Theorem	ressxr 11225	The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ℝ ⊆ ℝ*
Theorem	rexpssxrxp 11226	The Cartesian product of standard reals are a subset of the Cartesian product of extended reals. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
Theorem	rexr 11227	A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Theorem	0xr 11228	Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 0 ∈ ℝ*
Theorem	renepnf 11229	No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Theorem	renemnf 11230	No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
Theorem	rexrd 11231	A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	renepnfd 11232	No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ +∞)
Theorem	renemnfd 11233	No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ -∞)
Theorem	pnfex 11234	Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.)
⊢ +∞ ∈ V
Theorem	pnfxr 11235	Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
⊢ +∞ ∈ ℝ*
Theorem	pnfnemnf 11236	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 11237	Minus and plus infinity are different. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	mnfxr 11238	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 11239	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℝ*
Theorem	1xr 11240	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 1 ∈ ℝ*
Theorem	renfdisj 11241	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (ℝ ∩ {+∞, -∞}) = ∅
Theorem	ltrelxr 11242	"Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ < ⊆ (ℝ* × ℝ*)
Theorem	ltrel 11243	"Less than" is a relation. (Contributed by NM, 14-Oct-2005.)
⊢ Rel <
Theorem	lerelxr 11244	"Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ≤ ⊆ (ℝ* × ℝ*)
Theorem	lerel 11245	"Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ Rel ≤
Theorem	xrlenlt 11246	"Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	xrlenltd 11247	"Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	xrltnle 11248	"Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
Theorem	xrnltled 11249	"Not less than" implies "less than or equal to". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → ¬ 𝐵 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	ssxr 11250	The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (𝐴 ⊆ ℝ* → (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴))
Theorem	ltxrlt 11251	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.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵))
5.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axlttri 11252	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-lttri 11149 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	axlttrn 11253	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 11150 with ordering on the extended reals. New proofs should use lttr 11257 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	axltadd 11254	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd 11151 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	axmulgt0 11255	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 11152 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
Theorem	axsup 11256*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup 11153 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
5.2.4  Ordering on reals
Theorem	lttr 11257	Alias for axlttrn 11253, for naming consistency with lttri 11307. New proofs should generally use this instead of ax-pre-lttrn 11150. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	mulgt0 11258	The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵))
Theorem	lenlt 11259	'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
Theorem	ltnle 11260	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
Theorem	ltso 11261	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
⊢ < Or ℝ
Theorem	gtso 11262	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
⊢ ◡ < Or ℝ
Theorem	lttri2 11263	Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	lttri3 11264	Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
Theorem	lttri4 11265	Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
Theorem	letri3 11266	Trichotomy law. (Contributed by NM, 14-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
Theorem	leloe 11267	'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	eqlelt 11268	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵)))
Theorem	ltle 11269	'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
Theorem	leltne 11270	'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴))
Theorem	lelttr 11271	Transitive law. (Contributed by NM, 23-May-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	leltletr 11272	Transitive law, weaker form of lelttr 11271. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
Theorem	ltletr 11273	Transitive law. (Contributed by NM, 25-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
Theorem	ltleletr 11274	Transitive law, weaker form of ltletr 11273. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	letr 11275	Transitive law. (Contributed by NM, 12-Nov-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	ltnr 11276	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
Theorem	leid 11277	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴)
Theorem	ltne 11278	'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
Theorem	ltnsym 11279	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
Theorem	ltnsym2 11280	'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴))
Theorem	letric 11281	Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴))
Theorem	ltlen 11282	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴)))
Theorem	eqle 11283	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵)
Theorem	eqled 11284	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	ltadd2 11285	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	ne0gt0 11286	A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 ≠ 0 ↔ 0 < 𝐴))
Theorem	lecasei 11287	Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	lelttric 11288	Trichotomy law. (Contributed by NM, 4-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴))
Theorem	ltlecasei 11289	Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	ltnri 11290	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ ¬ 𝐴 < 𝐴
Theorem	eqlei 11291	Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵)
Theorem	eqlei2 11292	Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴)
Theorem	gtneii 11293	'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	ltneii 11294	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	lttri2i 11295	Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))
Theorem	lttri3i 11296	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))
Theorem	letri3i 11297	Consequence of trichotomy. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))
Theorem	leloei 11298	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
Theorem	ltleni 11299	'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))
Theorem	ltnsymi 11300	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)