HomeTheorem List (p. 106 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 106 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lesubadd2 10501 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.) |
     ![/\](wedge.gif "/\"){kind=small}     
 
 | ||
| Theorem | ltaddsub 10502 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
| ||
| Theorem | ltaddsub2 10503 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | leaddsub 10504 | 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
|
| ||
| Theorem | leaddsub2 10505 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
|
| ||
| Theorem | suble 10506 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) |
|
| ||
| Theorem | lesub 10507 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | ltsub23 10508 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.) |
|
| ||
| Theorem | ltsub13 10509 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | le2add 10510 | 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 10511 | Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.) |
|
| ||
| Theorem | leltadd 10512 | Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.) |
|
| ||
| Theorem | lt2add 10513 | 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 10514 | The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ||
| Theorem | addgegt0 10515 | The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | addgtge0 10516 | The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | addge0 10517 | The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | ltaddpos 10518 | Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.) |
| | ||
| Theorem | ltaddpos2 10519 | Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.) |
| | ||
| Theorem | ltsubpos 10520 | Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| | ||
| Theorem | posdif 10521 | Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | lesub1 10522 | 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 10523 | 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 10524 | Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | ltsub2 10525 | Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | lt2sub 10526 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
|
| ||
| Theorem | le2sub 10527 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
|
| ||
| Theorem | ltneg 10528 | 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 10529 | Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.) |
| | ||
| Theorem | ltnegcon2 10530 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.) |
|
| ||
| Theorem | leneg 10531 | 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 10532 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | lenegcon2 10533 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.) |
|
| ||
| Theorem | lt0neg1 10534 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
| | ||
| Theorem | lt0neg2 10535 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | le0neg1 10536 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | le0neg2 10537 | Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.) |
| | ||
| Theorem | addge01 10538 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
|
| ||
| Theorem | addge02 10539 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.) |
|
| ||
| Theorem | add20 10540 | 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.) |
| ||
| Theorem | subge0 10541 | Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | suble0 10542 | Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | leaddle0 10543 | 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.) |
|
| ||
| Theorem | subge02 10544 | Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.) |
| | ||
| Theorem | lesub0 10545 | Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | mulge0 10546 | The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
 | ||
| Theorem | mullt0 10547 | The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.) |
|
| ||
| Theorem | msqgt0 10548 | 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.) |
| ||
| Theorem | msqge0 10549 | A square is nonnegative. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | 0lt1 10550 | 0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.) |
 | ||
| Theorem | 0le1 10551 | 0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.) |
|
| ||
| Theorem | relin01 10552 | An interval law for less than or equal. (Contributed by Scott Fenton, 27-Jun-2013.) |
| ||
| Theorem | ltordlem 10553* | Lemma for ltord1 10554. (Contributed by Mario Carneiro, 14-Jun-2014.) |
  
   
| ||
| Theorem | ltord1 10554* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
|
| ||
| Theorem | leord1 10555* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
|
| ||
| Theorem | eqord1 10556* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
|
| ||
| Theorem | ltord2 10557* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
|
| ||
| Theorem | leord2 10558* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
|
| ||
| Theorem | eqord2 10559* | Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.) |
|
| ||
| Theorem | wloglei 10560* | Form of wlogle 10561 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 10561* |
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 10562 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
| | ||
| Theorem | gt0ne0i 10563 | Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.) |
| | ||
| Theorem | gt0ne0ii 10564 | Positive implies nonzero. (Contributed by NM, 15-May-1999.) |
| | ||
| Theorem | msqgt0i 10565 | 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.) |
| | ||
| Theorem | msqge0i 10566 | A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| | ||
| Theorem | addgt0i 10567 | Addition of 2 positive numbers is positive. (Contributed by NM, 16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | addge0i 10568 | Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM, 28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | addgegt0i 10569 | Addition of nonnegative and positive numbers is positive. (Contributed by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | addgt0ii 10570 | Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999.) |
| | ||
| Theorem | add20i 10571 | Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999.) |
| | ||
| Theorem | ltnegi 10572 | Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.) |
| | ||
| Theorem | lenegi 10573 | Negative of both sides of 'less than or equal to'. (Contributed by NM, 1-Aug-1999.) |
| | ||
| Theorem | ltnegcon2i 10574 | Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.) |
| | ||
| Theorem | mulge0i 10575 | The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.) |
| | ||
| Theorem | lesub0i 10576 | Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | ltaddposi 10577 | Adding a positive number to another number increases it. (Contributed by NM, 25-Aug-1999.) |
| | ||
| Theorem | posdifi 10578 | Comparison of two numbers whose difference is positive. (Contributed by NM, 19-Aug-2001.) |
| | ||
| Theorem | ltnegcon1i 10579 | Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.) |
| | ||
| Theorem | lenegcon1i 10580 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.) |
| | ||
| Theorem | subge0i 10581 | Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.) |
|
| ||
| Theorem | ltadd1i 10582 | Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.) |
|
| ||
| Theorem | leadd1i 10583 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.) |
|
| ||
| Theorem | leadd2i 10584 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.) |
|
| ||
| Theorem | ltsubaddi 10585 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | lesubaddi 10586 | '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 10587 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) |
|
| ||
| Theorem | lesubadd2i 10588 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.) |
|
| ||
| Theorem | ltaddsubi 10589 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.) |
|
| ||
| Theorem | lt2addi 10590 | Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
|
| ||
| Theorem | le2addi 10591 | Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.) |
|
| ||
| Theorem | gt0ne0d 10592 | Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | lt0ne0d 10593 | Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
| | ||
| Theorem | leidd 10594 | 'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | msqgt0d 10595 | A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | msqge0d 10596 | A square is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | lt0neg1d 10597 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | lt0neg2d 10598 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | le0neg1d 10599 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | le0neg2d 10600 | Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |