HomeTheorem List (p. 90 of 159)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 90 of 159) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lemul2 8901 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.) |
     ![/\](wedge.gif "/\"){kind=small}      
  
| ||
| Theorem | lemul1a 8902 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 21-Feb-2005.) |
|
| ||
| Theorem | lemul2a 8903 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
|
| ||
| Theorem | ltmul12a 8904 | Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.) |
| ||
| Theorem | lemul12b 8905 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
|
| ||
| Theorem | lemul12a 8906 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
|
| ||
| Theorem | mulgt1 8907 | The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) |
| ||
| Theorem | ltmulgt11 8908 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
| | ||
| Theorem | ltmulgt12 8909 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
| | ||
| Theorem | lemulge11 8910 | Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.) |
|
| ||
| Theorem | lemulge12 8911 | Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.) |
|
| ||
| Theorem | ltdiv1 8912 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ||
| Theorem | lediv1 8913 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | gt0div 8914 | Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.) |
| | ||
| Theorem | ge0div 8915 | Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.) |
| | ||
| Theorem | divgt0 8916 | The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.) |
|
| ||
| Theorem | divge0 8917 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
|
| ||
| Theorem | ltmuldiv 8918 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | ltmuldiv2 8919 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | ltdivmul 8920 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | ledivmul 8921 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
|
| ||
| Theorem | ltdivmul2 8922 | 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | lt2mul2div 8923 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
|
| ||
| Theorem | ledivmul2 8924 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
|
| ||
| Theorem | lemuldiv 8925 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
|
| ||
| Theorem | lemuldiv2 8926 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
|
| ||
| Theorem | ltrec 8927 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | lerec 8928 | 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 8929 | Lemma for lt2msq 8930. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | lt2msq 8930 | 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 8931 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
|
| ||
| Theorem | ltrec1 8932 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | lerec2 8933 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | ledivdiv 8934 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
|
| ||
| Theorem | lediv2 8935 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.) |
|
| ||
| Theorem | ltdiv23 8936 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
|
| ||
| Theorem | lediv23 8937 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
|
| ||
| Theorem | lediv12a 8938 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
|
| ||
| Theorem | lediv2a 8939 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
|
| ||
| Theorem | reclt1 8940 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
|
| ||
| Theorem | recgt1 8941 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
| | ||
| Theorem | recgt1i 8942 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
|
| ||
| Theorem | recp1lt1 8943 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
| ||
| Theorem | recreclt 8944 |
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28-Dec-2005.)
|
|
| ||
| Theorem | le2msq 8945 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | msq11 8946 | 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 8947 | 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 8948* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
 
| ||
| Theorem | ltp1i 8949 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
| ||
| Theorem | recgt0i 8950 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
|
| ||
| Theorem | recgt0ii 8951 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
 | ||
| Theorem | prodgt0i 8952 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
|
| ||
| Theorem | prodge0i 8953 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) |
|
| ||
| Theorem | divgt0i 8954 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
| | ||
| Theorem | divge0i 8955 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
| | ||
| Theorem | ltreci 8956 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
| | ||
| Theorem | lereci 8957 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
| | ||
| Theorem | lt2msqi 8958 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
| | ||
| Theorem | le2msqi 8959 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
| | ||
| Theorem | msq11i 8960 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
| | ||
| Theorem | divgt0i2i 8961 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
|
| ||
| Theorem | ltrecii 8962 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
| | ||
| Theorem | divgt0ii 8963 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
| | ||
| Theorem | ltmul1i 8964 | 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 8965 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
|
| ||
| Theorem | ltmuldivi 8966 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
|
| ||
| Theorem | ltmul2i 8967 | 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 8968 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
|
| ||
| Theorem | lemul2i 8969 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
|
| ||
| Theorem | ltdiv23i 8970 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
|
| ||
| Theorem | ltdiv23ii 8971 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
|
| ||
| Theorem | ltmul1ii 8972 | 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 8973 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
| | ||
| Theorem | ltp1d 8974 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
 | ||
| Theorem | lep1d 8975 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | ltm1d 8976 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
 | ||
| Theorem | lem1d 8977 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | recgt0d 8978 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | divgt0d 8979 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | mulgt1d 8980 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemulge11d 8981 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemulge12d 8982 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemul1ad 8983 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | lemul2ad 8984 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | ltmul12ad 8985 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | lemul12ad 8986 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | lemul12bd 8987 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | mulle0r 8988 | Multiplying a nonnegative number by a nonpositive number yields a nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.) |
|
| ||
| Theorem | lbreu 8989* | If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.) |
   
 | ||
| Theorem | lbcl 8990* | 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 8991* | 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 8992* | 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 8993* | 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 8994* | 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 | suprubex 8995* | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-Jan-2022.) |
  | ||
| Theorem | suprlubex 8996* | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-Jan-2022.) |
|
| ||
| Theorem | suprnubex 8997* | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-Jan-2022.) |
|
| ||
| Theorem | suprleubex 8998* | 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 | negiso 8999 | Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.) |
    
| ||
| Theorem | dfinfre 9000* |
The infimum of a set of reals . (Contributed by NM, 9-Oct-2005.)
(Revised by AV, 4-Sep-2020.)
|
inf   
 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |