Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



3.3.4 Ordering on reals (cont.)


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



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



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



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



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



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



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



Theorem  ltadd1 7219 
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 7220 
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 7221 
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26Oct1999.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

