Theorem List for Intuitionistic Logic Explorer - 7501-7600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mulneg12 7501 |
Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|
|
|
Theorem | mul2neg 7502 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed
by NM, 30-Jul-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | submul2 7503 |
Convert a subtraction to addition using multiplication by a negative.
(Contributed by NM, 2-Feb-2007.)
|
|
|
Theorem | mulm1 7504 |
Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|
|
|
Theorem | mulsub 7505 |
Product of two differences. (Contributed by NM, 14-Jan-2006.)
|
|
|
Theorem | mulsub2 7506 |
Swap the order of subtraction in a multiplication. (Contributed by Scott
Fenton, 24-Jun-2013.)
|
|
|
Theorem | mulm1i 7507 |
Product with minus one is negative. (Contributed by NM,
31-Jul-1999.)
|
|
|
Theorem | mulneg1i 7508 |
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 7509 |
Product with negative is negative of product. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul2negi 7510 |
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 7511 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26-Nov-1994.)
|
|
|
Theorem | subdiri 7512 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8-May-1999.)
|
|
|
Theorem | muladdi 7513 |
Product of two sums. (Contributed by NM, 17-May-1999.)
|
|
|
Theorem | mulm1d 7514 |
Product with minus one is negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mulneg1d 7515 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mulneg2d 7516 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | mul2negd 7517 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subdid 7518 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subdird 7519 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | muladdd 7520 |
Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mulsubd 7521 |
Product of two differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mulsubfacd 7522 |
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 7523 |
Addition to both sides of 'less than'. (Contributed by NM,
12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltadd2i 7524 |
Addition to both sides of 'less than'. (Contributed by NM,
21-Jan-1997.)
|
|
|
Theorem | ltadd2d 7525 |
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltadd2dd 7526 |
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
|
|
Theorem | ltletrd 7527 |
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9-Jan-2006.)
|
|
|
Theorem | ltaddneg 7528 |
Adding a negative number to another number decreases it. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | ltaddnegr 7529 |
Adding a negative number to another number decreases it. (Contributed by
AV, 19-Mar-2021.)
|
|
|
Theorem | lelttrdi 7530 |
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 7531 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt0ne0 7532 |
A number which is less than zero is not zero. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
|
|
Theorem | ltadd1 7533 |
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 7534 |
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 7535 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
|
|
Theorem | ltsubadd 7536 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsubadd2 7537 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
|
|
Theorem | lesubadd 7538 |
'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 7539 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
|
|
Theorem | ltaddsub 7540 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | ltaddsub2 7541 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | leaddsub 7542 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
|
|
Theorem | leaddsub2 7543 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
|
|
Theorem | suble 7544 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
|
|
Theorem | lesub 7545 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltsub23 7546 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4-Oct-1999.)
|
|
|
Theorem | ltsub13 7547 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | le2add 7548 |
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 7549 |
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 7550 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
|
|
Theorem | leltadd 7551 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
|
|
Theorem | addgt0 7552 |
The sum of 2 positive numbers is positive. (Contributed by NM,
1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgegt0 7553 |
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 7554 |
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 7555 |
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltaddpos 7556 |
Adding a positive number to another number increases it. (Contributed by
NM, 17-Nov-2004.)
|
|
|
Theorem | ltaddpos2 7557 |
Adding a positive number to another number increases it. (Contributed by
NM, 8-Apr-2005.)
|
|
|
Theorem | ltsubpos 7558 |
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 7559 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17-Nov-2004.)
|
|
|
Theorem | lesub1 7560 |
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 7561 |
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 7562 |
Subtraction from both sides of 'less than'. (Contributed by FL,
3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsub2 7563 |
Subtraction of both sides of 'less than'. (Contributed by NM,
29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt2sub 7564 |
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14-Apr-2016.)
|
|
|
Theorem | le2sub 7565 |
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14-Apr-2016.)
|
|
|
Theorem | ltneg 7566 |
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 7567 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
|
|
Theorem | ltnegcon2 7568 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
|
|
Theorem | leneg 7569 |
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 7570 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
|
|
Theorem | lenegcon2 7571 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
|
|
Theorem | lt0neg1 7572 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lt0neg2 7573 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
|
|
Theorem | le0neg1 7574 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
|
|
Theorem | le0neg2 7575 |
Comparison of a number and its negative to zero. (Contributed by NM,
24-Aug-1999.)
|
|
|
Theorem | addge01 7576 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | addge02 7577 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | add20 7578 |
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 7579 |
Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | suble0 7580 |
Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | leaddle0 7581 |
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 7582 |
Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | lesub0 7583 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mullt0 7584 |
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8-Jun-2009.)
|
|
|
Theorem | 0le1 7585 |
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29-Apr-2015.)
|
|
|
Theorem | leidi 7586 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | gt0ne0i 7587 |
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16-Sep-1999.)
|
|
|
Theorem | gt0ne0ii 7588 |
Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|
|
|
Theorem | addgt0i 7589 |
Addition of 2 positive numbers is positive. (Contributed by NM,
16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addge0i 7590 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgegt0i 7591 |
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addgt0ii 7592 |
Addition of 2 positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | add20i 7593 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28-Jul-1999.)
|
|
|
Theorem | ltnegi 7594 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | lenegi 7595 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1-Aug-1999.)
|
|
|
Theorem | ltnegcon2i 7596 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lesub0i 7597 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltaddposi 7598 |
Adding a positive number to another number increases it. (Contributed
by NM, 25-Aug-1999.)
|
|
|
Theorem | posdifi 7599 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19-Aug-2001.)
|
|
|
Theorem | ltnegcon1i 7600 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
|