HomeTheorem List (p. 114 of 484)
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. 114 of 484) | < 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-30767) |
Hilbert Space Explorer
(30768-32290) |
Users' Mathboxes
(32291-48346) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ltrel 11301 | "Less than" is a relation. (Contributed by NM, 14-Oct-2005.) |
| ⊢ Rel < | ||
| Theorem | lerelxr 11302 | "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ≤ ⊆ (ℝ* × ℝ*) | ||
| Theorem | lerel 11303 | "Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ Rel ≤ | ||
| Theorem | xrlenlt 11304 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | xrlenltd 11305 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | xrltnle 11306 | "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
| Theorem | xrnltled 11307 | "Not less than" implies "less than or equal to". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | ssxr 11308 | 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 11309 | 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 11310 | 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 11207 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | axlttrn 11311 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 11208 with ordering on the extended reals. New proofs should use lttr 11315 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | axltadd 11312 | 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 11209 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
| Theorem | axmulgt0 11313 | 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 11210 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵))) | ||
| Theorem | axsup 11314* | 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 11211 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
| Theorem | lttr 11315 | Alias for axlttrn 11311, for naming consistency with lttri 11365. New proofs should generally use this instead of ax-pre-lttrn 11208. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | mulgt0 11316 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵)) | ||
| Theorem | lenlt 11317 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | ltnle 11318 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
| Theorem | ltso 11319 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
| ⊢ < Or ℝ | ||
| Theorem | gtso 11320 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
| ⊢ ◡ < Or ℝ | ||
| Theorem | lttri2 11321 | Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | lttri3 11322 | Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
| Theorem | lttri4 11323 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | letri3 11324 | Trichotomy law. (Contributed by NM, 14-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
| Theorem | leloe 11325 | 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | eqlelt 11326 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵))) | ||
| Theorem | ltle 11327 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) | ||
| Theorem | leltne 11328 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) | ||
| Theorem | lelttr 11329 | Transitive law. (Contributed by NM, 23-May-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | leltletr 11330 | Transitive law, weaker form of lelttr 11329. (Contributed by AV, 14-Oct-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | ltletr 11331 | Transitive law. (Contributed by NM, 25-Aug-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) | ||
| Theorem | ltleletr 11332 | Transitive law, weaker form of ltletr 11331. (Contributed by AV, 14-Oct-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | letr 11333 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | ltnr 11334 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
| ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴) | ||
| Theorem | leid 11335 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴) | ||
| Theorem | ltne 11336 | 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) | ||
| Theorem | ltnsym 11337 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) | ||
| Theorem | ltnsym2 11338 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) | ||
| Theorem | letric 11339 | Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
| Theorem | ltlen 11340 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
| Theorem | eqle 11341 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) | ||
| Theorem | eqled 11342 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | ltadd2 11343 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
| Theorem | ne0gt0 11344 | A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 ≠ 0 ↔ 0 < 𝐴)) | ||
| Theorem | lecasei 11345 | Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | lelttric 11346 | Trichotomy law. (Contributed by NM, 4-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | ltlecasei 11347 | Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | ltnri 11348 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ ¬ 𝐴 < 𝐴 | ||
| Theorem | eqlei 11349 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵) | ||
| Theorem | eqlei2 11350 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴) | ||
| Theorem | gtneii 11351 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 | ||
| Theorem | ltneii 11352 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 | ||
| Theorem | lttri2i 11353 | Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | lttri3i 11354 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)) | ||
| Theorem | letri3i 11355 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)) | ||
| Theorem | leloei 11356 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)) | ||
| Theorem | ltleni 11357 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴)) | ||
| Theorem | ltnsymi 11358 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴) | ||
| Theorem | lenlti 11359 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴) | ||
| Theorem | ltnlei 11360 | 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴) | ||
| Theorem | ltlei 11361 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵) | ||
| Theorem | ltleii 11362 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≤ 𝐵 | ||
| Theorem | ltnei 11363 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 ≠ 𝐴) | ||
| Theorem | letrii 11364 | Trichotomy law for 'less than or equal to'. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴) | ||
| Theorem | lttri 11365 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) | ||
| Theorem | lelttri 11366 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) | ||
| Theorem | ltletri 11367 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) | ||
| Theorem | letri 11368 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶) | ||
| Theorem | le2tri3i 11369 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴)) | ||
| Theorem | ltadd2i 11370 | Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)) | ||
| Theorem | mulgt0i 11371 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) | ||
| Theorem | mulgt0ii 11372 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 · 𝐵) | ||
| Theorem | ltnrd 11373 | 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐴) | ||
| Theorem | gtned 11374 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
| Theorem | ltned 11375 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
| Theorem | ne0gt0d 11376 | A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
| Theorem | lttrid 11377 | Ordering on reals satisfies strict trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | lttri2d 11378 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | lttri3d 11379 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
| Theorem | lttri4d 11380 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴)) | ||
| Theorem | letri3d 11381 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
| Theorem | leloed 11382 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | ||
| Theorem | eqleltd 11383 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵))) | ||
| Theorem | ltlend 11384 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
| Theorem | lenltd 11385 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
| Theorem | ltnled 11386 | 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
| Theorem | ltled 11387 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | ltnsymd 11388 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) | ||
| Theorem | nltled 11389 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
| Theorem | lensymd 11390 | 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) | ||
| Theorem | letrid 11391 | Trichotomy law for 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
| Theorem | leltned 11392 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) | ||
| Theorem | leneltd 11393 | 'Less than or equal to' and 'not equals' implies 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
| Theorem | mulgt0d 11394 | The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 · 𝐵)) | ||
| Theorem | ltadd2d 11395 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) | ||
| Theorem | letrd 11396 | Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
| Theorem | lelttrd 11397 | Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | ltadd2dd 11398 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) | ||
| Theorem | ltletrd 11399 | Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | lttrd 11400 | Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |