![]() |
Metamath
Proof Explorer Theorem List (p. 448 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fprodcncf 44701* | The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ βπ β π΅ πΆ) β (π΄βcnββ)) | ||
Theorem | add1cncf 44702* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | add2cncf 44703* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub1cncfd 44704* | Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ β π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub2cncfd 44705* | Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsub2cncf 44706* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodadd2cncf 44707* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsubrecnncnvlem 44708* | 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 44709* | 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 44710* | 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 44711* | 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 44712* | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (π β π β β) β β’ (π β (β D (π₯ β β β¦ ((sinβπ₯)βπ))) = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)))) | ||
Theorem | dvcosre 44713 | The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (β D (π₯ β β β¦ (cosβπ₯))) = (π₯ β β β¦ -(sinβπ₯)) | ||
Theorem | dvsinax 44714* | 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 44715 | 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 44716* | Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) & β’ (π β π΅ β β) β β’ (π β (π D (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ 0)) | ||
Theorem | dvcnre 44717 | From complex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((πΉ:ββΆβ β§ β β dom (β D πΉ)) β (β D (πΉ βΎ β)) = ((β D πΉ) βΎ β)) | ||
Theorem | dvmptidg 44718* | Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β ((TopOpenββfld) βΎt π)) β β’ (π β (π D (π₯ β π΄ β¦ π₯)) = (π₯ β π΄ β¦ 1)) | ||
Theorem | dvresntr 44719 | 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 44720* | The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = (β D πΉ) β β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯))) | ||
Theorem | dvasinbx 44721* | 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 44722 | Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΉ:π΄βΆβ) β (β D (πΉ βΎ (π΅(,)πΆ))) = ((β D πΉ) βΎ (π΅(,)πΆ))) | ||
Theorem | dvdivf 44723 | 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 44724* | 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 44725 | 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 44726 | 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 44727* | 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 44728 | 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 44729* | 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 44730* | 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 44731* | 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 44732* | 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 44733* | 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 44734* | 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 44735* | 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 44736* | 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 44737 | π 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 44738* | Function-builder for derivative, product rule. A version of dvmptmul 25485 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) | ||
Theorem | dvnmptdivc 44739* | 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 44740 | If πΎ divides π but πΎ does not divide π, then πΎ does not divide (π + π). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((Β¬ πΎ β₯ π β§ πΎ β₯ π) β Β¬ πΎ β₯ (π + π))) | ||
Theorem | dvxpaek 44741* | Derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β) β β’ (π β (π D (π₯ β π β¦ ((π₯ + π΄)βπΎ))) = (π₯ β π β¦ (πΎ Β· ((π₯ + π΄)β(πΎ β 1))))) | ||
Theorem | dvnmptconst 44742* | The π-th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ 0)) | ||
Theorem | dvnxpaek 44743* | The π-th derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β0) & β’ πΉ = (π₯ β π β¦ ((π₯ + π΄)βπΎ)) β β’ ((π β§ π β β0) β ((π Dπ πΉ)βπ) = (π₯ β π β¦ if(πΎ < π, 0, (((!βπΎ) / (!β(πΎ β π))) Β· ((π₯ + π΄)β(πΎ β π)))))) | ||
Theorem | dvnmul 44744* | 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 44745* | Induction step for dvmptfprod 44746. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ β²ππ & β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ (π β π· β Fin) & β’ (π β πΈ β V) & β’ (π β Β¬ πΈ β π·) & β’ (π β (π· βͺ {πΈ}) β πΌ) & β’ (π β π β {β, β}) & β’ (((π β§ π₯ β π) β§ π β π·) β πΆ β β) & β’ (π β (π D (π₯ β π β¦ βπ β π· π΄)) = (π₯ β π β¦ Ξ£π β π· (πΆ Β· βπ β (π· β {π})π΄))) & β’ ((π β§ π₯ β π) β πΊ β β) & β’ (π β (π D (π₯ β π β¦ πΉ)) = (π₯ β π β¦ πΊ)) & β’ (π = πΈ β π΄ = πΉ) & β’ (π = πΈ β πΆ = πΊ) β β’ (π β (π D (π₯ β π β¦ βπ β (π· βͺ {πΈ})π΄)) = (π₯ β π β¦ Ξ£π β (π· βͺ {πΈ})(πΆ Β· βπ β ((π· βͺ {πΈ}) β {π})π΄))) | ||
Theorem | dvmptfprod 44746* | Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β πΌ β Fin) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΅ β β) & β’ ((π β§ π β πΌ) β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π = π β π΅ = πΆ) β β’ (π β (π D (π₯ β π β¦ βπ β πΌ π΄)) = (π₯ β π β¦ Ξ£π β πΌ (πΆ Β· βπ β (πΌ β {π})π΄))) | ||
Theorem | dvnprodlem1 44747* | π· is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π½ β β0) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β Β¬ π β π ) & β’ (π β (π βͺ {π}) β π) β β’ (π β π·:((πΆβ(π βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ )βπ))) | ||
Theorem | dvnprodlem2 44748* | Induction step for dvnprodlem2 44748. (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 44749* | 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 44750* | 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 44751* | 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 44752* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄[,]π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsin0pi 44753 | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | iblioosinexp 44754* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄(,)π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsinexplem1 44755* | 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 44756* | 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 44757* | A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β dom vol β§ (volβπ΄) β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β πΏ1) | ||
Theorem | itgeq1d 44758* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ = π΅) β β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | mbfres2cn 44759 | 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 25169 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β (πΉ βΎ π΅) β MblFn) & β’ (π β (πΉ βΎ πΆ) β MblFn) & β’ (π β (π΅ βͺ πΆ) = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | vol0 44760 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (volββ ) = 0 | ||
Theorem | ditgeqiooicc 44761* | 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 44762 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β dom vol β 0 β€ (volβπ΄)) | ||
Theorem | cnbdibl 44763* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β dom vol) & β’ (π β (volβπ΄) β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | snmbl 44764 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β {π΄} β dom vol) | ||
Theorem | ditgeq3d 44765* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β€ π΅) & β’ ((π β§ π₯ β (π΄(,)π΅)) β π· = πΈ) β β’ (π β β¨[π΄ β π΅]π· dπ₯ = β¨[π΄ β π΅]πΈ dπ₯) | ||
Theorem | iblempty 44766 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β πΏ1 | ||
Theorem | iblsplit 44767* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | volsn 44768 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (volβ{π΄}) = 0) | ||
Theorem | itgvol0 44769* | 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 44770* | Exercise: the integral of π₯ β¦ cosππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) & β’ (π β π΄ β 0) β β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) | ||
Theorem | iblsplitf 44771* | A version of iblsplit 44767 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | ibliooicc 44772* | 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 44773 | The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,]π΅)) = (π΅ β π΄)) | ||
Theorem | iblspltprt 44774* | 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 44775* | Exercise: the integral of π₯ β¦ sinππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) β β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) | ||
Theorem | itgsubsticclem 44776* | lemma for itgsubsticc 44777. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π’ β (πΎ[,]πΏ) β¦ πΆ) & β’ πΊ = (π’ β β β¦ if(π’ β (πΎ[,]πΏ), (πΉβπ’), if(π’ < πΎ, (πΉβπΎ), (πΉβπΏ)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β πΉ β ((πΎ[,]πΏ)βcnββ)) & β’ (π β πΎ β β) & β’ (π β πΏ β β) & β’ (π β πΎ β€ πΏ) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubsticc 44777* | Integration by u-substitution. The main difference with respect to itgsubst 25573 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 44778* | 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 44779 | 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 44780* | The β« integral splits on a given partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π:(π...π)βΆβ) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β β«((πβπ)[,](πβπ))π΄ dπ‘ = Ξ£π β (π..^π)β«((πβπ)[,](πβ(π + 1)))π΄ dπ‘) | ||
Theorem | itgiccshift 44781* | 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 44782* | 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 44783* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β¨[(π΄ β π) β (π΅ β π)](πΉβ(π + π )) dπ = β¨[π΄ β π΅](πΉβπ‘) dπ‘) | ||
Theorem | volico 44784 | The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) = if(π΄ < π΅, (π΅ β π΄), 0)) | ||
Theorem | sublevolico 44785 | 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β(π΄[,)π΅))) | ||
Theorem | dmvolss 44786 | Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β π« β | ||
Theorem | ismbl3 44787* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl2 25051, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))) β€ (vol*βπ₯))) | ||
Theorem | volioof 44788 | The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (vol β (,)):(β* Γ β*)βΆ(0[,]+β) | ||
Theorem | ovolsplit 44789 | The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) β β’ (π β (vol*βπ΄) β€ ((vol*β(π΄ β© π΅)) +π (vol*β(π΄ β π΅)))) | ||
Theorem | fvvolioof 44790 | The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β (,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))(,)(2nd β(πΉβπ))))) | ||
Theorem | volioore 44791 | The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) = if(π΄ β€ π΅, (π΅ β π΄), 0)) | ||
Theorem | fvvolicof 44792 | The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β [,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))[,)(2nd β(πΉβπ))))) | ||
Theorem | voliooico 44793 | An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄(,)π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | ismbl4 44794* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl 25050, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β(vol*βπ₯) = ((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))))) | ||
Theorem | volioofmpt 44795* | ((vol β (,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β* Γ β*)) β β’ (π β ((vol β (,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicoff 44796 | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ):π΄βΆ(0[,]+β)) | ||
Theorem | voliooicof 44797 | The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β)) β β’ (π β ((vol β (,)) β πΉ) = ((vol β [,)) β πΉ)) | ||
Theorem | volicofmpt 44798* | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicc 44799 | The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | voliccico 44800 | A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄[,]π΅)) = (volβ(π΄[,)π΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |