![]() |
Metamath
Proof Explorer Theorem List (p. 161 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 | bpoly2 16001 | The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.) |
β’ (π β β β (2 BernPoly π) = (((πβ2) β π) + (1 / 6))) | ||
Theorem | bpoly3 16002 | The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.) |
β’ (π β β β (3 BernPoly π) = (((πβ3) β ((3 / 2) Β· (πβ2))) + ((1 / 2) Β· π))) | ||
Theorem | bpoly4 16003 | The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.) |
β’ (π β β β (4 BernPoly π) = ((((πβ4) β (2 Β· (πβ3))) + (πβ2)) β (1 / ;30))) | ||
Theorem | fsumcube 16004* | Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.) |
β’ (π β β0 β Ξ£π β (0...π)(πβ3) = (((πβ2) Β· ((π + 1)β2)) / 4)) | ||
Syntax | ce 16005 | Extend class notation to include the exponential function. |
class exp | ||
Syntax | ceu 16006 | Extend class notation to include Euler's constant e = 2.71828.... |
class e | ||
Syntax | csin 16007 | Extend class notation to include the sine function. |
class sin | ||
Syntax | ccos 16008 | Extend class notation to include the cosine function. |
class cos | ||
Syntax | ctan 16009 | Extend class notation to include the tangent function. |
class tan | ||
Syntax | cpi 16010 | Extend class notation to include the constant pi, Ο = 3.14159.... |
class Ο | ||
Definition | df-ef 16011* | Define the exponential function. Its value at the complex number π΄ is (expβπ΄) and is called the "exponential of π΄"; see efval 16023. (Contributed by NM, 14-Mar-2005.) |
β’ exp = (π₯ β β β¦ Ξ£π β β0 ((π₯βπ) / (!βπ))) | ||
Definition | df-e 16012 | Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.) |
β’ e = (expβ1) | ||
Definition | df-sin 16013 | Define the sine function. (Contributed by NM, 14-Mar-2005.) |
β’ sin = (π₯ β β β¦ (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β· i))) | ||
Definition | df-cos 16014 | Define the cosine function. (Contributed by NM, 14-Mar-2005.) |
β’ cos = (π₯ β β β¦ (((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) / 2)) | ||
Definition | df-tan 16015 | Define the tangent function. We define it this way for cmpt 5232, which requires the form (π₯ β π΄ β¦ π΅). (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ tan = (π₯ β (β‘cos β (β β {0})) β¦ ((sinβπ₯) / (cosβπ₯))) | ||
Definition | df-pi 16016 | 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 16017 | Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.) |
β’ ((π΄ β β β§ πΎ β β0) β ((π΄βπΎ) / (!βπΎ)) β β) | ||
Theorem | reeftcl 16018 | 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 16019 | 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 16020* | 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 16021* | Lemma for efcl 16026. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15829 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 16022* | 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 16023* | Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 ((π΄βπ) / (!βπ))) | ||
Theorem | esum 16024 | Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.) |
β’ e = Ξ£π β β0 (1 / (!βπ)) | ||
Theorem | eff 16025 | 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 16026 | Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) β β) | ||
Theorem | efval2 16027* | Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β (expβπ΄) = Ξ£π β β0 (πΉβπ)) | ||
Theorem | efcvg 16028* | 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 16029* | 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 16030 | 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 16031 | The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (expβπ΄) β β) | ||
Theorem | ere 16032 | 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 16033 | Lemma for egt2lt3 16149. (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 16034 | 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 16035 | 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 16036* | Lemma for efadd 16037 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ πΊ = (π β β0 β¦ ((π΅βπ) / (!βπ))) & β’ π» = (π β β0 β¦ (((π΄ + π΅)βπ) / (!βπ))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (expβ(π΄ + π΅)) = ((expβπ΄) Β· (expβπ΅))) | ||
Theorem | efadd 16037 | 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 16038* | 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 16039 | Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.) |
β’ (π΄ β β β ((expβπ΄) Β· (expβ-π΄)) = 1) | ||
Theorem | efne0 16040 | 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 16041 | The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.) |
β’ (π΄ β β β (expβ-π΄) = (1 / (expβπ΄))) | ||
Theorem | eff2 16042 | The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) |
β’ exp:ββΆ(β β {0}) | ||
Theorem | efsub 16043 | Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (expβ(π΄ β π΅)) = ((expβπ΄) / (expβπ΅))) | ||
Theorem | efexp 16044 | 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 16045 | Value of the exponential function for integers. Special case of efval 16023. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ (π β β€ β (expβπ) = (eβπ)) | ||
Theorem | efgt0 16046 | 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 16047 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) β β+) | ||
Theorem | rpefcld 16048 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (expβπ΄) β β+) | ||
Theorem | eftlcvg 16049* | The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ ((π΄ β β β§ π β β0) β seqπ( + , πΉ) β dom β ) | ||
Theorem | eftlcl 16050* | 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 16051* | 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 16052* | 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 16053* | 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 16054* | 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 16055 | 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 16056* | 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 16057 | 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 16058 | 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 16059 | 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 16060 | 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 16061 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β€ π΅ β (expβπ΄) β€ (expβπ΅))) | ||
Theorem | reef11 16062 | 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 16063 | 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 16064 | 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 16065 | 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 16066 | 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 16067 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ sin:ββΆβ | ||
Theorem | cosf 16068 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ cos:ββΆβ | ||
Theorem | sincl 16069 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | coscl 16070 | 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 16071 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) = ((sinβπ΄) / (cosβπ΄))) | ||
Theorem | tancl 16072 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | sincld 16073 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | coscld 16074 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | tancld 16075 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | tanval2 16076 | 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 16077 | 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 16078 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | recosval 16079 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | efi4p 16080* | 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 16081* | 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 16082* | 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 16083 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | recoscl 16084 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | retancl 16085 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | resincld 16086 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | recoscld 16087 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | retancld 16088 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | sinneg 16089 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβ-π΄) = -(sinβπ΄)) | ||
Theorem | cosneg 16090 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβ-π΄) = (cosβπ΄)) | ||
Theorem | tanneg 16091 | 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 16092 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
β’ (sinβ0) = 0 | ||
Theorem | cos0 16093 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
β’ (cosβ0) = 1 | ||
Theorem | tan0 16094 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
β’ (tanβ0) = 0 | ||
Theorem | efival 16095 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) | ||
Theorem | efmival 16096 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
β’ (π΄ β β β (expβ(-i Β· π΄)) = ((cosβπ΄) β (i Β· (sinβπ΄)))) | ||
Theorem | sinhval 16097 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((sinβ(i Β· π΄)) / i) = (((expβπ΄) β (expβ-π΄)) / 2)) | ||
Theorem | coshval 16098 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) = (((expβπ΄) + (expβ-π΄)) / 2)) | ||
Theorem | resinhcl 16099 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((sinβ(i Β· π΄)) / i) β β) | ||
Theorem | rpcoshcl 16100 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) β β+) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |