Home | Metamath
Proof Explorer Theorem List (p. 439 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 | xlimpnfv 43801* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) | ||
Theorem | xlimclim2lem 43802* | Lemma for xlimclim2 43803. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) & β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimclim2 43803 | Given a sequence of extended reals, it converges to a real number π΄ w.r.t. the standard topology on the reals (see climreeq 43576), if and only if it converges to π΄ w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimmnf 43804* | A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) | ||
Theorem | xlimpnf 43805* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) | ||
Theorem | xlimmnfmpt 43806* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β*) & β’ πΉ = (π β π β¦ π΅) β β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π΅ β€ π₯)) | ||
Theorem | xlimpnfmpt 43807* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β*) & β’ πΉ = (π β π β¦ π΅) β β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) | ||
Theorem | climxlim2lem 43808 | In this lemma for climxlim2 43809 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | climxlim2 43809 | A sequence of extended reals, converging w.r.t. the standard topology on the complex numbers is a converging sequence w.r.t. the standard topology on the extended reals. This is non-trivial, because +β and -β could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | dfxlim2v 43810* | An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))))) | ||
Theorem | dfxlim2 43811* | An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))))) | ||
Theorem | climresd 43812 | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β ((πΉ βΎ (β€β₯βπ)) β π΄ β πΉ β π΄)) | ||
Theorem | climresdm 43813 | A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β (πΉ β dom β β (πΉ βΎ (β€β₯βπ)) β dom β )) | ||
Theorem | dmclimxlim 43814 | A real valued sequence that converges w.r.t. the topology on the complex numbers, converges w.r.t. the topology on the extended reals (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β dom β ) β β’ (π β πΉ β dom ~~>*) | ||
Theorem | xlimmnflimsup2 43815 | A sequence of extended reals converges to -β if and only if its superior limit is also -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*-β β (lim supβπΉ) = -β)) | ||
Theorem | xlimuni 43816 | An infinite sequence converges to at most one limit (w.r.t. to the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β πΉ~~>*π΄) & β’ (π β πΉ~~>*π΅) β β’ (π β π΄ = π΅) | ||
Theorem | xlimclimdm 43817 | A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*π΄) & β’ (π β π΄ β β) β β’ (π β πΉ β dom β ) | ||
Theorem | xlimfun 43818 | The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ Fun ~~>* | ||
Theorem | xlimmnflimsup 43819 | If a sequence of extended reals converges to -β then its superior limit is also -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*-β) β β’ (π β (lim supβπΉ) = -β) | ||
Theorem | xlimdm 43820 | Two ways to express that a function has a limit. (The expression (~~>*βπΉ) is sometimes useful as a shorthand for "the unique limit of the function πΉ"). (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (πΉ β dom ~~>* β πΉ~~>*(~~>*βπΉ)) | ||
Theorem | xlimpnfxnegmnf2 43821* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β (π β π β¦ -π(πΉβπ))~~>*-β)) | ||
Theorem | xlimresdm 43822 | A function converges in the extended reals iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β πΉ β (β* βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ β dom ~~>* β (πΉ βΎ (β€β₯βπ)) β dom ~~>*)) | ||
Theorem | xlimpnfliminf 43823 | If a sequence of extended reals converges to +β then its superior limit is also +β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*+β) β β’ (π β (lim infβπΉ) = +β) | ||
Theorem | xlimpnfliminf2 43824 | A sequence of extended reals converges to +β if and only if its superior limit is also +β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β (lim infβπΉ) = +β)) | ||
Theorem | xlimliminflimsup 43825 | A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ β dom ~~>* β (lim infβπΉ) = (lim supβπΉ))) | ||
Theorem | xlimlimsupleliminf 43826 | A sequence of extended reals converges if and only if its superior limit is smaller than or equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Dec-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ β dom ~~>* β (lim supβπΉ) β€ (lim infβπΉ))) | ||
Theorem | coseq0 43827 | A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β ((cosβπ΄) = 0 β ((π΄ / Ο) + (1 / 2)) β β€)) | ||
Theorem | sinmulcos 43828 | Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (cosβπ΅)) = (((sinβ(π΄ + π΅)) + (sinβ(π΄ β π΅))) / 2)) | ||
Theorem | coskpi2 43829 | The cosine of an integer multiple of negative Ο is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β€ β (cosβ(πΎ Β· Ο)) = if(2 β₯ πΎ, 1, -1)) | ||
Theorem | cosnegpi 43830 | The cosine of negative Ο is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (cosβ-Ο) = -1 | ||
Theorem | sinaover2ne0 43831 | If π΄ in (0, 2Ο) then sin(π΄ / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (sinβ(π΄ / 2)) β 0) | ||
Theorem | cosknegpi 43832 | The cosine of an integer multiple of negative Ο is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β€ β (cosβ(πΎ Β· -Ο)) = if(2 β₯ πΎ, 1, -1)) | ||
Theorem | mulcncff 43833 | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf Β· πΊ) β (πβcnββ)) | ||
Theorem | cncfmptssg 43834* | A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 43550 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ πΈ) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΆ β π΄) & β’ (π β π· β π΅) & β’ ((π β§ π₯ β πΆ) β πΈ β π·) β β’ (π β (π₯ β πΆ β¦ πΈ) β (πΆβcnβπ·)) | ||
Theorem | constcncfg 43835* | A constant function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β β) β β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) | ||
Theorem | idcncfg 43836* | The identity function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (π΄βcnβπ΅)) | ||
Theorem | cncfshift 43837* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β πΉ β (π΄βcnββ)) & β’ πΊ = (π₯ β π΅ β¦ (πΉβ(π₯ β π))) β β’ (π β πΊ β (π΅βcnββ)) | ||
Theorem | resincncf 43838 | sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (sin βΎ β) β (ββcnββ) | ||
Theorem | addccncf2 43839* | Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ (π΅ + π₯)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnββ)) | ||
Theorem | 0cnf 43840 | The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β ({β } Cn {β }) | ||
Theorem | fsumcncf 43841* | The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (πβcnββ)) | ||
Theorem | cncfperiod 43842* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β π΅ β dom πΉ) & β’ ((π β§ π₯ β π΄) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (πΉ βΎ π΄) β (π΄βcnββ)) β β’ (π β (πΉ βΎ π΅) β (π΅βcnββ)) | ||
Theorem | subcncff 43843 | The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf β πΊ) β (πβcnββ)) | ||
Theorem | negcncfg 43844* | The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (π΄βcnββ)) | ||
Theorem | cnfdmsn 43845* | A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β π β§ π΅ β π) β (π₯ β {π΄} β¦ π΅) β (π« {π΄} Cn π« {π΅})) | ||
Theorem | cncfcompt 43846* | Composition of continuous functions. A generalization of cncfmpt1f 24199 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) & β’ (π β πΉ β (πΆβcnβπ·)) β β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β (π΄βcnβπ·)) | ||
Theorem | addcncff 43847 | The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf + πΊ) β (πβcnββ)) | ||
Theorem | ioccncflimc 43848 | Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,]π΅)βcnββ)) β β’ (π β (πΉβπ΅) β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) | ||
Theorem | cncfuni 43849* | A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β βͺ π΅) & β’ ((π β§ π β π΅) β (π΄ β© π) β ((TopOpenββfld) βΎt π΄)) & β’ ((π β§ π β π΅) β (πΉ βΎ π) β ((π΄ β© π)βcnββ)) β β’ (π β πΉ β (π΄βcnββ)) | ||
Theorem | icccncfext 43850* | A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯πΉ & β’ π½ = (topGenβran (,)) & β’ π = βͺ πΎ & β’ πΊ = (π₯ β β β¦ if(π₯ β (π΄[,]π΅), (πΉβπ₯), if(π₯ < π΄, (πΉβπ΄), (πΉβπ΅)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΎ β Top) & β’ (π β πΉ β ((π½ βΎt (π΄[,]π΅)) Cn πΎ)) β β’ (π β (πΊ β (π½ Cn (πΎ βΎt ran πΉ)) β§ (πΊ βΎ (π΄[,]π΅)) = πΉ)) | ||
Theorem | cncficcgt0 43851* | A the absolute value of a continuous function on a closed interval, that is never 0, has a strictly positive lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β (π΄[,]π΅) β¦ πΆ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnβ(β β {0}))) β β’ (π β βπ¦ β β+ βπ₯ β (π΄[,]π΅)π¦ β€ (absβπΆ)) | ||
Theorem | icocncflimc 43852 | Limit at the lower bound, of a continuous function defined on a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,)π΅)βcnββ)) β β’ (π β (πΉβπ΄) β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) | ||
Theorem | cncfdmsn 43853* | A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β {π΄} β¦ π΅) β ({π΄}βcnβ{π΅})) | ||
Theorem | divcncff 43854 | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnβ(β β {0}))) β β’ (π β (πΉ βf / πΊ) β (πβcnββ)) | ||
Theorem | cncfshiftioo 43855* | A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ πΆ = (π΄(,)π΅) & β’ (π β π β β) & β’ π· = ((π΄ + π)(,)(π΅ + π)) & β’ (π β πΉ β (πΆβcnββ)) & β’ πΊ = (π₯ β π· β¦ (πΉβ(π₯ β π))) β β’ (π β πΊ β (π·βcnββ)) | ||
Theorem | cncfiooicclem1 43856* | A continuous function πΉ on an open interval (π΄(,)π΅) can be extended to a continuous function πΊ on the corresponding closed interval, if it has a finite right limit π in π΄ and a finite left limit πΏ in π΅. πΉ can be complex-valued. This lemma assumes π΄ < π΅, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | cncfiooicc 43857* | A continuous function πΉ on an open interval (π΄(,)π΅) can be extended to a continuous function πΊ on the corresponding closed interval, if it has a finite right limit π in π΄ and a finite left limit πΏ in π΅. πΉ can be complex-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | cncfiooiccre 43858* | A continuous function πΉ on an open interval (π΄(,)π΅) can be extended to a continuous function πΊ on the corresponding closed interval, if it has a finite right limit π in π΄ and a finite left limit πΏ in π΅. πΉ is assumed to be real-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | cncfioobdlem 43859* | πΊ actually extends πΉ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆπ) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β (πΊβπΆ) = (πΉβπΆ)) | ||
Theorem | cncfioobd 43860* | A continuous function πΉ on an open interval (π΄(,)π΅) with a finite right limit π in π΄ and a finite left limit πΏ in π΅ is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β βπ₯ β β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π₯) | ||
Theorem | jumpncnp 43861 | Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π΄ β β) & β’ π½ = (topGenβran (,)) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β) & β’ (π β π΅ β ((limPtβπ½)β(π΄ β© (-β(,)π΅)))) & β’ (π β π΅ β ((limPtβπ½)β(π΄ β© (π΅(,)+β)))) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π΅)) limβ π΅)) & β’ (π β π β ((πΉ βΎ (π΅(,)+β)) limβ π΅)) & β’ (π β πΏ β π ) β β’ (π β Β¬ πΉ β ((π½ CnP (TopOpenββfld))βπ΅)) | ||
Theorem | cxpcncf2 43862* | The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π΄ β (β β (-β(,]0)) β (π₯ β β β¦ (π΄βππ₯)) β (ββcnββ)) | ||
Theorem | fprodcncf 43863* | The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ βπ β π΅ πΆ) β (π΄βcnββ)) | ||
Theorem | add1cncf 43864* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | add2cncf 43865* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub1cncfd 43866* | Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ β π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub2cncfd 43867* | Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsub2cncf 43868* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodadd2cncf 43869* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsubrecnncnvlem 43870* | The sequence π of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ π = (π β β β¦ βπ β π΄ (π΅ β (1 / π))) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) & β’ πΊ = (π β β β¦ (1 / π)) β β’ (π β π β βπ β π΄ π΅) | ||
Theorem | fprodsubrecnncnv 43871* | The sequence π of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ π = (π β β β¦ βπ β π (π΄ β (1 / π))) β β’ (π β π β βπ β π π΄) | ||
Theorem | fprodaddrecnncnvlem 43872* | The sequence π of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ π = (π β β β¦ βπ β π΄ (π΅ + (1 / π))) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) & β’ πΊ = (π β β β¦ (1 / π)) β β’ (π β π β βπ β π΄ π΅) | ||
Theorem | fprodaddrecnncnv 43873* | The sequence π of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β β) & β’ π = (π β β β¦ βπ β π (π΄ + (1 / π))) β β’ (π β π β βπ β π π΄) | ||
Theorem | dvsinexp 43874* | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (π β π β β) β β’ (π β (β D (π₯ β β β¦ ((sinβπ₯)βπ))) = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)))) | ||
Theorem | dvcosre 43875 | The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (β D (π₯ β β β¦ (cosβπ₯))) = (π₯ β β β¦ -(sinβπ₯)) | ||
Theorem | dvsinax 43876* | Derivative exercise: the derivative with respect to y of sin(Ay), given a constant π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (β D (π¦ β β β¦ (sinβ(π΄ Β· π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) | ||
Theorem | dvsubf 43877 | The subtraction rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β dom (π D πΉ) = π) & β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ βf β πΊ)) = ((π D πΉ) βf β (π D πΊ))) | ||
Theorem | dvmptconst 43878* | Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) & β’ (π β π΅ β β) β β’ (π β (π D (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ 0)) | ||
Theorem | dvcnre 43879 | From complex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((πΉ:ββΆβ β§ β β dom (β D πΉ)) β (β D (πΉ βΎ β)) = ((β D πΉ) βΎ β)) | ||
Theorem | dvmptidg 43880* | Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) β β’ (π β (π D (π₯ β π΄ β¦ π₯)) = (π₯ β π΄ β¦ 1)) | ||
Theorem | dvresntr 43881 | Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β π) & β’ (π β πΉ:πβΆβ) & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β ((intβπ½)βπ) = π) β β’ (π β (π D πΉ) = (π D (πΉ βΎ π))) | ||
Theorem | fperdvper 43882* | The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = (β D πΉ) β β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯))) | ||
Theorem | dvasinbx 43883* | Derivative exercise: the derivative with respect to y of A x sin(By), given two constants π΄ and π΅. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (β D (π¦ β β β¦ (π΄ Β· (sinβ(π΅ Β· π¦))))) = (π¦ β β β¦ ((π΄ Β· π΅) Β· (cosβ(π΅ Β· π¦))))) | ||
Theorem | dvresioo 43884 | Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΉ:π΄βΆβ) β (β D (πΉ βΎ (π΅(,)πΆ))) = ((β D πΉ) βΎ (π΅(,)πΆ))) | ||
Theorem | dvdivf 43885 | The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆ(β β {0})) & β’ (π β dom (π D πΉ) = π) & β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ βf / πΊ)) = ((((π D πΉ) βf Β· πΊ) βf β ((π D πΊ) βf Β· πΉ)) βf / (πΊ βf Β· πΊ))) | ||
Theorem | dvdivbd 43886* | A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ πΆ)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ ((π β§ π₯ β π) β (absβπΆ) β€ π) & β’ ((π β§ π₯ β π) β (absβπ΅) β€ π ) & β’ ((π β§ π₯ β π) β (absβπ·) β€ π) & β’ ((π β§ π₯ β π) β (absβπ΄) β€ π) & β’ (π β (π D (π₯ β π β¦ π΅)) = (π₯ β π β¦ π·)) & β’ ((π β§ π₯ β π) β π· β β) & β’ (π β πΈ β β+) & β’ (π β βπ₯ β π πΈ β€ (absβπ΅)) & β’ πΉ = (π D (π₯ β π β¦ (π΄ / π΅))) β β’ (π β βπ β β βπ₯ β π (absβ(πΉβπ₯)) β€ π) | ||
Theorem | dvsubcncf 43887 | A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β (π D πΉ) β (πβcnββ)) & β’ (π β (π D πΊ) β (πβcnββ)) β β’ (π β (π D (πΉ βf β πΊ)) β (πβcnββ)) | ||
Theorem | dvmulcncf 43888 | A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β (π D πΉ) β (πβcnββ)) & β’ (π β (π D πΊ) β (πβcnββ)) β β’ (π β (π D (πΉ βf Β· πΊ)) β (πβcnββ)) | ||
Theorem | dvcosax 43889* | Derivative exercise: the derivative with respect to x of cos(Ax), given a constant π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (β D (π₯ β β β¦ (cosβ(π΄ Β· π₯)))) = (π₯ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π₯))))) | ||
Theorem | dvdivcncf 43890 | A sufficient condition for the derivative of a quotient to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆ(β β {0})) & β’ (π β (π D πΉ) β (πβcnββ)) & β’ (π β (π D πΊ) β (πβcnββ)) β β’ (π β (π D (πΉ βf / πΊ)) β (πβcnββ)) | ||
Theorem | dvbdfbdioolem1 43891* | Given a function with bounded derivative, on an open interval, here is an absolute bound to the difference of the image of two points in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β πΎ β β) & β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ πΎ) & β’ (π β πΆ β (π΄(,)π΅)) & β’ (π β π· β (πΆ(,)π΅)) β β’ (π β ((absβ((πΉβπ·) β (πΉβπΆ))) β€ (πΎ Β· (π· β πΆ)) β§ (absβ((πΉβπ·) β (πΉβπΆ))) β€ (πΎ Β· (π΅ β π΄)))) | ||
Theorem | dvbdfbdioolem2 43892* | A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β πΎ β β) & β’ (π β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ πΎ) & β’ π = ((absβ(πΉβ((π΄ + π΅) / 2))) + (πΎ Β· (π΅ β π΄))) β β’ (π β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) | ||
Theorem | dvbdfbdioo 43893* | A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) | ||
Theorem | ioodvbdlimc1lem1 43894* | If πΉ has bounded derivative on (π΄(,)π΅) then a sequence of points in its image converges to its lim sup. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) & β’ (π β π β β€) & β’ (π β π :(β€β₯βπ)βΆ(π΄(,)π΅)) & β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π βπ))) & β’ (π β π β dom β ) & β’ πΎ = inf({π β (β€β₯βπ) β£ βπ β (β€β₯βπ)(absβ((π βπ) β (π βπ))) < (π₯ / (sup(ran (π§ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ§))), β, < ) + 1))}, β, < ) β β’ (π β π β (lim supβπ)) | ||
Theorem | ioodvbdlimc1lem2 43895* | Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) & β’ π = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) & β’ π = ((ββ(1 / (π΅ β π΄))) + 1) & β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π΄ + (1 / π)))) & β’ π = (π β (β€β₯βπ) β¦ (π΄ + (1 / π))) & β’ π = if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) & β’ (π β (((((π β§ π₯ β β+) β§ π β (β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΄)) < (1 / π))) β β’ (π β (lim supβπ) β (πΉ limβ π΄)) | ||
Theorem | ioodvbdlimc1 43896* | A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) β β’ (π β (πΉ limβ π΄) β β ) | ||
Theorem | ioodvbdlimc2lem 43897* | Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) & β’ π = sup(ran (π₯ β (π΄(,)π΅) β¦ (absβ((β D πΉ)βπ₯))), β, < ) & β’ π = ((ββ(1 / (π΅ β π΄))) + 1) & β’ π = (π β (β€β₯βπ) β¦ (πΉβ(π΅ β (1 / π)))) & β’ π = (π β (β€β₯βπ) β¦ (π΅ β (1 / π))) & β’ π = if(π β€ ((ββ(π / (π₯ / 2))) + 1), ((ββ(π / (π₯ / 2))) + 1), π) & β’ (π β (((((π β§ π₯ β β+) β§ π β (β€β₯βπ)) β§ (absβ((πβπ) β (lim supβπ))) < (π₯ / 2)) β§ π§ β (π΄(,)π΅)) β§ (absβ(π§ β π΅)) < (1 / π))) β β’ (π β (lim supβπ) β (πΉ limβ π΅)) | ||
Theorem | ioodvbdlimc2 43898* | A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β dom (β D πΉ) = (π΄(,)π΅)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π¦) β β’ (π β (πΉ limβ π΅) β β ) | ||
Theorem | dvdmsscn 43899 | π is a subset of β. This statement is very often used when computing derivatives. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) β β’ (π β π β β) | ||
Theorem | dvmptmulf 43900* | Function-builder for derivative, product rule. A version of dvmptmul 25247 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |