![]() |
Metamath
Proof Explorer Theorem List (p. 447 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ioccncflimc 44601 | 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 44602* | 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 44603* | 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 44604* | 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 44605 | 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 44606* | A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β {π΄} β¦ π΅) β ({π΄}βcnβ{π΅})) | ||
Theorem | divcncff 44607 | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnβ(β β {0}))) β β’ (π β (πΉ βf / πΊ) β (πβcnββ)) | ||
Theorem | cncfshiftioo 44608* | 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 44609* | 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 44610* | 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 44611* | 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 44612* | πΊ actually extends πΉ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆπ) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β (πΊβπΆ) = (πΉβπΆ)) | ||
Theorem | cncfioobd 44613* | 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 44614 | 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 44615* | The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π΄ β (β β (-β(,]0)) β (π₯ β β β¦ (π΄βππ₯)) β (ββcnββ)) | ||
Theorem | fprodcncf 44616* | The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ βπ β π΅ πΆ) β (π΄βcnββ)) | ||
Theorem | add1cncf 44617* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | add2cncf 44618* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub1cncfd 44619* | Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ β π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub2cncfd 44620* | Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsub2cncf 44621* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodadd2cncf 44622* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsubrecnncnvlem 44623* | 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 44624* | 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 44625* | 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 44626* | 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 44627* | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (π β π β β) β β’ (π β (β D (π₯ β β β¦ ((sinβπ₯)βπ))) = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)))) | ||
Theorem | dvcosre 44628 | The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (β D (π₯ β β β¦ (cosβπ₯))) = (π₯ β β β¦ -(sinβπ₯)) | ||
Theorem | dvsinax 44629* | 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 44630 | 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 44631* | Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) & β’ (π β π΅ β β) β β’ (π β (π D (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ 0)) | ||
Theorem | dvcnre 44632 | From complex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((πΉ:ββΆβ β§ β β dom (β D πΉ)) β (β D (πΉ βΎ β)) = ((β D πΉ) βΎ β)) | ||
Theorem | dvmptidg 44633* | Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) β β’ (π β (π D (π₯ β π΄ β¦ π₯)) = (π₯ β π΄ β¦ 1)) | ||
Theorem | dvresntr 44634 | 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 44635* | The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = (β D πΉ) β β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯))) | ||
Theorem | dvasinbx 44636* | 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 44637 | Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΉ:π΄βΆβ) β (β D (πΉ βΎ (π΅(,)πΆ))) = ((β D πΉ) βΎ (π΅(,)πΆ))) | ||
Theorem | dvdivf 44638 | 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 44639* | 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 44640 | 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 44641 | 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 44642* | 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 44643 | 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 44644* | 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 44645* | 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 44646* | 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 44647* | 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 44648* | 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 44649* | 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 44650* | 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 44651* | 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 44652 | π 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 44653* | Function-builder for derivative, product rule. A version of dvmptmul 25478 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) | ||
Theorem | dvnmptdivc 44654* | 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 44655 | If πΎ divides π but πΎ does not divide π, then πΎ does not divide (π + π). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((Β¬ πΎ β₯ π β§ πΎ β₯ π) β Β¬ πΎ β₯ (π + π))) | ||
Theorem | dvxpaek 44656* | Derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β) β β’ (π β (π D (π₯ β π β¦ ((π₯ + π΄)βπΎ))) = (π₯ β π β¦ (πΎ Β· ((π₯ + π΄)β(πΎ β 1))))) | ||
Theorem | dvnmptconst 44657* | The π-th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ 0)) | ||
Theorem | dvnxpaek 44658* | The π-th derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β0) & β’ πΉ = (π₯ β π β¦ ((π₯ + π΄)βπΎ)) β β’ ((π β§ π β β0) β ((π Dπ πΉ)βπ) = (π₯ β π β¦ if(πΎ < π, 0, (((!βπΎ) / (!β(πΎ β π))) Β· ((π₯ + π΄)β(πΎ β π)))))) | ||
Theorem | dvnmul 44659* | 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 44660* | Induction step for dvmptfprod 44661. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ β²ππ & β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ (π β π· β Fin) & β’ (π β πΈ β V) & β’ (π β Β¬ πΈ β π·) & β’ (π β (π· βͺ {πΈ}) β πΌ) & β’ (π β π β {β, β}) & β’ (((π β§ π₯ β π) β§ π β π·) β πΆ β β) & β’ (π β (π D (π₯ β π β¦ βπ β π· π΄)) = (π₯ β π β¦ Ξ£π β π· (πΆ Β· βπ β (π· β {π})π΄))) & β’ ((π β§ π₯ β π) β πΊ β β) & β’ (π β (π D (π₯ β π β¦ πΉ)) = (π₯ β π β¦ πΊ)) & β’ (π = πΈ β π΄ = πΉ) & β’ (π = πΈ β πΆ = πΊ) β β’ (π β (π D (π₯ β π β¦ βπ β (π· βͺ {πΈ})π΄)) = (π₯ β π β¦ Ξ£π β (π· βͺ {πΈ})(πΆ Β· βπ β ((π· βͺ {πΈ}) β {π})π΄))) | ||
Theorem | dvmptfprod 44661* | Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β πΌ β Fin) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΅ β β) & β’ ((π β§ π β πΌ) β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π = π β π΅ = πΆ) β β’ (π β (π D (π₯ β π β¦ βπ β πΌ π΄)) = (π₯ β π β¦ Ξ£π β πΌ (πΆ Β· βπ β (πΌ β {π})π΄))) | ||
Theorem | dvnprodlem1 44662* | π· is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π½ β β0) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β Β¬ π β π ) & β’ (π β (π βͺ {π}) β π) β β’ (π β π·:((πΆβ(π βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ )βπ))) | ||
Theorem | dvnprodlem2 44663* | Induction step for dvnprodlem2 44663. (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 44664* | 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 44665* | 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 44666* | 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 44667* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄[,]π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsin0pi 44668 | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | iblioosinexp 44669* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄(,)π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsinexplem1 44670* | Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π₯ β β β¦ ((sinβπ₯)βπ)) & β’ πΊ = (π₯ β β β¦ -(cosβπ₯)) & β’ π» = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯))) & β’ πΌ = (π₯ β β β¦ (((sinβπ₯)βπ) Β· (sinβπ₯))) & β’ πΏ = (π₯ β β β¦ (((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)) Β· -(cosβπ₯))) & β’ π = (π₯ β β β¦ (((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1)))) & β’ (π β π β β) β β’ (π β β«(0(,)Ο)(((sinβπ₯)βπ) Β· (sinβπ₯)) dπ₯ = (π Β· β«(0(,)Ο)(((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1))) dπ₯)) | ||
Theorem | itgsinexp 44671* | A recursive formula for the integral of sin^N on the interval (0,Ο) . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β (β€β₯β2)) β β’ (π β (πΌβπ) = (((π β 1) / π) Β· (πΌβ(π β 2)))) | ||
Theorem | iblconstmpt 44672* | A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β dom vol β§ (volβπ΄) β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β πΏ1) | ||
Theorem | itgeq1d 44673* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ = π΅) β β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | mbfres2cn 44674 | Measurability of a piecewise function: if πΉ is measurable on subsets π΅ and πΆ of its domain, and these pieces make up all of π΄, then πΉ is measurable on the whole domain. Similar to mbfres2 25162 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β (πΉ βΎ π΅) β MblFn) & β’ (π β (πΉ βΎ πΆ) β MblFn) & β’ (π β (π΅ βͺ πΆ) = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | vol0 44675 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (volββ ) = 0 | ||
Theorem | ditgeqiooicc 44676* | A function πΉ on an open interval, has the same directed integral as its extension πΊ on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) β β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β¨[π΄ β π΅](πΊβπ₯) dπ₯) | ||
Theorem | volge0 44677 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β dom vol β 0 β€ (volβπ΄)) | ||
Theorem | cnbdibl 44678* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β dom vol) & β’ (π β (volβπ΄) β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | snmbl 44679 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β {π΄} β dom vol) | ||
Theorem | ditgeq3d 44680* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β€ π΅) & β’ ((π β§ π₯ β (π΄(,)π΅)) β π· = πΈ) β β’ (π β β¨[π΄ β π΅]π· dπ₯ = β¨[π΄ β π΅]πΈ dπ₯) | ||
Theorem | iblempty 44681 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β πΏ1 | ||
Theorem | iblsplit 44682* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | volsn 44683 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (volβ{π΄}) = 0) | ||
Theorem | itgvol0 44684* | If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β§ β«π΄π΅ dπ₯ = 0)) | ||
Theorem | itgcoscmulx 44685* | Exercise: the integral of π₯ β¦ cosππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) & β’ (π β π΄ β 0) β β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) | ||
Theorem | iblsplitf 44686* | A version of iblsplit 44682 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | ibliooicc 44687* | If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π₯ β (π΄(,)π΅) β¦ πΆ) β πΏ1) & β’ ((π β§ π₯ β (π΄[,]π΅)) β πΆ β β) β β’ (π β (π₯ β (π΄[,]π΅) β¦ πΆ) β πΏ1) | ||
Theorem | volioc 44688 | The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,]π΅)) = (π΅ β π΄)) | ||
Theorem | iblspltprt 44689* | If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π‘π & β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ ((π β§ π β (π...π)) β (πβπ) β β) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β (π‘ β ((πβπ)[,](πβπ)) β¦ π΄) β πΏ1) | ||
Theorem | itgsincmulx 44690* | Exercise: the integral of π₯ β¦ sinππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) β β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) | ||
Theorem | itgsubsticclem 44691* | lemma for itgsubsticc 44692. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π’ β (πΎ[,]πΏ) β¦ πΆ) & β’ πΊ = (π’ β β β¦ if(π’ β (πΎ[,]πΏ), (πΉβπ’), if(π’ < πΎ, (πΉβπΎ), (πΉβπΏ)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β πΉ β ((πΎ[,]πΏ)βcnββ)) & β’ (π β πΎ β β) & β’ (π β πΏ β β) & β’ (π β πΎ β€ πΏ) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubsticc 44692* | Integration by u-substitution. The main difference with respect to itgsubst 25566 is that here we consider the range of π΄(π₯) to be in the closed interval (πΎ[,]πΏ). If π΄(π₯) is a continuous, differentiable function from [π, π] to (π, π), whose derivative is continuous and integrable, and πΆ(π’) is a continuous function on (π, π), then the integral of πΆ(π’) from πΎ = π΄(π) to πΏ = π΄(π) is equal to the integral of πΆ(π΄(π₯)) D π΄(π₯) from π to π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π’ β (πΎ[,]πΏ) β¦ πΆ) β ((πΎ[,]πΏ)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) & β’ (π β πΎ β β) & β’ (π β πΏ β β) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgioocnicc 44693* | The integral of a piecewise continuous function πΉ on an open interval is equal to the integral of the continuous function πΊ, in the corresponding closed interval. πΊ is equal to πΉ on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β (πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) & β’ (π β (π΄[,]π΅) β dom πΉ) & β’ (π β π β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) & β’ (π β πΏ β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) β β’ (π β (πΊ β πΏ1 β§ β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯)) | ||
Theorem | iblcncfioo 44694 | A continuous function πΉ on an open interval (π΄(,)π΅) with a finite right limit π in π΄ and a finite left limit πΏ in π΅ is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΉ β πΏ1) | ||
Theorem | itgspltprt 44695* | The β« integral splits on a given partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π:(π...π)βΆβ) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β β«((πβπ)[,](πβπ))π΄ dπ‘ = Ξ£π β (π..^π)β«((πβπ)[,](πβ(π + 1)))π΄ dπ‘) | ||
Theorem | itgiccshift 44696* | The integral of a function, πΉ stays the same if its closed interval domain is shifted by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β π β β+) & β’ πΊ = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgperiod 44697* | The integral of a periodic function, with period π stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β+) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgsbtaddcnst 44698* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β¨[(π΄ β π) β (π΅ β π)](πΉβ(π + π )) dπ = β¨[π΄ β π΅](πΉβπ‘) dπ‘) | ||
Theorem | volico 44699 | The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) = if(π΄ < π΅, (π΅ β π΄), 0)) | ||
Theorem | sublevolico 44700 | The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΅ β π΄) β€ (volβ(π΄[,)π΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |