![]() |
Metamath
Proof Explorer Theorem List (p. 449 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | abslt2sqd 44801 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (absβπ΄) < (absβπ΅)) β β’ (π β (π΄β2) < (π΅β2)) | ||
Theorem | qenom 44802 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β β Ο | ||
Theorem | qct 44803 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β βΌ Ο | ||
Theorem | xrltnled 44804 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ < π΅ β Β¬ π΅ β€ π΄)) | ||
Theorem | lenlteq 44805 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β Β¬ π΄ < π΅) β β’ (π β π΄ = π΅) | ||
Theorem | xrred 44806 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΄ β -β) & β’ (π β π΄ β +β) β β’ (π β π΄ β β) | ||
Theorem | rr2sscn2 44807 | The cartesian square of β is a subset of the cartesian square of β. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (β Γ β) β (β Γ β) | ||
Theorem | infxr 44808* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β βπ₯ β π΄ Β¬ π₯ < π΅) & β’ (π β βπ₯ β β (π΅ < π₯ β βπ¦ β π΄ π¦ < π₯)) β β’ (π β inf(π΄, β*, < ) = π΅) | ||
Theorem | infxrunb2 44809* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ < π₯ β inf(π΄, β*, < ) = -β)) | ||
Theorem | infxrbnd2 44810* | 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 44811 | Lemma for infleinf 44813, case π΅ β β β§ -β < inf(π΅, β*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β β+) & β’ (π β π β π΅) & β’ (π β π β€ (inf(π΅, β*, < ) +π (π / 2))) & β’ (π β π β π΄) & β’ (π β π β€ (π +π (π / 2))) β β’ (π β inf(π΄, β*, < ) β€ (inf(π΅, β*, < ) +π π)) | ||
Theorem | infleinflem2 44812 | Lemma for infleinf 44813, when inf(π΅, β*, < ) = -β. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β β) & β’ (π β π β π΅) & β’ (π β π < (π β 2)) & β’ (π β π β π΄) & β’ (π β π β€ (π +π 1)) β β’ (π β π < π ) | ||
Theorem | infleinf 44813* | 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 44814* | 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 44815* | 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 44816 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β π β β€) | ||
Theorem | suplesup2 44817* | 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 44818 | π 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 44819 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β β β | ||
Theorem | fzct 44820 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π...π) βΌ Ο | ||
Theorem | rpgtrecnn 44821* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π΄ β β+ β βπ β β (1 / π) < π΄) | ||
Theorem | fzossuz 44822 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) β (β€β₯βπ) | ||
Theorem | infxrrefi 44823 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΄ β Fin β§ π΄ β β ) β inf(π΄, β*, < ) = inf(π΄, β, < )) | ||
Theorem | xrralrecnnle 44824* | 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 44825 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) βΌ Ο | ||
Theorem | frexr 44826 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) β β’ (π β πΉ:π΄βΆβ*) | ||
Theorem | nnrecrp 44827 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β β β (1 / π) β β+) | ||
Theorem | reclt0d 44828 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ < 0) β β’ (π β (1 / π΄) < 0) | ||
Theorem | lt0neg1dd 44829 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ < 0) β β’ (π β 0 < -π΄) | ||
Theorem | infxrcld 44830 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β inf(π΄, β*, < ) β β*) | ||
Theorem | xrralrecnnge 44831* | 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 44832 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (π΄ < 0 β (1 / π΄) < 0)) | ||
Theorem | ltmulneg 44833 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β πΆ < 0) β β’ (π β (π΄ < π΅ β (π΅ Β· πΆ) < (π΄ Β· πΆ))) | ||
Theorem | allbutfi 44834* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 44526 and eliuniin2 44547 (here, the precondition can be dropped; see eliuniincex 44536). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = (β€β₯βπ) & β’ π΄ = βͺ π β π β© π β (β€β₯βπ)π΅ β β’ (π β π΄ β βπ β π βπ β (β€β₯βπ)π β π΅) | ||
Theorem | ltdiv23neg 44835 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ < 0) & β’ (π β πΆ β β) & β’ (π β πΆ < 0) β β’ (π β ((π΄ / π΅) < πΆ β (π΄ / πΆ) < π΅)) | ||
Theorem | xreqnltd 44836 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΄ = π΅) β β’ (π β Β¬ π΄ < π΅) | ||
Theorem | mnfnre2 44837 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ Β¬ -β β β | ||
Theorem | zssxr 44838 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β€ β β* | ||
Theorem | fisupclrnmpt 44839* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π Or π΄) & β’ (π β π΅ β Fin) & β’ (π β π΅ β β ) & β’ ((π β§ π₯ β π΅) β πΆ β π΄) β β’ (π β sup(ran (π₯ β π΅ β¦ πΆ), π΄, π ) β π΄) | ||
Theorem | supxrunb3 44840* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ β€ π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | elfzod 44841 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β π β β€) & β’ (π β πΎ < π) β β’ (π β πΎ β (π..^π)) | ||
Theorem | fimaxre4 44842* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β βπ¦ β β βπ₯ β π΄ π΅ β€ π¦) | ||
Theorem | ren0 44843 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β β β | ||
Theorem | eluzelz2 44844 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) β β’ (π β π β π β β€) | ||
Theorem | resabs2d 44845 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΅ β πΆ) β β’ (π β ((π΄ βΎ π΅) βΎ πΆ) = (π΄ βΎ π΅)) | ||
Theorem | uzid2 44846 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β (β€β₯βπ) β π β (β€β₯βπ)) | ||
Theorem | supxrleubrnmpt 44847* | 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 44848 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) β β’ π β β | ||
Theorem | uzssd 44849 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β (β€β₯βπ) β (β€β₯βπ)) | ||
Theorem | eluzd 44850 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β€ π) β β’ (π β π β π) | ||
Theorem | infxrlbrnmpt2 44851* | 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 44852 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (π΄ β β β (π΄ β -β β§ π΄ β +β))) | ||
Theorem | uz0 44853 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (Β¬ π β β€ β (β€β₯βπ) = β ) | ||
Theorem | eluzelz2d 44854 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) β β’ (π β π β β€) | ||
Theorem | infleinf2 44855* | 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 44856* | "Unbounded below" expressed with < and with β€. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (βπ€ β β βπ¦ β π΄ π¦ < π€ β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯)) | ||
Theorem | uzidd2 44857 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π β π) | ||
Theorem | uzssd2 44858 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) β β’ (π β (β€β₯βπ) β π) | ||
Theorem | rexabslelem 44859* | 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 44860* | 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 44861* | Given a "for all but finitely many" condition, the condition holds from π on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ π΄ = βͺ π β π β© π β (β€β₯βπ)π΅ & β’ (π β π β π΄) & β’ π = inf({π β π β£ βπ β (β€β₯βπ)π β π΅}, β, < ) β β’ (π β (π β π β§ βπ β (β€β₯βπ)π β π΅)) | ||
Theorem | supxrrernmpt 44862* | 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 44863* | 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 44864* | 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 44865* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ β€ π₯ β inf(π΄, β*, < ) = -β)) | ||
Theorem | uzn0d 44866 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π β β ) | ||
Theorem | uzssd3 44867 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) β β’ (π β π β (β€β₯βπ) β π) | ||
Theorem | rexabsle2 44868* | 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 44869* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β (βπ¦ β β βπ₯ β π΄ π΅ β€ π¦ β inf(ran (π₯ β π΄ β¦ π΅), β*, < ) = -β)) | ||
Theorem | supxrre3rnmpt 44870* | 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 44871* | 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 44872* | 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 44873 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) β β’ (π β π΄ β β*) | ||
Theorem | supxrmnf2 44874 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β* β sup((π΄ β {-β}), β*, < ) = sup(π΄, β*, < )) | ||
Theorem | supxrcli 44875 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ β β* β β’ sup(π΄, β*, < ) β β* | ||
Theorem | uzid3 44876 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) β β’ (π β π β π β (β€β₯βπ)) | ||
Theorem | infxrlesupxr 44877 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 44890. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) & β’ (π β π΄ β β ) β β’ (π β inf(π΄, β*, < ) β€ sup(π΄, β*, < )) | ||
Theorem | xnegeqd 44878 | Equality of two extended numbers with -π in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ = π΅) β β’ (π β -ππ΄ = -ππ΅) | ||
Theorem | xnegrecl 44879 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β β -ππ΄ β β) | ||
Theorem | xnegnegi 44880 | Extended real version of negneg 11535. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ β β* β β’ -π-ππ΄ = π΄ | ||
Theorem | xnegeqi 44881 | Equality of two extended numbers with -π in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ = π΅ β β’ -ππ΄ = -ππ΅ | ||
Theorem | nfxnegd 44882 | Deduction version of nfxneg 44902. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯-ππ΄) | ||
Theorem | xnegnegd 44883 | Extended real version of negnegd 11587. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) β β’ (π β -π-ππ΄ = π΄) | ||
Theorem | uzred 44884 | An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π΄ β π) β β’ (π β π΄ β β) | ||
Theorem | xnegcli 44885 | Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ β β* β β’ -ππ΄ β β* | ||
Theorem | supminfrnmpt 44886* | The indexed supremum of a bounded-above set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ (π β π΄ β β ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β βπ¦ β β βπ₯ β π΄ π΅ β€ π¦) β β’ (π β sup(ran (π₯ β π΄ β¦ π΅), β, < ) = -inf(ran (π₯ β π΄ β¦ -π΅), β, < )) | ||
Theorem | infxrpnf 44887 | Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β* β inf((π΄ βͺ {+β}), β*, < ) = inf(π΄, β*, < )) | ||
Theorem | infxrrnmptcl 44888* | The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β inf(ran (π₯ β π΄ β¦ π΅), β*, < ) β β*) | ||
Theorem | leneg2d 44889 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ β€ -π΅ β π΅ β€ -π΄)) | ||
Theorem | supxrltinfxr 44890 | The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ sup(β , β*, < ) < inf(β , β*, < ) | ||
Theorem | max1d 44891 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β π΄ β€ if(π΄ β€ π΅, π΅, π΄)) | ||
Theorem | supxrleubrnmptf 44892 | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯πΆ & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β*) β β’ (π β (sup(ran (π₯ β π΄ β¦ π΅), β*, < ) β€ πΆ β βπ₯ β π΄ π΅ β€ πΆ)) | ||
Theorem | nleltd 44893 | 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β Β¬ π΅ β€ π΄) β β’ (π β π΄ < π΅) | ||
Theorem | zxrd 44894 | An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β€) β β’ (π β π΄ β β*) | ||
Theorem | infxrgelbrnmpt 44895* | The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β*) β β’ (π β (πΆ β€ inf(ran (π₯ β π΄ β¦ π΅), β*, < ) β βπ₯ β π΄ πΆ β€ π΅)) | ||
Theorem | rphalfltd 44896 | Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β+) β β’ (π β (π΄ / 2) < π΄) | ||
Theorem | uzssz2 44897 | An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) β β’ π β β€ | ||
Theorem | leneg3d 44898 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (-π΄ β€ π΅ β -π΅ β€ π΄)) | ||
Theorem | max2d 44899 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β π΅ β€ if(π΄ β€ π΅, π΅, π΄)) | ||
Theorem | uzn0bi 44900 | The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((β€β₯βπ) β β β π β β€) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |