![]() |
Metamath
Proof Explorer Theorem List (p. 122 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ltrec 12101 | 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 12102 | 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 12103 | Lemma for lt2msq 12104. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต)) | ||
Theorem | lt2msq 12104 | 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 12105 | Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) | ||
Theorem | ltrec1 12106 | Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((1 / ๐ด) < ๐ต โ (1 / ๐ต) < ๐ด)) | ||
Theorem | lerec2 12107 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด โค (1 / ๐ต) โ ๐ต โค (1 / ๐ด))) | ||
Theorem | ledivdiv 12108 | Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.) |
โข ((((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โง ((๐ถ โ โ โง 0 < ๐ถ) โง (๐ท โ โ โง 0 < ๐ท))) โ ((๐ด / ๐ต) โค (๐ถ / ๐ท) โ (๐ท / ๐ถ) โค (๐ต / ๐ด))) | ||
Theorem | lediv2 12109 | 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 12110 | Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.) |
โข ((๐ด โ โ โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต)) | ||
Theorem | lediv23 12111 | Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.) |
โข ((๐ด โ โ โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ด / ๐ต) โค ๐ถ โ (๐ด / ๐ถ) โค ๐ต)) | ||
Theorem | lediv12a 12112 | Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.) |
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โง ((๐ถ โ โ โง ๐ท โ โ) โง (0 < ๐ถ โง ๐ถ โค ๐ท))) โ (๐ด / ๐ท) โค (๐ต / ๐ถ)) | ||
Theorem | lediv2a 12113 | 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 12114 | 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 12115 | 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 12116 | 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 12117 | Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (๐ด / (1 + ๐ด)) < 1) | ||
Theorem | recreclt 12118 | 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 12119 | 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 12120 | 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 12121 | "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 12122* | If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.) |
โข ((๐ด โ โ โง 0 โค ๐ด โง โ๐ฅ โ โ (0 < ๐ฅ โ ๐ด < ๐ฅ)) โ ๐ด = 0) | ||
Theorem | ltp1i 12123 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
โข ๐ด โ โ โ โข ๐ด < (๐ด + 1) | ||
Theorem | recgt0i 12124 | 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 12125 | 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 12126 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 < (๐ด ยท ๐ต)) โ 0 < ๐ต) | ||
Theorem | divgt0i 12127 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ 0 < (๐ด / ๐ต)) | ||
Theorem | divge0i 12128 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 < ๐ต) โ 0 โค (๐ด / ๐ต)) | ||
Theorem | ltreci 12129 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) | ||
Theorem | lereci 12130 | The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) | ||
Theorem | lt2msqi 12131 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) | ||
Theorem | le2msqi 12132 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ (๐ด โค ๐ต โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ต))) | ||
Theorem | msq11i 12133 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ ((๐ด ยท ๐ด) = (๐ต ยท ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | divgt0i2i 12134 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ต โ โข (0 < ๐ด โ 0 < (๐ด / ๐ต)) | ||
Theorem | ltrecii 12135 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ด & โข 0 < ๐ต โ โข (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด)) | ||
Theorem | divgt0ii 12136 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ด & โข 0 < ๐ต โ โข 0 < (๐ด / ๐ต) | ||
Theorem | ltmul1i 12137 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด < ๐ต โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ))) | ||
Theorem | ltdiv1i 12138 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ))) | ||
Theorem | ltmuldivi 12139 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ ((๐ด ยท ๐ถ) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | ltmul2i 12140 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด < ๐ต โ (๐ถ ยท ๐ด) < (๐ถ ยท ๐ต))) | ||
Theorem | lemul1i 12141 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) | ||
Theorem | lemul2i 12142 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด โค ๐ต โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต))) | ||
Theorem | ltdiv23i 12143 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((0 < ๐ต โง 0 < ๐ถ) โ ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต)) | ||
Theorem | ledivp1i 12144 | "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.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ถ โง ๐ด โค (๐ต / (๐ถ + 1))) โ (๐ด ยท ๐ถ) โค ๐ต) | ||
Theorem | ltdivp1i 12145 | Less-than and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท ๐ถ) < ๐ต) | ||
Theorem | ltdiv23ii 12146 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข 0 < ๐ต & โข 0 < ๐ถ โ โข ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต) | ||
Theorem | ltmul1ii 12147 | 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.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข 0 < ๐ถ โ โข (๐ด < ๐ต โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ)) | ||
Theorem | ltdiv1ii 12148 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข 0 < ๐ถ โ โข (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ)) | ||
Theorem | ltp1d 12149 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด < (๐ด + 1)) | ||
Theorem | lep1d 12150 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โค (๐ด + 1)) | ||
Theorem | ltm1d 12151 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด โ 1) < ๐ด) | ||
Theorem | lem1d 12152 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด โ 1) โค ๐ด) | ||
Theorem | recgt0d 12153 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 < ๐ด) โ โข (๐ โ 0 < (1 / ๐ด)) | ||
Theorem | divgt0d 12154 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด) & โข (๐ โ 0 < ๐ต) โ โข (๐ โ 0 < (๐ด / ๐ต)) | ||
Theorem | mulgt1d 12155 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 1 < ๐ด) & โข (๐ โ 1 < ๐ต) โ โข (๐ โ 1 < (๐ด ยท ๐ต)) | ||
Theorem | lemulge11d 12156 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 1 โค ๐ต) โ โข (๐ โ ๐ด โค (๐ด ยท ๐ต)) | ||
Theorem | lemulge12d 12157 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 1 โค ๐ต) โ โข (๐ โ ๐ด โค (๐ต ยท ๐ด)) | ||
Theorem | lemul1ad 12158 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) | ||
Theorem | lemul2ad 12159 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต)) | ||
Theorem | ltmul12ad 12160 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด < ๐ต) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ถ < ๐ท) โ โข (๐ โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) | ||
Theorem | lemul12ad 12161 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โค ๐ท) โ โข (๐ โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท)) | ||
Theorem | lemul12bd 12162 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ท) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โค ๐ท) โ โข (๐ โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท)) | ||
Theorem | fimaxre 12163* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Steven Nguyen, 3-Jun-2023.) |
โข ((๐ด โ โ โง ๐ด โ Fin โง ๐ด โ โ ) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) | ||
Theorem | fimaxre2 12164* | 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.) |
โข ((๐ด โ โ โง ๐ด โ Fin) โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) | ||
Theorem | fimaxre3 12165* | A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.) |
โข ((๐ด โ Fin โง โ๐ฆ โ ๐ด ๐ต โ โ) โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ต โค ๐ฅ) | ||
Theorem | fiminre 12166* | A nonempty finite set of real numbers has a minimum. Analogous to fimaxre 12163. (Contributed by AV, 9-Aug-2020.) (Proof shortened by Steven Nguyen, 3-Jun-2023.) |
โข ((๐ด โ โ โง ๐ด โ Fin โง ๐ด โ โ ) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | fiminre2 12167* | A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข ((๐ด โ โ โง ๐ด โ Fin) โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | negfi 12168* | The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.) |
โข ((๐ด โ โ โง ๐ด โ Fin) โ {๐ โ โ โฃ -๐ โ ๐ด} โ Fin) | ||
Theorem | lbreu 12169* | If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.) |
โข ((๐ โ โ โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ฅ โค ๐ฆ) โ โ!๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ฅ โค ๐ฆ) | ||
Theorem | lbcl 12170* | 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 12171* | 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 12172* | 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 12173* | 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 12174* | 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 12175* | 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 12176* | A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง))) | ||
Theorem | infm3lem 12177* | Lemma for infm3 12178. (Contributed by NM, 14-Jun-2005.) |
โข (๐ฅ โ โ โ โ๐ฆ โ โ ๐ฅ = -๐ฆ) | ||
Theorem | infm3 12178* | 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 12176.) (Contributed by NM, 14-Jun-2005.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) โ โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฆ < ๐ฅ โง โ๐ฆ โ โ (๐ฅ < ๐ฆ โ โ๐ง โ ๐ด ๐ง < ๐ฆ))) | ||
Theorem | suprcl 12179* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) โ โ) | ||
Theorem | suprub 12180* | 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.) |
โข (((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง ๐ต โ ๐ด) โ ๐ต โค sup(๐ด, โ, < )) | ||
Theorem | suprubd 12181* | Natural deduction form of suprubd 12181. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ ๐ด) โ โข (๐ โ ๐ต โค sup(๐ด, โ, < )) | ||
Theorem | suprcld 12182* | Natural deduction form of suprcl 12179. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ โ sup(๐ด, โ, < ) โ โ) | ||
Theorem | suprlub 12183* | 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.) |
โข (((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง ๐ต โ โ) โ (๐ต < sup(๐ด, โ, < ) โ โ๐ง โ ๐ด ๐ต < ๐ง)) | ||
Theorem | suprnub 12184* | 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.) |
โข (((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง ๐ต โ โ) โ (ยฌ ๐ต < sup(๐ด, โ, < ) โ โ๐ง โ ๐ด ยฌ ๐ต < ๐ง)) | ||
Theorem | suprleub 12185* | 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.) |
โข (((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง ๐ต โ โ) โ (sup(๐ด, โ, < ) โค ๐ต โ โ๐ง โ ๐ด ๐ง โค ๐ต)) | ||
Theorem | supaddc 12186* | The supremum function distributes over addition in a sense similar to that in supmul1 12188. (Contributed by Brendan Leahy, 25-Sep-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ โ) & โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด ๐ง = (๐ฃ + ๐ต)} โ โข (๐ โ (sup(๐ด, โ, < ) + ๐ต) = sup(๐ถ, โ, < )) | ||
Theorem | supadd 12187* | The supremum function distributes over addition in a sense similar to that in supmul 12191. (Contributed by Brendan Leahy, 26-Sep-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) & โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ + ๐)} โ โข (๐ โ (sup(๐ด, โ, < ) + sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) | ||
Theorem | supmul1 12188* | The supremum function distributes over multiplication, in the sense that ๐ด ยท (sup๐ต) = sup(๐ด ยท ๐ต), where ๐ด ยท ๐ต is shorthand for {๐ด ยท ๐ โฃ ๐ โ ๐ต} and is defined as ๐ถ below. This is the simple version, with only one set argument; see supmul 12191 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ต ๐ง = (๐ด ยท ๐ฃ)} & โข (๐ โ ((๐ด โ โ โง 0 โค ๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ (๐ด ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) | ||
Theorem | supmullem1 12189* | Lemma for supmul 12191. (Contributed by Mario Carneiro, 5-Jul-2013.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} & โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < ))) | ||
Theorem | supmullem2 12190* | Lemma for supmul 12191. (Contributed by Mario Carneiro, 5-Jul-2013.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} & โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ (๐ถ โ โ โง ๐ถ โ โ โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ)) | ||
Theorem | supmul 12191* | The supremum function distributes over multiplication, in the sense that (sup๐ด) ยท (sup๐ต) = sup(๐ด ยท ๐ต), 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 10983). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} & โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) | ||
Theorem | sup3ii 12192* | A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง)) | ||
Theorem | suprclii 12193* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข sup(๐ด, โ, < ) โ โ | ||
Theorem | suprubii 12194* | 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.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ต โ ๐ด โ ๐ต โค sup(๐ด, โ, < )) | ||
Theorem | suprlubii 12195* | 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.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ต โ โ โ (๐ต < sup(๐ด, โ, < ) โ โ๐ง โ ๐ด ๐ต < ๐ง)) | ||
Theorem | suprnubii 12196* | 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.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ต โ โ โ (ยฌ ๐ต < sup(๐ด, โ, < ) โ โ๐ง โ ๐ด ยฌ ๐ต < ๐ง)) | ||
Theorem | suprleubii 12197* | 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.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ต โ โ โ (sup(๐ด, โ, < ) โค ๐ต โ โ๐ง โ ๐ด ๐ง โค ๐ต)) | ||
Theorem | riotaneg 12198* | The negative of the unique real such that ๐. (Contributed by NM, 13-Jun-2005.) |
โข (๐ฅ = -๐ฆ โ (๐ โ ๐)) โ โข (โ!๐ฅ โ โ ๐ โ (โฉ๐ฅ โ โ ๐) = -(โฉ๐ฆ โ โ ๐)) | ||
Theorem | negiso 12199 | Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.) |
โข ๐น = (๐ฅ โ โ โฆ -๐ฅ) โ โข (๐น Isom < , โก < (โ, โ) โง โก๐น = ๐น) | ||
Theorem | dfinfre 12200* | 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 > |