HomeTheorem List (p. 108 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 108 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | divrec 10701 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
     ![/\](wedge.gif "/\"){kind=small}       
  | ||
| Theorem | divrec2 10702 | Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006.) |
|
| ||
| Theorem | divass 10703 | An associative law for division. (Contributed by NM, 2-Aug-2004.) |
| ||
| Theorem | div23 10704 | A commutative/associative law for division. (Contributed by NM, 2-Aug-2004.) |
|
| ||
| Theorem | div32 10705 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | div13 10706 | A commutative/associative law for division. (Contributed by NM, 22-Apr-2005.) |
|
| ||
| Theorem | div12 10707 | A commutative/associative law for division. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | divmulass 10708 | An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021.) |
| ||
| Theorem | divmulasscom 10709 | An associative/commutative law for division and multiplication. (Contributed by AV, 10-Jul-2021.) |
|
| ||
| Theorem | divdir 10710 | Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ||
| Theorem | divcan3 10711 | A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | divcan4 10712 | A cancellation law for division. (Contributed by NM, 8-Feb-2005.) |
|
| ||
| Theorem | div11 10713 | One-to-one relationship for division. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
 | ||
| Theorem | divid 10714 | A number divided by itself is one. (Contributed by NM, 1-Aug-2004.) |
|
| ||
| Theorem | div0 10715 | Division into zero is zero. (Contributed by NM, 14-Mar-2005.) |
|
| ||
| Theorem | div1 10716 | A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | 1div1e1 10717 | 1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) |
| | ||
| Theorem | diveq1 10718 | Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
|
| ||
| Theorem | divneg 10719 | Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004.) |
| ||
| Theorem | muldivdir 10720 | Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021.) |
|
| ||
| Theorem | divsubdir 10721 | Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.) |
| ||
| Theorem | recrec 10722 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 26-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | rec11 10723 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | rec11r 10724 | Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.) |
|
| ||
| Theorem | divmuldiv 10725 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) |
|
| ||
| Theorem | divdivdiv 10726 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) |
|
| ||
| Theorem | divcan5 10727 | Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006.) |
|
| ||
| Theorem | divmul13 10728 | Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005.) |
|
| ||
| Theorem | divmul24 10729 | Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005.) |
|
| ||
| Theorem | divmuleq 10730 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014.) |
|
| ||
| Theorem | recdiv 10731 | The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004.) |
|
| ||
| Theorem | divcan6 10732 | Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007.) |
|
| ||
| Theorem | divdiv32 10733 | Swap denominators in a division. (Contributed by NM, 2-Aug-2004.) |
|
| ||
| Theorem | divcan7 10734 | Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013.) |
|
| ||
| Theorem | dmdcan 10735 | Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
|
| ||
| Theorem | divdiv1 10736 | Division into a fraction. (Contributed by NM, 31-Dec-2007.) |
|
| ||
| Theorem | divdiv2 10737 | Division by a fraction. (Contributed by NM, 27-Dec-2008.) |
|
| ||
| Theorem | recdiv2 10738 | Division into a reciprocal. (Contributed by NM, 19-Oct-2007.) |
|
| ||
| Theorem | ddcan 10739 | Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.) |
|
| ||
| Theorem | divadddiv 10740 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 2-May-2016.) |
|
| ||
| Theorem | divsubdiv 10741 | Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
|
| ||
| Theorem | conjmul 10742 | Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 12-Nov-2006.) |
 
| ||
| Theorem | rereccl 10743 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ||
| Theorem | redivcl 10744 | Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | eqneg 10745 | A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | eqnegd 10746 | A complex number equals its negative iff it is zero. Deduction form of eqneg 10745. (Contributed by David Moews, 28-Feb-2017.) |
 
| ||
| Theorem | eqnegad 10747 | If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 10745. (Contributed by David Moews, 28-Feb-2017.) |
 | ||
