![]() |
Metamath
Proof Explorer Theorem List (p. 161 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bpolycl 16001 | Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
β’ ((π β β0 β§ π β β) β (π BernPoly π) β β) | ||
Theorem | bpolysum 16002* | A sum for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
β’ ((π β β0 β§ π β β) β Ξ£π β (0...π)((πCπ) Β· ((π BernPoly π) / ((π β π) + 1))) = (πβπ)) | ||
Theorem | bpolydiflem 16003* | Lemma for bpolydif 16004. (Contributed by Scott Fenton, 12-Jun-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ ((π β§ π β (1...(π β 1))) β ((π BernPoly (π + 1)) β (π BernPoly π)) = (π Β· (πβ(π β 1)))) β β’ (π β ((π BernPoly (π + 1)) β (π BernPoly π)) = (π Β· (πβ(π β 1)))) | ||
Theorem | bpolydif 16004 | Calculate the difference between successive values of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 26-May-2014.) |
β’ ((π β β β§ π β β) β ((π BernPoly (π + 1)) β (π BernPoly π)) = (π Β· (πβ(π β 1)))) | ||
Theorem | fsumkthpow 16005* | A closed-form expression for the sum of πΎ-th powers. (Contributed by Scott Fenton, 16-May-2014.) This is Metamath 100 proof #77. (Revised by Mario Carneiro, 16-Jun-2014.) |
β’ ((πΎ β β0 β§ π β β0) β Ξ£π β (0...π)(πβπΎ) = ((((πΎ + 1) BernPoly (π + 1)) β ((πΎ + 1) BernPoly 0)) / (πΎ + 1))) | ||
Theorem | bpoly2 16006 | The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.) |
β’ (π β β β (2 BernPoly π) = (((πβ2) β π) + (1 / 6))) | ||
Theorem | bpoly3 16007 | The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.) |
β’ (π β β β (3 BernPoly π) = (((πβ3) β ((3 / 2) Β· (πβ2))) + ((1 / 2) Β· π))) | ||
Theorem | bpoly4 16008 | The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.) |
β’ (π β β β (4 BernPoly π) = ((((πβ4) β (2 Β· (πβ3))) + (πβ2)) β (1 / ;30))) | ||
Theorem | fsumcube 16009* | Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.) |
β’ (π β β0 β Ξ£π β (0...π)(πβ3) = (((πβ2) Β· ((π + 1)β2)) / 4)) | ||
Syntax | ce 16010 | Extend class notation to include the exponential function. |
class exp | ||
Syntax | ceu 16011 | Extend class notation to include Euler's constant e = 2.71828.... |
class e | ||
Syntax | csin 16012 | Extend class notation to include the sine function. |
class sin | ||
Syntax | ccos 16013 | Extend class notation to include the cosine function. |
class cos | ||
Syntax | ctan 16014 | Extend class notation to include the tangent function. |
class tan | ||
Syntax | cpi 16015 | Extend class notation to include the constant pi, Ο = 3.14159.... |
class Ο | ||
Definition | df-ef 16016* | Define the exponential function. Its value at the complex number π΄ is (expβπ΄) and is called the "exponential of π΄"; see efval 16028. (Contributed by NM, 14-Mar-2005.) |
β’ exp = (π₯ β β β¦ Ξ£π β β0 ((π₯βπ) / (!βπ))) | ||
Definition | df-e 16017 | Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.) |
β’ e = (expβ1) | ||
Definition | df-sin 16018 | Define the sine function. (Contributed by NM, 14-Mar-2005.) |
β’ sin = (π₯ β β β¦ (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β· i))) | ||
Definition | df-cos 16019 | Define the cosine function. (Contributed by NM, 14-Mar-2005.) |
β’ cos = (π₯ β β β¦ (((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) / 2)) | ||
Definition | df-tan 16020 | Define the tangent function. We define it this way for cmpt 5231, which requires the form (π₯ β π΄ β¦ π΅). (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ tan = (π₯ β (β‘cos β (β β {0})) β¦ ((sinβπ₯) / (cosβπ₯))) | ||
Definition | df-pi 16021 | Define the constant pi, Ο = 3.14159..., which is the smallest positive number whose sine is zero. Definition of Ο in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.) |
β’ Ο = inf((β+ β© (β‘sin β {0})), β, < ) | ||
Theorem | eftcl 16022 | Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.) |
β’ ((π΄ β β β§ πΎ β β0) β ((π΄βπΎ) / (!βπΎ)) β β) | ||
Theorem | reeftcl 16023 | The terms of the series expansion of the exponential function at a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.) |
β’ ((π΄ β β β§ πΎ β β0) β ((π΄βπΎ) / (!βπΎ)) β β) | ||
Theorem | eftabs 16024 | The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.) |
β’ ((π΄ β β β§ πΎ β β0) β (absβ((π΄βπΎ) / (!βπΎ))) = (((absβπ΄)βπΎ) / (!βπΎ))) | ||
Theorem | eftval 16025* | The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π β β0 β (πΉβπ) = ((π΄βπ) / (!βπ))) | ||
Theorem | efcllem 16026* | Lemma for efcl 16031. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15834 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) (Proof shortened by AV, 9-Jul-2022.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β seq0( + , πΉ) β dom β ) | ||
Theorem | ef0lem 16027* | The series defining the exponential function converges in the (trivial) case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ = 0 β seq0( + , πΉ) β 1) | ||
Theorem | efval 16028* | Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 ((π΄βπ) / (!βπ))) | ||
Theorem | esum 16029 | Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.) |
β’ e = Ξ£π β β0 (1 / (!βπ)) | ||
Theorem | eff 16030 | Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) |
β’ exp:ββΆβ | ||
Theorem | efcl 16031 | Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) β β) | ||
Theorem | efval2 16032* | Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 (πΉβπ)) | ||
Theorem | efcvg 16033* | The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β seq0( + , πΉ) β (expβπ΄)) | ||
Theorem | efcvgfsum 16034* | Exponential function convergence in terms of a sequence of partial finite sums. (Contributed by NM, 10-Jan-2006.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ πΉ = (π β β0 β¦ Ξ£π β (0...π)((π΄βπ) / (!βπ))) β β’ (π΄ β β β πΉ β (expβπ΄)) | ||
Theorem | reefcl 16035 | The exponential function is real if its argument is real. (Contributed by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ (π΄ β β β (expβπ΄) β β) | ||
Theorem | reefcld 16036 | The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (expβπ΄) β β) | ||
Theorem | ere 16037 | Euler's constant e = 2.71828... is a real number. (Contributed by NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.) |
β’ e β β | ||
Theorem | ege2le3 16038 | Lemma for egt2lt3 16154. (Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) |
β’ πΉ = (π β β β¦ (2 Β· ((1 / 2)βπ))) & β’ πΊ = (π β β0 β¦ (1 / (!βπ))) β β’ (2 β€ e β§ e β€ 3) | ||
Theorem | ef0 16039 | Value of the exponential function at 0. Equation 2 of [Gleason] p. 308. (Contributed by Steve Rodriguez, 27-Jun-2006.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ (expβ0) = 1 | ||
Theorem | efcj 16040 | The exponential of a complex conjugate. Equation 3 of [Gleason] p. 308. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ (π΄ β β β (expβ(ββπ΄)) = (ββ(expβπ΄))) | ||
Theorem | efaddlem 16041* | Lemma for efadd 16042 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ πΊ = (π β β0 β¦ ((π΅βπ) / (!βπ))) & β’ π» = (π β β0 β¦ (((π΄ + π΅)βπ) / (!βπ))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (expβ(π΄ + π΅)) = ((expβπ΄) Β· (expβπ΅))) | ||
Theorem | efadd 16042 | Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (expβ(π΄ + π΅)) = ((expβπ΄) Β· (expβπ΅))) | ||
Theorem | fprodefsum 16043* | Move the exponential function from inside a finite product to outside a finite sum. (Contributed by Scott Fenton, 26-Dec-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β π΄ β β) β β’ (π β βπ β (π...π)(expβπ΄) = (expβΞ£π β (π...π)π΄)) | ||
Theorem | efcan 16044 | Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.) |
β’ (π΄ β β β ((expβπ΄) Β· (expβ-π΄)) = 1) | ||
Theorem | efne0 16045 | The exponential of a complex number is nonzero. Corollary 15-4.3 of [Gleason] p. 309. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ (π΄ β β β (expβπ΄) β 0) | ||
Theorem | efneg 16046 | The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.) |
β’ (π΄ β β β (expβ-π΄) = (1 / (expβπ΄))) | ||
Theorem | eff2 16047 | The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) |
β’ exp:ββΆ(β β {0}) | ||
Theorem | efsub 16048 | Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (expβ(π΄ β π΅)) = ((expβπ΄) / (expβπ΅))) | ||
Theorem | efexp 16049 | The exponential of an integer power. Corollary 15-4.4 of [Gleason] p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ ((π΄ β β β§ π β β€) β (expβ(π Β· π΄)) = ((expβπ΄)βπ)) | ||
Theorem | efzval 16050 | Value of the exponential function for integers. Special case of efval 16028. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ (π β β€ β (expβπ) = (eβπ)) | ||
Theorem | efgt0 16051 | The exponential of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β 0 < (expβπ΄)) | ||
Theorem | rpefcl 16052 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) β β+) | ||
Theorem | rpefcld 16053 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (expβπ΄) β β+) | ||
Theorem | eftlcvg 16054* | The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ ((π΄ β β β§ π β β0) β seqπ( + , πΉ) β dom β ) | ||
Theorem | eftlcl 16055* | Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ ((π΄ β β β§ π β β0) β Ξ£π β (β€β₯βπ)(πΉβπ) β β) | ||
Theorem | reeftlcl 16056* | Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ ((π΄ β β β§ π β β0) β Ξ£π β (β€β₯βπ)(πΉβπ) β β) | ||
Theorem | eftlub 16057* | An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ πΊ = (π β β0 β¦ (((absβπ΄)βπ) / (!βπ))) & β’ π» = (π β β0 β¦ ((((absβπ΄)βπ) / (!βπ)) Β· ((1 / (π + 1))βπ))) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (absβπ΄) β€ 1) β β’ (π β (absβΞ£π β (β€β₯βπ)(πΉβπ)) β€ (((absβπ΄)βπ) Β· ((π + 1) / ((!βπ) Β· π)))) | ||
Theorem | efsep 16058* | Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ π = (π + 1) & β’ π β β0 & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (expβπ΄) = (π΅ + Ξ£π β (β€β₯βπ)(πΉβπ))) & β’ (π β (π΅ + ((π΄βπ) / (!βπ))) = π·) β β’ (π β (expβπ΄) = (π· + Ξ£π β (β€β₯βπ)(πΉβπ))) | ||
Theorem | effsumlt 16059* | The partial sums of the series expansion of the exponential function at a positive real number are bounded by the value of the function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ (π β π΄ β β+) & β’ (π β π β β0) β β’ (π β (seq0( + , πΉ)βπ) < (expβπ΄)) | ||
Theorem | eft0val 16060 | The value of the first term of the series expansion of the exponential function is 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ (π΄ β β β ((π΄β0) / (!β0)) = 1) | ||
Theorem | ef4p 16061* | Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β (expβπ΄) = ((((1 + π΄) + ((π΄β2) / 2)) + ((π΄β3) / 6)) + Ξ£π β (β€β₯β4)(πΉβπ))) | ||
Theorem | efgt1p2 16062 | The exponential of a positive real number is greater than the sum of the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (π΄ β β+ β ((1 + π΄) + ((π΄β2) / 2)) < (expβπ΄)) | ||
Theorem | efgt1p 16063 | The exponential of a positive real number is greater than 1 plus that number. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β+ β (1 + π΄) < (expβπ΄)) | ||
Theorem | efgt1 16064 | The exponential of a positive real number is greater than 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β+ β 1 < (expβπ΄)) | ||
Theorem | eflt 16065 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 17-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β (expβπ΄) < (expβπ΅))) | ||
Theorem | efle 16066 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β€ π΅ β (expβπ΄) β€ (expβπ΅))) | ||
Theorem | reef11 16067 | The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Mario Carneiro, 11-Mar-2014.) |
β’ ((π΄ β β β§ π΅ β β) β ((expβπ΄) = (expβπ΅) β π΄ = π΅)) | ||
Theorem | reeff1 16068 | The exponential function maps real arguments one-to-one to positive reals. (Contributed by Steve Rodriguez, 25-Aug-2007.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (exp βΎ β):ββ1-1ββ+ | ||
Theorem | eflegeo 16069 | The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΄ < 1) β β’ (π β (expβπ΄) β€ (1 / (1 β π΄))) | ||
Theorem | sinval 16070 | Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (sinβπ΄) = (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i))) | ||
Theorem | cosval 16071 | Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (cosβπ΄) = (((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2)) | ||
Theorem | sinf 16072 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ sin:ββΆβ | ||
Theorem | cosf 16073 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ cos:ββΆβ | ||
Theorem | sincl 16074 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | coscl 16075 | Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | tanval 16076 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) = ((sinβπ΄) / (cosβπ΄))) | ||
Theorem | tancl 16077 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | sincld 16078 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | coscld 16079 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | tancld 16080 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | tanval2 16081 | Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) = (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (i Β· ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) | ||
Theorem | tanval3 16082 | Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ ((expβ(2 Β· (i Β· π΄))) + 1) β 0) β (tanβπ΄) = (((expβ(2 Β· (i Β· π΄))) β 1) / (i Β· ((expβ(2 Β· (i Β· π΄))) + 1)))) | ||
Theorem | resinval 16083 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | recosval 16084 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | efi4p 16085* | Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β β β (expβ(i Β· π΄)) = (((1 β ((π΄β2) / 2)) + (i Β· (π΄ β ((π΄β3) / 6)))) + Ξ£π β (β€β₯β4)(πΉβπ))) | ||
Theorem | resin4p 16086* | Separate out the first four terms of the infinite series expansion of the sine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β β β (sinβπ΄) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β (β€β₯β4)(πΉβπ)))) | ||
Theorem | recos4p 16087* | Separate out the first four terms of the infinite series expansion of the cosine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β β β (cosβπ΄) = ((1 β ((π΄β2) / 2)) + (ββΞ£π β (β€β₯β4)(πΉβπ)))) | ||
Theorem | resincl 16088 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | recoscl 16089 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | retancl 16090 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | resincld 16091 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | recoscld 16092 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | retancld 16093 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | sinneg 16094 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβ-π΄) = -(sinβπ΄)) | ||
Theorem | cosneg 16095 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβ-π΄) = (cosβπ΄)) | ||
Theorem | tanneg 16096 | The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβ-π΄) = -(tanβπ΄)) | ||
Theorem | sin0 16097 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
β’ (sinβ0) = 0 | ||
Theorem | cos0 16098 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
β’ (cosβ0) = 1 | ||
Theorem | tan0 16099 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
β’ (tanβ0) = 0 | ||
Theorem | efival 16100 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |