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