Type  Label  Description 
Statement 

Theorem  ltsubadd 7501 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21Jan1997.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  ltsubadd2 7502 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21Jan1997.)



Theorem  lesubadd 7503 
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 17Nov2004.) (Proof shortened by Mario Carneiro,
27May2016.)



Theorem  lesubadd2 7504 
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10Aug1999.)



Theorem  ltaddsub 7505 
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17Nov2004.)



Theorem  ltaddsub2 7506 
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17Nov2004.)



Theorem  leaddsub 7507 
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6Apr2005.)



Theorem  leaddsub2 7508 
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6Apr2005.)



Theorem  suble 7509 
Swap subtrahends in an inequality. (Contributed by NM, 29Sep2005.)



Theorem  lesub 7510 
Swap subtrahends in an inequality. (Contributed by NM, 29Sep2005.)
(Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  ltsub23 7511 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4Oct1999.)



Theorem  ltsub13 7512 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17Nov2004.)



Theorem  le2add 7513 
Adding both sides of two 'less than or equal to' relations. (Contributed
by NM, 17Apr2005.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  lt2add 7514 
Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol]
p. 20. (Contributed by NM, 15Aug1999.) (Proof shortened by Mario
Carneiro, 27May2016.)



Theorem  ltleadd 7515 
Adding both sides of two orderings. (Contributed by NM, 23Dec2007.)



Theorem  leltadd 7516 
Adding both sides of two orderings. (Contributed by NM, 15Aug2008.)



Theorem  addgt0 7517 
The sum of 2 positive numbers is positive. (Contributed by NM,
1Jun2005.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  addgegt0 7518 
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28Dec2005.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  addgtge0 7519 
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28Dec2005.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  addge0 7520 
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17Mar2005.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  ltaddpos 7521 
Adding a positive number to another number increases it. (Contributed by
NM, 17Nov2004.)



Theorem  ltaddpos2 7522 
Adding a positive number to another number increases it. (Contributed by
NM, 8Apr2005.)



Theorem  ltsubpos 7523 
Subtracting a positive number from another number decreases it.
(Contributed by NM, 17Nov2004.) (Proof shortened by Andrew Salmon,
19Nov2011.)



Theorem  posdif 7524 
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17Nov2004.)



Theorem  lesub1 7525 
Subtraction from both sides of 'less than or equal to'. (Contributed by
NM, 13May2004.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  lesub2 7526 
Subtraction of both sides of 'less than or equal to'. (Contributed by NM,
29Sep2005.) (Revised by Mario Carneiro, 27May2016.)



Theorem  ltsub1 7527 
Subtraction from both sides of 'less than'. (Contributed by FL,
3Jan2008.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  ltsub2 7528 
Subtraction of both sides of 'less than'. (Contributed by NM,
29Sep2005.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  lt2sub 7529 
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14Apr2016.)



Theorem  le2sub 7530 
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14Apr2016.)



Theorem  ltneg 7531 
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 27Aug1999.) (Proof shortened by Mario Carneiro,
27May2016.)



Theorem  ltnegcon1 7532 
Contraposition of negative in 'less than'. (Contributed by NM,
8Nov2004.)



Theorem  ltnegcon2 7533 
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25Feb2015.)



Theorem  leneg 7534 
Negative of both sides of 'less than or equal to'. (Contributed by NM,
12Sep1999.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  lenegcon1 7535 
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10May2004.)



Theorem  lenegcon2 7536 
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8Oct2005.)



Theorem  lt0neg1 7537 
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14May1999.)



Theorem  lt0neg2 7538 
Comparison of a number and its negative to zero. (Contributed by NM,
10May2004.)



Theorem  le0neg1 7539 
Comparison of a number and its negative to zero. (Contributed by NM,
10May2004.)



Theorem  le0neg2 7540 
Comparison of a number and its negative to zero. (Contributed by NM,
24Aug1999.)



Theorem  addge01 7541 
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21Feb2005.)



Theorem  addge02 7542 
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27Jul2005.)



Theorem  add20 7543 
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
Jeff Madsen, 2Sep2009.) (Proof shortened by Mario Carneiro,
27May2016.)



Theorem  subge0 7544 
Nonnegative subtraction. (Contributed by NM, 14Mar2005.) (Proof
shortened by Mario Carneiro, 27May2016.)



Theorem  suble0 7545 
Nonpositive subtraction. (Contributed by NM, 20Mar2008.) (Proof
shortened by Mario Carneiro, 27May2016.)



Theorem  leaddle0 7546 
The sum of a real number and a second real number is less then the real
number iff the second real number is negative. (Contributed by Alexander
van der Vekens, 30May2018.)



