HomeTheorem List (p. 91 of 167)
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. 91 of 167) | < 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 | div11apd 9001 | One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.) |
           #     | ||
| Theorem | divmuldivapd 9002 | Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.) |
 # # 
| ||
| Theorem | divmuleqapd 9003 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
# #
| ||
| Theorem | rerecclapd 9004 | Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.) |
 # 
| ||
| Theorem | redivclapd 9005 | Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.) |
| #
| ||
| Theorem | diveqap1bd 9006 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8875. Converse of diveqap1d 8968. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.) |
| # | ||
| Theorem | div2subap 9007 | Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.) |
![/\](wedge.gif "/\"){kind=small}
#
| ||
| Theorem | div2subapd 9008 | Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2subap 9007. (Contributed by David Moews, 28-Feb-2017.) |
| #
| ||
| Theorem | subrecap 9009 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.) |
| #
#
| ||
| Theorem | subrecapi 9010 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
| # #
| ||
| Theorem | subrecapd 9011 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
| #
#
| ||
| Theorem | mvllmulapd 9012 | Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| #
| ||
| Theorem | rerecapb 9013* | A real number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 18-Jan-2025.) |
#  
| ||
| Theorem | ltp1 9014 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
  | ||
| Theorem | lep1 9015 | A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.) |
| ||
| Theorem | ltm1 9016 | A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.) |
|
| ||
| Theorem | lem1 9017 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.) |
|
| ||
| Theorem | letrp1 9018 | A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.) |
|
| ||
| Theorem | p1le 9019 | A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.) |
|
| ||
| Theorem | recgt0 9020 | 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.) |
|
| ||
| Theorem | prodgt0gt0 9021 |
Infer that a multiplicand is positive from a positive multiplier and
positive product. See prodgt0 9022 for the same theorem with
replaced by the weaker condition
. (Contributed by Jim
Kingdon, 29-Feb-2020.)
|
|
| ||
| Theorem | prodgt0 9022 | 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.) |
|
| ||
| Theorem | prodgt02 9023 | Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.) |
|
| ||
| Theorem | prodge0 9024 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | prodge02 9025 | Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.) |
|
| ||
| Theorem | ltmul2 9026 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) |
|
| ||
| Theorem | lemul2 9027 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.) |
|
| ||
| Theorem | lemul1a 9028 | 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 9029 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
|
| ||
| Theorem | ltmul12a 9030 | Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.) |
|
| ||
| Theorem | lemul12b 9031 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
|
| ||
| Theorem | lemul12a 9032 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
|
| ||
| Theorem | mulgt1 9033 | The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) |
|
| ||
| Theorem | ltmulgt11 9034 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
| | ||
| Theorem | ltmulgt12 9035 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
| | ||
| Theorem | lemulge11 9036 | Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.) |
|
| ||
| Theorem | lemulge12 9037 | Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.) |
|
| ||
| Theorem | ltdiv1 9038 | 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 9039 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | gt0div 9040 | Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.) |
| | ||
| Theorem | ge0div 9041 | Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.) |
| | ||
| Theorem | divgt0 9042 | The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.) |
|
| ||
| Theorem | divge0 9043 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
|
| ||
| Theorem | ltmuldiv 9044 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | ltmuldiv2 9045 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | ltdivmul 9046 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
|
| ||
| Theorem | ledivmul 9047 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
|
| ||
| Theorem | ltdivmul2 9048 | 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | lt2mul2div 9049 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
|
| ||
| Theorem | ledivmul2 9050 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
|
| ||
| Theorem | lemuldiv 9051 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
|
| ||
| Theorem | lemuldiv2 9052 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
|
| ||
| Theorem | ltrec 9053 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | lerec 9054 | 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 9055 | Lemma for lt2msq 9056. (Contributed by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | lt2msq 9056 | 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 9057 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
|
| ||
| Theorem | ltrec1 9058 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | lerec2 9059 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
|
| ||
| Theorem | ledivdiv 9060 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
|
| ||
| Theorem | lediv2 9061 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.) |
|
| ||
| Theorem | ltdiv23 9062 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
|
| ||
| Theorem | lediv23 9063 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
|
| ||
| Theorem | lediv12a 9064 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
|
| ||
| Theorem | lediv2a 9065 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
|
| ||
| Theorem | reclt1 9066 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.) |
|
| ||
| Theorem | recgt1 9067 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.) |
| | ||
| Theorem | recgt1i 9068 | The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.) |
|
| ||
| Theorem | recp1lt1 9069 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
|
| ||
| Theorem | recreclt 9070 |
Given a positive number , construct a new positive number less than
both and 1.
(Contributed by NM, 28-Dec-2005.)
|
|
| ||
| Theorem | le2msq 9071 | The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | msq11 9072 | 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 9073 | 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 9074* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
| ||
| Theorem | ltp1i 9075 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
|
| ||
| Theorem | recgt0i 9076 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
|
| ||
| Theorem | recgt0ii 9077 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.) |
| | ||
| Theorem | prodgt0i 9078 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
|
| ||
| Theorem | prodge0i 9079 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) |
|
| ||
| Theorem | divgt0i 9080 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
| | ||
| Theorem | divge0i 9081 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
| | ||
| Theorem | ltreci 9082 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
| | ||
| Theorem | lereci 9083 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
| | ||
| Theorem | lt2msqi 9084 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
| | ||
| Theorem | le2msqi 9085 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
| | ||
| Theorem | msq11i 9086 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
| | ||
| Theorem | divgt0i2i 9087 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
|
| ||
| Theorem | ltrecii 9088 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
| | ||
| Theorem | divgt0ii 9089 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
| | ||
| Theorem | ltmul1i 9090 | 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 9091 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
|
| ||
| Theorem | ltmuldivi 9092 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
|
| ||
| Theorem | ltmul2i 9093 | 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 9094 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
|
| ||
| Theorem | lemul2i 9095 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
|
| ||
| Theorem | ltdiv23i 9096 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
|
| ||
| Theorem | ltdiv23ii 9097 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
|
| ||
| Theorem | ltmul1ii 9098 | 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 9099 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
| | ||
| Theorem | ltp1d 9100 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |