HomeTheorem List (p. 95 of 325)
Unicode version.
| Home |
Metamath
Proof Explorer Theorem List (p. 95 of 325) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nnncan1d 9401 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
              | ||
| Theorem | nnncan2d 9402 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | npncan3d 9403 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| ||
| Theorem | pnpcand 9404 | Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | pnpcan2d 9405 | Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | pnncand 9406 | Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | ppncand 9407 | Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subcand 9408 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | subcan2d 9409 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 22-Sep-2016.) |
| | ||
| Theorem | subcanad 9410 | Cancellation law for subtraction. Deduction form of subcan 9312. Generalization of subcand 9408. (Contributed by David Moews, 28-Feb-2017.) |
| ||
| Theorem | subneintrd 9411 | Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcand 9408. (Contributed by David Moews, 28-Feb-2017.) |
 | ||
| Theorem | subcan2ad 9412 | Cancellation law for subtraction. Deduction form of subcan2 9282. Generalization of subcan2d 9409. (Contributed by David Moews, 28-Feb-2017.) |
|
| ||
| Theorem | subneintr2d 9413 | Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcan2d 9409. (Contributed by David Moews, 28-Feb-2017.) |
| | ||
| Theorem | addsub4d 9414 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| ||
| Theorem | subadd4d 9415 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | sub4d 9416 | Rearrangement of 4 terms in a subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | 2addsubd 9417 | Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | addsubeq4d 9418 | Relation between sums and differences. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subeq0bd 9419 | If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 9377. Converse of subeq0d 9375. Contrapositive of subne0ad 9378. (Contributed by David Moews, 28-Feb-2017.) |
 | ||
| Theorem | renegcld 9420 | Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
  | ||
| Theorem | resubcld 9421 | Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | muladd 9422 | Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | subdi 9423 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | subdir 9424 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.) |
|
| ||
| Theorem | ine0 9425 |
The imaginary unit 
is not zero. (Contributed by NM,
6-May-1999.)
|
| | ||
| Theorem | mulneg1 9426 | 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 9427 | The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.) |
|
| ||
| Theorem | mulneg12 9428 | Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.) |
| | ||
| Theorem | mul2neg 9429 | 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 9430 | Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.) |
|
| ||
| Theorem | mulm1 9431 | Product with minus one is negative. (Contributed by NM, 16-Nov-1999.) |
| ||
| Theorem | mulsub 9432 | Product of two differences. (Contributed by NM, 14-Jan-2006.) |
|
| ||
| Theorem | mulsub2 9433 | Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
|
| ||
| Theorem | mulm1i 9434 | Product with minus one is negative. (Contributed by NM, 31-Jul-1999.) |
| | ||
| Theorem | mulneg1i 9435 | 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 9436 | Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | mul2negi 9437 | 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 9438 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.) |
|
| ||
| Theorem | subdiri 9439 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.) |
|
| ||
| Theorem | muladdi 9440 | Product of two sums. (Contributed by NM, 17-May-1999.) |
|
| ||
| Theorem | mulm1d 9441 | Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | mulneg1d 9442 | Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | mulneg2d 9443 | Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | mul2negd 9444 | Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subdid 9445 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subdird 9446 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | muladdd 9447 | Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | mulsubd 9448 | Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | gt0ne0 9449 | Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
 | ||
| Theorem | lt0ne0 9450 | A number which is less than zero is not zero. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
|
| ||
| Theorem | ltadd1 9451 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | leadd1 9452 | 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 9453 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.) |
| | ||
| Theorem | ltsubadd 9454 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | ltsubadd2 9455 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) |
|
| ||
| Theorem | lesubadd 9456 | '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 9457 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.) |
|
| ||
| Theorem | ltaddsub 9458 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | ltaddsub2 9459 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | leaddsub 9460 | 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
|
| ||
| Theorem | leaddsub2 9461 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
|
| ||
| Theorem | suble 9462 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) |
|
| ||
| Theorem | lesub 9463 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | ltsub23 9464 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.) |
|
| ||
| Theorem | ltsub13 9465 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | le2add 9466 | 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 9467 | Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.) |
|
| ||
| Theorem | leltadd 9468 | Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.) |
|
| ||
| Theorem | lt2add 9469 | 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 9470 | The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | addgegt0 9471 | 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 9472 | 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 9473 | The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | ltaddpos 9474 | Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.) |
| | ||
| Theorem | ltaddpos2 9475 | Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.) |
| | ||
| Theorem | ltsubpos 9476 | 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 9477 | Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.) |
|
| ||
| Theorem | lesub1 9478 | 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 9479 | 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 9480 | Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | ltsub2 9481 | Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | lt2sub 9482 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
|
| ||
| Theorem | le2sub 9483 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
|
| ||
| Theorem | ltneg 9484 | 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 9485 | Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.) |
| | ||
| Theorem | ltnegcon2 9486 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.) |
|
| ||
| Theorem | leneg 9487 | 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 9488 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | lenegcon2 9489 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.) |
|
| ||
| Theorem | lt0neg1 9490 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
| | ||
| Theorem | lt0neg2 9491 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | le0neg1 9492 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | le0neg2 9493 | Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.) |
| | ||
| Theorem | addge01 9494 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
|
| ||
| Theorem | addge02 9495 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.) |
|
| ||
| Theorem | add20 9496 | 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 9497 | Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | suble0 9498 | Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subge02 9499 | Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.) |
| | ||
| Theorem | lesub0 9500 | Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |