![]() |
Metamath
Proof Explorer Theorem List (p. 454 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 | xlimclimdm 45301 | 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 45302 | The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ Fun ~~>* | ||
Theorem | xlimmnflimsup 45303 | 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 45304 | 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 45305* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β (π β π β¦ -π(πΉβπ))~~>*-β)) | ||
Theorem | xlimresdm 45306 | 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 45307 | 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 45308 | 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 45309 | 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 45310 | 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 45311 | A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β ((cosβπ΄) = 0 β ((π΄ / Ο) + (1 / 2)) β β€)) | ||
Theorem | sinmulcos 45312 | Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (cosβπ΅)) = (((sinβ(π΄ + π΅)) + (sinβ(π΄ β π΅))) / 2)) | ||
Theorem | coskpi2 45313 | 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 45314 | The cosine of negative Ο is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (cosβ-Ο) = -1 | ||
Theorem | sinaover2ne0 45315 | If π΄ in (0, 2Ο) then sin(π΄ / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (sinβ(π΄ / 2)) β 0) | ||
Theorem | cosknegpi 45316 | 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 45317 | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf Β· πΊ) β (πβcnββ)) | ||
Theorem | cncfmptssg 45318* | A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 45034 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ πΈ) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΆ β π΄) & β’ (π β π· β π΅) & β’ ((π β§ π₯ β πΆ) β πΈ β π·) β β’ (π β (π₯ β πΆ β¦ πΈ) β (πΆβcnβπ·)) | ||
Theorem | constcncfg 45319* | A constant function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β β) β β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) | ||
Theorem | idcncfg 45320* | The identity function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (π΄βcnβπ΅)) | ||
Theorem | cncfshift 45321* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β πΉ β (π΄βcnββ)) & β’ πΊ = (π₯ β π΅ β¦ (πΉβ(π₯ β π))) β β’ (π β πΊ β (π΅βcnββ)) | ||
Theorem | resincncf 45322 | sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (sin βΎ β) β (ββcnββ) | ||
Theorem | addccncf2 45323* | Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ (π΅ + π₯)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnββ)) | ||
Theorem | 0cnf 45324 | The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β ({β } Cn {β }) | ||
Theorem | fsumcncf 45325* | The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (πβcnββ)) | ||
Theorem | cncfperiod 45326* | 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 45327 | The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf β πΊ) β (πβcnββ)) | ||
Theorem | negcncfg 45328* | The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (π΄βcnββ)) | ||
Theorem | cnfdmsn 45329* | A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β π β§ π΅ β π) β (π₯ β {π΄} β¦ π΅) β (π« {π΄} Cn π« {π΅})) | ||
Theorem | cncfcompt 45330* | Composition of continuous functions. A generalization of cncfmpt1f 24847 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) & β’ (π β πΉ β (πΆβcnβπ·)) β β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β (π΄βcnβπ·)) | ||
Theorem | addcncff 45331 | The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf + πΊ) β (πβcnββ)) | ||
Theorem | ioccncflimc 45332 | 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 45333* | 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 45334* | 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 45335* | 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 45336 | 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 45337* | A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β {π΄} β¦ π΅) β ({π΄}βcnβ{π΅})) | ||
Theorem | divcncff 45338 | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnβ(β β {0}))) β β’ (π β (πΉ βf / πΊ) β (πβcnββ)) | ||
Theorem | cncfshiftioo 45339* | 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 45340* | 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 45341* | 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 45342* | 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 45343* | πΊ actually extends πΉ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆπ) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β (πΊβπΆ) = (πΉβπΆ)) | ||
Theorem | cncfioobd 45344* | 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 45345 | 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 45346* | The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π΄ β (β β (-β(,]0)) β (π₯ β β β¦ (π΄βππ₯)) β (ββcnββ)) | ||
Theorem | fprodcncf 45347* | The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ βπ β π΅ πΆ) β (π΄βcnββ)) | ||
Theorem | add1cncf 45348* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | add2cncf 45349* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub1cncfd 45350* | Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ β π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub2cncfd 45351* | Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsub2cncf 45352* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodadd2cncf 45353* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsubrecnncnvlem 45354* | 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 45355* | 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 45356* | 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 45357* | 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 45358* | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (π β π β β) β β’ (π β (β D (π₯ β β β¦ ((sinβπ₯)βπ))) = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)))) | ||
Theorem | dvcosre 45359 | The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (β D (π₯ β β β¦ (cosβπ₯))) = (π₯ β β β¦ -(sinβπ₯)) | ||
Theorem | dvsinax 45360* | 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 45361 | 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 45362* | Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) & β’ (π β π΅ β β) β β’ (π β (π D (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ 0)) | ||
Theorem | dvcnre 45363 | From complex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((πΉ:ββΆβ β§ β β dom (β D πΉ)) β (β D (πΉ βΎ β)) = ((β D πΉ) βΎ β)) | ||
Theorem | dvmptidg 45364* | Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) β β’ (π β (π D (π₯ β π΄ β¦ π₯)) = (π₯ β π΄ β¦ 1)) | ||
Theorem | dvresntr 45365 | 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 45366* | The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = (β D πΉ) β β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯))) | ||
Theorem | dvasinbx 45367* | 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 45368 | Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΉ:π΄βΆβ) β (β D (πΉ βΎ (π΅(,)πΆ))) = ((β D πΉ) βΎ (π΅(,)πΆ))) | ||
Theorem | dvdivf 45369 | 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 45370* | 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 45371 | 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 45372 | 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 45373* | 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 45374 | 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 45375* | 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 45376* | 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 45377* | 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 45378* | 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 45379* | 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 45380* | 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 45381* | 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 45382* | 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 45383 | π 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 45384* | Function-builder for derivative, product rule. A version of dvmptmul 25906 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) | ||
Theorem | dvnmptdivc 45385* | Function-builder for iterated derivative, division rule for constant divisor. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π β§ π β (0...π)) β π΅ β β) & β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ π΅)) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π β β0) β β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ (π΄ / πΆ)))βπ) = (π₯ β π β¦ (π΅ / πΆ))) | ||
Theorem | dvdsn1add 45386 | If πΎ divides π but πΎ does not divide π, then πΎ does not divide (π + π). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((Β¬ πΎ β₯ π β§ πΎ β₯ π) β Β¬ πΎ β₯ (π + π))) | ||
Theorem | dvxpaek 45387* | Derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β) β β’ (π β (π D (π₯ β π β¦ ((π₯ + π΄)βπΎ))) = (π₯ β π β¦ (πΎ Β· ((π₯ + π΄)β(πΎ β 1))))) | ||
Theorem | dvnmptconst 45388* | The π-th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ 0)) | ||
Theorem | dvnxpaek 45389* | The π-th derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β0) & β’ πΉ = (π₯ β π β¦ ((π₯ + π΄)βπΎ)) β β’ ((π β§ π β β0) β ((π Dπ πΉ)βπ) = (π₯ β π β¦ if(πΎ < π, 0, (((!βπΎ) / (!β(πΎ β π))) Β· ((π₯ + π΄)β(πΎ β π)))))) | ||
Theorem | dvnmul 45390* | Function-builder for the π-th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ π΄) & β’ πΊ = (π₯ β π β¦ π΅) & β’ ((π β§ π β (0...π)) β ((π Dπ πΉ)βπ):πβΆβ) & β’ ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) & β’ πΆ = (π β (0...π) β¦ ((π Dπ πΉ)βπ)) & β’ π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ)) β β’ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) | ||
Theorem | dvmptfprodlem 45391* | Induction step for dvmptfprod 45392. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ β²ππ & β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ (π β π· β Fin) & β’ (π β πΈ β V) & β’ (π β Β¬ πΈ β π·) & β’ (π β (π· βͺ {πΈ}) β πΌ) & β’ (π β π β {β, β}) & β’ (((π β§ π₯ β π) β§ π β π·) β πΆ β β) & β’ (π β (π D (π₯ β π β¦ βπ β π· π΄)) = (π₯ β π β¦ Ξ£π β π· (πΆ Β· βπ β (π· β {π})π΄))) & β’ ((π β§ π₯ β π) β πΊ β β) & β’ (π β (π D (π₯ β π β¦ πΉ)) = (π₯ β π β¦ πΊ)) & β’ (π = πΈ β π΄ = πΉ) & β’ (π = πΈ β πΆ = πΊ) β β’ (π β (π D (π₯ β π β¦ βπ β (π· βͺ {πΈ})π΄)) = (π₯ β π β¦ Ξ£π β (π· βͺ {πΈ})(πΆ Β· βπ β ((π· βͺ {πΈ}) β {π})π΄))) | ||
Theorem | dvmptfprod 45392* | Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β πΌ β Fin) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΅ β β) & β’ ((π β§ π β πΌ) β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π = π β π΅ = πΆ) β β’ (π β (π D (π₯ β π β¦ βπ β πΌ π΄)) = (π₯ β π β¦ Ξ£π β πΌ (πΆ Β· βπ β (πΌ β {π})π΄))) | ||
Theorem | dvnprodlem1 45393* | π· is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π½ β β0) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β Β¬ π β π ) & β’ (π β (π βͺ {π}) β π) β β’ (π β π·:((πΆβ(π βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ )βπ))) | ||
Theorem | dvnprodlem2 45394* | Induction step for dvnprodlem2 45394. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π β π) & β’ (π β π β (π β π )) & β’ (π β βπ β (0...π)((π Dπ (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ )βπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) & β’ (π β π½ β (0...π)) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) β β’ (π β ((π Dπ (π₯ β π β¦ βπ‘ β (π βͺ {π})((π»βπ‘)βπ₯)))βπ½) = (π₯ β π β¦ Ξ£π β ((πΆβ(π βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | dvnprodlem3 45395* | The multinomial formula for the π-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) & β’ π· = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | dvnprod 45396* | The multinomial formula for the π-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | itgsin0pilem1 45397* | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΆ = (π‘ β (0[,]Ο) β¦ -(cosβπ‘)) β β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | ibliccsinexp 45398* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄[,]π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsin0pi 45399 | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | iblioosinexp 45400* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄(,)π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |