Type  Label  Description 
Statement 

Theorem  mulneg1i 7401 
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 10Feb1995.) (Revised by Mario Carneiro,
27May2016.)



Theorem  mulneg2i 7402 
Product with negative is negative of product. (Contributed by NM,
31Jul1999.) (Revised by Mario Carneiro, 27May2016.)



Theorem  mul2negi 7403 
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by NM, 14Feb1995.) (Revised by Mario Carneiro,
27May2016.)



Theorem  subdii 7404 
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26Nov1994.)



Theorem  subdiri 7405 
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8May1999.)



Theorem  muladdi 7406 
Product of two sums. (Contributed by NM, 17May1999.)



Theorem  mulm1d 7407 
Product with minus one is negative. (Contributed by Mario Carneiro,
27May2016.)



Theorem  mulneg1d 7408 
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27May2016.)



Theorem  mulneg2d 7409 
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  mul2negd 7410 
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  subdid 7411 
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  subdird 7412 
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  muladdd 7413 
Product of two sums. (Contributed by Mario Carneiro, 27May2016.)



Theorem  mulsubd 7414 
Product of two differences. (Contributed by Mario Carneiro,
27May2016.)



Theorem  mulsubfacd 7415 
Multiplication followed by the subtraction of a factor. (Contributed by
Alexander van der Vekens, 28Aug2018.)



3.3.4 Ordering on reals (cont.)


Theorem  ltadd2 7416 
Addition to both sides of 'less than'. (Contributed by NM,
12Nov1999.) (Revised by Mario Carneiro, 27May2016.)



Theorem  ltadd2i 7417 
Addition to both sides of 'less than'. (Contributed by NM,
21Jan1997.)



Theorem  ltadd2d 7418 
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27May2016.)



Theorem  ltadd2dd 7419 
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30May2016.)



Theorem  ltletrd 7420 
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9Jan2006.)



Theorem  lelttrdi 7421 
If a number is less than another number, and the other number is less
than or equal to a third number, the first number is less than the third
number. (Contributed by Alexander van der Vekens, 24Mar2018.)



Theorem  gt0ne0 7422 
Positive implies nonzero. (Contributed by NM, 3Oct1999.) (Proof
shortened by Mario Carneiro, 27May2016.)



Theorem  lt0ne0 7423 
A number which is less than zero is not zero. (Contributed by Stefan
O'Rear, 13Sep2014.)



Theorem  ltadd1 7424 
Addition to both sides of 'less than'. Part of definition 11.2.7(vi) of
[HoTT], p. (varies). (Contributed by NM,
12Nov1999.) (Proof shortened
by Mario Carneiro, 27May2016.)



Theorem  leadd1 7425 
Addition to both sides of 'less than or equal to'. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 18Oct1999.)
(Proof shortened by Mario Carneiro, 27May2016.)



Theorem  leadd2 7426 
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26Oct1999.)



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  lt2add 7440 
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 7441 
Adding both sides of two orderings. (Contributed by NM, 23Dec2007.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ltneg 7457 
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 7458 
Contraposition of negative in 'less than'. (Contributed by NM,
8Nov2004.)



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  leaddle0 7472 
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 7473 
Nonnegative subtraction. (Contributed by NM, 27Jul2005.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