Theorem  subge02 7547 
Nonnegative subtraction. (Contributed by NM, 27Jul2005.)



Theorem  lesub0 7548 
Lemma to show a nonnegative number is zero. (Contributed by NM,
8Oct1999.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  mullt0 7549 
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8Jun2009.)



Theorem  0le1 7550 
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29Apr2015.)



Theorem  leidi 7551 
'Less than or equal to' is reflexive. (Contributed by NM,
18Aug1999.)



Theorem  gt0ne0i 7552 
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16Sep1999.)



Theorem  gt0ne0ii 7553 
Positive implies nonzero. (Contributed by NM, 15May1999.)



Theorem  addgt0i 7554 
Addition of 2 positive numbers is positive. (Contributed by NM,
16May1999.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  addge0i 7555 
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28May1999.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  addgegt0i 7556 
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25Sep1999.) (Revised by Mario Carneiro, 27May2016.)



Theorem  addgt0ii 7557 
Addition of 2 positive numbers is positive. (Contributed by NM,
18May1999.)



Theorem  add20i 7558 
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28Jul1999.)



Theorem  ltnegi 7559 
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21Jan1997.)



Theorem  lenegi 7560 
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1Aug1999.)



Theorem  ltnegcon2i 7561 
Contraposition of negative in 'less than'. (Contributed by NM,
14May1999.)



Theorem  lesub0i 7562 
Lemma to show a nonnegative number is zero. (Contributed by NM,
8Oct1999.) (Proof shortened by Andrew Salmon, 19Nov2011.)



Theorem  ltaddposi 7563 
Adding a positive number to another number increases it. (Contributed
by NM, 25Aug1999.)



Theorem  posdifi 7564 
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19Aug2001.)



Theorem  ltnegcon1i 7565 
Contraposition of negative in 'less than'. (Contributed by NM,
14May1999.)



Theorem  lenegcon1i 7566 
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 6Apr2005.)



Theorem  subge0i 7567 
Nonnegative subtraction. (Contributed by NM, 13Aug2000.)



Theorem  ltadd1i 7568 
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by NM, 21Jan1997.)



Theorem  leadd1i 7569 
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11Aug1999.)



Theorem  leadd2i 7570 
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11Aug1999.)



Theorem  ltsubaddi 7571 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21Jan1997.) (Proof shortened by Andrew Salmon,
19Nov2011.)



Theorem  lesubaddi 7572 
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 30Sep1999.) (Proof shortened by Andrew Salmon,
19Nov2011.)



Theorem  ltsubadd2i 7573 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21Jan1997.)



Theorem  lesubadd2i 7574 
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3Aug1999.)



Theorem  ltaddsubi 7575 
'Less than' relationship between subtraction and addition. (Contributed
by NM, 14May1999.)



Theorem  lt2addi 7576 
Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
(Contributed by NM, 14May1999.)



Theorem  le2addi 7577 
Adding both side of two inequalities. (Contributed by NM,
16Sep1999.)



Theorem  gt0ne0d 7578 
Positive implies nonzero. (Contributed by Mario Carneiro,
27May2016.)



Theorem  lt0ne0d 7579 
Something less than zero is not zero. Deduction form. (Contributed by
David Moews, 28Feb2017.)



Theorem  leidd 7580 
'Less than or equal to' is reflexive. (Contributed by Mario Carneiro,
27May2016.)



Theorem  lt0neg1d 7581 
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  lt0neg2d 7582 
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  le0neg1d 7583 
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  le0neg2d 7584 
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  addgegt0d 7585 
Addition of nonnegative and positive numbers is positive.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  addgt0d 7586 
Addition of 2 positive numbers is positive. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  addge0d 7587 
Addition of 2 nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27May2016.)



Theorem  ltnegd 7588 
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  lenegd 7589 
Negative of both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27May2016.)



Theorem  ltnegcon1d 7590 
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  ltnegcon2d 7591 
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  lenegcon1d 7592 
Contraposition of negative in 'less than or equal to'. (Contributed
by Mario Carneiro, 27May2016.)



Theorem  lenegcon2d 7593 
Contraposition of negative in 'less than or equal to'. (Contributed
by Mario Carneiro, 27May2016.)



Theorem  ltaddposd 7594 
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 27May2016.)



Theorem  ltaddpos2d 7595 
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 27May2016.)



Theorem  ltsubposd 7596 
Subtracting a positive number from another number decreases it.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  posdifd 7597 
Comparison of two numbers whose difference is positive. (Contributed by
Mario Carneiro, 27May2016.)



Theorem  addge01d 7598 
A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  addge02d 7599 
A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  subge0d 7600 
Nonnegative subtraction. (Contributed by Mario Carneiro,
27May2016.)

