![]() |
Metamath
Proof Explorer Theorem List (p. 264 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ulmrel 26301 | The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ Rel (βπ’βπ) | ||
Theorem | ulmscl 26302 | Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β π β V) | ||
Theorem | ulmval 26303* | Express the predicate: The sequence of functions πΉ converges uniformly to πΊ on π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (π β π β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β βm π) β§ πΊ:πβΆβ β§ βπ₯ β β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) | ||
Theorem | ulmcl 26304 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) | ||
Theorem | ulmf 26305* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β βπ β β€ πΉ:(β€β₯βπ)βΆ(β βm π)) | ||
Theorem | ulmpm 26306 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β πΉ β ((β βm π) βpm β€)) | ||
Theorem | ulmf2 26307 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ ((πΉ Fn π β§ πΉ(βπ’βπ)πΊ) β πΉ:πβΆ(β βm π)) | ||
Theorem | ulm2 26308* | Simplify ulmval 26303 when πΉ and πΊ are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) & β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) β β’ (π β (πΉ(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) | ||
Theorem | ulmi 26309* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) & β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β πΆ β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < πΆ) | ||
Theorem | ulmclm 26310* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π΄ β π) & β’ (π β π» β π) & β’ ((π β§ π β π) β ((πΉβπ)βπ΄) = (π»βπ)) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β π» β (πΊβπ΄)) | ||
Theorem | ulmres 26311 | A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ(βπ’βπ)πΊ β (πΉ βΎ π)(βπ’βπ)πΊ)) | ||
Theorem | ulmshftlem 26312* | Lemma for ulmshft 26313. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯β(π + πΎ)) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π» = (π β π β¦ (πΉβ(π β πΎ)))) β β’ (π β (πΉ(βπ’βπ)πΊ β π»(βπ’βπ)πΊ)) | ||
Theorem | ulmshft 26313* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯β(π + πΎ)) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π» = (π β π β¦ (πΉβ(π β πΎ)))) β β’ (π β (πΉ(βπ’βπ)πΊ β π»(βπ’βπ)πΊ)) | ||
Theorem | ulm0 26314 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) β β’ ((π β§ π = β ) β πΉ(βπ’βπ)πΊ) | ||
Theorem | ulmuni 26315 | A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β πΊ = π») | ||
Theorem | ulmdm 26316 | 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 Mario Carneiro, 5-Jul-2017.) |
β’ (πΉ β dom (βπ’βπ) β πΉ(βπ’βπ)((βπ’βπ)βπΉ)) | ||
Theorem | ulmcaulem 26317* | Lemma for ulmcau 26318 and ulmcau2 26319: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 15326. (Contributed by Mario Carneiro, 1-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) | ||
Theorem | ulmcau 26318* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < π₯ there is a π such that for all π β€ π the functions πΉ(π) and πΉ(π) are uniformly within π₯ of each other on π. This is the four-quantifier version, see ulmcau2 26319 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ β dom (βπ’βπ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) | ||
Theorem | ulmcau2 26319* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < π₯ there is a π such that for all π β€ π, π the functions πΉ(π) and πΉ(π) are uniformly within π₯ of each other on π. (Contributed by Mario Carneiro, 1-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ β dom (βπ’βπ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) | ||
Theorem | ulmss 26320* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β π΄ β π) & β’ (π β (π₯ β π β¦ π΄)(βπ’βπ)πΊ) β β’ (π β (π₯ β π β¦ (π΄ βΎ π))(βπ’βπ)(πΊ βΎ π)) | ||
Theorem | ulmbdd 26321* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ π β π) β βπ₯ β β βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯) | ||
Theorem | ulmcn 26322 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(πβcnββ)) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β πΊ β (πβcnββ)) | ||
Theorem | ulmdvlem1 26323* | Lemma for ulmdv 26326. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») & β’ ((π β§ π) β πΆ β π) & β’ ((π β§ π) β π β β+) & β’ ((π β§ π) β π β β+) & β’ ((π β§ π) β π β β+) & β’ ((π β§ π) β π < π) & β’ ((π β§ π) β (πΆ(ballβ((abs β β ) βΎ (π Γ π)))π) β π) & β’ ((π β§ π) β (absβ(π β πΆ)) < π) & β’ ((π β§ π) β π β π) & β’ ((π β§ π) β βπ β (β€β₯βπ)βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π / 2) / 2)) & β’ ((π β§ π) β (absβ(((π D (πΉβπ))βπΆ) β (π»βπΆ))) < (π / 2)) & β’ ((π β§ π) β π β π) & β’ ((π β§ π) β π β πΆ) & β’ ((π β§ π) β ((absβ(π β πΆ)) < π β (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) < ((π / 2) / 2))) β β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β (π»βπΆ))) < π ) | ||
Theorem | ulmdvlem2 26324* | Lemma for ulmdv 26326. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β β’ ((π β§ π β π) β dom (π D (πΉβπ)) = π) | ||
Theorem | ulmdvlem3 26325* | Lemma for ulmdv 26326. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β β’ ((π β§ π§ β π) β π§(π D πΊ)(π»βπ§)) | ||
Theorem | ulmdv 26326* | If πΉ is a sequence of differentiable functions on π which converge pointwise to πΊ, and the derivatives of πΉ(π) converge uniformly to π», then πΊ is differentiable with derivative π». (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β β’ (π β (π D πΊ) = π») | ||
Theorem | mtest 26327* | The Weierstrass M-test. If πΉ is a sequence of functions which are uniformly bounded by the convergent sequence π(π), then the series generated by the sequence πΉ converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π β π) & β’ ((π β§ π β π) β (πβπ) β β) & β’ ((π β§ (π β π β§ π§ β π)) β (absβ((πΉβπ)βπ§)) β€ (πβπ)) & β’ (π β seqπ( + , π) β dom β ) β β’ (π β seqπ( βf + , πΉ) β dom (βπ’βπ)) | ||
Theorem | mtestbdd 26328* | Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π β π) & β’ ((π β§ π β π) β (πβπ) β β) & β’ ((π β§ (π β π β§ π§ β π)) β (absβ((πΉβπ)βπ§)) β€ (πβπ)) & β’ (π β seqπ( + , π) β dom β ) & β’ (π β seqπ( βf + , πΉ)(βπ’βπ)π) β β’ (π β βπ₯ β β βπ§ β π (absβ(πβπ§)) β€ π₯) | ||
Theorem | mbfulm 26329 | A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim 25584.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆMblFn) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β πΊ β MblFn) | ||
Theorem | iblulm 26330 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπΏ1) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β (volβπ) β β) β β’ (π β πΊ β πΏ1) | ||
Theorem | itgulm 26331* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπΏ1) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β (volβπ) β β) β β’ (π β (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) β β«π(πΊβπ₯) dπ₯) | ||
Theorem | itgulm2 26332* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (π₯ β π β¦ π΄) β πΏ1) & β’ (π β (π β π β¦ (π₯ β π β¦ π΄))(βπ’βπ)(π₯ β π β¦ π΅)) & β’ (π β (volβπ) β β) β β’ (π β ((π₯ β π β¦ π΅) β πΏ1 β§ (π β π β¦ β«ππ΄ dπ₯) β β«ππ΅ dπ₯)) | ||
Theorem | pserval 26333* | Value of the function πΊ that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) β β’ (π β β β (πΊβπ) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) | ||
Theorem | pserval2 26334* | Value of the function πΊ that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) β β’ ((π β β β§ π β β0) β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) | ||
Theorem | psergf 26335* | The sequence of terms in the infinite sequence defining a power series for fixed π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) β β’ (π β (πΊβπ):β0βΆβ) | ||
Theorem | radcnvlem1 26336* | Lemma for radcnvlt1 26341, radcnvle 26343. If π is a point closer to zero than π and the power series converges at π, then it converges absolutely at π, even if the terms in the sequence are multiplied by π. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (absβπ) < (absβπ)) & β’ (π β seq0( + , (πΊβπ)) β dom β ) & β’ π» = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) β β’ (π β seq0( + , π») β dom β ) | ||
Theorem | radcnvlem2 26337* | Lemma for radcnvlt1 26341, radcnvle 26343. If π is a point closer to zero than π and the power series converges at π, then it converges absolutely at π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (absβπ) < (absβπ)) & β’ (π β seq0( + , (πΊβπ)) β dom β ) β β’ (π β seq0( + , (abs β (πΊβπ))) β dom β ) | ||
Theorem | radcnvlem3 26338* | Lemma for radcnvlt1 26341, radcnvle 26343. If π is a point closer to zero than π and the power series converges at π, then it converges at π. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (absβπ) < (absβπ)) & β’ (π β seq0( + , (πΊβπ)) β dom β ) β β’ (π β seq0( + , (πΊβπ)) β dom β ) | ||
Theorem | radcnv0 26339* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) β β’ (π β 0 β {π β β β£ seq0( + , (πΊβπ)) β dom β }) | ||
Theorem | radcnvcl 26340* | The radius of convergence π of an infinite series is a nonnegative extended real number. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) β β’ (π β π β (0[,]+β)) | ||
Theorem | radcnvlt1 26341* | If π is within the open disk of radius π centered at zero, then the infinite series converges absolutely at π, and also converges when the series is multiplied by π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ (π β π β β) & β’ (π β (absβπ) < π ) & β’ π» = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) β β’ (π β (seq0( + , π») β dom β β§ seq0( + , (abs β (πΊβπ))) β dom β )) | ||
Theorem | radcnvlt2 26342* | If π is within the open disk of radius π centered at zero, then the infinite series converges at π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ (π β π β β) & β’ (π β (absβπ) < π ) β β’ (π β seq0( + , (πΊβπ)) β dom β ) | ||
Theorem | radcnvle 26343* | If π is a convergent point of the infinite series, then π is within the closed disk of radius π centered at zero. Or, by contraposition, the series diverges at any point strictly more than π from the origin. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ (π β π β β) & β’ (π β seq0( + , (πΊβπ)) β dom β ) β β’ (π β (absβπ) β€ π ) | ||
Theorem | dvradcnv 26344* | The radius of convergence of the (formal) derivative π» of the power series πΊ is at least as large as the radius of convergence of πΊ. (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β0 β¦ (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β (absβπ) < π ) β β’ (π β seq0( + , π») β dom β ) | ||
Theorem | pserulm 26345* | If π is a region contained in a circle of radius π < π , then the sequence of partial sums of the infinite series converges uniformly on π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) & β’ (π β π β β) & β’ (π β π < π ) & β’ (π β π β (β‘abs β (0[,]π))) β β’ (π β π»(βπ’βπ)πΉ) | ||
Theorem | psercn2 26346* | Since by pserulm 26345 the series converges uniformly, it is also continuous by ulmcn 26322. (Contributed by Mario Carneiro, 3-Mar-2015.) Avoid ax-mulf 11210. (Revised by GG, 16-Mar-2025.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) & β’ (π β π β β) & β’ (π β π < π ) & β’ (π β π β (β‘abs β (0[,]π))) β β’ (π β πΉ β (πβcnββ)) | ||
Theorem | psercn2OLD 26347* | Obsolete version of psercn2 26346 as of 16-Apr-2025. (Contributed by Mario Carneiro, 3-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π» = (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) & β’ (π β π β β) & β’ (π β π < π ) & β’ (π β π β (β‘abs β (0[,]π))) β β’ (π β πΉ β (πβcnββ)) | ||
Theorem | psercnlem2 26348* | Lemma for psercn 26350. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ ((π β§ π β π) β (π β β+ β§ (absβπ) < π β§ π < π )) β β’ ((π β§ π β π) β (π β (0(ballβ(abs β β ))π) β§ (0(ballβ(abs β β ))π) β (β‘abs β (0[,]π)) β§ (β‘abs β (0[,]π)) β π)) | ||
Theorem | psercnlem1 26349* | Lemma for psercn 26350. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ π = if(π β β, (((absβπ) + π ) / 2), ((absβπ) + 1)) β β’ ((π β§ π β π) β (π β β+ β§ (absβπ) < π β§ π < π )) | ||
Theorem | psercn 26350* | An infinite series converges to a continuous function on the open disk of radius π , where π is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ π = if(π β β, (((absβπ) + π ) / 2), ((absβπ) + 1)) β β’ (π β πΉ β (πβcnββ)) | ||
Theorem | pserdvlem1 26351* | Lemma for pserdv 26353. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ π = if(π β β, (((absβπ) + π ) / 2), ((absβπ) + 1)) β β’ ((π β§ π β π) β ((((absβπ) + π) / 2) β β+ β§ (absβπ) < (((absβπ) + π) / 2) β§ (((absβπ) + π) / 2) < π )) | ||
Theorem | pserdvlem2 26352* | Lemma for pserdv 26353. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ π = if(π β β, (((absβπ) + π ) / 2), ((absβπ) + 1)) & β’ π΅ = (0(ballβ(abs β β ))(((absβπ) + π) / 2)) β β’ ((π β§ π β π) β (β D (πΉ βΎ π΅)) = (π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))) | ||
Theorem | pserdv 26353* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ π = if(π β β, (((absβπ) + π ) / 2), ((absβπ) + 1)) & β’ π΅ = (0(ballβ(abs β β ))(((absβπ) + π) / 2)) β β’ (π β (β D πΉ) = (π¦ β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))) | ||
Theorem | pserdv2 26354* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ π = (β‘abs β (0[,)π )) & β’ π = if(π β β, (((absβπ) + π ) / 2), ((absβπ) + 1)) & β’ π΅ = (0(ballβ(abs β β ))(((absβπ) + π) / 2)) β β’ (π β (β D πΉ) = (π¦ β π β¦ Ξ£π β β ((π Β· (π΄βπ)) Β· (π¦β(π β 1))))) | ||
Theorem | abelthlem1 26355* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) β β’ (π β 1 β€ sup({π β β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*, < )) | ||
Theorem | abelthlem2 26356* | Lemma for abelth 26365. The peculiar region π, known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing 1. Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} β β’ (π β (1 β π β§ (π β {1}) β (0(ballβ(abs β β ))1))) | ||
Theorem | abelthlem3 26357* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} β β’ ((π β§ π β π) β seq0( + , (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) | ||
Theorem | abelthlem4 26358* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) β β’ (π β πΉ:πβΆβ) | ||
Theorem | abelthlem5 26359* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) & β’ (π β seq0( + , π΄) β 0) β β’ ((π β§ π β (0(ballβ(abs β β ))1)) β seq0( + , (π β β0 β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))) β dom β ) | ||
Theorem | abelthlem6 26360* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 2-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) & β’ (π β seq0( + , π΄) β 0) & β’ (π β π β (π β {1})) β β’ (π β (πΉβπ) = ((1 β π) Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) | ||
Theorem | abelthlem7a 26361* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) & β’ (π β seq0( + , π΄) β 0) & β’ (π β π β (π β {1})) β β’ (π β (π β β β§ (absβ(1 β π)) β€ (π Β· (1 β (absβπ))))) | ||
Theorem | abelthlem7 26362* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 2-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) & β’ (π β seq0( + , π΄) β 0) & β’ (π β π β (π β {1})) & β’ (π β π β β+) & β’ (π β π β β0) & β’ (π β βπ β (β€β₯βπ)(absβ(seq0( + , π΄)βπ)) < π ) & β’ (π β (absβ(1 β π)) < (π / (Ξ£π β (0...(π β 1))(absβ(seq0( + , π΄)βπ)) + 1))) β β’ (π β (absβ(πΉβπ)) < ((π + 1) Β· π )) | ||
Theorem | abelthlem8 26363* | Lemma for abelth 26365. (Contributed by Mario Carneiro, 2-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) & β’ (π β seq0( + , π΄) β 0) β β’ ((π β§ π β β+) β βπ€ β β+ βπ¦ β π ((absβ(1 β π¦)) < π€ β (absβ((πΉβ1) β (πΉβπ¦))) < π )) | ||
Theorem | abelthlem9 26364* | Lemma for abelth 26365. By adjusting the constant term, we can assume that the entire series converges to 0. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) β β’ ((π β§ π β β+) β βπ€ β β+ βπ¦ β π ((absβ(1 β π¦)) < π€ β (absβ((πΉβ1) β (πΉβπ¦))) < π )) | ||
Theorem | abelth 26365* | Abel's theorem. If the power series Ξ£π β β0π΄(π)(π₯βπ) is convergent at 1, then it is equal to the limit from "below", along a Stolz angle π (note that the π = 1 case of a Stolz angle is the real line [0, 1]). (Continuity on π β {1} follows more generally from psercn 26350.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ (π β π β β) & β’ (π β 0 β€ π) & β’ π = {π§ β β β£ (absβ(1 β π§)) β€ (π Β· (1 β (absβπ§)))} & β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) β β’ (π β πΉ β (πβcnββ)) | ||
Theorem | abelth2 26366* | Abel's theorem, restricted to the [0, 1] interval. (Contributed by Mario Carneiro, 2-Apr-2015.) |
β’ (π β π΄:β0βΆβ) & β’ (π β seq0( + , π΄) β dom β ) & β’ πΉ = (π₯ β (0[,]1) β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) β β’ (π β πΉ β ((0[,]1)βcnββ)) | ||
Theorem | efcn 26367 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
β’ exp β (ββcnββ) | ||
Theorem | sincn 26368 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
β’ sin β (ββcnββ) | ||
Theorem | coscn 26369 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
β’ cos β (ββcnββ) | ||
Theorem | reeff1olem 26370* | Lemma for reeff1o 26371. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ ((π β β β§ 1 < π) β βπ₯ β β (expβπ₯) = π) | ||
Theorem | reeff1o 26371 | The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (exp βΎ β):ββ1-1-ontoββ+ | ||
Theorem | reefiso 26372 | The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.) |
β’ (exp βΎ β) Isom < , < (β, β+) | ||
Theorem | efcvx 26373 | The exponential function on the reals is a strictly convex function. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (((π΄ β β β§ π΅ β β β§ π΄ < π΅) β§ π β (0(,)1)) β (expβ((π Β· π΄) + ((1 β π) Β· π΅))) < ((π Β· (expβπ΄)) + ((1 β π) Β· (expβπ΅)))) | ||
Theorem | reefgim 26374 | The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.) |
β’ π = ((mulGrpββfld) βΎs β+) β β’ (exp βΎ β) β (βfld GrpIso π) | ||
Theorem | pilem1 26375 | Lemma for pire 26380, pigt2lt4 26378 and sinpi 26379. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (π΄ β (β+ β© (β‘sin β {0})) β (π΄ β β+ β§ (sinβπ΄) = 0)) | ||
Theorem | pilem2 26376 | Lemma for pire 26380, pigt2lt4 26378 and sinpi 26379. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
β’ (π β π΄ β (2(,)4)) & β’ (π β π΅ β β+) & β’ (π β (sinβπ΄) = 0) & β’ (π β (sinβπ΅) = 0) β β’ (π β ((Ο + π΄) / 2) β€ π΅) | ||
Theorem | pilem3 26377 | Lemma for pire 26380, pigt2lt4 26378 and sinpi 26379. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.) (Proof shortened by BJ, 30-Jun-2022.) |
β’ (Ο β (2(,)4) β§ (sinβΟ) = 0) | ||
Theorem | pigt2lt4 26378 | Ο is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ (2 < Ο β§ Ο < 4) | ||
Theorem | sinpi 26379 | The sine of Ο is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (sinβΟ) = 0 | ||
Theorem | pire 26380 | Ο is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ Ο β β | ||
Theorem | picn 26381 | Ο is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ Ο β β | ||
Theorem | pipos 26382 | Ο is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ 0 < Ο | ||
Theorem | pirp 26383 | Ο is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ Ο β β+ | ||
Theorem | negpicn 26384 | -Ο is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -Ο β β | ||
Theorem | sinhalfpilem 26385 | Lemma for sinhalfpi 26390 and coshalfpi 26391. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ ((sinβ(Ο / 2)) = 1 β§ (cosβ(Ο / 2)) = 0) | ||
Theorem | halfpire 26386 | Ο / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
β’ (Ο / 2) β β | ||
Theorem | neghalfpire 26387 | -Ο / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -(Ο / 2) β β | ||
Theorem | neghalfpirx 26388 | -Ο / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -(Ο / 2) β β* | ||
Theorem | pidiv2halves 26389 | Adding Ο / 2 to itself gives Ο. See 2halves 12462. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ ((Ο / 2) + (Ο / 2)) = Ο | ||
Theorem | sinhalfpi 26390 | The sine of Ο / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (sinβ(Ο / 2)) = 1 | ||
Theorem | coshalfpi 26391 | The cosine of Ο / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (cosβ(Ο / 2)) = 0 | ||
Theorem | cosneghalfpi 26392 | The cosine of -Ο / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
β’ (cosβ-(Ο / 2)) = 0 | ||
Theorem | efhalfpi 26393 | The exponential of iΟ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (expβ(i Β· (Ο / 2))) = i | ||
Theorem | cospi 26394 | The cosine of Ο is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (cosβΟ) = -1 | ||
Theorem | efipi 26395 | The exponential of i Β· Ο is -1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (expβ(i Β· Ο)) = -1 | ||
Theorem | eulerid 26396 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ ((expβ(i Β· Ο)) + 1) = 0 | ||
Theorem | sin2pi 26397 | The sine of 2Ο is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (sinβ(2 Β· Ο)) = 0 | ||
Theorem | cos2pi 26398 | The cosine of 2Ο is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (cosβ(2 Β· Ο)) = 1 | ||
Theorem | ef2pi 26399 | The exponential of 2Οi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (expβ(i Β· (2 Β· Ο))) = 1 | ||
Theorem | ef2kpi 26400 | If πΎ is an integer, then the exponential of 2πΎΟi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (πΎ β β€ β (expβ((i Β· (2 Β· Ο)) Β· πΎ)) = 1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |