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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | supsubc 43301* | 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 43302* | 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 43303 | 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 43304 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) β β’ (π β (1 < π΅ β (π΄ / π΅) < π΄)) | ||
Theorem | xrltned 43305 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β π΄ β π΅) | ||
Theorem | nnsplit 43306 | Express the set of positive integers as the disjoint (see nnuzdisj 43303) union of the first π values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β β β β = ((1...π) βͺ (β€β₯β(π + 1)))) | ||
Theorem | divdiv3d 43307 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β 0) & β’ (π β πΆ β 0) β β’ (π β ((π΄ / π΅) / πΆ) = (π΄ / (πΆ Β· π΅))) | ||
Theorem | abslt2sqd 43308 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (absβπ΄) < (absβπ΅)) β β’ (π β (π΄β2) < (π΅β2)) | ||
Theorem | qenom 43309 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β β Ο | ||
Theorem | qct 43310 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β βΌ Ο | ||
Theorem | xrltnled 43311 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ < π΅ β Β¬ π΅ β€ π΄)) | ||
Theorem | lenlteq 43312 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β Β¬ π΄ < π΅) β β’ (π β π΄ = π΅) | ||
Theorem | xrred 43313 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΄ β -β) & β’ (π β π΄ β +β) β β’ (π β π΄ β β) | ||
Theorem | rr2sscn2 43314 | The cartesian square of β is a subset of the cartesian square of β. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (β Γ β) β (β Γ β) | ||
Theorem | infxr 43315* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β βπ₯ β π΄ Β¬ π₯ < π΅) & β’ (π β βπ₯ β β (π΅ < π₯ β βπ¦ β π΄ π¦ < π₯)) β β’ (π β inf(π΄, β*, < ) = π΅) | ||
Theorem | infxrunb2 43316* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ < π₯ β inf(π΄, β*, < ) = -β)) | ||
Theorem | infxrbnd2 43317* | 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 43318 | Lemma for infleinf 43320, case π΅ β β β§ -β < inf(π΅, β*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β β+) & β’ (π β π β π΅) & β’ (π β π β€ (inf(π΅, β*, < ) +π (π / 2))) & β’ (π β π β π΄) & β’ (π β π β€ (π +π (π / 2))) β β’ (π β inf(π΄, β*, < ) β€ (inf(π΅, β*, < ) +π π)) | ||
Theorem | infleinflem2 43319 | Lemma for infleinf 43320, when inf(π΅, β*, < ) = -β. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β β) & β’ (π β π β π΅) & β’ (π β π < (π β 2)) & β’ (π β π β π΄) & β’ (π β π β€ (π +π 1)) β β’ (π β π < π ) | ||
Theorem | infleinf 43320* | 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 43321* | 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 43322* | 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 43323 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β π β β€) | ||
Theorem | suplesup2 43324* | 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 43325 | π 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 43326 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β β β | ||
Theorem | fzct 43327 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π...π) βΌ Ο | ||
Theorem | rpgtrecnn 43328* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π΄ β β+ β βπ β β (1 / π) < π΄) | ||
Theorem | fzossuz 43329 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) β (β€β₯βπ) | ||
Theorem | infxrrefi 43330 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΄ β Fin β§ π΄ β β ) β inf(π΄, β*, < ) = inf(π΄, β, < )) | ||
Theorem | xrralrecnnle 43331* | 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 43332 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) βΌ Ο | ||
Theorem | frexr 43333 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) β β’ (π β πΉ:π΄βΆβ*) | ||
Theorem | nnrecrp 43334 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β β β (1 / π) β β+) | ||
Theorem | reclt0d 43335 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ < 0) β β’ (π β (1 / π΄) < 0) | ||
Theorem | lt0neg1dd 43336 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ < 0) β β’ (π β 0 < -π΄) | ||
Theorem | mnfled 43337 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β -β β€ π΄) | ||
Theorem | infxrcld 43338 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β inf(π΄, β*, < ) β β*) | ||
Theorem | xrralrecnnge 43339* | 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 43340 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (π΄ < 0 β (1 / π΄) < 0)) | ||
Theorem | ltmulneg 43341 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β πΆ < 0) β β’ (π β (π΄ < π΅ β (π΅ Β· πΆ) < (π΄ Β· πΆ))) | ||
Theorem | allbutfi 43342* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 43043 and eliuniin2 43064 (here, the precondition can be dropped; see eliuniincex 43053). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π = (β€β₯βπ) & β’ π΄ = βͺ π β π β© π β (β€β₯βπ)π΅ β β’ (π β π΄ β βπ β π βπ β (β€β₯βπ)π β π΅) | ||
Theorem | ltdiv23neg 43343 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ < 0) & β’ (π β πΆ β β) & β’ (π β πΆ < 0) β β’ (π β ((π΄ / π΅) < πΆ β (π΄ / πΆ) < π΅)) | ||
Theorem | xreqnltd 43344 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΄ = π΅) β β’ (π β Β¬ π΄ < π΅) | ||
Theorem | mnfnre2 43345 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ Β¬ -β β β | ||
Theorem | zssxr 43346 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β€ β β* | ||
Theorem | fisupclrnmpt 43347* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π Or π΄) & β’ (π β π΅ β Fin) & β’ (π β π΅ β β ) & β’ ((π β§ π₯ β π΅) β πΆ β π΄) β β’ (π β sup(ran (π₯ β π΅ β¦ πΆ), π΄, π ) β π΄) | ||
Theorem | supxrunb3 43348* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ β€ π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | elfzod 43349 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β π β β€) & β’ (π β πΎ < π) β β’ (π β πΎ β (π..^π)) | ||
Theorem | fimaxre4 43350* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β βπ¦ β β βπ₯ β π΄ π΅ β€ π¦) | ||
Theorem | ren0 43351 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β β β | ||
Theorem | eluzelz2 43352 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) β β’ (π β π β π β β€) | ||
Theorem | resabs2d 43353 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΅ β πΆ) β β’ (π β ((π΄ βΎ π΅) βΎ πΆ) = (π΄ βΎ π΅)) | ||
Theorem | uzid2 43354 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β (β€β₯βπ) β π β (β€β₯βπ)) | ||
Theorem | supxrleubrnmpt 43355* | 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 43356 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) β β’ π β β | ||
Theorem | uzssd 43357 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β (β€β₯βπ) β (β€β₯βπ)) | ||
Theorem | eluzd 43358 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β€ π) β β’ (π β π β π) | ||
Theorem | infxrlbrnmpt2 43359* | 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 43360 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (π΄ β β β (π΄ β -β β§ π΄ β +β))) | ||
Theorem | uz0 43361 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (Β¬ π β β€ β (β€β₯βπ) = β ) | ||
Theorem | eluzelz2d 43362 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) β β’ (π β π β β€) | ||
Theorem | infleinf2 43363* | 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 43364* | "Unbounded below" expressed with < and with β€. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (βπ€ β β βπ¦ β π΄ π¦ < π€ β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯)) | ||
Theorem | uzidd2 43365 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π β π) | ||
Theorem | uzssd2 43366 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) β β’ (π β (β€β₯βπ) β π) | ||
Theorem | rexabslelem 43367* | 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 43368* | 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 43369* | Given a "for all but finitely many" condition, the condition holds from π on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ π΄ = βͺ π β π β© π β (β€β₯βπ)π΅ & β’ (π β π β π΄) & β’ π = inf({π β π β£ βπ β (β€β₯βπ)π β π΅}, β, < ) β β’ (π β (π β π β§ βπ β (β€β₯βπ)π β π΅)) | ||
Theorem | supxrrernmpt 43370* | 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 43371* | 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 43372* | 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 43373* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ β€ π₯ β inf(π΄, β*, < ) = -β)) | ||
Theorem | uzn0d 43374 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π β β ) | ||
Theorem | uzssd3 43375 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) β β’ (π β π β (β€β₯βπ) β π) | ||
Theorem | rexabsle2 43376* | 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 43377* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β (βπ¦ β β βπ₯ β π΄ π΅ β€ π¦ β inf(ran (π₯ β π΄ β¦ π΅), β*, < ) = -β)) | ||
Theorem | supxrre3rnmpt 43378* | 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 43379* | 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 43380* | 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 43381 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) β β’ (π β π΄ β β*) | ||
Theorem | supxrmnf2 43382 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β* β sup((π΄ β {-β}), β*, < ) = sup(π΄, β*, < )) | ||
Theorem | supxrcli 43383 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ β β* β β’ sup(π΄, β*, < ) β β* | ||
Theorem | uzid3 43384 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) β β’ (π β π β π β (β€β₯βπ)) | ||
Theorem | infxrlesupxr 43385 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 43398. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) & β’ (π β π΄ β β ) β β’ (π β inf(π΄, β*, < ) β€ sup(π΄, β*, < )) | ||
Theorem | xnegeqd 43386 | Equality of two extended numbers with -π in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ = π΅) β β’ (π β -ππ΄ = -ππ΅) | ||
Theorem | xnegrecl 43387 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β β -ππ΄ β β) | ||
Theorem | xnegnegi 43388 | Extended real version of negneg 11385. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ β β* β β’ -π-ππ΄ = π΄ | ||
Theorem | xnegeqi 43389 | Equality of two extended numbers with -π in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ = π΅ β β’ -ππ΄ = -ππ΅ | ||
Theorem | nfxnegd 43390 | Deduction version of nfxneg 43410. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯-ππ΄) | ||
Theorem | xnegnegd 43391 | Extended real version of negnegd 11437. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) β β’ (π β -π-ππ΄ = π΄) | ||
Theorem | uzred 43392 | An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π΄ β π) β β’ (π β π΄ β β) | ||
Theorem | xnegcli 43393 | Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π΄ β β* β β’ -ππ΄ β β* | ||
Theorem | supminfrnmpt 43394* | 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 43395 | Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β* β inf((π΄ βͺ {+β}), β*, < ) = inf(π΄, β*, < )) | ||
Theorem | infxrrnmptcl 43396* | 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 43397 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ β€ -π΅ β π΅ β€ -π΄)) | ||
Theorem | supxrltinfxr 43398 | 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 43399 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β π΄ β€ if(π΄ β€ π΅, π΅, π΄)) | ||
Theorem | supxrleubrnmptf 43400 | 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 (π₯ β π΄ β¦ π΅), β*, < ) β€ πΆ β βπ₯ β π΄ π΅ β€ πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |