HomeTheorem List (p. 102 of 426)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 102 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lerelxr 10101 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ≤ ⊆ (ℝ* × ℝ*) | ||
| Theorem | lerel 10102 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ Rel ≤ | ||
| Theorem | xrlenlt 10103 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | xrlenltd 10104 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | xrltnle 10105 | 'Less than' expressed in terms of 'less than or equal to', for extended reals. (Contributed by NM, 6-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
| Theorem | xrnltled 10106 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | ssxr 10107 | 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 10108 | 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 10109 | 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 10010 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | axlttrn 10110 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 10011 with ordering on the extended reals. New proofs should use lttr 10114 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | axltadd 10111 | 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 10012 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
| Theorem | axmulgt0 10112 | 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 10013 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵))) | ||
| Theorem | axsup 10113* | 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 10014 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
| Theorem | lttr 10114 | Alias for axlttrn 10110, for naming consistency with lttri 10163. New proofs should generally use this instead of ax-pre-lttrn 10011. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | mulgt0 10115 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵)) | ||
| Theorem | lenlt 10116 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | ltnle 10117 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
| Theorem | ltso 10118 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
| ⊢ < Or ℝ | ||
| Theorem | gtso 10119 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
| ⊢ ◡ < Or ℝ | ||
| Theorem | lttri2 10120 | Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | lttri3 10121 | Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
| Theorem | lttri4 10122 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | letri3 10123 | Trichotomy law. (Contributed by NM, 14-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
| Theorem | leloe 10124 | 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | eqlelt 10125 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵))) | ||
| Theorem | ltle 10126 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) | ||
| Theorem | leltne 10127 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) | ||
| Theorem | lelttr 10128 | Transitive law. (Contributed by NM, 23-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | ltletr 10129 | Transitive law. (Contributed by NM, 25-Aug-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | ltleletr 10130 | Transitive law, weaker form of ltletr 10129. (Contributed by AV, 14-Oct-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | letr 10131 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | ltnr 10132 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
| ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴) | ||
| Theorem | leid 10133 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴) | ||
| Theorem | ltne 10134 | 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) | ||
| Theorem | ltnsym 10135 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) | ||
| Theorem | ltnsym2 10136 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) | ||
| Theorem | letric 10137 | Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
| Theorem | ltlen 10138 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
| Theorem | eqle 10139 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) | ||
| Theorem | eqled 10140 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | ltadd2 10141 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
| Theorem | ne0gt0 10142 | A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 ≠ 0 ↔ 0 < 𝐴)) | ||
| Theorem | lecasei 10143 | Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | lelttric 10144 | Trichotomy law. (Contributed by NM, 4-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | ltlecasei 10145 | Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | ltnri 10146 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ ¬ 𝐴 < 𝐴 | ||
| Theorem | eqlei 10147 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵) | ||
| Theorem | eqlei2 10148 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴) | ||
| Theorem | gtneii 10149 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 | ||
| Theorem | ltneii 10150 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 | ||
| Theorem | lttri2i 10151 | Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | lttri3i 10152 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)) | ||
| Theorem | letri3i 10153 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)) | ||
| Theorem | leloei 10154 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)) | ||
| Theorem | ltleni 10155 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴)) | ||
| Theorem | ltnsymi 10156 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴) | ||
| Theorem | lenlti 10157 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴) | ||
| Theorem | ltnlei 10158 | 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴) | ||
| Theorem | ltlei 10159 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵) | ||
| Theorem | ltleii 10160 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≤ 𝐵 | ||
| Theorem | ltnei 10161 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 ≠ 𝐴) | ||
| Theorem | letrii 10162 | Trichotomy law for 'less than or equal to'. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴) | ||
| Theorem | lttri 10163 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) | ||
| Theorem | lelttri 10164 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) | ||
| Theorem | ltletri 10165 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) | ||
| Theorem | letri 10166 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶) | ||
| Theorem | le2tri3i 10167 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴)) | ||
| Theorem | ltadd2i 10168 | Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)) | ||
| Theorem | mulgt0i 10169 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) | ||
| Theorem | mulgt0ii 10170 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 · 𝐵) | ||
| Theorem | ltnrd 10171 | 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐴) | ||
| Theorem | gtned 10172 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
| Theorem | ltned 10173 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
| Theorem | ne0gt0d 10174 | A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
| Theorem | lttrid 10175 | Ordering on reals satisfies strict trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | lttri2d 10176 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | lttri3d 10177 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
| Theorem | lttri4d 10178 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | letri3d 10179 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
| Theorem | leloed 10180 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | eqleltd 10181 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵))) | ||
| Theorem | ltlend 10182 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
| Theorem | lenltd 10183 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | ltnled 10184 | 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
| Theorem | ltled 10185 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | ltnsymd 10186 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) | ||
| Theorem | nltled 10187 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | lensymd 10188 | 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) | ||
| Theorem | letrid 10189 | Trichotomy law for 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
| Theorem | leltned 10190 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) | ||
| Theorem | leneltd 10191 | 'Less than or equal to' and 'not equals' implies 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
| Theorem | mulgt0d 10192 | The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 · 𝐵)) | ||
| Theorem | ltadd2d 10193 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
| Theorem | letrd 10194 | Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
| Theorem | lelttrd 10195 | Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | ltadd2dd 10196 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) | ||
| Theorem | ltletrd 10197 | Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | lttrd 10198 | Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | lelttrdi 10199 | If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018.) |
| ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) | ||
| Theorem | dedekind 10200* | The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 10014 with appropriate adjustments, states that, if 𝐴 completely preceeds 𝐵, then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |