Home | Metamath
Proof Explorer Theorem List (p. 112 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lesubadd2 11101 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) | ||
Theorem | ltaddsub 11102 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) | ||
Theorem | ltaddsub2 11103 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) | ||
Theorem | leaddsub 11104 | 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵))) | ||
Theorem | leaddsub2 11105 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) | ||
Theorem | suble 11106 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵)) | ||
Theorem | lesub 11107 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴))) | ||
Theorem | ltsub23 11108 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵)) | ||
Theorem | ltsub13 11109 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴))) | ||
Theorem | le2add 11110 | Adding both sides of two 'less than or equal to' relations. (Contributed by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) | ||
Theorem | ltleadd 11111 | Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) | ||
Theorem | leltadd 11112 | Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) | ||
Theorem | lt2add 11113 | Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) | ||
Theorem | addgt0 11114 | The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgegt0 11115 | The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgtge0 11116 | The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ 𝐵)) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addge0 11117 | The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) | ||
Theorem | ltaddpos 11118 | Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | ltaddpos2 11119 | Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵))) | ||
Theorem | ltsubpos 11120 | Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵)) | ||
Theorem | posdif 11121 | Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) | ||
Theorem | lesub1 11122 | Subtraction from both sides of 'less than or equal to'. (Contributed by NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝐶) ≤ (𝐵 − 𝐶))) | ||
Theorem | lesub2 11123 | Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴))) | ||
Theorem | ltsub1 11124 | Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶))) | ||
Theorem | ltsub2 11125 | Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴))) | ||
Theorem | lt2sub 11126 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷))) | ||
Theorem | le2sub 11127 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷))) | ||
Theorem | ltneg 11128 | Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) | ||
Theorem | ltnegcon1 11129 | Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)) | ||
Theorem | ltnegcon2 11130 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)) | ||
Theorem | leneg 11131 | Negative of both sides of 'less than or equal to'. (Contributed by NM, 12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)) | ||
Theorem | lenegcon1 11132 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) | ||
Theorem | lenegcon2 11133 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) | ||
Theorem | lt0neg1 11134 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < -𝐴)) | ||
Theorem | lt0neg2 11135 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0)) | ||
Theorem | le0neg1 11136 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) | ||
Theorem | le0neg2 11137 | Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.) |
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0)) | ||
Theorem | addge01 11138 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵))) | ||
Theorem | addge02 11139 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴))) | ||
Theorem | add20 11140 | Two nonnegative numbers are zero iff their sum is zero. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) | ||
Theorem | subge0 11141 | Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | suble0 11142 | Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | leaddle0 11143 | The sum of a real number and a second real number is less than the real number iff the second real number is negative. (Contributed by Alexander van der Vekens, 30-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐴 ↔ 𝐵 ≤ 0)) | ||
Theorem | subge02 11144 | Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴)) | ||
Theorem | lesub0 11145 | Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0)) | ||
Theorem | mulge0 11146 | The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | mullt0 11147 | The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 𝐵 < 0)) → 0 < (𝐴 · 𝐵)) | ||
Theorem | msqgt0 11148 | A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by NM, 6-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴 · 𝐴)) | ||
Theorem | msqge0 11149 | A square is nonnegative. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴)) | ||
Theorem | 0lt1 11150 | 0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.) |
⊢ 0 < 1 | ||
Theorem | 0le1 11151 | 0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ 0 ≤ 1 | ||
Theorem | relin01 11152 | An interval law for less than or equal. (Contributed by Scott Fenton, 27-Jun-2013.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ∨ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1) ∨ 1 ≤ 𝐴)) | ||
Theorem | ltordlem 11153* | Lemma for ltord1 11154. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 → 𝑀 < 𝑁)) | ||
Theorem | ltord1 11154* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑀 < 𝑁)) | ||
Theorem | leord1 11155* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 ≤ 𝐷 ↔ 𝑀 ≤ 𝑁)) | ||
Theorem | eqord1 11156* | A strictly increasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁)) | ||
Theorem | ltord2 11157* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑁 < 𝑀)) | ||
Theorem | leord2 11158* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 ≤ 𝐷 ↔ 𝑁 ≤ 𝑀)) | ||
Theorem | eqord2 11159* | A strictly decreasing real function on a subset of ℝ is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) & ⊢ 𝑆 ⊆ ℝ & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐵 < 𝐴)) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 ↔ 𝑀 = 𝑁)) | ||
Theorem | wloglei 11160* | Form of wlogle 11161 where both sides of the equivalence are proven rather than showing that they are equivalent to each other. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → 𝑆 ⊆ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦)) → 𝜃) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝜒) | ||
Theorem | wlogle 11161* | If the predicate 𝜒(𝑥, 𝑦) is symmetric under interchange of 𝑥, 𝑦, then "without loss of generality" we can assume that 𝑥 ≤ 𝑦. (Contributed by Mario Carneiro, 18-Aug-2014.) (Revised by Mario Carneiro, 11-Sep-2014.) |
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → 𝑆 ⊆ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝜒) | ||
Theorem | leidi 11162 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ≤ 𝐴 | ||
Theorem | gt0ne0i 11163 | Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 < 𝐴 → 𝐴 ≠ 0) | ||
Theorem | gt0ne0ii 11164 | Positive implies nonzero. (Contributed by NM, 15-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ≠ 0 | ||
Theorem | msqgt0i 11165 | A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≠ 0 → 0 < (𝐴 · 𝐴)) | ||
Theorem | msqge0i 11166 | A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 0 ≤ (𝐴 · 𝐴) | ||
Theorem | addgt0i 11167 | Addition of 2 positive numbers is positive. (Contributed by NM, 16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addge0i 11168 | Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM, 28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 + 𝐵)) | ||
Theorem | addgegt0i 11169 | Addition of nonnegative and positive numbers is positive. (Contributed by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgt0ii 11170 | Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 + 𝐵) | ||
Theorem | add20i 11171 | Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) | ||
Theorem | ltnegi 11172 | Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ -𝐵 < -𝐴) | ||
Theorem | lenegi 11173 | Negative of both sides of 'less than or equal to'. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴) | ||
Theorem | ltnegcon2i 11174 | Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < -𝐵 ↔ 𝐵 < -𝐴) | ||
Theorem | mulge0i 11175 | The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | lesub0i 11176 | Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0) | ||
Theorem | ltaddposi 11177 | Adding a positive number to another number increases it. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)) | ||
Theorem | posdifi 11178 | Comparison of two numbers whose difference is positive. (Contributed by NM, 19-Aug-2001.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)) | ||
Theorem | ltnegcon1i 11179 | Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴) | ||
Theorem | lenegcon1i 11180 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴) | ||
Theorem | subge0i 11181 | Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴) | ||
Theorem | ltadd1i 11182 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)) | ||
Theorem | leadd1i 11183 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)) | ||
Theorem | leadd2i 11184 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)) | ||
Theorem | ltsubaddi 11185 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵)) | ||
Theorem | lesubaddi 11186 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵)) | ||
Theorem | ltsubadd2i 11187 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)) | ||
Theorem | lesubadd2i 11188 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶)) | ||
Theorem | ltaddsubi 11189 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵)) | ||
Theorem | lt2addi 11190 | Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | le2addi 11191 | Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) | ||
Theorem | gt0ne0d 11192 | Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | lt0ne0d 11193 | Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | leidd 11194 | 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) | ||
Theorem | msqgt0d 11195 | A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → 0 < (𝐴 · 𝐴)) | ||
Theorem | msqge0d 11196 | A square is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐴)) | ||
Theorem | lt0neg1d 11197 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 0 ↔ 0 < -𝐴)) | ||
Theorem | lt0neg2d 11198 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ -𝐴 < 0)) | ||
Theorem | le0neg1d 11199 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) | ||
Theorem | le0neg2d 11200 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |