Home | Metamath
Proof Explorer Theorem List (p. 436 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iooltub 43501 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,)π΅)) β πΆ < π΅) | ||
Theorem | ioontr 43502 | The interior of an interval in the standard topology on β is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅) | ||
Theorem | snunioo1 43503 | The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β ((π΄(,)π΅) βͺ {π΄}) = (π΄[,)π΅)) | ||
Theorem | lbioc 43504 | A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ Β¬ π΄ β (π΄(,]π΅) | ||
Theorem | ioomidp 43505 | The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β ((π΄ + π΅) / 2) β (π΄(,)π΅)) | ||
Theorem | iccdifioo 43506 | If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β ((π΄[,]π΅) β (π΄(,)π΅)) = {π΄, π΅}) | ||
Theorem | iccdifprioo 43507 | An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,]π΅) β {π΄, π΅}) = (π΄(,)π΅)) | ||
Theorem | ioossioobi 43508 | Biconditional form of ioossioo 13286. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π· β β*) & β’ (π β πΆ < π·) β β’ (π β ((πΆ(,)π·) β (π΄(,)π΅) β (π΄ β€ πΆ β§ π· β€ π΅))) | ||
Theorem | iccshift 43509* | A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β ((π΄ + π)[,](π΅ + π)) = {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) | ||
Theorem | iccsuble 43510 | An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β π· β (π΄[,]π΅)) β β’ (π β (πΆ β π·) β€ (π΅ β π΄)) | ||
Theorem | iocopn 43511 | A left-open right-closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ β β) & β’ πΎ = (topGenβran (,)) & β’ π½ = (πΎ βΎt (π΄(,]π΅)) & β’ (π β π΄ β€ πΆ) & β’ (π β π΅ β β) β β’ (π β (πΆ(,]π΅) β π½) | ||
Theorem | eliccelioc 43512 | Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β*) β β’ (π β (πΆ β (π΄(,]π΅) β (πΆ β (π΄[,]π΅) β§ πΆ β π΄))) | ||
Theorem | iooshift 43513* | An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β ((π΄ + π)(,)(π΅ + π)) = {π€ β β β£ βπ§ β (π΄(,)π΅)π€ = (π§ + π)}) | ||
Theorem | iccintsng 43514 | Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ β€ π΅ β§ π΅ β€ πΆ)) β ((π΄[,]π΅) β© (π΅[,]πΆ)) = {π΅}) | ||
Theorem | icoiccdif 43515 | Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = ((π΄[,]π΅) β {π΅})) | ||
Theorem | icoopn 43516 | A left-closed right-open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β*) & β’ (π β π΅ β β*) & β’ πΎ = (topGenβran (,)) & β’ π½ = (πΎ βΎt (π΄[,)π΅)) & β’ (π β πΆ β€ π΅) β β’ (π β (π΄[,)πΆ) β π½) | ||
Theorem | icoub 43517 | A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π΄ β β* β Β¬ π΅ β (π΄[,)π΅)) | ||
Theorem | eliccxrd 43518 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄[,]π΅)) | ||
Theorem | pnfel0pnf 43519 | +β is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ +β β (0[,]+β) | ||
Theorem | eliccnelico 43520 | An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β Β¬ πΆ β (π΄[,)π΅)) β β’ (π β πΆ = π΅) | ||
Theorem | eliccelicod 43521 | A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β πΆ β π΅) β β’ (π β πΆ β (π΄[,)π΅)) | ||
Theorem | ge0xrre 43522 | A nonnegative extended real that is not +β is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π΄ β (0[,]+β) β§ π΄ β +β) β π΄ β β) | ||
Theorem | ge0lere 43523 | A nonnegative extended Real number smaller than or equal to a Real number, is a Real number. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β (0[,]+β)) & β’ (π β π΅ β€ π΄) β β’ (π β π΅ β β) | ||
Theorem | elicores 43524* | Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π΄ β ran ([,) βΎ (β Γ β)) β βπ₯ β β βπ¦ β β π΄ = (π₯[,)π¦)) | ||
Theorem | inficc 43525 | The infimum of a nonempty set, included in a closed interval, is a member of the interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π β β ) β β’ (π β inf(π, β*, < ) β (π΄[,]π΅)) | ||
Theorem | qinioo 43526 | The rational numbers are dense in β. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β ((β β© (π΄(,)π΅)) = β β π΅ β€ π΄)) | ||
Theorem | lenelioc 43527 | A real number smaller than or equal to the lower bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β πΆ β€ π΄) β β’ (π β Β¬ πΆ β (π΄(,]π΅)) | ||
Theorem | ioonct 43528 | A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄(,)π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | xrgtnelicc 43529 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ < πΆ) β β’ (π β Β¬ πΆ β (π΄[,]π΅)) | ||
Theorem | iccdificc 43530 | The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ π΅) β β’ (π β ((π΄[,]πΆ) β (π΄[,]π΅)) = (π΅(,]πΆ)) | ||
Theorem | iocnct 43531 | A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄(,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iccnct 43532 | A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄[,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iooiinicc 43533* | A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β β© π β β ((π΄ β (1 / π))(,)(π΅ + (1 / π))) = (π΄[,]π΅)) | ||
Theorem | iccgelbd 43534 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iooltubd 43535 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | icoltubd 43536 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | qelioo 43537* | The rational numbers are dense in β*: any two extended real numbers have a rational between them. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β βπ₯ β β π₯ β (π΄(,)π΅)) | ||
Theorem | tgqioo2 43538* | Every open set of reals is the (countable) union of open interval with rational bounds. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β π½) β β’ (π β βπ(π β ((,) β (β Γ β)) β§ π΄ = βͺ π)) | ||
Theorem | iccleubd 43539 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | elioored 43540 | A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β (π΅(,)πΆ)) β β’ (π β π΄ β β) | ||
Theorem | ioogtlbd 43541 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | ioofun 43542 | (,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ Fun (,) | ||
Theorem | icomnfinre 43543 | A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β ((-β[,)π΄) β© β) = (-β(,)π΄)) | ||
Theorem | sqrlearg 43544 | The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) β β’ (π β ((π΄β2) β€ π΄ β π΄ β (0[,]1))) | ||
Theorem | ressiocsup 43545 | If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = sup(π΄, β*, < ) & β’ (π β π β π΄) & β’ πΌ = (-β(,]π) β β’ (π β π΄ β πΌ) | ||
Theorem | ressioosup 43546 | If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = sup(π΄, β*, < ) & β’ (π β Β¬ π β π΄) & β’ πΌ = (-β(,)π) β β’ (π β π΄ β πΌ) | ||
Theorem | iooiinioc 43547* | A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) β β’ (π β β© π β β (π΄(,)(π΅ + (1 / π))) = (π΄(,]π΅)) | ||
Theorem | ressiooinf 43548 | If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = inf(π΄, β*, < ) & β’ (π β Β¬ π β π΄) & β’ πΌ = (π(,)+β) β β’ (π β π΄ β πΌ) | ||
Theorem | icogelbd 43549 | An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iocleubd 43550 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | uzinico 43551 | An upper interval of integers is the intersection of the integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π = (β€ β© (π[,)+β))) | ||
Theorem | preimaiocmnf 43552* | Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β€ π΅}) | ||
Theorem | uzinico2 43553 | An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β (β€β₯βπ) = ((β€β₯βπ) β© (π[,)+β))) | ||
Theorem | uzinico3 43554 | An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π = (π β© (π[,)+β))) | ||
Theorem | icossico2 43555 | Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ β€ π΄) β β’ (π β (π΄[,)πΆ) β (π΅[,)πΆ)) | ||
Theorem | dmico 43556 | The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ dom [,) = (β* Γ β*) | ||
Theorem | ndmico 43557 | The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (Β¬ (π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = β ) | ||
Theorem | uzubioo 43558* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π(,)+β)π β π) | ||
Theorem | uzubico 43559* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π[,)+β)π β π) | ||
Theorem | uzubioo2 43560* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯(,)+β)π β π) | ||
Theorem | uzubico2 43561* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯[,)+β)π β π) | ||
Theorem | iocgtlbd 43562 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | xrtgioo2 43563 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to β. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (topGenβran (,)) = ((ordTopβ β€ ) βΎt β) | ||
Theorem | tgioo4 43564 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (topGenβran (,)) = ((TopOpenββfld) βΎt β) | ||
Theorem | fsummulc1f 43565* | Closure of a finite sum of complex numbers π΄(π). A version of fsummulc1 15604 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ (π β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (Ξ£π β π΄ π΅ Β· πΆ) = Ξ£π β π΄ (π΅ Β· πΆ)) | ||
Theorem | fsumnncl 43566* | Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumge0cl 43567* | The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | fsumf1of 43568* | Re-index a finite sum using a bijection. Same as fsumf1o 15542, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | fsumiunss 43569* | Sum over a disjoint indexed union, intersected with a finite set π·. Similar to fsumiun 15640, but here π΄ and π΅ need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ (π β π· β Fin) β β’ (π β Ξ£π β βͺ π₯ β π΄ (π΅ β© π·)πΆ = Ξ£π₯ β {π₯ β π΄ β£ (π΅ β© π·) β β }Ξ£π β (π΅ β© π·)πΆ) | ||
Theorem | fsumreclf 43570* | Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumlessf 43571* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) & β’ (π β πΆ β π΄) β β’ (π β Ξ£π β πΆ π΅ β€ Ξ£π β π΄ π΅) | ||
Theorem | fsumsupp0 43572* | Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆβ) β β’ (π β Ξ£π β (πΉ supp 0)(πΉβπ) = Ξ£π β π΄ (πΉβπ)) | ||
Theorem | fsumsermpt 43573* | A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΄ β β) & β’ πΉ = (π β π β¦ Ξ£π β (π...π)π΄) & β’ πΊ = seqπ( + , (π β π β¦ π΄)) β β’ (π β πΉ = πΊ) | ||
Theorem | fmul01 43574* | Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ (π β πΎ β (πΏ...π)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) β β’ (π β (0 β€ (π΄βπΎ) β§ (π΄βπΎ) β€ 1)) | ||
Theorem | fmulcl 43575* | If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ (π β π β (1...π)) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β V) β β’ (π β π β π) | ||
Theorem | fmuldfeqlem1 43576* | induction step for the proof of fmuldfeq 43577. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ (π β π β V) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β (1...π)) & β’ (π β (π + 1) β (1...π)) & β’ (π β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) & β’ ((π β§ π β π) β π:πβΆβ) β β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) | ||
Theorem | fmuldfeq 43577* | X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β V) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π) β π:πβΆβ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) β β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) | ||
Theorem | fmul01lt1lem1 43578* | Given a finite multiplication of values betweeen 0 and 1, a value larger than its first element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β (π΅βπΏ) < πΈ) β β’ (π β (π΄βπ) < πΈ) | ||
Theorem | fmul01lt1lem2 43579* | Given a finite multiplication of values betweeen 0 and 1, a value πΈ larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β π½ β (πΏ...π)) & β’ (π β (π΅βπ½) < πΈ) β β’ (π β (π΄βπ) < πΈ) | ||
Theorem | fmul01lt1 43580* | Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ β²ππ΄ & β’ π΄ = seq1( Β· , π΅) & β’ (π β π β β) & β’ (π β π΅:(1...π)βΆβ) & β’ ((π β§ π β (1...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (1...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β βπ β (1...π)(π΅βπ) < πΈ) β β’ (π β (π΄βπ) < πΈ) | ||
Theorem | cncfmptss 43581* | A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²π₯πΉ & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΆ β π΄) β β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) β (πΆβcnβπ΅)) | ||
Theorem | rrpsscn 43582 | The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β+ β β | ||
Theorem | mulc1cncfg 43583* | A version of mulc1cncf 24190 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ β²π₯πΉ & β’ β²π₯π & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π΅ β β) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯))) β (π΄βcnββ)) | ||
Theorem | infrglb 43584* | The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
β’ (((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β§ π΅ β β) β (inf(π΄, β, < ) < π΅ β βπ§ β π΄ π§ < π΅)) | ||
Theorem | expcnfg 43585* | If πΉ is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 24211. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²π₯πΉ & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π β β0) β β’ (π β (π₯ β π΄ β¦ ((πΉβπ₯)βπ)) β (π΄βcnββ)) | ||
Theorem | prodeq2ad 43586* | Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β βπ β π΄ π΅ = βπ β π΄ πΆ) | ||
Theorem | fprodsplit1 43587* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ ((π β§ π = πΆ) β π΅ = π·) β β’ (π β βπ β π΄ π΅ = (π· Β· βπ β (π΄ β {πΆ})π΅)) | ||
Theorem | fprodexp 43588* | Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π β β0) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β βπ β π΄ (π΅βπ) = (βπ β π΄ π΅βπ)) | ||
Theorem | fprodabs2 43589* | The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (absββπ β π΄ π΅) = βπ β π΄ (absβπ΅)) | ||
Theorem | fprod0 43590* | A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππΆ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π = πΎ β π΅ = πΆ) & β’ (π β πΎ β π΄) & β’ (π β πΆ = 0) β β’ (π β βπ β π΄ π΅ = 0) | ||
Theorem | mccllem 43591* | * Induction step for mccl 43592. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β π΄) & β’ (π β π· β (π΄ β πΆ)) & β’ (π β π΅ β (β0 βm (πΆ βͺ {π·}))) & β’ (π β βπ β (β0 βm πΆ)((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) β β) β β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / βπ β (πΆ βͺ {π·})(!β(π΅βπ))) β β) | ||
Theorem | mccl 43592* | A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π β π΄ β Fin) & β’ (π β π΅ β (β0 βm π΄)) β β’ (π β ((!βΞ£π β π΄ (π΅βπ)) / βπ β π΄ (!β(π΅βπ))) β β) | ||
Theorem | fprodcnlem 43593* | A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) & β’ (π β π β π΄) & β’ (π β π β (π΄ β π)) & β’ (π β (π₯ β π β¦ βπ β π π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ βπ β (π βͺ {π})π΅) β (π½ Cn πΎ)) | ||
Theorem | fprodcn 43594* | A finite product of functions to complex numbers from a common topological space is continuous. The class expression for π΅ normally contains free variables π and π₯ to index it. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ βπ β π΄ π΅) β (π½ Cn πΎ)) | ||
Theorem | clim1fr1 43595* | A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π β β β¦ (((π΄ Β· π) + π΅) / (π΄ Β· π))) & β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) β β’ (π β πΉ β 1) | ||
Theorem | isumneg 43596* | Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β Ξ£π β π π΄ β β) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π -π΄ = -Ξ£π β π π΄) | ||
Theorem | climrec 43597* | Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ β π΄) & β’ (π β π΄ β 0) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = (1 / (πΊβπ))) & β’ (π β π» β π) β β’ (π β π» β (1 / π΄)) | ||
Theorem | climmulf 43598* | A version of climmul 15449 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) Β· (πΊβπ))) β β’ (π β π» β (π΄ Β· π΅)) | ||
Theorem | climexp 43599* | The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) & β’ (π β π β β0) & β’ (π β π» β π) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) β β’ (π β π» β (π΄βπ)) | ||
Theorem | climinf 43600* | A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β, < )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |