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