Type | Label | Description |
Statement |
|
Theorem | lt2add 8401 |
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 | ltleadd 8402 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด < ๐ถ โง ๐ต โค ๐ท) โ (๐ด + ๐ต) < (๐ถ + ๐ท))) |
|
Theorem | leltadd 8403 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โค ๐ถ โง ๐ต < ๐ท) โ (๐ด + ๐ต) < (๐ถ + ๐ท))) |
|
Theorem | addgt0 8404 |
The sum of 2 positive numbers is positive. (Contributed by NM,
1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 < ๐ด โง 0 < ๐ต)) โ 0 < (๐ด + ๐ต)) |
|
Theorem | addgegt0 8405 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง 0 < ๐ต)) โ 0 < (๐ด + ๐ต)) |
|
Theorem | addgtge0 8406 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 < ๐ด โง 0 โค ๐ต)) โ 0 < (๐ด + ๐ต)) |
|
Theorem | addge0 8407 |
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด + ๐ต)) |
|
Theorem | ltaddpos 8408 |
Adding a positive number to another number increases it. (Contributed by
NM, 17-Nov-2004.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 < ๐ด โ ๐ต < (๐ต + ๐ด))) |
|
Theorem | ltaddpos2 8409 |
Adding a positive number to another number increases it. (Contributed by
NM, 8-Apr-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 < ๐ด โ ๐ต < (๐ด + ๐ต))) |
|
Theorem | ltsubpos 8410 |
Subtracting a positive number from another number decreases it.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 < ๐ด โ (๐ต โ ๐ด) < ๐ต)) |
|
Theorem | posdif 8411 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17-Nov-2004.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
|
Theorem | lesub1 8412 |
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 8413 |
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 8414 |
Subtraction from both sides of 'less than'. (Contributed by FL,
3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ด โ ๐ถ) < (๐ต โ ๐ถ))) |
|
Theorem | ltsub2 8415 |
Subtraction of both sides of 'less than'. (Contributed by NM,
29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ถ โ ๐ต) < (๐ถ โ ๐ด))) |
|
Theorem | lt2sub 8416 |
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14-Apr-2016.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด < ๐ถ โง ๐ท < ๐ต) โ (๐ด โ ๐ต) < (๐ถ โ ๐ท))) |
|
Theorem | le2sub 8417 |
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14-Apr-2016.)
|
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โค ๐ถ โง ๐ท โค ๐ต) โ (๐ด โ ๐ต) โค (๐ถ โ ๐ท))) |
|
Theorem | ltneg 8418 |
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 8419 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด < ๐ต โ -๐ต < ๐ด)) |
|
Theorem | ltnegcon2 8420 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < -๐ต โ ๐ต < -๐ด)) |
|
Theorem | leneg 8421 |
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 8422 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด โค ๐ต โ -๐ต โค ๐ด)) |
|
Theorem | lenegcon2 8423 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค -๐ต โ ๐ต โค -๐ด)) |
|
Theorem | lt0neg1 8424 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
โข (๐ด โ โ โ (๐ด < 0 โ 0 < -๐ด)) |
|
Theorem | lt0neg2 8425 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
โข (๐ด โ โ โ (0 < ๐ด โ -๐ด < 0)) |
|
Theorem | le0neg1 8426 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
โข (๐ด โ โ โ (๐ด โค 0 โ 0 โค -๐ด)) |
|
Theorem | le0neg2 8427 |
Comparison of a number and its negative to zero. (Contributed by NM,
24-Aug-1999.)
|
โข (๐ด โ โ โ (0 โค ๐ด โ -๐ด โค 0)) |
|
Theorem | addge01 8428 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21-Feb-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค ๐ต โ ๐ด โค (๐ด + ๐ต))) |
|
Theorem | addge02 8429 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27-Jul-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค ๐ต โ ๐ด โค (๐ต + ๐ด))) |
|
Theorem | add20 8430 |
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.)
|
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต) = 0 โ (๐ด = 0 โง ๐ต = 0))) |
|
Theorem | subge0 8431 |
Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค (๐ด โ ๐ต) โ ๐ต โค ๐ด)) |
|
Theorem | suble0 8432 |
Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) โค 0 โ ๐ด โค ๐ต)) |
|
Theorem | leaddle0 8433 |
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, 30-May-2018.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โค ๐ด โ ๐ต โค 0)) |
|
Theorem | subge02 8434 |
Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค ๐ต โ (๐ด โ ๐ต) โค ๐ด)) |
|
Theorem | lesub0 8435 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค ๐ด โง ๐ต โค (๐ต โ ๐ด)) โ ๐ด = 0)) |
|
Theorem | mullt0 8436 |
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8-Jun-2009.)
|
โข (((๐ด โ โ โง ๐ด < 0) โง (๐ต โ โ โง ๐ต < 0)) โ 0 < (๐ด ยท ๐ต)) |
|
Theorem | 0le1 8437 |
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29-Apr-2015.)
|
โข 0 โค 1 |
|
Theorem | ltordlem 8438* |
Lemma for eqord1 8439. (Contributed by Mario Carneiro,
14-Jun-2014.)
|
โข (๐ฅ = ๐ฆ โ ๐ด = ๐ต)
& โข (๐ฅ = ๐ถ โ ๐ด = ๐)
& โข (๐ฅ = ๐ท โ ๐ด = ๐)
& โข ๐ โ โ & โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ < ๐ฆ โ ๐ด < ๐ต)) โ โข ((๐ โง (๐ถ โ ๐ โง ๐ท โ ๐)) โ (๐ถ < ๐ท โ ๐ < ๐)) |
|
Theorem | eqord1 8439* |
A strictly increasing real function on a subset of โ is
one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised
by Jim Kingdon, 20-Dec-2022.)
|
โข (๐ฅ = ๐ฆ โ ๐ด = ๐ต)
& โข (๐ฅ = ๐ถ โ ๐ด = ๐)
& โข (๐ฅ = ๐ท โ ๐ด = ๐)
& โข ๐ โ โ & โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ < ๐ฆ โ ๐ด < ๐ต)) โ โข ((๐ โง (๐ถ โ ๐ โง ๐ท โ ๐)) โ (๐ถ = ๐ท โ ๐ = ๐)) |
|
Theorem | eqord2 8440* |
A strictly decreasing real function on a subset of โ is one-to-one.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
โข (๐ฅ = ๐ฆ โ ๐ด = ๐ต)
& โข (๐ฅ = ๐ถ โ ๐ด = ๐)
& โข (๐ฅ = ๐ท โ ๐ด = ๐)
& โข ๐ โ โ & โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ < ๐ฆ โ ๐ต < ๐ด)) โ โข ((๐ โง (๐ถ โ ๐ โง ๐ท โ ๐)) โ (๐ถ = ๐ท โ ๐ = ๐)) |
|
Theorem | leidi 8441 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
โข ๐ด โ โ
โ โข ๐ด โค ๐ด |
|
Theorem | gt0ne0i 8442 |
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16-Sep-1999.)
|
โข ๐ด โ โ
โ โข (0 < ๐ด โ ๐ด โ 0) |
|
Theorem | gt0ne0ii 8443 |
Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|
โข ๐ด โ โ & โข 0 < ๐ด โ โข ๐ด โ 0 |
|
Theorem | addgt0i 8444 |
Addition of 2 positive numbers is positive. (Contributed by NM,
16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ 0 < (๐ด + ๐ต)) |
|
Theorem | addge0i 8445 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ 0 โค (๐ด + ๐ต)) |
|
Theorem | addgegt0i 8446 |
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข ((0 โค ๐ด โง 0 < ๐ต) โ 0 < (๐ด + ๐ต)) |
|
Theorem | addgt0ii 8447 |
Addition of 2 positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ด & โข 0 < ๐ต โ โข 0 < (๐ด + ๐ต) |
|
Theorem | add20i 8448 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28-Jul-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ ((๐ด + ๐ต) = 0 โ (๐ด = 0 โง ๐ต = 0))) |
|
Theorem | ltnegi 8449 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (๐ด < ๐ต โ -๐ต < -๐ด) |
|
Theorem | lenegi 8450 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1-Aug-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (๐ด โค ๐ต โ -๐ต โค -๐ด) |
|
Theorem | ltnegcon2i 8451 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (๐ด < -๐ต โ ๐ต < -๐ด) |
|
Theorem | lesub0i 8452 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข ((0 โค ๐ด โง ๐ต โค (๐ต โ ๐ด)) โ ๐ด = 0) |
|
Theorem | ltaddposi 8453 |
Adding a positive number to another number increases it. (Contributed
by NM, 25-Aug-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (0 < ๐ด โ ๐ต < (๐ต + ๐ด)) |
|
Theorem | posdifi 8454 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19-Aug-2001.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (๐ด < ๐ต โ 0 < (๐ต โ ๐ด)) |
|
Theorem | ltnegcon1i 8455 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (-๐ด < ๐ต โ -๐ต < ๐ด) |
|
Theorem | lenegcon1i 8456 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 6-Apr-2005.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (-๐ด โค ๐ต โ -๐ต โค ๐ด) |
|
Theorem | subge0i 8457 |
Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|
โข ๐ด โ โ & โข ๐ต โ
โ โ โข (0 โค (๐ด โ ๐ต) โ ๐ต โค ๐ด) |
|
Theorem | ltadd1i 8458 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข (๐ด < ๐ต โ (๐ด + ๐ถ) < (๐ต + ๐ถ)) |
|
Theorem | leadd1i 8459 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข (๐ด โค ๐ต โ (๐ด + ๐ถ) โค (๐ต + ๐ถ)) |
|
Theorem | leadd2i 8460 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข (๐ด โค ๐ต โ (๐ถ + ๐ด) โค (๐ถ + ๐ต)) |
|
Theorem | ltsubaddi 8461 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข ((๐ด โ ๐ต) < ๐ถ โ ๐ด < (๐ถ + ๐ต)) |
|
Theorem | lesubaddi 8462 |
'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 8463 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข ((๐ด โ ๐ต) < ๐ถ โ ๐ด < (๐ต + ๐ถ)) |
|
Theorem | lesubadd2i 8464 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3-Aug-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข ((๐ด โ ๐ต) โค ๐ถ โ ๐ด โค (๐ต + ๐ถ)) |
|
Theorem | ltaddsubi 8465 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 14-May-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ
โ โ โข ((๐ด + ๐ต) < ๐ถ โ ๐ด < (๐ถ โ ๐ต)) |
|
Theorem | lt2addi 8466 |
Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ
โ โ โข ((๐ด < ๐ถ โง ๐ต < ๐ท) โ (๐ด + ๐ต) < (๐ถ + ๐ท)) |
|
Theorem | le2addi 8467 |
Adding both side of two inequalities. (Contributed by NM,
16-Sep-1999.)
|
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ
โ โ โข ((๐ด โค ๐ถ โง ๐ต โค ๐ท) โ (๐ด + ๐ต) โค (๐ถ + ๐ท)) |
|
Theorem | gt0ne0d 8468 |
Positive implies nonzero. (Contributed by Mario Carneiro,
27-May-2016.)
|
โข (๐ โ 0 < ๐ด) โ โข (๐ โ ๐ด โ 0) |
|
Theorem | lt0ne0d 8469 |
Something less than zero is not zero. Deduction form. See also
lt0ap0d 8605 which is similar but for apartness.
(Contributed by David
Moews, 28-Feb-2017.)
|
โข (๐ โ ๐ด < 0) โ โข (๐ โ ๐ด โ 0) |
|
Theorem | leidd 8470 |
'Less than or equal to' is reflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ ๐ด โค ๐ด) |
|
Theorem | lt0neg1d 8471 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (๐ด < 0 โ 0 < -๐ด)) |
|
Theorem | lt0neg2d 8472 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (0 < ๐ด โ -๐ด < 0)) |
|
Theorem | le0neg1d 8473 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (๐ด โค 0 โ 0 โค -๐ด)) |
|
Theorem | le0neg2d 8474 |
Comparison of a number and its negative to zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ)
โ โข (๐ โ (0 โค ๐ด โ -๐ด โค 0)) |
|
Theorem | addgegt0d 8475 |
Addition of nonnegative and positive numbers is positive.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด)
& โข (๐ โ 0 < ๐ต) โ โข (๐ โ 0 < (๐ด + ๐ต)) |
|
Theorem | addgtge0d 8476 |
Addition of positive and nonnegative numbers is positive.
(Contributed by Asger C. Ipsen, 12-May-2021.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด)
& โข (๐ โ 0 โค ๐ต) โ โข (๐ โ 0 < (๐ด + ๐ต)) |
|
Theorem | addgt0d 8477 |
Addition of 2 positive numbers is positive. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด)
& โข (๐ โ 0 < ๐ต) โ โข (๐ โ 0 < (๐ด + ๐ต)) |
|
Theorem | addge0d 8478 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด)
& โข (๐ โ 0 โค ๐ต) โ โข (๐ โ 0 โค (๐ด + ๐ต)) |
|
Theorem | ltnegd 8479 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (๐ด < ๐ต โ -๐ต < -๐ด)) |
|
Theorem | lenegd 8480 |
Negative of both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (๐ด โค ๐ต โ -๐ต โค -๐ด)) |
|
Theorem | ltnegcon1d 8481 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ -๐ด < ๐ต) โ โข (๐ โ -๐ต < ๐ด) |
|
Theorem | ltnegcon2d 8482 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด < -๐ต) โ โข (๐ โ ๐ต < -๐ด) |
|
Theorem | lenegcon1d 8483 |
Contraposition of negative in 'less than or equal to'. (Contributed
by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ -๐ด โค ๐ต) โ โข (๐ โ -๐ต โค ๐ด) |
|
Theorem | lenegcon2d 8484 |
Contraposition of negative in 'less than or equal to'. (Contributed
by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โค -๐ต) โ โข (๐ โ ๐ต โค -๐ด) |
|
Theorem | ltaddposd 8485 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 < ๐ด โ ๐ต < (๐ต + ๐ด))) |
|
Theorem | ltaddpos2d 8486 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 < ๐ด โ ๐ต < (๐ด + ๐ต))) |
|
Theorem | ltsubposd 8487 |
Subtracting a positive number from another number decreases it.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 < ๐ด โ (๐ต โ ๐ด) < ๐ต)) |
|
Theorem | posdifd 8488 |
Comparison of two numbers whose difference is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
|
Theorem | addge01d 8489 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 โค ๐ต โ ๐ด โค (๐ด + ๐ต))) |
|
Theorem | addge02d 8490 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 โค ๐ต โ ๐ด โค (๐ต + ๐ด))) |
|
Theorem | subge0d 8491 |
Nonnegative subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 โค (๐ด โ ๐ต) โ ๐ต โค ๐ด)) |
|
Theorem | suble0d 8492 |
Nonpositive subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ ((๐ด โ ๐ต) โค 0 โ ๐ด โค ๐ต)) |
|
Theorem | subge02d 8493 |
Nonnegative subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ)
โ โข (๐ โ (0 โค ๐ต โ (๐ด โ ๐ต) โค ๐ด)) |
|
Theorem | ltadd1d 8494 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ (๐ด < ๐ต โ (๐ด + ๐ถ) < (๐ต + ๐ถ))) |
|
Theorem | leadd1d 8495 |
Addition to both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ (๐ด โค ๐ต โ (๐ด + ๐ถ) โค (๐ต + ๐ถ))) |
|
Theorem | leadd2d 8496 |
Addition to both sides of 'less than or equal to'. (Contributed by
Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ (๐ด โค ๐ต โ (๐ถ + ๐ด) โค (๐ถ + ๐ต))) |
|
Theorem | ltsubaddd 8497 |
'Less than' relationship between subtraction and addition. (Contributed
by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ ((๐ด โ ๐ต) < ๐ถ โ ๐ด < (๐ถ + ๐ต))) |
|
Theorem | lesubaddd 8498 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ ((๐ด โ ๐ต) โค ๐ถ โ ๐ด โค (๐ถ + ๐ต))) |
|
Theorem | ltsubadd2d 8499 |
'Less than' relationship between subtraction and addition. (Contributed
by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ ((๐ด โ ๐ต) < ๐ถ โ ๐ด < (๐ต + ๐ถ))) |
|
Theorem | lesubadd2d 8500 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by Mario Carneiro, 27-May-2016.)
|
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ)
โ โข (๐ โ ((๐ด โ ๐ต) โค ๐ถ โ ๐ด โค (๐ต + ๐ถ))) |