Home | Metamath
Proof Explorer Theorem List (p. 116 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mvrraddd 11501 | Move the right term in a sum on the RHS to the LHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด = (๐ต + ๐ถ)) โ โข (๐ โ (๐ด โ ๐ถ) = ๐ต) | ||
Theorem | mvrladdd 11502 | Move the left term in a sum on the RHS to the LHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด = (๐ต + ๐ถ)) โ โข (๐ โ (๐ด โ ๐ต) = ๐ถ) | ||
Theorem | assraddsubd 11503 | Associate RHS addition-subtraction. (Contributed by David A. Wheeler, 15-Oct-2018.) |
โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ด = ((๐ต + ๐ถ) โ ๐ท)) โ โข (๐ โ ๐ด = (๐ต + (๐ถ โ ๐ท))) | ||
Theorem | subaddeqd 11504 | Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ (๐ด + ๐ต) = (๐ถ + ๐ท)) โ โข (๐ โ (๐ด โ ๐ท) = (๐ถ โ ๐ต)) | ||
Theorem | addlsub 11505 | Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด + ๐ต) = ๐ถ โ ๐ด = (๐ถ โ ๐ต))) | ||
Theorem | addrsub 11506 | Right-subtraction: Subtraction of the right summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด + ๐ต) = ๐ถ โ ๐ต = (๐ถ โ ๐ด))) | ||
Theorem | subexsub 11507 | A subtraction law: Exchanging the subtrahend and the result of the subtraction. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ด = (๐ถ โ ๐ต) โ ๐ต = (๐ถ โ ๐ด))) | ||
Theorem | addid0 11508 | If adding a number to a another number yields the other number, the added number must be 0. This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021.) |
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + ๐) = ๐ โ ๐ = 0)) | ||
Theorem | addn0nid 11509 | Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021.) |
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ (๐ + ๐) โ ๐) | ||
Theorem | pnpncand 11510 | Addition/subtraction cancellation law. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด + (๐ต โ ๐ถ)) + (๐ถ โ ๐ต)) = ๐ด) | ||
Theorem | subeqrev 11511 | Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โ ๐ต) = (๐ถ โ ๐ท) โ (๐ต โ ๐ด) = (๐ท โ ๐ถ))) | ||
Theorem | addeq0 11512 | Two complex numbers add up to zero iff they are each other's opposites. (Contributed by Thierry Arnoux, 2-May-2017.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) = 0 โ ๐ด = -๐ต)) | ||
Theorem | pncan1 11513 | Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
โข (๐ด โ โ โ ((๐ด + 1) โ 1) = ๐ด) | ||
Theorem | npcan1 11514 | Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.) |
โข (๐ด โ โ โ ((๐ด โ 1) + 1) = ๐ด) | ||
Theorem | subeq0bd 11515 | If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 11456. Converse of subeq0d 11454. Contrapositive of subne0ad 11457. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ด โ ๐ต) = 0) | ||
Theorem | renegcld 11516 | Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ -๐ด โ โ) | ||
Theorem | resubcld 11517 | Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โ ๐ต) โ โ) | ||
Theorem | negn0 11518* | The image under negation of a nonempty set of reals is nonempty. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ด โ โ โง ๐ด โ โ ) โ {๐ง โ โ โฃ -๐ง โ ๐ด} โ โ ) | ||
Theorem | negf1o 11519* | Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020.) |
โข ๐น = (๐ฅ โ ๐ด โฆ -๐ฅ) โ โข (๐ด โ โ โ ๐น:๐ดโ1-1-ontoโ{๐ โ โ โฃ -๐ โ ๐ด}) | ||
Theorem | kcnktkm1cn 11520 | k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
โข (๐พ โ โ โ (๐พ ยท (๐พ โ 1)) โ โ) | ||
Theorem | muladd 11521 | Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) | ||
Theorem | subdi 11522 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต โ ๐ถ)) = ((๐ด ยท ๐ต) โ (๐ด ยท ๐ถ))) | ||
Theorem | subdir 11523 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ถ))) | ||
Theorem | ine0 11524 | The imaginary unit i is not zero. (Contributed by NM, 6-May-1999.) |
โข i โ 0 | ||
Theorem | mulneg1 11525 | Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด ยท ๐ต) = -(๐ด ยท ๐ต)) | ||
Theorem | mulneg2 11526 | The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท -๐ต) = -(๐ด ยท ๐ต)) | ||
Theorem | mulneg12 11527 | Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด ยท ๐ต) = (๐ด ยท -๐ต)) | ||
Theorem | mul2neg 11528 | 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 11529 | Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โ (๐ต ยท ๐ถ)) = (๐ด + (๐ต ยท -๐ถ))) | ||
Theorem | mulm1 11530 | Product with minus one is negative. (Contributed by NM, 16-Nov-1999.) |
โข (๐ด โ โ โ (-1 ยท ๐ด) = -๐ด) | ||
Theorem | addneg1mul 11531 | Addition with product with minus one is a subtraction. (Contributed by AV, 18-Oct-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + (-1 ยท ๐ต)) = (๐ด โ ๐ต)) | ||
Theorem | mulsub 11532 | Product of two differences. (Contributed by NM, 14-Jan-2006.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โ ๐ต) ยท (๐ถ โ ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) | ||
Theorem | mulsub2 11533 | Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โ ๐ต) ยท (๐ถ โ ๐ท)) = ((๐ต โ ๐ด) ยท (๐ท โ ๐ถ))) | ||
Theorem | mulm1i 11534 | Product with minus one is negative. (Contributed by NM, 31-Jul-1999.) |
โข ๐ด โ โ โ โข (-1 ยท ๐ด) = -๐ด | ||
Theorem | mulneg1i 11535 | 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 11536 | Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด ยท -๐ต) = -(๐ด ยท ๐ต) | ||
Theorem | mul2negi 11537 | 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 11538 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (๐ด ยท (๐ต โ ๐ถ)) = ((๐ด ยท ๐ต) โ (๐ด ยท ๐ถ)) | ||
Theorem | subdiri 11539 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด โ ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ถ)) | ||
Theorem | muladdi 11540 | Product of two sums. (Contributed by NM, 17-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) | ||
Theorem | mulm1d 11541 | Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (-1 ยท ๐ด) = -๐ด) | ||
Theorem | mulneg1d 11542 | Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (-๐ด ยท ๐ต) = -(๐ด ยท ๐ต)) | ||
Theorem | mulneg2d 11543 | Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด ยท -๐ต) = -(๐ด ยท ๐ต)) | ||
Theorem | mul2negd 11544 | Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (-๐ด ยท -๐ต) = (๐ด ยท ๐ต)) | ||
Theorem | subdid 11545 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ด ยท (๐ต โ ๐ถ)) = ((๐ด ยท ๐ต) โ (๐ด ยท ๐ถ))) | ||
Theorem | subdird 11546 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด โ ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ถ))) | ||
Theorem | muladdd 11547 | Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) โ โข (๐ โ ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) | ||
Theorem | mulsubd 11548 | Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) โ โข (๐ โ ((๐ด โ ๐ต) ยท (๐ถ โ ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) | ||
Theorem | muls1d 11549 | Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด ยท (๐ต โ 1)) = ((๐ด ยท ๐ต) โ ๐ด)) | ||
Theorem | mulsubfacd 11550 | Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ((๐ด ยท ๐ต) โ ๐ต) = ((๐ด โ 1) ยท ๐ต)) | ||
Theorem | addmulsub 11551 | The product of a sum and a difference. (Contributed by AV, 5-Mar-2023.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท (๐ถ โ ๐ท)) = (((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ)) โ ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) | ||
Theorem | subaddmulsub 11552 | The difference with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ) โง ๐ธ โ โ) โ (๐ธ โ ((๐ด + ๐ต) ยท (๐ถ โ ๐ท))) = (((๐ธ โ (๐ด ยท ๐ถ)) โ (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) | ||
Theorem | mulsubaddmulsub 11553 | A special difference of a product with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ต ยท ๐ถ) โ ((๐ด + ๐ต) ยท (๐ถ โ ๐ท))) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ (๐ด ยท ๐ถ))) | ||
Theorem | gt0ne0 11554 | Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ ๐ด โ 0) | ||
Theorem | lt0ne0 11555 | A number which is less than zero is not zero. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
โข ((๐ด โ โ โง ๐ด < 0) โ ๐ด โ 0) | ||
Theorem | ltadd1 11556 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ด + ๐ถ) < (๐ต + ๐ถ))) | ||
Theorem | leadd1 11557 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 18-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โค ๐ต โ (๐ด + ๐ถ) โค (๐ต + ๐ถ))) | ||
Theorem | leadd2 11558 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โค ๐ต โ (๐ถ + ๐ด) โค (๐ถ + ๐ต))) | ||
Theorem | ltsubadd 11559 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) < ๐ถ โ ๐ด < (๐ถ + ๐ต))) | ||
Theorem | ltsubadd2 11560 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) < ๐ถ โ ๐ด < (๐ต + ๐ถ))) | ||
Theorem | lesubadd 11561 | '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 11562 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) โค ๐ถ โ ๐ด โค (๐ต + ๐ถ))) | ||
Theorem | ltaddsub 11563 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) < ๐ถ โ ๐ด < (๐ถ โ ๐ต))) | ||
Theorem | ltaddsub2 11564 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) < ๐ถ โ ๐ต < (๐ถ โ ๐ด))) | ||
Theorem | leaddsub 11565 | 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) โค ๐ถ โ ๐ด โค (๐ถ โ ๐ต))) | ||
Theorem | leaddsub2 11566 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) โค ๐ถ โ ๐ต โค (๐ถ โ ๐ด))) | ||
Theorem | suble 11567 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) โค ๐ถ โ (๐ด โ ๐ถ) โค ๐ต)) | ||
Theorem | lesub 11568 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โค (๐ต โ ๐ถ) โ ๐ถ โค (๐ต โ ๐ด))) | ||
Theorem | ltsub23 11569 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) < ๐ถ โ (๐ด โ ๐ถ) < ๐ต)) | ||
Theorem | ltsub13 11570 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < (๐ต โ ๐ถ) โ ๐ถ < (๐ต โ ๐ด))) | ||
Theorem | le2add 11571 | 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 | ltleadd 11572 | Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด < ๐ถ โง ๐ต โค ๐ท) โ (๐ด + ๐ต) < (๐ถ + ๐ท))) | ||
Theorem | leltadd 11573 | Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โค ๐ถ โง ๐ต < ๐ท) โ (๐ด + ๐ต) < (๐ถ + ๐ท))) | ||
Theorem | lt2add 11574 | 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 | addgt0 11575 | 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 11576 | 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 11577 | 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 11578 | 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 11579 | Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 < ๐ด โ ๐ต < (๐ต + ๐ด))) | ||
Theorem | ltaddpos2 11580 | Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 < ๐ด โ ๐ต < (๐ด + ๐ต))) | ||
Theorem | ltsubpos 11581 | 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 11582 | Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) | ||
Theorem | lesub1 11583 | 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 11584 | 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 11585 | Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ด โ ๐ถ) < (๐ต โ ๐ถ))) | ||
Theorem | ltsub2 11586 | Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ถ โ ๐ต) < (๐ถ โ ๐ด))) | ||
Theorem | lt2sub 11587 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด < ๐ถ โง ๐ท < ๐ต) โ (๐ด โ ๐ต) < (๐ถ โ ๐ท))) | ||
Theorem | le2sub 11588 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด โค ๐ถ โง ๐ท โค ๐ต) โ (๐ด โ ๐ต) โค (๐ถ โ ๐ท))) | ||
Theorem | ltneg 11589 | 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 11590 | Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด < ๐ต โ -๐ต < ๐ด)) | ||
Theorem | ltnegcon2 11591 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < -๐ต โ ๐ต < -๐ด)) | ||
Theorem | leneg 11592 | 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 11593 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด โค ๐ต โ -๐ต โค ๐ด)) | ||
Theorem | lenegcon2 11594 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค -๐ต โ ๐ต โค -๐ด)) | ||
Theorem | lt0neg1 11595 | 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 11596 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
โข (๐ด โ โ โ (0 < ๐ด โ -๐ด < 0)) | ||
Theorem | le0neg1 11597 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
โข (๐ด โ โ โ (๐ด โค 0 โ 0 โค -๐ด)) | ||
Theorem | le0neg2 11598 | Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.) |
โข (๐ด โ โ โ (0 โค ๐ด โ -๐ด โค 0)) | ||
Theorem | addge01 11599 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค ๐ต โ ๐ด โค (๐ด + ๐ต))) | ||
Theorem | addge02 11600 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค ๐ต โ ๐ด โค (๐ต + ๐ด))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |