Home | Metamath
Proof Explorer Theorem List (p. 120 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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | div12d 11901 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ (๐ด ยท (๐ต / ๐ถ)) = (๐ต ยท (๐ด / ๐ถ))) | ||
Theorem | div23d 11902 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ ((๐ด ยท ๐ต) / ๐ถ) = ((๐ด / ๐ถ) ยท ๐ต)) | ||
Theorem | divdird 11903 | Distribution of division over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ ((๐ด + ๐ต) / ๐ถ) = ((๐ด / ๐ถ) + (๐ต / ๐ถ))) | ||
Theorem | divsubdird 11904 | Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ ((๐ด โ ๐ต) / ๐ถ) = ((๐ด / ๐ถ) โ (๐ต / ๐ถ))) | ||
Theorem | div11d 11905 | One-to-one relationship for division. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ โ 0) & โข (๐ โ (๐ด / ๐ถ) = (๐ต / ๐ถ)) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | divmuldivd 11906 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) โ โข (๐ โ ((๐ด / ๐ต) ยท (๐ถ / ๐ท)) = ((๐ด ยท ๐ถ) / (๐ต ยท ๐ท))) | ||
Theorem | divmul13d 11907 | Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) โ โข (๐ โ ((๐ด / ๐ต) ยท (๐ถ / ๐ท)) = ((๐ถ / ๐ต) ยท (๐ด / ๐ท))) | ||
Theorem | divmul24d 11908 | Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) โ โข (๐ โ ((๐ด / ๐ต) ยท (๐ถ / ๐ท)) = ((๐ด / ๐ท) ยท (๐ถ / ๐ต))) | ||
Theorem | divadddivd 11909 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) โ โข (๐ โ ((๐ด / ๐ต) + (๐ถ / ๐ท)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) / (๐ต ยท ๐ท))) | ||
Theorem | divsubdivd 11910 | Subtraction of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) โ โข (๐ โ ((๐ด / ๐ต) โ (๐ถ / ๐ท)) = (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) / (๐ต ยท ๐ท))) | ||
Theorem | divmuleqd 11911 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) โ โข (๐ โ ((๐ด / ๐ต) = (๐ถ / ๐ท) โ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต))) | ||
Theorem | divdivdivd 11912 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ท โ 0) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ ((๐ด / ๐ต) / (๐ถ / ๐ท)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) | ||
Theorem | diveq1bd 11913 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 11780. Converse of diveq1d 11873. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ด / ๐ต) = 1) | ||
Theorem | div2sub 11914 | Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ โง ๐ถ โ ๐ท)) โ ((๐ด โ ๐ต) / (๐ถ โ ๐ท)) = ((๐ต โ ๐ด) / (๐ท โ ๐ถ))) | ||
Theorem | div2subd 11915 | Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 11914. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ถ โ ๐ท) โ โข (๐ โ ((๐ด โ ๐ต) / (๐ถ โ ๐ท)) = ((๐ต โ ๐ด) / (๐ท โ ๐ถ))) | ||
Theorem | rereccld 11916 | Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (1 / ๐ด) โ โ) | ||
Theorem | redivcld 11917 | Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ด / ๐ต) โ โ) | ||
Theorem | subrec 11918 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((1 / ๐ด) โ (1 / ๐ต)) = ((๐ต โ ๐ด) / (๐ด ยท ๐ต))) | ||
Theorem | subreci 11919 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ด โ 0 & โข ๐ต โ 0 โ โข ((1 / ๐ด) โ (1 / ๐ต)) = ((๐ต โ ๐ด) / (๐ด ยท ๐ต)) | ||
Theorem | subrecd 11920 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ ((1 / ๐ด) โ (1 / ๐ต)) = ((๐ต โ ๐ด) / (๐ด ยท ๐ต))) | ||
Theorem | mvllmuld 11921 | Move the left term in a product on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ (๐ด ยท ๐ต) = ๐ถ) โ โข (๐ โ ๐ต = (๐ถ / ๐ด)) | ||
Theorem | mvllmuli 11922 | Move the left term in a product on the LHS to the RHS, inference form. Uses divcan4i 11836. (Contributed by David A. Wheeler, 11-Oct-2018.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ด โ 0 & โข (๐ด ยท ๐ต) = ๐ถ โ โข ๐ต = (๐ถ / ๐ด) | ||
Theorem | ldiv 11923 | Left-division. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ ((๐ด ยท ๐ต) = ๐ถ โ ๐ด = (๐ถ / ๐ต))) | ||
Theorem | rdiv 11924 | Right-division. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ ((๐ด ยท ๐ต) = ๐ถ โ ๐ต = (๐ถ / ๐ด))) | ||
Theorem | mdiv 11925 | A division law. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (๐ด = (๐ถ / ๐ต) โ ๐ต = (๐ถ / ๐ด))) | ||
Theorem | lineq 11926 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (((๐ด ยท ๐) + ๐ต) = ๐ โ ๐ = ((๐ โ ๐ต) / ๐ด))) | ||
Theorem | elimgt0 11927 | Hypothesis for weak deduction theorem to eliminate 0 < ๐ด. (Contributed by NM, 15-May-1999.) |
โข 0 < if(0 < ๐ด, ๐ด, 1) | ||
Theorem | elimge0 11928 | Hypothesis for weak deduction theorem to eliminate 0 โค ๐ด. (Contributed by NM, 30-Jul-1999.) |
โข 0 โค if(0 โค ๐ด, ๐ด, 0) | ||
Theorem | ltp1 11929 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
โข (๐ด โ โ โ ๐ด < (๐ด + 1)) | ||
Theorem | lep1 11930 | A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.) |
โข (๐ด โ โ โ ๐ด โค (๐ด + 1)) | ||
Theorem | ltm1 11931 | A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.) |
โข (๐ด โ โ โ (๐ด โ 1) < ๐ด) | ||
Theorem | lem1 11932 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.) |
โข (๐ด โ โ โ (๐ด โ 1) โค ๐ด) | ||
Theorem | letrp1 11933 | A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โค ๐ต) โ ๐ด โค (๐ต + 1)) | ||
Theorem | p1le 11934 | A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + 1) โค ๐ต) โ ๐ด โค ๐ต) | ||
Theorem | recgt0 11935 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 25-Aug-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ 0 < (1 / ๐ด)) | ||
Theorem | prodgt0 11936 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 < ๐ต) | ||
Theorem | prodgt02 11937 | Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ต โง 0 < (๐ด ยท ๐ต))) โ 0 < ๐ด) | ||
Theorem | ltmul1a 11938 | Lemma for ltmul1 11939. Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 15-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โง ๐ด < ๐ต) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ)) | ||
Theorem | ltmul1 11939 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ))) | ||
Theorem | ltmul2 11940 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ถ ยท ๐ด) < (๐ถ ยท ๐ต))) | ||
Theorem | lemul1 11941 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) | ||
Theorem | lemul2 11942 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด โค ๐ต โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต))) | ||
Theorem | lemul1a 11943 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค ๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) | ||
Theorem | lemul2a 11944 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค ๐ถ)) โง ๐ด โค ๐ต) โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต)) | ||
Theorem | ltmul12a 11945 | Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.) |
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด < ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 โค ๐ถ โง ๐ถ < ๐ท))) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) | ||
Theorem | lemul12b 11946 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
โข ((((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ) โง (๐ถ โ โ โง (๐ท โ โ โง 0 โค ๐ท))) โ ((๐ด โค ๐ต โง ๐ถ โค ๐ท) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท))) | ||
Theorem | lemul12a 11947 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
โข ((((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ) โง ((๐ถ โ โ โง 0 โค ๐ถ) โง ๐ท โ โ)) โ ((๐ด โค ๐ต โง ๐ถ โค ๐ท) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท))) | ||
Theorem | mulgt1 11948 | The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (1 < ๐ด โง 1 < ๐ต)) โ 1 < (๐ด ยท ๐ต)) | ||
Theorem | ltmulgt11 11949 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 0 < ๐ด) โ (1 < ๐ต โ ๐ด < (๐ด ยท ๐ต))) | ||
Theorem | ltmulgt12 11950 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 0 < ๐ด) โ (1 < ๐ต โ ๐ด < (๐ต ยท ๐ด))) | ||
Theorem | lemulge11 11951 | Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง 1 โค ๐ต)) โ ๐ด โค (๐ด ยท ๐ต)) | ||
Theorem | lemulge12 11952 | Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง 1 โค ๐ต)) โ ๐ด โค (๐ต ยท ๐ด)) | ||
Theorem | ltdiv1 11953 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ))) | ||
Theorem | lediv1 11954 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด โค ๐ต โ (๐ด / ๐ถ) โค (๐ต / ๐ถ))) | ||
Theorem | gt0div 11955 | Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 0 < ๐ต) โ (0 < ๐ด โ 0 < (๐ด / ๐ต))) | ||
Theorem | ge0div 11956 | Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 0 < ๐ต) โ (0 โค ๐ด โ 0 โค (๐ด / ๐ต))) | ||
Theorem | divgt0 11957 | The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < (๐ด / ๐ต)) | ||
Theorem | divge0 11958 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค (๐ด / ๐ต)) | ||
Theorem | mulge0b 11959 | A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค (๐ด ยท ๐ต) โ ((๐ด โค 0 โง ๐ต โค 0) โจ (0 โค ๐ด โง 0 โค ๐ต)))) | ||
Theorem | mulle0b 11960 | A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) โค 0 โ ((๐ด โค 0 โง 0 โค ๐ต) โจ (0 โค ๐ด โง ๐ต โค 0)))) | ||
Theorem | mulsuble0b 11961 | A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด โ ๐ต) ยท (๐ถ โ ๐ต)) โค 0 โ ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โจ (๐ถ โค ๐ต โง ๐ต โค ๐ด)))) | ||
Theorem | ltmuldiv 11962 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด ยท ๐ถ) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | ltmuldiv2 11963 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ถ ยท ๐ด) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | ltdivmul 11964 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ถ) < ๐ต โ ๐ด < (๐ถ ยท ๐ต))) | ||
Theorem | ledivmul 11965 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ถ) โค ๐ต โ ๐ด โค (๐ถ ยท ๐ต))) | ||
Theorem | ltdivmul2 11966 | 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ถ) < ๐ต โ ๐ด < (๐ต ยท ๐ถ))) | ||
Theorem | lt2mul2div 11967 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
โข (((๐ด โ โ โง (๐ต โ โ โง 0 < ๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 < ๐ท))) โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ (๐ด / ๐ท) < (๐ถ / ๐ต))) | ||
Theorem | ledivmul2 11968 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ถ) โค ๐ต โ ๐ด โค (๐ต ยท ๐ถ))) | ||
Theorem | lemuldiv 11969 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด ยท ๐ถ) โค ๐ต โ ๐ด โค (๐ต / ๐ถ))) | ||
Theorem | lemuldiv2 11970 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ถ ยท ๐ด) โค ๐ต โ ๐ด โค (๐ต / ๐ถ))) | ||
Theorem | ltrec 11971 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) | ||
Theorem | lerec 11972 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) | ||
Theorem | lt2msq1 11973 | Lemma for lt2msq 11974. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต)) | ||
Theorem | lt2msq 11974 | Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) | ||
Theorem | ltdiv2 11975 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) | ||
Theorem | ltrec1 11976 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((1 / ๐ด) < ๐ต โ (1 / ๐ต) < ๐ด)) | ||
Theorem | lerec2 11977 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด โค (1 / ๐ต) โ ๐ต โค (1 / ๐ด))) | ||
Theorem | ledivdiv 11978 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
โข ((((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โง ((๐ถ โ โ โง 0 < ๐ถ) โง (๐ท โ โ โง 0 < ๐ท))) โ ((๐ด / ๐ต) โค (๐ถ / ๐ท) โ (๐ท / ๐ถ) โค (๐ต / ๐ด))) | ||
Theorem | lediv2 11979 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด โค ๐ต โ (๐ถ / ๐ต) โค (๐ถ / ๐ด))) | ||
Theorem | ltdiv23 11980 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
โข ((๐ด โ โ โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต)) | ||
Theorem | lediv23 11981 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
โข ((๐ด โ โ โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ต) โค ๐ถ โ (๐ด / ๐ถ) โค ๐ต)) | ||
Theorem | lediv12a 11982 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 < ๐ถ โง ๐ถ โค ๐ท))) โ (๐ด / ๐ท) โค (๐ต / ๐ถ)) | ||
Theorem | lediv2a 11983 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
โข ((((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 โค ๐ถ)) โง ๐ด โค ๐ต) โ (๐ถ / ๐ต) โค (๐ถ / ๐ด)) | ||
Theorem | reclt1 11984 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ (๐ด < 1 โ 1 < (1 / ๐ด))) | ||
Theorem | recgt1 11985 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ (1 < ๐ด โ (1 / ๐ด) < 1)) | ||
Theorem | recgt1i 11986 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
โข ((๐ด โ โ โง 1 < ๐ด) โ (0 < (1 / ๐ด) โง (1 / ๐ด) < 1)) | ||
Theorem | recp1lt1 11987 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (๐ด / (1 + ๐ด)) < 1) | ||
Theorem | recreclt 11988 | Given a positive number ๐ด, construct a new positive number less than both ๐ด and 1. (Contributed by NM, 28-Dec-2005.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ ((1 / (1 + (1 / ๐ด))) < 1 โง (1 / (1 + (1 / ๐ด))) < ๐ด)) | ||
Theorem | le2msq 11989 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ต))) | ||
Theorem | msq11 11990 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) = (๐ต ยท ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | ledivp1 11991 | "Less than or equal to" and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ๐ด) | ||
Theorem | squeeze0 11992* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
โข ((๐ด โ โ โง 0 โค ๐ด โง โ๐ฅ โ โ (0 < ๐ฅ โ ๐ด < ๐ฅ)) โ ๐ด = 0) | ||
Theorem | ltp1i 11993 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
โข ๐ด โ โ โ โข ๐ด < (๐ด + 1) | ||
Theorem | recgt0i 11994 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
โข ๐ด โ โ โ โข (0 < ๐ด โ 0 < (1 / ๐ด)) | ||
Theorem | recgt0ii 11995 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
โข ๐ด โ โ & โข 0 < ๐ด โ โข 0 < (1 / ๐ด) | ||
Theorem | prodgt0i 11996 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 < (๐ด ยท ๐ต)) โ 0 < ๐ต) | ||
Theorem | divgt0i 11997 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ 0 < (๐ด / ๐ต)) | ||
Theorem | divge0i 11998 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 < ๐ต) โ 0 โค (๐ด / ๐ต)) | ||
Theorem | ltreci 11999 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) | ||
Theorem | lereci 12000 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |