![]() |
Metamath
Proof Explorer Theorem List (p. 120 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | divcan4 11901 | A cancellation law for division. (Contributed by NM, 8-Feb-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ด ยท ๐ต) / ๐ต) = ๐ด) | ||
Theorem | div11 11902 | One-to-one relationship for division. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด / ๐ถ) = (๐ต / ๐ถ) โ ๐ด = ๐ต)) | ||
Theorem | divid 11903 | A number divided by itself is one. (Contributed by NM, 1-Aug-2004.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (๐ด / ๐ด) = 1) | ||
Theorem | div0 11904 | Division into zero is zero. (Contributed by NM, 14-Mar-2005.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (0 / ๐ด) = 0) | ||
Theorem | div1 11905 | A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข (๐ด โ โ โ (๐ด / 1) = ๐ด) | ||
Theorem | 1div1e1 11906 | 1 divided by 1 is 1. (Contributed by David A. Wheeler, 7-Dec-2018.) |
โข (1 / 1) = 1 | ||
Theorem | diveq1 11907 | Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ด / ๐ต) = 1 โ ๐ด = ๐ต)) | ||
Theorem | divneg 11908 | Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ -(๐ด / ๐ต) = (-๐ด / ๐ต)) | ||
Theorem | muldivdir 11909 | Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถ ยท ๐ด) + ๐ต) / ๐ถ) = (๐ด + (๐ต / ๐ถ))) | ||
Theorem | divsubdir 11910 | Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด โ ๐ต) / ๐ถ) = ((๐ด / ๐ถ) โ (๐ต / ๐ถ))) | ||
Theorem | subdivcomb1 11911 | Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถ ยท ๐ด) โ ๐ต) / ๐ถ) = (๐ด โ (๐ต / ๐ถ))) | ||
Theorem | subdivcomb2 11912 | Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด โ (๐ถ ยท ๐ต)) / ๐ถ) = ((๐ด / ๐ถ) โ ๐ต)) | ||
Theorem | recrec 11913 | 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.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / (1 / ๐ด)) = ๐ด) | ||
Theorem | rec11 11914 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((1 / ๐ด) = (1 / ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | rec11r 11915 | Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((1 / ๐ด) = ๐ต โ (1 / ๐ต) = ๐ด)) | ||
Theorem | divmuldiv 11916 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) = ((๐ด ยท ๐ต) / (๐ถ ยท ๐ท))) | ||
Theorem | divdivdiv 11917 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) |
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ต) / (๐ถ / ๐ท)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) | ||
Theorem | divcan5 11918 | Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006.) |
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ถ ยท ๐ด) / (๐ถ ยท ๐ต)) = (๐ด / ๐ต)) | ||
Theorem | divmul13 11919 | Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) = ((๐ต / ๐ถ) ยท (๐ด / ๐ท))) | ||
Theorem | divmul24 11920 | Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) = ((๐ด / ๐ท) ยท (๐ต / ๐ถ))) | ||
Theorem | divmuleq 11921 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) = (๐ต / ๐ท) โ (๐ด ยท ๐ท) = (๐ต ยท ๐ถ))) | ||
Theorem | recdiv 11922 | The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (1 / (๐ด / ๐ต)) = (๐ต / ๐ด)) | ||
Theorem | divcan6 11923 | Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด / ๐ต) ยท (๐ต / ๐ด)) = 1) | ||
Theorem | divdiv32 11924 | Swap denominators in a division. (Contributed by NM, 2-Aug-2004.) |
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด / ๐ต) / ๐ถ) = ((๐ด / ๐ถ) / ๐ต)) | ||
Theorem | divcan7 11925 | Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013.) |
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด / ๐ถ) / (๐ต / ๐ถ)) = (๐ด / ๐ต)) | ||
Theorem | dmdcan 11926 | Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ถ โ โ) โ ((๐ด / ๐ต) ยท (๐ถ / ๐ด)) = (๐ถ / ๐ต)) | ||
Theorem | divdiv1 11927 | Division into a fraction. (Contributed by NM, 31-Dec-2007.) |
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ด / ๐ต) / ๐ถ) = (๐ด / (๐ต ยท ๐ถ))) | ||
Theorem | divdiv2 11928 | Division by a fraction. (Contributed by NM, 27-Dec-2008.) |
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ด / (๐ต / ๐ถ)) = ((๐ด ยท ๐ถ) / ๐ต)) | ||
Theorem | recdiv2 11929 | Division into a reciprocal. (Contributed by NM, 19-Oct-2007.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((1 / ๐ด) / ๐ต) = (1 / (๐ด ยท ๐ต))) | ||
Theorem | ddcan 11930 | Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ด / (๐ด / ๐ต)) = ๐ต) | ||
Theorem | divadddiv 11931 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 2-May-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) + (๐ต / ๐ท)) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) | ||
Theorem | divsubdiv 11932 | Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) โ (๐ต / ๐ท)) = (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) | ||
Theorem | conjmul 11933 | 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.) |
โข (((๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ (((1 / ๐) + (1 / ๐)) = 1 โ ((๐ โ 1) ยท (๐ โ 1)) = 1)) | ||
Theorem | rereccl 11934 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ โ) | ||
Theorem | redivcl 11935 | Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) | ||
Theorem | eqneg 11936 | A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (๐ด โ โ โ (๐ด = -๐ด โ ๐ด = 0)) | ||
Theorem | eqnegd 11937 | A complex number equals its negative iff it is zero. Deduction form of eqneg 11936. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด = -๐ด โ ๐ด = 0)) | ||
Theorem | eqnegad 11938 | If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 11936. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด = -๐ด) โ โข (๐ โ ๐ด = 0) | ||
Theorem | div2neg 11939 | Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (-๐ด / -๐ต) = (๐ด / ๐ต)) | ||
Theorem | divneg2 11940 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ -(๐ด / ๐ต) = (๐ด / -๐ต)) | ||
Theorem | recclzi 11941 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
โข ๐ด โ โ โ โข (๐ด โ 0 โ (1 / ๐ด) โ โ) | ||
Theorem | recne0zi 11942 | The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ โ โข (๐ด โ 0 โ (1 / ๐ด) โ 0) | ||
Theorem | recidzi 11943 | Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ โ โข (๐ด โ 0 โ (๐ด ยท (1 / ๐ด)) = 1) | ||
Theorem | div1i 11944 | A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) |
โข ๐ด โ โ โ โข (๐ด / 1) = ๐ด | ||
Theorem | eqnegi 11945 | A number equal to its negative is zero. (Contributed by NM, 29-May-1999.) |
โข ๐ด โ โ โ โข (๐ด = -๐ด โ ๐ด = 0) | ||
Theorem | reccli 11946 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข (1 / ๐ด) โ โ | ||
Theorem | recidi 11947 | Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข (๐ด ยท (1 / ๐ด)) = 1 | ||
Theorem | recreci 11948 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข (1 / (1 / ๐ด)) = ๐ด | ||
Theorem | dividi 11949 | A number divided by itself is one. (Contributed by NM, 9-Feb-1995.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข (๐ด / ๐ด) = 1 | ||
Theorem | div0i 11950 | Division into zero is zero. (Contributed by NM, 12-Aug-1999.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข (0 / ๐ด) = 0 | ||
Theorem | divclzi 11951 | Closure law for division. (Contributed by NM, 7-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (๐ด / ๐ต) โ โ) | ||
Theorem | divcan1zi 11952 | A cancellation law for division. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ ((๐ด / ๐ต) ยท ๐ต) = ๐ด) | ||
Theorem | divcan2zi 11953 | A cancellation law for division. (Contributed by NM, 10-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (๐ต ยท (๐ด / ๐ต)) = ๐ด) | ||
Theorem | divreczi 11954 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 11-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (๐ด / ๐ต) = (๐ด ยท (1 / ๐ต))) | ||
Theorem | divcan3zi 11955 | A cancellation law for division. (Eliminates a hypothesis of divcan3i 11962 with the weak deduction theorem.) (Contributed by NM, 3-Feb-2004.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ ((๐ต ยท ๐ด) / ๐ต) = ๐ด) | ||
Theorem | divcan4zi 11956 | A cancellation law for division. (Contributed by NM, 12-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ ((๐ด ยท ๐ต) / ๐ต) = ๐ด) | ||
Theorem | rec11i 11957 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((๐ด โ 0 โง ๐ต โ 0) โ ((1 / ๐ด) = (1 / ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | divcli 11958 | Closure law for division. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข (๐ด / ๐ต) โ โ | ||
Theorem | divcan2i 11959 | A cancellation law for division. (Contributed by NM, 9-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข (๐ต ยท (๐ด / ๐ต)) = ๐ด | ||
Theorem | divcan1i 11960 | A cancellation law for division. (Contributed by NM, 18-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข ((๐ด / ๐ต) ยท ๐ต) = ๐ด | ||
Theorem | divreci 11961 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข (๐ด / ๐ต) = (๐ด ยท (1 / ๐ต)) | ||
Theorem | divcan3i 11962 | A cancellation law for division. (Contributed by NM, 16-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข ((๐ต ยท ๐ด) / ๐ต) = ๐ด | ||
Theorem | divcan4i 11963 | A cancellation law for division. (Contributed by NM, 18-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข ((๐ด ยท ๐ต) / ๐ต) = ๐ด | ||
Theorem | divne0i 11964 | The ratio of nonzero numbers is nonzero. (Contributed by NM, 9-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ด โ 0 & โข ๐ต โ 0 โ โข (๐ด / ๐ต) โ 0 | ||
Theorem | rec11ii 11965 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ด โ 0 & โข ๐ต โ 0 โ โข ((1 / ๐ด) = (1 / ๐ต) โ ๐ด = ๐ต) | ||
Theorem | divasszi 11966 | An associative law for division. (Contributed by NM, 12-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (๐ถ โ 0 โ ((๐ด ยท ๐ต) / ๐ถ) = (๐ด ยท (๐ต / ๐ถ))) | ||
Theorem | divmulzi 11967 | Relationship between division and multiplication. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (๐ต โ 0 โ ((๐ด / ๐ต) = ๐ถ โ (๐ต ยท ๐ถ) = ๐ด)) | ||
Theorem | divdirzi 11968 | Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (๐ถ โ 0 โ ((๐ด + ๐ต) / ๐ถ) = ((๐ด / ๐ถ) + (๐ต / ๐ถ))) | ||
Theorem | divdiv23zi 11969 | Swap denominators in a division. (Contributed by NM, 15-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ต โ 0 โง ๐ถ โ 0) โ ((๐ด / ๐ต) / ๐ถ) = ((๐ด / ๐ถ) / ๐ต)) | ||
Theorem | divmuli 11970 | Relationship between division and multiplication. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ต โ 0 โ โข ((๐ด / ๐ต) = ๐ถ โ (๐ต ยท ๐ถ) = ๐ด) | ||
Theorem | divdiv32i 11971 | Swap denominators in a division. (Contributed by NM, 15-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ต โ 0 & โข ๐ถ โ 0 โ โข ((๐ด / ๐ต) / ๐ถ) = ((๐ด / ๐ถ) / ๐ต) | ||
Theorem | divassi 11972 | An associative law for division. (Contributed by NM, 15-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ถ โ 0 โ โข ((๐ด ยท ๐ต) / ๐ถ) = (๐ด ยท (๐ต / ๐ถ)) | ||
Theorem | divdiri 11973 | Distribution of division over addition. (Contributed by NM, 16-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ถ โ 0 โ โข ((๐ด + ๐ต) / ๐ถ) = ((๐ด / ๐ถ) + (๐ต / ๐ถ)) | ||
Theorem | div23i 11974 | A commutative/associative law for division. (Contributed by NM, 3-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ถ โ 0 โ โข ((๐ด ยท ๐ต) / ๐ถ) = ((๐ด / ๐ถ) ยท ๐ต) | ||
Theorem | div11i 11975 | One-to-one relationship for division. (Contributed by NM, 20-Aug-2001.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ถ โ 0 โ โข ((๐ด / ๐ถ) = (๐ต / ๐ถ) โ ๐ด = ๐ต) | ||
Theorem | divmuldivi 11976 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 16-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ & โข ๐ต โ 0 & โข ๐ท โ 0 โ โข ((๐ด / ๐ต) ยท (๐ถ / ๐ท)) = ((๐ด ยท ๐ถ) / (๐ต ยท ๐ท)) | ||
Theorem | divmul13i 11977 | Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ & โข ๐ต โ 0 & โข ๐ท โ 0 โ โข ((๐ด / ๐ต) ยท (๐ถ / ๐ท)) = ((๐ถ / ๐ต) ยท (๐ด / ๐ท)) | ||
Theorem | divadddivi 11978 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 21-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ & โข ๐ต โ 0 & โข ๐ท โ 0 โ โข ((๐ด / ๐ต) + (๐ถ / ๐ท)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) / (๐ต ยท ๐ท)) | ||
Theorem | divdivdivi 11979 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 22-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข ๐ท โ โ & โข ๐ต โ 0 & โข ๐ท โ 0 & โข ๐ถ โ 0 โ โข ((๐ด / ๐ต) / (๐ถ / ๐ท)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)) | ||
Theorem | rerecclzi 11980 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
โข ๐ด โ โ โ โข (๐ด โ 0 โ (1 / ๐ด) โ โ) | ||
Theorem | rereccli 11981 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
โข ๐ด โ โ & โข ๐ด โ 0 โ โข (1 / ๐ด) โ โ | ||
Theorem | redivclzi 11982 | Closure law for division of reals. (Contributed by NM, 9-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (๐ด / ๐ต) โ โ) | ||
Theorem | redivcli 11983 | Closure law for division of reals. (Contributed by NM, 9-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ต โ 0 โ โข (๐ด / ๐ต) โ โ | ||
Theorem | div1d 11984 | A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด / 1) = ๐ด) | ||
Theorem | reccld 11985 | Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (1 / ๐ด) โ โ) | ||
Theorem | recne0d 11986 | The reciprocal of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (1 / ๐ด) โ 0) | ||
Theorem | recidd 11987 | Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (๐ด ยท (1 / ๐ด)) = 1) | ||
Theorem | recid2d 11988 | Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ ((1 / ๐ด) ยท ๐ด) = 1) | ||
Theorem | recrecd 11989 | A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (1 / (1 / ๐ด)) = ๐ด) | ||
Theorem | dividd 11990 | A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (๐ด / ๐ด) = 1) | ||
Theorem | div0d 11991 | Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (0 / ๐ด) = 0) | ||
Theorem | divcld 11992 | Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ด / ๐ต) โ โ) | ||
Theorem | divcan1d 11993 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ ((๐ด / ๐ต) ยท ๐ต) = ๐ด) | ||
Theorem | divcan2d 11994 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ต ยท (๐ด / ๐ต)) = ๐ด) | ||
Theorem | divrecd 11995 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ด / ๐ต) = (๐ด ยท (1 / ๐ต))) | ||
Theorem | divrec2d 11996 | Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ด / ๐ต) = ((1 / ๐ต) ยท ๐ด)) | ||
Theorem | divcan3d 11997 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ ((๐ต ยท ๐ด) / ๐ต) = ๐ด) | ||
Theorem | divcan4d 11998 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ ((๐ด ยท ๐ต) / ๐ต) = ๐ด) | ||
Theorem | diveq0d 11999 | A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ (๐ด / ๐ต) = 0) โ โข (๐ โ ๐ด = 0) | ||
Theorem | diveq1d 12000 | Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ (๐ด / ๐ต) = 1) โ โข (๐ โ ๐ด = ๐ต) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |