![]() |
Metamath
Proof Explorer Theorem List (p. 124 of 473) | < 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-29758) |
![]() (29759-31281) |
![]() (31282-47222) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3p2e5 12301 | 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
⊢ (3 + 2) = 5 | ||
Theorem | 3p3e6 12302 | 3 + 3 = 6. (Contributed by NM, 11-May-2004.) |
⊢ (3 + 3) = 6 | ||
Theorem | 4p2e6 12303 | 4 + 2 = 6. (Contributed by NM, 11-May-2004.) |
⊢ (4 + 2) = 6 | ||
Theorem | 4p3e7 12304 | 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
⊢ (4 + 3) = 7 | ||
Theorem | 4p4e8 12305 | 4 + 4 = 8. (Contributed by NM, 11-May-2004.) |
⊢ (4 + 4) = 8 | ||
Theorem | 5p2e7 12306 | 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
⊢ (5 + 2) = 7 | ||
Theorem | 5p3e8 12307 | 5 + 3 = 8. (Contributed by NM, 11-May-2004.) |
⊢ (5 + 3) = 8 | ||
Theorem | 5p4e9 12308 | 5 + 4 = 9. (Contributed by NM, 11-May-2004.) |
⊢ (5 + 4) = 9 | ||
Theorem | 6p2e8 12309 | 6 + 2 = 8. (Contributed by NM, 11-May-2004.) |
⊢ (6 + 2) = 8 | ||
Theorem | 6p3e9 12310 | 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
⊢ (6 + 3) = 9 | ||
Theorem | 7p2e9 12311 | 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
⊢ (7 + 2) = 9 | ||
Theorem | 1t1e1 12312 | 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 · 1) = 1 | ||
Theorem | 2t1e2 12313 | 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (2 · 1) = 2 | ||
Theorem | 2t2e4 12314 | 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
⊢ (2 · 2) = 4 | ||
Theorem | 3t1e3 12315 | 3 times 1 equals 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (3 · 1) = 3 | ||
Theorem | 3t2e6 12316 | 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
⊢ (3 · 2) = 6 | ||
Theorem | 3t3e9 12317 | 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
⊢ (3 · 3) = 9 | ||
Theorem | 4t2e8 12318 | 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
⊢ (4 · 2) = 8 | ||
Theorem | 2t0e0 12319 | 2 times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 · 0) = 0 | ||
Theorem | 4d2e2 12320 | One half of four is two. (Contributed by NM, 3-Sep-1999.) |
⊢ (4 / 2) = 2 | ||
Theorem | 1lt2 12321 | 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
⊢ 1 < 2 | ||
Theorem | 2lt3 12322 | 2 is less than 3. (Contributed by NM, 26-Sep-2010.) |
⊢ 2 < 3 | ||
Theorem | 1lt3 12323 | 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
⊢ 1 < 3 | ||
Theorem | 3lt4 12324 | 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 4 | ||
Theorem | 2lt4 12325 | 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 4 | ||
Theorem | 1lt4 12326 | 1 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 4 | ||
Theorem | 4lt5 12327 | 4 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 5 | ||
Theorem | 3lt5 12328 | 3 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 5 | ||
Theorem | 2lt5 12329 | 2 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 5 | ||
Theorem | 1lt5 12330 | 1 is less than 5. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 5 | ||
Theorem | 5lt6 12331 | 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 < 6 | ||
Theorem | 4lt6 12332 | 4 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 6 | ||
Theorem | 3lt6 12333 | 3 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 6 | ||
Theorem | 2lt6 12334 | 2 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 6 | ||
Theorem | 1lt6 12335 | 1 is less than 6. (Contributed by NM, 19-Oct-2012.) |
⊢ 1 < 6 | ||
Theorem | 6lt7 12336 | 6 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 6 < 7 | ||
Theorem | 5lt7 12337 | 5 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 < 7 | ||
Theorem | 4lt7 12338 | 4 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 7 | ||
Theorem | 3lt7 12339 | 3 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 7 | ||
Theorem | 2lt7 12340 | 2 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 7 | ||
Theorem | 1lt7 12341 | 1 is less than 7. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 7 | ||
Theorem | 7lt8 12342 | 7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 7 < 8 | ||
Theorem | 6lt8 12343 | 6 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 6 < 8 | ||
Theorem | 5lt8 12344 | 5 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 5 < 8 | ||
Theorem | 4lt8 12345 | 4 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 4 < 8 | ||
Theorem | 3lt8 12346 | 3 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 3 < 8 | ||
Theorem | 2lt8 12347 | 2 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 2 < 8 | ||
Theorem | 1lt8 12348 | 1 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ 1 < 8 | ||
Theorem | 8lt9 12349 | 8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014.) |
⊢ 8 < 9 | ||
Theorem | 7lt9 12350 | 7 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 7 < 9 | ||
Theorem | 6lt9 12351 | 6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 6 < 9 | ||
Theorem | 5lt9 12352 | 5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 5 < 9 | ||
Theorem | 4lt9 12353 | 4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 4 < 9 | ||
Theorem | 3lt9 12354 | 3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 3 < 9 | ||
Theorem | 2lt9 12355 | 2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 2 < 9 | ||
Theorem | 1lt9 12356 | 1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) |
⊢ 1 < 9 | ||
Theorem | 0ne2 12357 | 0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 2 | ||
Theorem | 1ne2 12358 | 1 is not equal to 2. (Contributed by NM, 19-Oct-2012.) |
⊢ 1 ≠ 2 | ||
Theorem | 1le2 12359 | 1 is less than or equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 ≤ 2 | ||
Theorem | 2cnne0 12360 | 2 is a nonzero complex number. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ (2 ∈ ℂ ∧ 2 ≠ 0) | ||
Theorem | 2rene0 12361 | 2 is a nonzero real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 ∈ ℝ ∧ 2 ≠ 0) | ||
Theorem | 1le3 12362 | 1 is less than or equal to 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 ≤ 3 | ||
Theorem | neg1mulneg1e1 12363 | -1 · -1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (-1 · -1) = 1 | ||
Theorem | halfre 12364 | One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 / 2) ∈ ℝ | ||
Theorem | halfcn 12365 | One-half is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 / 2) ∈ ℂ | ||
Theorem | halfgt0 12366 | One-half is greater than zero. (Contributed by NM, 24-Feb-2005.) |
⊢ 0 < (1 / 2) | ||
Theorem | halfge0 12367 | One-half is not negative. (Contributed by AV, 7-Jun-2020.) |
⊢ 0 ≤ (1 / 2) | ||
Theorem | halflt1 12368 | One-half is less than one. (Contributed by NM, 24-Feb-2005.) |
⊢ (1 / 2) < 1 | ||
Theorem | 1mhlfehlf 12369 | Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ (1 − (1 / 2)) = (1 / 2) | ||
Theorem | 8th4div3 12370 | An eighth of four thirds is a sixth. (Contributed by Paul Chapman, 24-Nov-2007.) |
⊢ ((1 / 8) · (4 / 3)) = (1 / 6) | ||
Theorem | halfpm6th 12371 | One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008.) |
⊢ (((1 / 2) − (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 / 3)) | ||
Theorem | it0e0 12372 | i times 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (i · 0) = 0 | ||
Theorem | 2mulicn 12373 | (2 · i) ∈ ℂ. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 · i) ∈ ℂ | ||
Theorem | 2muline0 12374 | (2 · i) ≠ 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 · i) ≠ 0 | ||
Theorem | halfcl 12375 | Closure of half of a number. (Contributed by NM, 1-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈ ℂ) | ||
Theorem | rehalfcl 12376 | Real closure of half. (Contributed by NM, 1-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ) | ||
Theorem | half0 12377 | Half of a number is zero iff the number is zero. (Contributed by NM, 20-Apr-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) = 0 ↔ 𝐴 = 0)) | ||
Theorem | 2halves 12378 | Two halves make a whole. (Contributed by NM, 11-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) | ||
Theorem | halfpos2 12379 | A number is positive iff its half is positive. (Contributed by NM, 10-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ 0 < (𝐴 / 2))) | ||
Theorem | halfpos 12380 | A positive number is greater than its half. (Contributed by NM, 28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (𝐴 / 2) < 𝐴)) | ||
Theorem | halfnneg2 12381 | A number is nonnegative iff its half is nonnegative. (Contributed by NM, 9-Dec-2005.) |
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 2))) | ||
Theorem | halfaddsubcl 12382 | Closure of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) / 2) ∈ ℂ ∧ ((𝐴 − 𝐵) / 2) ∈ ℂ)) | ||
Theorem | halfaddsub 12383 | Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2)) = 𝐴 ∧ (((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)) = 𝐵)) | ||
Theorem | subhalfhalf 12384 | Subtracting the half of a number from the number yields the half of the number. (Contributed by AV, 28-Jun-2021.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − (𝐴 / 2)) = (𝐴 / 2)) | ||
Theorem | lt2halves 12385 | A sum is less than the whole if each term is less than half. (Contributed by NM, 13-Dec-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < (𝐶 / 2) ∧ 𝐵 < (𝐶 / 2)) → (𝐴 + 𝐵) < 𝐶)) | ||
Theorem | addltmul 12386 | Sum is less than product for numbers greater than 2. (Contributed by Stefan Allan, 24-Sep-2010.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵)) | ||
Theorem | nominpos 12387* | There is no smallest positive real number. (Contributed by NM, 28-Oct-2004.) |
⊢ ¬ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ¬ ∃𝑦 ∈ ℝ (0 < 𝑦 ∧ 𝑦 < 𝑥)) | ||
Theorem | avglt1 12388 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) | ||
Theorem | avglt2 12389 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) | ||
Theorem | avgle1 12390 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ ((𝐴 + 𝐵) / 2))) | ||
Theorem | avgle2 12391 | Ordering property for average. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ((𝐴 + 𝐵) / 2) ≤ 𝐵)) | ||
Theorem | avgle 12392 | The average of two numbers is less than or equal to at least one of them. (Contributed by NM, 9-Dec-2005.) (Revised by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + 𝐵) / 2) ≤ 𝐴 ∨ ((𝐴 + 𝐵) / 2) ≤ 𝐵)) | ||
Theorem | 2timesd 12393 | Two times a number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴)) | ||
Theorem | times2d 12394 | A number times 2. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 2) = (𝐴 + 𝐴)) | ||
Theorem | halfcld 12395 | Closure of half of a number (frequently used special case). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ) | ||
Theorem | 2halvesd 12396 | Two halves make a whole. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) | ||
Theorem | rehalfcld 12397 | Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ) | ||
Theorem | lt2halvesd 12398 | A sum is less than the whole if each term is less than half. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐶 / 2)) & ⊢ (𝜑 → 𝐵 < (𝐶 / 2)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < 𝐶) | ||
Theorem | rehalfcli 12399 | Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 / 2) ∈ ℝ | ||
Theorem | lt2addmuld 12400 | If two real numbers are less than a third real number, the sum of the two real numbers is less than twice the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (2 · 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |