Home | Metamath
Proof Explorer Theorem List (p. 110 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 | lt2mul2div 10901 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
Theorem | ledivmul2 10902 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
Theorem | lemuldiv 10903 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
Theorem | lemuldiv2 10904 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
Theorem | ltrec 10905 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | lerec 10906 | 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.) |
Theorem | lt2msq1 10907 | Lemma for lt2msq 10908. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lt2msq 10908 | Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | ltdiv2 10909 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
Theorem | ltrec1 10910 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
Theorem | lerec2 10911 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
Theorem | ledivdiv 10912 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
Theorem | lediv2 10913 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.) |
Theorem | ltdiv23 10914 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
Theorem | lediv23 10915 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
Theorem | lediv12a 10916 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
Theorem | lediv2a 10917 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
Theorem | reclt1 10918 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
Theorem | recgt1 10919 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
Theorem | recgt1i 10920 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
Theorem | recp1lt1 10921 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
Theorem | recreclt 10922 | Given a positive number , construct a new positive number less than both and 1. (Contributed by NM, 28-Dec-2005.) |
Theorem | le2msq 10923 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | msq11 10924 | 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.) |
Theorem | ledivp1 10925 | 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.) |
Theorem | squeeze0 10926* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
Theorem | ltp1i 10927 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
Theorem | recgt0i 10928 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
Theorem | recgt0ii 10929 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
Theorem | prodgt0i 10930 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
Theorem | prodge0i 10931 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) |
Theorem | divgt0i 10932 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | divge0i 10933 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
Theorem | ltreci 10934 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
Theorem | lereci 10935 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
Theorem | lt2msqi 10936 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
Theorem | le2msqi 10937 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
Theorem | msq11i 10938 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
Theorem | divgt0i2i 10939 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | ltrecii 10940 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
Theorem | divgt0ii 10941 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
Theorem | ltmul1i 10942 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
Theorem | ltdiv1i 10943 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
Theorem | ltmuldivi 10944 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
Theorem | ltmul2i 10945 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
Theorem | lemul1i 10946 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
Theorem | lemul2i 10947 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
Theorem | ltdiv23i 10948 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
Theorem | ledivp1i 10949 | Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
Theorem | ltdivp1i 10950 | Less-than and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
Theorem | ltdiv23ii 10951 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
Theorem | ltmul1ii 10952 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.) |
Theorem | ltdiv1ii 10953 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
Theorem | ltp1d 10954 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lep1d 10955 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltm1d 10956 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lem1d 10957 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | recgt0d 10958 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | divgt0d 10959 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | mulgt1d 10960 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemulge11d 10961 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemulge12d 10962 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul1ad 10963 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul2ad 10964 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltmul12ad 10965 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul12ad 10966 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lemul12bd 10967 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | fimaxre 10968* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fimaxre2 10969* | A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.) |
Theorem | fimaxre3 10970* | A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.) |
Theorem | negfi 10971* | The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.) |
Theorem | fiminre 10972* | A nonempty finite set of real numbers has a minimum. Analogous to fimaxre 10968. (Contributed by AV, 9-Aug-2020.) |
Theorem | lbreu 10973* | If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.) |
Theorem | lbcl 10974* | If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
Theorem | lble 10975* | If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | lbinf 10976* | If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
inf | ||
Theorem | lbinfcl 10977* | If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
inf | ||
Theorem | lbinfle 10978* | If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
inf | ||
Theorem | sup2 10979* | A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997.) |
Theorem | sup3 10980* | A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.) |
Theorem | infm3lem 10981* | Lemma for infm3 10982. (Contributed by NM, 14-Jun-2005.) |
Theorem | infm3 10982* | The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 10980.) (Contributed by NM, 14-Jun-2005.) |
Theorem | suprcl 10983* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.) |
Theorem | suprub 10984* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004.) |
Theorem | suprubd 10985* | Natural deduction form of suprubd 10985. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | suprcld 10986* | Natural deduction form of suprcl 10983. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | suprlub 10987* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
Theorem | suprnub 10988* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
Theorem | suprleub 10989* | The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.) |
Theorem | supaddc 10990* | The supremum function distributes over addition in a sense similar to that in supmul1 10992. (Contributed by Brendan Leahy, 25-Sep-2017.) |
Theorem | supadd 10991* | The supremum function distributes over addition in a sense similar to that in supmul 10995. (Contributed by Brendan Leahy, 26-Sep-2017.) |
Theorem | supmul1 10992* | The supremum function distributes over multiplication, in the sense that , where is shorthand for and is defined as below. This is the simple version, with only one set argument; see supmul 10995 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.) |
Theorem | supmullem1 10993* | Lemma for supmul 10995. (Contributed by Mario Carneiro, 5-Jul-2013.) |
Theorem | supmullem2 10994* | Lemma for supmul 10995. (Contributed by Mario Carneiro, 5-Jul-2013.) |
Theorem | supmul 10995* | The supremum function distributes over multiplication, in the sense that , where is shorthand for and is defined as below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp 9806). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.) |
Theorem | sup3ii 10996* | A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.) |
Theorem | suprclii 10997* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.) |
Theorem | suprubii 10998* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999.) |
Theorem | suprlubii 10999* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
Theorem | suprnubii 11000* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |