Home | Metamath
Proof Explorer Theorem List (p. 113 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | le0neg2d 11201 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0)) | ||
Theorem | addgegt0d 11202 | Addition of nonnegative and positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgtge0d 11203 | Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgt0d 11204 | Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 + 𝐵)) | ||
Theorem | addge0d 11205 | Addition of 2 nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 + 𝐵)) | ||
Theorem | mulge0d 11206 | The product of two nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | ltnegd 11207 | Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) | ||
Theorem | lenegd 11208 | Negative of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)) | ||
Theorem | ltnegcon1d 11209 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → -𝐴 < 𝐵) ⇒ ⊢ (𝜑 → -𝐵 < 𝐴) | ||
Theorem | ltnegcon2d 11210 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < -𝐵) ⇒ ⊢ (𝜑 → 𝐵 < -𝐴) | ||
Theorem | lenegcon1d 11211 | Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → -𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → -𝐵 ≤ 𝐴) | ||
Theorem | lenegcon2d 11212 | Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ -𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ -𝐴) | ||
Theorem | ltaddposd 11213 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | ltaddpos2d 11214 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵))) | ||
Theorem | ltsubposd 11215 | Subtracting a positive number from another number decreases it. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵)) | ||
Theorem | posdifd 11216 | Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) | ||
Theorem | addge01d 11217 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵))) | ||
Theorem | addge02d 11218 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴))) | ||
Theorem | subge0d 11219 | Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | suble0d 11220 | Nonpositive subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | subge02d 11221 | Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴)) | ||
Theorem | ltadd1d 11222 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))) | ||
Theorem | leadd1d 11223 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))) | ||
Theorem | leadd2d 11224 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))) | ||
Theorem | ltsubaddd 11225 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) | ||
Theorem | lesubaddd 11226 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵))) | ||
Theorem | ltsubadd2d 11227 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | lesubadd2d 11228 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) | ||
Theorem | ltaddsubd 11229 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) | ||
Theorem | ltaddsub2d 11230 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) | ||
Theorem | leaddsub2d 11231 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) | ||
Theorem | subled 11232 | Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 − 𝐵) ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) ≤ 𝐵) | ||
Theorem | lesubd 11233 | Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ≤ (𝐵 − 𝐴)) | ||
Theorem | ltsub23d 11234 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 − 𝐵) < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) < 𝐵) | ||
Theorem | ltsub13d 11235 | 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐶 < (𝐵 − 𝐴)) | ||
Theorem | lesub1d 11236 | Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝐶) ≤ (𝐵 − 𝐶))) | ||
Theorem | lesub2d 11237 | Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴))) | ||
Theorem | ltsub1d 11238 | Subtraction from both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶))) | ||
Theorem | ltsub2d 11239 | Subtraction of both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴))) | ||
Theorem | ltadd1dd 11240 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) < (𝐵 + 𝐶)) | ||
Theorem | ltsub1dd 11241 | Subtraction from both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) < (𝐵 − 𝐶)) | ||
Theorem | ltsub2dd 11242 | Subtraction of both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 − 𝐵) < (𝐶 − 𝐴)) | ||
Theorem | leadd1dd 11243 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)) | ||
Theorem | leadd2dd 11244 | Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)) | ||
Theorem | lesub1dd 11245 | Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) ≤ (𝐵 − 𝐶)) | ||
Theorem | lesub2dd 11246 | Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 − 𝐵) ≤ (𝐶 − 𝐴)) | ||
Theorem | lesub3d 11247 | The result of subtracting a number less than or equal to an intermediate number from a number greater than or equal to a third number increased by the intermediate number is greater than or equal to the third number. (Contributed by AV, 13-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → (𝑋 + 𝐶) ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ≤ 𝑋) ⇒ ⊢ (𝜑 → 𝐶 ≤ (𝐴 − 𝐵)) | ||
Theorem | le2addd 11248 | Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) | ||
Theorem | le2subd 11249 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 − 𝐷) ≤ (𝐶 − 𝐵)) | ||
Theorem | ltleaddd 11250 | Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | leltaddd 11251 | Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | lt2addd 11252 | Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (𝐶 + 𝐷)) | ||
Theorem | lt2subd 11253 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐷) ⇒ ⊢ (𝜑 → (𝐴 − 𝐷) < (𝐶 − 𝐵)) | ||
Theorem | possumd 11254 | Condition for a positive sum. (Contributed by Scott Fenton, 16-Dec-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (0 < (𝐴 + 𝐵) ↔ -𝐵 < 𝐴)) | ||
Theorem | sublt0d 11255 | When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) < 0 ↔ 𝐴 < 𝐵)) | ||
Theorem | ltaddsublt 11256 | Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 ↔ ((𝐴 + 𝐵) − 𝐶) < 𝐴)) | ||
Theorem | 1le1 11257 | One is less than or equal to one. (Contributed by David A. Wheeler, 16-Jul-2016.) |
⊢ 1 ≤ 1 | ||
Theorem | ixi 11258 | i times itself is minus 1. (Contributed by NM, 6-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (i · i) = -1 | ||
Theorem | recextlem1 11259 | Lemma for recex 11261. (Contributed by Eric Schmidt, 23-May-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))) | ||
Theorem | recextlem2 11260 | Lemma for recex 11261. (Contributed by Eric Schmidt, 23-May-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) ≠ 0) → ((𝐴 · 𝐴) + (𝐵 · 𝐵)) ≠ 0) | ||
Theorem | recex 11261* | Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1) | ||
Theorem | mulcand 11262 | Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 26-Jan-1995.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | mulcan2d 11263 | Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | mulcanad 11264 | Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand 11262. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → (𝐶 · 𝐴) = (𝐶 · 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | mulcan2ad 11265 | Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcan2d 11263. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐵 · 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | mulcan 11266 | Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | mulcan2 11267 | Cancellation law for multiplication. (Contributed by NM, 21-Jan-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | mulcani 11268 | Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 26-Jan-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐶 ≠ 0 ⇒ ⊢ ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵) | ||
Theorem | mul0or 11269 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0))) | ||
Theorem | mulne0b 11270 | The product of two nonzero numbers is nonzero. (Contributed by NM, 1-Aug-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0)) | ||
Theorem | mulne0 11271 | The product of two nonzero numbers is nonzero. (Contributed by NM, 30-Dec-2007.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ≠ 0) | ||
Theorem | mulne0i 11272 | The product of two nonzero numbers is nonzero. (Contributed by NM, 15-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ≠ 0 ⇒ ⊢ (𝐴 · 𝐵) ≠ 0 | ||
Theorem | muleqadd 11273 | Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 13-Nov-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 + 𝐵) ↔ ((𝐴 − 1) · (𝐵 − 1)) = 1)) | ||
Theorem | receu 11274* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 17-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) | ||
Theorem | mulnzcnopr 11275 | Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.) |
⊢ ( · ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0}) | ||
Theorem | msq0i 11276 | A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0) | ||
Theorem | mul0ori 11277 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 7-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)) | ||
Theorem | msq0d 11278 | A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | mul0ord 11279 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0))) | ||
Theorem | mulne0bd 11280 | The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0)) | ||
Theorem | mulne0d 11281 | The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0) | ||
Theorem | mulcan1g 11282 | A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 · 𝐶) ↔ (𝐴 = 0 ∨ 𝐵 = 𝐶))) | ||
Theorem | mulcan2g 11283 | A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐶 = 0))) | ||
Theorem | mulne0bad 11284 | A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11281 and consequence of mulne0bd 11280. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | mulne0bbd 11285 | A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11281 and consequence of mulne0bd 11280. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐵 ≠ 0) | ||
Syntax | cdiv 11286 | Extend class notation to include division. |
class / | ||
Definition | df-div 11287* | Define division. Theorem divmuli 11383 relates it to multiplication, and divcli 11371 and redivcli 11396 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divval 11289 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.) |
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥)) | ||
Theorem | 1div0 11288 | You can't divide by zero, because division explicitly excludes zero from the domain of the function. Thus, by the definition of function value, it evaluates to the empty set. (This theorem is for information only and normally is not referenced by other proofs. To be meaningful, it assumes that ∅ is not a complex number, which depends on the particular complex number construction that is used.) (Contributed by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.) |
⊢ (1 / 0) = ∅ | ||
Theorem | divval 11289* | Value of division: if 𝐴 and 𝐵 are complex numbers with 𝐵 nonzero, then (𝐴 / 𝐵) is the (unique) complex number such that (𝐵 · 𝑥) = 𝐴. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) | ||
Theorem | divmul 11290 | Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 17-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴)) | ||
Theorem | divmul2 11291 | Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵))) | ||
Theorem | divmul3 11292 | Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶))) | ||
Theorem | divcl 11293 | Closure law for division. (Contributed by NM, 21-Jul-2001.) (Proof shortened by Mario Carneiro, 17-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ) | ||
Theorem | reccl 11294 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ) | ||
Theorem | divcan2 11295 | A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴) | ||
Theorem | divcan1 11296 | A cancellation law for division. (Contributed by NM, 5-Jun-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴) | ||
Theorem | diveq0 11297 | A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0)) | ||
Theorem | divne0b 11298 | The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0)) | ||
Theorem | divne0 11299 | The ratio of nonzero numbers is nonzero. (Contributed by NM, 28-Dec-2007.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ≠ 0) | ||
Theorem | recne0 11300 | The reciprocal of a nonzero number is nonzero. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ≠ 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |