Home | Metamath
Proof Explorer Theorem List (p. 434 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 | xadd0ge2 43301 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ๐ด โค (๐ต +๐ ๐ด)) | ||
Theorem | nepnfltpnf 43302 | An extended real that is not +โ is less than +โ. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข (๐ โ ๐ด โ +โ) & โข (๐ โ ๐ด โ โ*) โ โข (๐ โ ๐ด < +โ) | ||
Theorem | ltadd12dd 43303 | Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ด < ๐ถ) & โข (๐ โ ๐ต < ๐ท) โ โข (๐ โ (๐ด + ๐ต) < (๐ถ + ๐ท)) | ||
Theorem | nemnftgtmnft 43304 | An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข ((๐ด โ โ* โง ๐ด โ -โ) โ -โ < ๐ด) | ||
Theorem | xrgtso 43305 | 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข โก < Or โ* | ||
Theorem | rpex 43306 | The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข โ+ โ V | ||
Theorem | xrge0ge0 43307 | A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข (๐ด โ (0[,]+โ) โ 0 โค ๐ด) | ||
Theorem | xrssre 43308 | A subset of extended reals that does not contain +โ and -โ is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ยฌ +โ โ ๐ด) & โข (๐ โ ยฌ -โ โ ๐ด) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | ssuzfz 43309 | A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ด โ Fin) โ โข (๐ โ ๐ด โ (๐...sup(๐ด, โ, < ))) | ||
Theorem | absfun 43310 | The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข Fun abs | ||
Theorem | infrpge 43311* | The infimum of a nonempty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ โ๐ง โ ๐ด ๐ง โค (inf(๐ด, โ*, < ) +๐ ๐ต)) | ||
Theorem | xrlexaddrp 43312* | If an extended real number ๐ด can be approximated from above, adding positive reals to ๐ต, then ๐ด is less than or equal to ๐ต. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข ((๐ โง ๐ฅ โ โ+) โ ๐ด โค (๐ต +๐ ๐ฅ)) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | supsubc 43313* | The supremum function distributes over subtraction in a sense similar to that in supaddc 12056. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ โ ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) & โข (๐ โ ๐ต โ โ) & โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด ๐ง = (๐ฃ โ ๐ต)} โ โข (๐ โ (sup(๐ด, โ, < ) โ ๐ต) = sup(๐ถ, โ, < )) | ||
Theorem | xralrple2 43314* | Show that ๐ด is less than ๐ต by showing that there is no positive bound on the difference. A variant on xralrple 13053. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ (0[,)+โ)) โ โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค ((1 + ๐ฅ) ยท ๐ต))) | ||
Theorem | nnuzdisj 43315 | The first ๐ elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
โข ((1...๐) โฉ (โคโฅโ(๐ + 1))) = โ | ||
Theorem | ltdivgt1 43316 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (1 < ๐ต โ (๐ด / ๐ต) < ๐ด)) | ||
Theorem | xrltned 43317 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ด โ ๐ต) | ||
Theorem | nnsplit 43318 | Express the set of positive integers as the disjoint (see nnuzdisj 43315) union of the first ๐ values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
โข (๐ โ โ โ โ = ((1...๐) โช (โคโฅโ(๐ + 1)))) | ||
Theorem | divdiv3d 43319 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ต โ 0) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ ((๐ด / ๐ต) / ๐ถ) = (๐ด / (๐ถ ยท ๐ต))) | ||
Theorem | abslt2sqd 43320 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (absโ๐ด) < (absโ๐ต)) โ โข (๐ โ (๐ดโ2) < (๐ตโ2)) | ||
Theorem | qenom 43321 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
โข โ โ ฯ | ||
Theorem | qct 43322 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
โข โ โผ ฯ | ||
Theorem | xrltnled 43323 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) โ โข (๐ โ (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด)) | ||
Theorem | lenlteq 43324 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ยฌ ๐ด < ๐ต) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | xrred 43325 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ด โ -โ) & โข (๐ โ ๐ด โ +โ) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rr2sscn2 43326 | The cartesian square of โ is a subset of the cartesian square of โ. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (โ ร โ) โ (โ ร โ) | ||
Theorem | infxr 43327* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข โฒ๐ฅ๐ & โข โฒ๐ฆ๐ & โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ โ๐ฅ โ ๐ด ยฌ ๐ฅ < ๐ต) & โข (๐ โ โ๐ฅ โ โ (๐ต < ๐ฅ โ โ๐ฆ โ ๐ด ๐ฆ < ๐ฅ)) โ โข (๐ โ inf(๐ด, โ*, < ) = ๐ต) | ||
Theorem | infxrunb2 43328* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ด โ โ* โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ < ๐ฅ โ inf(๐ด, โ*, < ) = -โ)) | ||
Theorem | infxrbnd2 43329* | The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ด โ โ* โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ โ -โ < inf(๐ด, โ*, < ))) | ||
Theorem | infleinflem1 43330 | Lemma for infleinf 43332, case ๐ต โ โ โง -โ < inf(๐ต, โ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ โ โ+) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โค (inf(๐ต, โ*, < ) +๐ (๐ / 2))) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐ โค (๐ +๐ (๐ / 2))) โ โข (๐ โ inf(๐ด, โ*, < ) โค (inf(๐ต, โ*, < ) +๐ ๐)) | ||
Theorem | infleinflem2 43331 | Lemma for infleinf 43332, when inf(๐ต, โ*, < ) = -โ. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ < (๐ โ 2)) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐ โค (๐ +๐ 1)) โ โข (๐ โ ๐ < ๐ ) | ||
Theorem | infleinf 43332* | If any element of ๐ต can be approximated from above by members of ๐ด, then the infimum of ๐ด is less than or equal to the infimum of ๐ต. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ โ+) โ โ๐ง โ ๐ด ๐ง โค (๐ฅ +๐ ๐ฆ)) โ โข (๐ โ inf(๐ด, โ*, < ) โค inf(๐ต, โ*, < )) | ||
Theorem | xralrple4 43333* | Show that ๐ด is less than ๐ต by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ) โ โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ฅโ๐)))) | ||
Theorem | xralrple3 43334* | Show that ๐ด is less than ๐ต by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) โ โข (๐ โ (๐ด โค ๐ต โ โ๐ฅ โ โ+ ๐ด โค (๐ต + (๐ถ ยท ๐ฅ)))) | ||
Theorem | eluzelzd 43335 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ ๐ โ โค) | ||
Theorem | suplesup2 43336* | If any element of ๐ด is less than or equal to an element in ๐ต, then the supremum of ๐ด is less than or equal to the supremum of ๐ต. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข ((๐ โง ๐ฅ โ ๐ด) โ โ๐ฆ โ ๐ต ๐ฅ โค ๐ฆ) โ โข (๐ โ sup(๐ด, โ*, < ) โค sup(๐ต, โ*, < )) | ||
Theorem | recnnltrp 43337 | ๐ is a natural number large enough that its reciprocal is smaller than the given positive ๐ธ. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข ๐ = ((โโ(1 / ๐ธ)) + 1) โ โข (๐ธ โ โ+ โ (๐ โ โ โง (1 / ๐) < ๐ธ)) | ||
Theorem | nnn0 43338 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข โ โ โ | ||
Theorem | fzct 43339 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐...๐) โผ ฯ | ||
Theorem | rpgtrecnn 43340* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐ด โ โ+ โ โ๐ โ โ (1 / ๐) < ๐ด) | ||
Theorem | fzossuz 43341 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐..^๐) โ (โคโฅโ๐) | ||
Theorem | infxrrefi 43342 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข ((๐ด โ โ โง ๐ด โ Fin โง ๐ด โ โ ) โ inf(๐ด, โ*, < ) = inf(๐ด, โ, < )) | ||
Theorem | xrralrecnnle 43343* | Show that ๐ด is less than ๐ต by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โค ๐ต โ โ๐ โ โ ๐ด โค (๐ต + (1 / ๐)))) | ||
Theorem | fzoct 43344 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
โข (๐..^๐) โผ ฯ | ||
Theorem | frexr 43345 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐น:๐ดโถโ) โ โข (๐ โ ๐น:๐ดโถโ*) | ||
Theorem | nnrecrp 43346 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ โ โ (1 / ๐) โ โ+) | ||
Theorem | reclt0d 43347 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด < 0) โ โข (๐ โ (1 / ๐ด) < 0) | ||
Theorem | lt0neg1dd 43348 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด < 0) โ โข (๐ โ 0 < -๐ด) | ||
Theorem | mnfled 43349 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ -โ โค ๐ด) | ||
Theorem | infxrcld 43350 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ inf(๐ด, โ*, < ) โ โ*) | ||
Theorem | xrralrecnnge 43351* | Show that ๐ด is less than ๐ต by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ*) โ โข (๐ โ (๐ด โค ๐ต โ โ๐ โ โ (๐ด โ (1 / ๐)) โค ๐ต)) | ||
Theorem | reclt0 43352 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (๐ด < 0 โ (1 / ๐ด) < 0)) | ||
Theorem | ltmulneg 43353 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ < 0) โ โข (๐ โ (๐ด < ๐ต โ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ))) | ||
Theorem | allbutfi 43354* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 43042 and eliuniin2 43063 (here, the precondition can be dropped; see eliuniincex 43052). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข ๐ = (โคโฅโ๐) & โข ๐ด = โช ๐ โ ๐ โฉ ๐ โ (โคโฅโ๐)๐ต โ โข (๐ โ ๐ด โ โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ โ ๐ต) | ||
Theorem | ltdiv23neg 43355 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต < 0) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ถ < 0) โ โข (๐ โ ((๐ด / ๐ต) < ๐ถ โ (๐ด / ๐ถ) < ๐ต)) | ||
Theorem | xreqnltd 43356 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ ยฌ ๐ด < ๐ต) | ||
Theorem | mnfnre2 43357 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ยฌ -โ โ โ | ||
Theorem | zssxr 43358 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โค โ โ* | ||
Theorem | fisupclrnmpt 43359* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ Or ๐ด) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ต โ โ ) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ ๐ด) โ โข (๐ โ sup(ran (๐ฅ โ ๐ต โฆ ๐ถ), ๐ด, ๐ ) โ ๐ด) | ||
Theorem | supxrunb3 43360* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ โ sup(๐ด, โ*, < ) = +โ)) | ||
Theorem | elfzod 43361 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐พ โ (โคโฅโ๐)) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ < ๐) โ โข (๐ โ ๐พ โ (๐..^๐)) | ||
Theorem | fimaxre4 43362* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ) | ||
Theorem | ren0 43363 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โ โ โ | ||
Theorem | eluzelz2 43364 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ ๐ โ โค) | ||
Theorem | resabs2d 43365 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ต โ ๐ถ) โ โข (๐ โ ((๐ด โพ ๐ต) โพ ๐ถ) = (๐ด โพ ๐ต)) | ||
Theorem | uzid2 43366 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ (โคโฅโ๐) โ ๐ โ (โคโฅโ๐)) | ||
Theorem | supxrleubrnmpt 43367* | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ โ*) โ โข (๐ โ (sup(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) โค ๐ถ โ โ๐ฅ โ ๐ด ๐ต โค ๐ถ)) | ||
Theorem | uzssre2 43368 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) โ โข ๐ โ โ | ||
Theorem | uzssd 43369 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ (โคโฅโ๐) โ (โคโฅโ๐)) | ||
Theorem | eluzd 43370 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โค ๐) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | infxrlbrnmpt2 43371* | A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ ๐ด) & โข (๐ โ ๐ท โ โ*) & โข (๐ฅ = ๐ถ โ ๐ต = ๐ท) โ โข (๐ โ inf(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) โค ๐ท) | ||
Theorem | xrre4 43372 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (๐ด โ โ โ (๐ด โ -โ โง ๐ด โ +โ))) | ||
Theorem | uz0 43373 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (ยฌ ๐ โ โค โ (โคโฅโ๐) = โ ) | ||
Theorem | eluzelz2d 43374 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ๐ โ โค) | ||
Theorem | infleinf2 43375* | If any element in ๐ต is greater than or equal to an element in ๐ด, then the infimum of ๐ด is less than or equal to the infimum of ๐ต. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข โฒ๐ฆ๐ & โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข ((๐ โง ๐ฅ โ ๐ต) โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ โ inf(๐ด, โ*, < ) โค inf(๐ต, โ*, < )) | ||
Theorem | unb2ltle 43376* | "Unbounded below" expressed with < and with โค. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (โ๐ค โ โ โ๐ฆ โ ๐ด ๐ฆ < ๐ค โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) | ||
Theorem | uzidd2 43377 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ โ โค) & โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ ๐) | ||
Theorem | uzssd2 43378 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ (โคโฅโ๐) โ ๐) | ||
Theorem | rexabslelem 43379* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โ๐ฆ โ โ โ๐ฅ โ ๐ด (absโ๐ต) โค ๐ฆ โ (โ๐ค โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ค โง โ๐ง โ โ โ๐ฅ โ ๐ด ๐ง โค ๐ต))) | ||
Theorem | rexabsle 43380* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โ๐ฆ โ โ โ๐ฅ โ ๐ด (absโ๐ต) โค ๐ฆ โ (โ๐ค โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ค โง โ๐ง โ โ โ๐ฅ โ ๐ด ๐ง โค ๐ต))) | ||
Theorem | allbutfiinf 43381* | Given a "for all but finitely many" condition, the condition holds from ๐ on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) & โข ๐ด = โช ๐ โ ๐ โฉ ๐ โ (โคโฅโ๐)๐ต & โข (๐ โ ๐ โ ๐ด) & โข ๐ = inf({๐ โ ๐ โฃ โ๐ โ (โคโฅโ๐)๐ โ ๐ต}, โ, < ) โ โข (๐ โ (๐ โ ๐ โง โ๐ โ (โคโฅโ๐)๐ โ ๐ต)) | ||
Theorem | supxrrernmpt 43382* | The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ โ ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ) โ โข (๐ โ sup(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) = sup(ran (๐ฅ โ ๐ด โฆ ๐ต), โ, < )) | ||
Theorem | suprleubrnmpt 43383* | The supremum of a nonempty bounded indexed set of reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ โ ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (sup(ran (๐ฅ โ ๐ด โฆ ๐ต), โ, < ) โค ๐ถ โ โ๐ฅ โ ๐ด ๐ต โค ๐ถ)) | ||
Theorem | infrnmptle 43384* | An indexed infimum of extended reals is smaller than another indexed infimum of extended reals, when every indexed element is smaller than the corresponding one. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ*) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ*) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โค ๐ถ) โ โข (๐ โ inf(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) โค inf(ran (๐ฅ โ ๐ด โฆ ๐ถ), โ*, < )) | ||
Theorem | infxrunb3 43385* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ด โ โ* โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ โ inf(๐ด, โ*, < ) = -โ)) | ||
Theorem | uzn0d 43386 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ ๐ โ โค) & โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ โ ) | ||
Theorem | uzssd3 43387 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ (โคโฅโ๐) โ ๐) | ||
Theorem | rexabsle2 43388* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โ๐ฆ โ โ โ๐ฅ โ ๐ด (absโ๐ต) โค ๐ฆ โ (โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ โง โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ฆ โค ๐ต))) | ||
Theorem | infxrunb3rnmpt 43389* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข โฒ๐ฆ๐ & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ*) โ โข (๐ โ (โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ โ inf(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) = -โ)) | ||
Theorem | supxrre3rnmpt 43390* | The indexed supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐ฅ๐ & โข (๐ โ ๐ด โ โ ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (sup(ran (๐ฅ โ ๐ด โฆ ๐ต), โ*, < ) โ โ โ โ๐ฆ โ โ โ๐ฅ โ ๐ด ๐ต โค ๐ฆ)) | ||
Theorem | uzublem 43391* | A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐๐ & โข โฒ๐๐ & โข (๐ โ ๐ โ โค) & โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โ) & โข ๐ = sup(ran (๐ โ (๐...๐พ) โฆ ๐ต), โ, < ) & โข ๐ = if(๐ โค ๐, ๐, ๐) & โข (๐ โ ๐พ โ ๐) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) & โข (๐ โ โ๐ โ (โคโฅโ๐พ)๐ต โค ๐) โ โข (๐ โ โ๐ฅ โ โ โ๐ โ ๐ ๐ต โค ๐ฅ) | ||
Theorem | uzub 43392* | A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข โฒ๐๐ & โข (๐ โ ๐ โ โค) & โข ๐ = (โคโฅโ๐) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ โข (๐ โ (โ๐ฅ โ โ โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ต โค ๐ฅ โ โ๐ฅ โ โ โ๐ โ ๐ ๐ต โค ๐ฅ)) | ||
Theorem | ssrexr 43393 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ*) | ||
Theorem | supxrmnf2 43394 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ* โ sup((๐ด โ {-โ}), โ*, < ) = sup(๐ด, โ*, < )) | ||
Theorem | supxrcli 43395 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ด โ โ* โ โข sup(๐ด, โ*, < ) โ โ* | ||
Theorem | uzid3 43396 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ ๐ โ (โคโฅโ๐)) | ||
Theorem | infxrlesupxr 43397 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 43410. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ด โ โ ) โ โข (๐ โ inf(๐ด, โ*, < ) โค sup(๐ด, โ*, < )) | ||
Theorem | xnegeqd 43398 | Equality of two extended numbers with -๐ in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ -๐๐ด = -๐๐ต) | ||
Theorem | xnegrecl 43399 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ด โ โ โ -๐๐ด โ โ) | ||
Theorem | xnegnegi 43400 | Extended real version of negneg 11385. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข ๐ด โ โ* โ โข -๐-๐๐ด = ๐ด |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |