Theorem List for Intuitionistic Logic Explorer - 7401-7500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mulneg1i 7401 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 10-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mulneg2i 7402 |
Product with negative is negative of product. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul2negi 7403 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subdii 7404 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26-Nov-1994.)
|
|
|
Theorem | subdiri 7405 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8-May-1999.)
|
|
|
Theorem | muladdi 7406 |
Product of two sums. (Contributed by NM, 17-May-1999.)
|
|
|
Theorem | mulm1d 7407 |
Product with minus one is negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mulneg1d 7408 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mulneg2d 7409 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | mul2negd 7410 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subdid 7411 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subdird 7412 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | muladdd 7413 |
Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mulsubd 7414 |
Product of two differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mulsubfacd 7415 |
Multiplication followed by the subtraction of a factor. (Contributed by
Alexander van der Vekens, 28-Aug-2018.)
|
|
|
3.3.4 Ordering on reals (cont.)
|
|
Theorem | ltadd2 7416 |
Addition to both sides of 'less than'. (Contributed by NM,
12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltadd2i 7417 |
Addition to both sides of 'less than'. (Contributed by NM,
21-Jan-1997.)
|
|
|
Theorem | ltadd2d 7418 |
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltadd2dd 7419 |
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
|
|
Theorem | ltletrd 7420 |
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9-Jan-2006.)
|
|
|
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, 24-Mar-2018.)
|
|
|
Theorem | gt0ne0 7422 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt0ne0 7423 |
A number which is less than zero is not zero. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
|
|
Theorem | ltadd1 7424 |
Addition to both sides of 'less than'. Part of definition 11.2.7(vi) of
[HoTT], p. (varies). (Contributed by NM,
12-Nov-1999.) (Proof shortened
by Mario Carneiro, 27-May-2016.)
|
|
|
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, 18-Oct-1999.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | leadd2 7426 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
|
|
Theorem | ltsubadd 7427 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsubadd2 7428 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
|
|
Theorem | lesubadd 7429 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | lesubadd2 7430 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
|
|
Theorem | ltaddsub 7431 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | ltaddsub2 7432 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | leaddsub 7433 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
|
|
Theorem | leaddsub2 7434 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
|
|
Theorem | suble 7435 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
|
|
Theorem | lesub 7436 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltsub23 7437 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4-Oct-1999.)
|
|
|
Theorem | ltsub13 7438 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | le2add 7439 |
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 | lt2add 7440 |
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 7441 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
|
|
Theorem | leltadd 7442 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
|
|
Theorem | addgt0 7443 |
The sum of 2 positive numbers is positive. (Contributed by NM,
1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgegt0 7444 |
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 7445 |
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 7446 |
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltaddpos 7447 |
Adding a positive number to another number increases it. (Contributed by
NM, 17-Nov-2004.)
|
|
|
Theorem | ltaddpos2 7448 |
Adding a positive number to another number increases it. (Contributed by
NM, 8-Apr-2005.)
|
|
|
Theorem | ltsubpos 7449 |
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 7450 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17-Nov-2004.)
|
|
|
Theorem | lesub1 7451 |
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 7452 |
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 7453 |
Subtraction from both sides of 'less than'. (Contributed by FL,
3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsub2 7454 |
Subtraction of both sides of 'less than'. (Contributed by NM,
29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt2sub 7455 |
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14-Apr-2016.)
|
|
|
Theorem | le2sub 7456 |
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14-Apr-2016.)
|
|
|
Theorem | ltneg 7457 |
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 7458 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
|
|
Theorem | ltnegcon2 7459 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
|
|
Theorem | leneg 7460 |
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 7461 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
|
|
Theorem | lenegcon2 7462 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
|
|
Theorem | lt0neg1 7463 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lt0neg2 7464 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
|
|
Theorem | le0neg1 7465 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
|
|
Theorem | le0neg2 7466 |
Comparison of a number and its negative to zero. (Contributed by NM,
24-Aug-1999.)
|
|
|
Theorem | addge01 7467 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | addge02 7468 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | add20 7469 |
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 7470 |
Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | suble0 7471 |
Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
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, 30-May-2018.)
|
|
|
Theorem | subge02 7473 |
Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | lesub0 7474 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mullt0 7475 |
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8-Jun-2009.)
|
|
|
Theorem | 0le1 7476 |
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29-Apr-2015.)
|
|
|
Theorem | leidi 7477 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | gt0ne0i 7478 |
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16-Sep-1999.)
|
|
|
Theorem | gt0ne0ii 7479 |
Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|
|
|
Theorem | addgt0i 7480 |
Addition of 2 positive numbers is positive. (Contributed by NM,
16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addge0i 7481 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgegt0i 7482 |
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addgt0ii 7483 |
Addition of 2 positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | add20i 7484 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28-Jul-1999.)
|
|
|
Theorem | ltnegi 7485 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | lenegi 7486 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1-Aug-1999.)
|
|
|
Theorem | ltnegcon2i 7487 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lesub0i 7488 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltaddposi 7489 |
Adding a positive number to another number increases it. (Contributed
by NM, 25-Aug-1999.)
|
|
|
Theorem | posdifi 7490 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19-Aug-2001.)
|
|
|
Theorem | ltnegcon1i 7491 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lenegcon1i 7492 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 6-Apr-2005.)
|
|
|
Theorem | subge0i 7493 |
Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|
|
|
Theorem | ltadd1i 7494 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | leadd1i 7495 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
|
|
Theorem | leadd2i 7496 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
|
|
Theorem | ltsubaddi 7497 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
|
|
Theorem | lesubaddi 7498 |
'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 7499 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
|
|
Theorem | lesubadd2i 7500 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3-Aug-1999.)
|
|