| Theorem | div2neg 10748 | Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.) |
|
| ||
| Theorem | divneg2 10749 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.) |
|
| ||
| Theorem | recclzi 10750 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | recne0zi 10751 | The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.) |
|
| ||
| Theorem | recidzi 10752 | Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.) |
|
| ||
| Theorem | div1i 10753 | A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) |
| | ||
| Theorem | eqnegi 10754 | A number equal to its negative is zero. (Contributed by NM, 29-May-1999.) |
|
| ||
| Theorem | reccli 10755 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | recidi 10756 | Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.) |
|
| ||
| Theorem | recreci 10757 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.) |
|
| ||
| Theorem | dividi 10758 | A number divided by itself is one. (Contributed by NM, 9-Feb-1995.) |
|
| ||
| Theorem | div0i 10759 | Division into zero is zero. (Contributed by NM, 12-Aug-1999.) |
|
| ||
| Theorem | divclzi 10760 | Closure law for division. (Contributed by NM, 7-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.) |
|
| ||
| Theorem | divcan1zi 10761 | A cancellation law for division. (Contributed by NM, 2-Oct-1999.) |
|
| ||
| Theorem | divcan2zi 10762 | A cancellation law for division. (Contributed by NM, 10-Aug-1999.) |
| | ||
| Theorem | divreczi 10763 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 11-Oct-1999.) |
|
| ||
| Theorem | divcan3zi 10764 | A cancellation law for division. (Eliminates a hypothesis of divcan3i 10771 with the weak deduction theorem.) (Contributed by NM, 3-Feb-2004.) |
|
| ||
| Theorem | divcan4zi 10765 | A cancellation law for division. (Contributed by NM, 12-Oct-1999.) |
|
| ||
| Theorem | rec11i 10766 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) |
|
| ||
| Theorem | divcli 10767 | Closure law for division. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.) |
| | ||
| Theorem | divcan2i 10768 | A cancellation law for division. (Contributed by NM, 9-Feb-1995.) |
| | ||
| Theorem | divcan1i 10769 | A cancellation law for division. (Contributed by NM, 18-May-1999.) |
| | ||
| Theorem | divreci 10770 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.) |
|
| ||
| Theorem | divcan3i 10771 | A cancellation law for division. (Contributed by NM, 16-Feb-1995.) |
| | ||
| Theorem | divcan4i 10772 | A cancellation law for division. (Contributed by NM, 18-May-1999.) |
| | ||
| Theorem | divne0i 10773 | The ratio of nonzero numbers is nonzero. (Contributed by NM, 9-Feb-1995.) |
| | ||
| Theorem | rec11ii 10774 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) |
|
| ||
| Theorem | divasszi 10775 | An associative law for division. (Contributed by NM, 12-Aug-1999.) |
| | ||
| Theorem | divmulzi 10776 | Relationship between division and multiplication. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.) |
|
| ||
| Theorem | divdirzi 10777 | Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) |
|
| ||
| Theorem | divdiv23zi 10778 | Swap denominators in a division. (Contributed by NM, 15-Sep-1999.) |
|
| ||
| Theorem | divmuli 10779 | Relationship between division and multiplication. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.) |
|
| ||
| Theorem | divdiv32i 10780 | Swap denominators in a division. (Contributed by NM, 15-Sep-1999.) |
|
| ||
| Theorem | divassi 10781 | An associative law for division. (Contributed by NM, 15-Feb-1995.) |
|
| ||
| Theorem | divdiri 10782 | Distribution of division over addition. (Contributed by NM, 16-Feb-1995.) |
|
| ||
| Theorem | div23i 10783 | A commutative/associative law for division. (Contributed by NM, 3-Sep-1999.) |
|
| ||
| Theorem | div11i 10784 | One-to-one relationship for division. (Contributed by NM, 20-Aug-2001.) |
|
| ||
| Theorem | divmuldivi 10785 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 16-Feb-1995.) |
|
| ||
| Theorem | divmul13i 10786 | Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999.) |
|
| ||
| Theorem | divadddivi 10787 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 21-Feb-1995.) |
|
| ||
| Theorem | divdivdivi 10788 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 22-Feb-1995.) |
|
| ||
| Theorem | rerecclzi 10789 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | rereccli 10790 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | redivclzi 10791 | Closure law for division of reals. (Contributed by NM, 9-May-1999.) |
|
| ||
| Theorem | redivcli 10792 | Closure law for division of reals. (Contributed by NM, 9-May-1999.) |
| | ||
| Theorem | div1d 10793 | A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | reccld 10794 | Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | recne0d 10795 | The reciprocal of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | recidd 10796 | Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | recid2d 10797 | Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | recrecd 10798 | A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | dividd 10799 | A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | div0d 10800 | Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |