![]() |
Metamath
Proof Explorer Theorem List (p. 122 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lemul1a 12101 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) | ||
Theorem | lemul2a 12102 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) | ||
Theorem | ltmul12a 12103 | Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.) |
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (𝐴 · 𝐶) < (𝐵 · 𝐷)) | ||
Theorem | lemul12b 12104 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) | ||
Theorem | lemul12a 12105 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ ((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) | ||
Theorem | mulgt1 12106 | The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵)) | ||
Theorem | ltmulgt11 12107 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐴 · 𝐵))) | ||
Theorem | ltmulgt12 12108 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐵 · 𝐴))) | ||
Theorem | lemulge11 12109 | Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐴 · 𝐵)) | ||
Theorem | lemulge12 12110 | Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐵 · 𝐴)) | ||
Theorem | ltdiv1 12111 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) | ||
Theorem | lediv1 12112 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))) | ||
Theorem | gt0div 12113 | Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵))) | ||
Theorem | ge0div 12114 | Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) | ||
Theorem | divgt0 12115 | The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 / 𝐵)) | ||
Theorem | divge0 12116 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) | ||
Theorem | mulge0b 12117 | A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 · 𝐵) ↔ ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))) | ||
Theorem | mulle0b 12118 | A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) ≤ 0 ↔ ((𝐴 ≤ 0 ∧ 0 ≤ 𝐵) ∨ (0 ≤ 𝐴 ∧ 𝐵 ≤ 0)))) | ||
Theorem | mulsuble0b 12119 | A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 − 𝐵) · (𝐶 − 𝐵)) ≤ 0 ↔ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ (𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))) | ||
Theorem | ltmuldiv 12120 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltmuldiv2 12121 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltdivmul 12122 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) | ||
Theorem | ledivmul 12123 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵))) | ||
Theorem | ltdivmul2 12124 | 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) | ||
Theorem | lt2mul2div 12125 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) | ||
Theorem | ledivmul2 12126 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶))) | ||
Theorem | lemuldiv 12127 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | lemuldiv2 12128 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | ltrec 12129 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) | ||
Theorem | lerec 12130 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) | ||
Theorem | lt2msq1 12131 | Lemma for lt2msq 12132. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴 · 𝐴) < (𝐵 · 𝐵)) | ||
Theorem | lt2msq 12132 | Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵))) | ||
Theorem | ltdiv2 12133 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) | ||
Theorem | ltrec1 12134 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((1 / 𝐴) < 𝐵 ↔ (1 / 𝐵) < 𝐴)) | ||
Theorem | lerec2 12135 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 ≤ (1 / 𝐵) ↔ 𝐵 ≤ (1 / 𝐴))) | ||
Theorem | ledivdiv 12136 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (𝐷 / 𝐶) ≤ (𝐵 / 𝐴))) | ||
Theorem | lediv2 12137 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) | ||
Theorem | ltdiv23 12138 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) | ||
Theorem | lediv23 12139 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ (𝐴 / 𝐶) ≤ 𝐵)) | ||
Theorem | lediv12a 12140 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) | ||
Theorem | lediv2a 12141 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)) | ||
Theorem | reclt1 12142 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (𝐴 < 1 ↔ 1 < (1 / 𝐴))) | ||
Theorem | recgt1 12143 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐴 ↔ (1 / 𝐴) < 1)) | ||
Theorem | recgt1i 12144 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (0 < (1 / 𝐴) ∧ (1 / 𝐴) < 1)) | ||
Theorem | recp1lt1 12145 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 / (1 + 𝐴)) < 1) | ||
Theorem | recreclt 12146 | Given a positive number 𝐴, construct a new positive number less than both 𝐴 and 1. (Contributed by NM, 28-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ((1 / (1 + (1 / 𝐴))) < 1 ∧ (1 / (1 + (1 / 𝐴))) < 𝐴)) | ||
Theorem | le2msq 12147 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵))) | ||
Theorem | msq11 12148 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | ledivp1 12149 | "Less than or equal to" and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ 𝐴) | ||
Theorem | squeeze0 12150* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0) | ||
Theorem | ltp1i 12151 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 < (𝐴 + 1) | ||
Theorem | recgt0i 12152 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 < 𝐴 → 0 < (1 / 𝐴)) | ||
Theorem | recgt0ii 12153 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 0 < (1 / 𝐴) | ||
Theorem | prodgt0i 12154 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵)) → 0 < 𝐵) | ||
Theorem | divgt0i 12155 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 / 𝐵)) | ||
Theorem | divge0i 12156 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 ≤ (𝐴 / 𝐵)) | ||
Theorem | ltreci 12157 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) | ||
Theorem | lereci 12158 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) | ||
Theorem | lt2msqi 12159 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐴) < (𝐵 · 𝐵))) | ||
Theorem | le2msqi 12160 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵))) | ||
Theorem | msq11i 12161 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 · 𝐴) = (𝐵 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | divgt0i2i 12162 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐵 ⇒ ⊢ (0 < 𝐴 → 0 < (𝐴 / 𝐵)) | ||
Theorem | ltrecii 12163 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)) | ||
Theorem | divgt0ii 12164 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 / 𝐵) | ||
Theorem | ltmul1i 12165 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) | ||
Theorem | ltdiv1i 12166 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) | ||
Theorem | ltmuldivi 12167 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (0 < 𝐶 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltmul2i 12168 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) | ||
Theorem | lemul1i 12169 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) | ||
Theorem | lemul2i 12170 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (0 < 𝐶 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) | ||
Theorem | ltdiv23i 12171 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((0 < 𝐵 ∧ 0 < 𝐶) → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) | ||
Theorem | ledivp1i 12172 | "Less than or equal to" and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · 𝐶) ≤ 𝐵) | ||
Theorem | ltdivp1i 12173 | Less-than and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 < (𝐵 / (𝐶 + 1))) → (𝐴 · 𝐶) < 𝐵) | ||
Theorem | ltdiv23ii 12174 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 0 < 𝐵 & ⊢ 0 < 𝐶 ⇒ ⊢ ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵) | ||
Theorem | ltmul1ii 12175 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 0 < 𝐶 ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)) | ||
Theorem | ltdiv1ii 12176 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 0 < 𝐶 ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)) | ||
Theorem | ltp1d 12177 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 < (𝐴 + 1)) | ||
Theorem | lep1d 12178 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1)) | ||
Theorem | ltm1d 12179 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 − 1) < 𝐴) | ||
Theorem | lem1d 12180 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 − 1) ≤ 𝐴) | ||
Theorem | recgt0d 12181 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 0 < (1 / 𝐴)) | ||
Theorem | divgt0d 12182 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 / 𝐵)) | ||
Theorem | mulgt1d 12183 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 1 < 𝐵) ⇒ ⊢ (𝜑 → 1 < (𝐴 · 𝐵)) | ||
Theorem | lemulge11d 12184 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 1 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 · 𝐵)) | ||
Theorem | lemulge12d 12185 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 1 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐵 · 𝐴)) | ||
Theorem | lemul1ad 12186 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) | ||
Theorem | lemul2ad 12187 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) | ||
Theorem | ltmul12ad 12188 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐷)) | ||
Theorem | lemul12ad 12189 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)) | ||
Theorem | lemul12bd 12190 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐷) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)) | ||
Theorem | fimaxre 12191* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Steven Nguyen, 3-Jun-2023.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) | ||
Theorem | fimaxre2 12192* | A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) | ||
Theorem | fimaxre3 12193* | A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑦 ∈ 𝐴 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝐵 ≤ 𝑥) | ||
Theorem | fiminre 12194* | A nonempty finite set of real numbers has a minimum. Analogous to fimaxre 12191. (Contributed by AV, 9-Aug-2020.) (Proof shortened by Steven Nguyen, 3-Jun-2023.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | fiminre2 12195* | A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | negfi 12196* | The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin) | ||
Theorem | lbreu 12197* | If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.) |
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ∃!𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) | ||
Theorem | lbcl 12198* | If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆) | ||
Theorem | lble 12199* | If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ≤ 𝐴) | ||
Theorem | lbinf 12200* | If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → inf(𝑆, ℝ, < ) = (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |