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