![]() |
Metamath
Proof Explorer Theorem List (p. 113 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reex 11201 | The real numbers form a set. See also reexALT 12968. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℝ ∈ V | ||
Theorem | reelprrecn 11202 | Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℝ ∈ {ℝ, ℂ} | ||
Theorem | cnelprrecn 11203 | Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℂ ∈ {ℝ, ℂ} | ||
Theorem | elimne0 11204 | Hypothesis for weak deduction theorem to eliminate 𝐴 ≠ 0. (Contributed by NM, 15-May-1999.) |
⊢ if(𝐴 ≠ 0, 𝐴, 1) ≠ 0 | ||
Theorem | adddir 11205 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | 0cn 11206 | Zero is a complex number. See also 0cnALT 11448. (Contributed by NM, 19-Feb-2005.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnd 11207 | Zero is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℂ) | ||
Theorem | c0ex 11208 | Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ∈ V | ||
Theorem | 1cnd 11209 | One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 1 ∈ ℂ) | ||
Theorem | 1ex 11210 | One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 1 ∈ V | ||
Theorem | cnre 11211* | Alias for ax-cnre 11183, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | mulrid 11212 | The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | ||
Theorem | mullid 11213 | Identity law for multiplication. See mulrid 11212 for commuted version. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | 1re 11214 | The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11168, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 1 ∈ ℝ | ||
Theorem | 1red 11215 | The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 1 ∈ ℝ) | ||
Theorem | 0re 11216 | The number 0 is real. Remark: the first step could also be ax-icn 11169. See also 0reALT 11557. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.) |
⊢ 0 ∈ ℝ | ||
Theorem | 0red 11217 | The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℝ) | ||
Theorem | mulridi 11218 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 1) = 𝐴 | ||
Theorem | mullidi 11219 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (1 · 𝐴) = 𝐴 | ||
Theorem | addcli 11220 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℂ | ||
Theorem | mulcli 11221 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℂ | ||
Theorem | mulcomi 11222 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | mulcomli 11223 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (𝐵 · 𝐴) = 𝐶 | ||
Theorem | addassi 11224 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | mulassi 11225 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | adddii 11226 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) | ||
Theorem | adddiri 11227 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)) | ||
Theorem | recni 11228 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | readdcli 11229 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℝ | ||
Theorem | remulcli 11230 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℝ | ||
Theorem | mulridd 11231 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐴) | ||
Theorem | mullidd 11232 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐴) | ||
Theorem | addcld 11233 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | mulcld 11234 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | mulcomd 11235 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addassd 11236 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulassd 11237 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddid 11238 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | adddird 11239 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | adddirp1d 11240 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵)) | ||
Theorem | joinlmuladdmuld 11241 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷) | ||
Theorem | recnd 11242 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | readdcld 11243 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | remulcld 11244 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) | ||
Syntax | cpnf 11245 | Plus infinity. |
class +∞ | ||
Syntax | cmnf 11246 | Minus infinity. |
class -∞ | ||
Syntax | cxr 11247 | The set of extended reals (includes plus and minus infinity). |
class ℝ* | ||
Syntax | clt 11248 | 'Less than' predicate (extended to include the extended reals). |
class < | ||
Syntax | cle 11249 | Extend wff notation to include the 'less than or equal to' relation. |
class ≤ | ||
Definition | df-pnf 11250 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that +∞ be a set not in ℝ and different from -∞
(df-mnf 11251). 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 11255,
mnfnre 11257, and pnfnemnf 11269.
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 11251 | 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 11257 and pnfnemnf 11269). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
⊢ -∞ = 𝒫 +∞ | ||
Definition | df-xr 11252 | 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 11253* | 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 11254 | Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 11300 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.) |
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < ) | ||
Theorem | pnfnre 11255 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
⊢ +∞ ∉ ℝ | ||
Theorem | pnfnre2 11256 | Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ¬ +∞ ∈ ℝ | ||
Theorem | mnfnre 11257 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
⊢ -∞ ∉ ℝ | ||
Theorem | ressxr 11258 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
⊢ ℝ ⊆ ℝ* | ||
Theorem | rexpssxrxp 11259 | 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 11260 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | ||
Theorem | 0xr 11261 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
⊢ 0 ∈ ℝ* | ||
Theorem | renepnf 11262 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) | ||
Theorem | renemnf 11263 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) | ||
Theorem | rexrd 11264 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | renepnfd 11265 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≠ +∞) | ||
Theorem | renemnfd 11266 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≠ -∞) | ||
Theorem | pnfex 11267 | Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.) |
⊢ +∞ ∈ V | ||
Theorem | pnfxr 11268 | 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 11269 | Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.) |
⊢ +∞ ≠ -∞ | ||
Theorem | mnfnepnf 11270 | Minus and plus infinity are different. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -∞ ≠ +∞ | ||
Theorem | mnfxr 11271 | 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 11272 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℝ* | ||
Theorem | 1xr 11273 | 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 1 ∈ ℝ* | ||
Theorem | renfdisj 11274 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (ℝ ∩ {+∞, -∞}) = ∅ | ||
Theorem | ltrelxr 11275 | "Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ < ⊆ (ℝ* × ℝ*) | ||
Theorem | ltrel 11276 | "Less than" is a relation. (Contributed by NM, 14-Oct-2005.) |
⊢ Rel < | ||
Theorem | lerelxr 11277 | "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ≤ ⊆ (ℝ* × ℝ*) | ||
Theorem | lerel 11278 | "Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ Rel ≤ | ||
Theorem | xrlenlt 11279 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
Theorem | xrlenltd 11280 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
Theorem | xrltnle 11281 | "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
Theorem | xrnltled 11282 | "Not less than" implies "less than or equal to". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | ssxr 11283 | 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 11284 | 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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵)) | ||
Theorem | axlttri 11285 | 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 11184 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | axlttrn 11286 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 11185 with ordering on the extended reals. New proofs should use lttr 11290 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | axltadd 11287 | 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 11186 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
Theorem | axmulgt0 11288 | 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 11187 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵))) | ||
Theorem | axsup 11289* | 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 11188 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | lttr 11290 | Alias for axlttrn 11286, for naming consistency with lttri 11340. New proofs should generally use this instead of ax-pre-lttrn 11185. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | mulgt0 11291 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵)) | ||
Theorem | lenlt 11292 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
Theorem | ltnle 11293 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
Theorem | ltso 11294 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
⊢ < Or ℝ | ||
Theorem | gtso 11295 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
⊢ ◡ < Or ℝ | ||
Theorem | lttri2 11296 | Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | lttri3 11297 | Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
Theorem | lttri4 11298 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴)) | ||
Theorem | letri3 11299 | Trichotomy law. (Contributed by NM, 14-May-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
Theorem | leloe 11300 | 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |