Home | Metamath
Proof Explorer Theorem List (p. 121 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lt2msqi 12001 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) | ||
Theorem | le2msqi 12002 | The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ (๐ด โค ๐ต โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ต))) | ||
Theorem | msq11i 12003 | The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 โค ๐ด โง 0 โค ๐ต) โ ((๐ด ยท ๐ด) = (๐ต ยท ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | divgt0i2i 12004 | The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ต โ โข (0 < ๐ด โ 0 < (๐ด / ๐ต)) | ||
Theorem | ltrecii 12005 | The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ด & โข 0 < ๐ต โ โข (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด)) | ||
Theorem | divgt0ii 12006 | The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ด & โข 0 < ๐ต โ โข 0 < (๐ด / ๐ต) | ||
Theorem | ltmul1i 12007 | 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 12008 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ))) | ||
Theorem | ltmuldivi 12009 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ ((๐ด ยท ๐ถ) < ๐ต โ ๐ด < (๐ต / ๐ถ))) | ||
Theorem | ltmul2i 12010 | 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 12011 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) | ||
Theorem | lemul2i 12012 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (0 < ๐ถ โ (๐ด โค ๐ต โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต))) | ||
Theorem | ltdiv23i 12013 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((0 < ๐ต โง 0 < ๐ถ) โ ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต)) | ||
Theorem | ledivp1i 12014 | "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 12015 | 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 12016 | Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข 0 < ๐ต & โข 0 < ๐ถ โ โข ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต) | ||
Theorem | ltmul1ii 12017 | 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 12018 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ & โข 0 < ๐ถ โ โข (๐ด < ๐ต โ (๐ด / ๐ถ) < (๐ต / ๐ถ)) | ||
Theorem | ltp1d 12019 | A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด < (๐ด + 1)) | ||
Theorem | lep1d 12020 | A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โค (๐ด + 1)) | ||
Theorem | ltm1d 12021 | A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด โ 1) < ๐ด) | ||
Theorem | lem1d 12022 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด โ 1) โค ๐ด) | ||
Theorem | recgt0d 12023 | 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 12024 | The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด) & โข (๐ โ 0 < ๐ต) โ โข (๐ โ 0 < (๐ด / ๐ต)) | ||
Theorem | mulgt1d 12025 | The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 1 < ๐ด) & โข (๐ โ 1 < ๐ต) โ โข (๐ โ 1 < (๐ด ยท ๐ต)) | ||
Theorem | lemulge11d 12026 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 1 โค ๐ต) โ โข (๐ โ ๐ด โค (๐ด ยท ๐ต)) | ||
Theorem | lemulge12d 12027 | Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 1 โค ๐ต) โ โข (๐ โ ๐ด โค (๐ต ยท ๐ด)) | ||
Theorem | lemul1ad 12028 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) | ||
Theorem | lemul2ad 12029 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ถ ยท ๐ด) โค (๐ถ ยท ๐ต)) | ||
Theorem | ltmul12ad 12030 | Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด < ๐ต) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ถ < ๐ท) โ โข (๐ โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ท)) | ||
Theorem | lemul12ad 12031 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โค ๐ท) โ โข (๐ โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท)) | ||
Theorem | lemul12bd 12032 | Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ท) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ถ โค ๐ท) โ โข (๐ โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท)) | ||
Theorem | fimaxre 12033* | 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 12034* | 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 12035* | A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.) |
โข ((๐ด โ Fin โง โ๐ฆ โ ๐ด ๐ต โ โ) โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ต โค ๐ฅ) | ||
Theorem | fiminre 12036* | A nonempty finite set of real numbers has a minimum. Analogous to fimaxre 12033. (Contributed by AV, 9-Aug-2020.) (Proof shortened by Steven Nguyen, 3-Jun-2023.) |
โข ((๐ด โ โ โง ๐ด โ Fin โง ๐ด โ โ ) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | fiminre2 12037* | A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข ((๐ด โ โ โง ๐ด โ Fin) โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | negfi 12038* | The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.) |
โข ((๐ด โ โ โง ๐ด โ Fin) โ {๐ โ โ โฃ -๐ โ ๐ด} โ Fin) | ||
Theorem | lbreu 12039* | If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.) |
โข ((๐ โ โ โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ฅ โค ๐ฆ) โ โ!๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ฅ โค ๐ฆ) | ||
Theorem | lbcl 12040* | 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 12041* | 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 12042* | 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 12043* | 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 12044* | 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 12045* | 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 12046* | A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง))) | ||
Theorem | infm3lem 12047* | Lemma for infm3 12048. (Contributed by NM, 14-Jun-2005.) |
โข (๐ฅ โ โ โ โ๐ฆ โ โ ๐ฅ = -๐ฆ) | ||
Theorem | infm3 12048* | 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 12046.) (Contributed by NM, 14-Jun-2005.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) โ โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฆ < ๐ฅ โง โ๐ฆ โ โ (๐ฅ < ๐ฆ โ โ๐ง โ ๐ด ๐ง < ๐ฆ))) | ||
Theorem | suprcl 12049* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) โ โ) | ||
Theorem | suprub 12050* | 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 12051* | Natural deduction form of suprubd 12051. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ ๐ด) โ โข (๐ โ ๐ต โค sup(๐ด, โ, < )) | ||
Theorem | suprcld 12052* | Natural deduction form of suprcl 12049. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ โ sup(๐ด, โ, < ) โ โ) | ||
Theorem | suprlub 12053* | 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 12054* | 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 12055* | 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 12056* | The supremum function distributes over addition in a sense similar to that in supmul1 12058. (Contributed by Brendan Leahy, 25-Sep-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ โ) & โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด ๐ง = (๐ฃ + ๐ต)} โ โข (๐ โ (sup(๐ด, โ, < ) + ๐ต) = sup(๐ถ, โ, < )) | ||
Theorem | supadd 12057* | The supremum function distributes over addition in a sense similar to that in supmul 12061. (Contributed by Brendan Leahy, 26-Sep-2017.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) & โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ + ๐)} โ โข (๐ โ (sup(๐ด, โ, < ) + sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) | ||
Theorem | supmul1 12058* | 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 12061 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ต ๐ง = (๐ด ยท ๐ฃ)} & โข (๐ โ ((๐ด โ โ โง 0 โค ๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ (๐ด ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) | ||
Theorem | supmullem1 12059* | Lemma for supmul 12061. (Contributed by Mario Carneiro, 5-Jul-2013.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} & โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < ))) | ||
Theorem | supmullem2 12060* | Lemma for supmul 12061. (Contributed by Mario Carneiro, 5-Jul-2013.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} & โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ (๐ถ โ โ โง ๐ถ โ โ โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ)) | ||
Theorem | supmul 12061* | 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 10854). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.) |
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} & โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) โ โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) | ||
Theorem | sup3ii 12062* | A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง)) | ||
Theorem | suprclii 12063* | Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.) |
โข (๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข sup(๐ด, โ, < ) โ โ | ||
Theorem | suprubii 12064* | 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 12065* | 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 12066* | 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 12067* | 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 12068* | The negative of the unique real such that ๐. (Contributed by NM, 13-Jun-2005.) |
โข (๐ฅ = -๐ฆ โ (๐ โ ๐)) โ โข (โ!๐ฅ โ โ ๐ โ (โฉ๐ฅ โ โ ๐) = -(โฉ๐ฆ โ โ ๐)) | ||
Theorem | negiso 12069 | 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 12070* | The infimum of a set of reals ๐ด. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
โข (๐ด โ โ โ inf(๐ด, โ, < ) = โช {๐ฅ โ โ โฃ (โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ โง โ๐ฆ โ โ (๐ฅ < ๐ฆ โ โ๐ง โ ๐ด ๐ง < ๐ฆ))}) | ||
Theorem | infrecl 12071* | 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 12072* | 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 12073* | 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 12074* | 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 12075 | 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(๐ต, โ, < ) โค ๐ด) | ||
Theorem | supfirege 12076 | The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019.) |
โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ถ โ ๐ต) & โข (๐ โ ๐ = sup(๐ต, โ, < )) โ โข (๐ โ ๐ถ โค ๐) | ||
Theorem | inelr 12077 | The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.) |
โข ยฌ i โ โ | ||
Theorem | rimul 12078 | A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง (i ยท ๐ด) โ โ) โ ๐ด = 0) | ||
Theorem | cru 12079 | The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท)) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) | ||
Theorem | crne0 12080 | The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ 0 โจ ๐ต โ 0) โ (๐ด + (i ยท ๐ต)) โ 0)) | ||
Theorem | creur 12081* | The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข (๐ด โ โ โ โ!๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) | ||
Theorem | creui 12082* | The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข (๐ด โ โ โ โ!๐ฆ โ โ โ๐ฅ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) | ||
Theorem | cju 12083* | The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.) |
โข (๐ด โ โ โ โ!๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) | ||
Theorem | ofsubeq0 12084 | Function analogue of subeq0 11361. (Contributed by Mario Carneiro, 24-Jul-2014.) |
โข ((๐ด โ ๐ โง ๐น:๐ดโถโ โง ๐บ:๐ดโถโ) โ ((๐น โf โ ๐บ) = (๐ด ร {0}) โ ๐น = ๐บ)) | ||
Theorem | ofnegsub 12085 | Function analogue of negsub 11383. (Contributed by Mario Carneiro, 24-Jul-2014.) |
โข ((๐ด โ ๐ โง ๐น:๐ดโถโ โง ๐บ:๐ดโถโ) โ (๐น โf + ((๐ด ร {-1}) โf ยท ๐บ)) = (๐น โf โ ๐บ)) | ||
Theorem | ofsubge0 12086 | Function analogue of subge0 11602. (Contributed by Mario Carneiro, 24-Jul-2014.) |
โข ((๐ด โ ๐ โง ๐น:๐ดโถโ โง ๐บ:๐ดโถโ) โ ((๐ด ร {0}) โr โค (๐น โf โ ๐บ) โ ๐บ โr โค ๐น)) | ||
Syntax | cn 12087 | Extend class notation to include the class of positive integers. |
class โ | ||
Definition | df-nn 12088 |
Define the set of positive integers. Some authors, especially in analysis
books, call these the natural numbers, whereas other authors choose to
include 0 in their definition of natural numbers. Note that โ is a
subset of complex numbers (nnsscn 12092), in contrast to the more elementary
ordinal natural numbers ฯ, df-om 7794). See nnind 12105 for the
principle of mathematical induction. See df-n0 12348 for the set of
nonnegative integers โ0. See dfn2 12360
for โ defined in terms of
โ0.
This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9511 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 12101 (or its slight variant dfnn2 12100). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.) |
โข โ = (rec((๐ฅ โ V โฆ (๐ฅ + 1)), 1) โ ฯ) | ||
Theorem | nnexALT 12089 | Alternate proof of nnex 12093, more direct, that makes use of ax-rep 5241. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข โ โ V | ||
Theorem | peano5nni 12090* | Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข ((1 โ ๐ด โง โ๐ฅ โ ๐ด (๐ฅ + 1) โ ๐ด) โ โ โ ๐ด) | ||
Theorem | nnssre 12091 | The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
โข โ โ โ | ||
Theorem | nnsscn 12092 | The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 12091 and ax-resscn 11042 at the cost of using more axioms. (Contributed by NM, 2-Aug-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
โข โ โ โ | ||
Theorem | nnex 12093 | The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข โ โ V | ||
Theorem | nnre 12094 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
โข (๐ด โ โ โ ๐ด โ โ) | ||
Theorem | nncn 12095 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
โข (๐ด โ โ โ ๐ด โ โ) | ||
Theorem | nnrei 12096 | A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
โข ๐ด โ โ โ โข ๐ด โ โ | ||
Theorem | nncni 12097 | A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
โข ๐ด โ โ โ โข ๐ด โ โ | ||
Theorem | 1nn 12098 | Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข 1 โ โ | ||
Theorem | peano2nn 12099 | Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข (๐ด โ โ โ (๐ด + 1) โ โ) | ||
Theorem | dfnn2 12100* | Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 12088 replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) |
โข โ = โฉ {๐ฅ โฃ (1 โ ๐ฅ โง โ๐ฆ โ ๐ฅ (๐ฆ + 1) โ ๐ฅ)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |