Home | Metamath
Proof Explorer Theorem List (p. 160 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efcvg 15901* | 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 15902* | 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 15903 | 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 15904 | The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (expβπ΄) β β) | ||
Theorem | ere 15905 | 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 15906 | Lemma for egt2lt3 16022. (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 15907 | 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 15908 | 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 15909* | Lemma for efadd 15910 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) & β’ πΊ = (π β β0 β¦ ((π΅βπ) / (!βπ))) & β’ π» = (π β β0 β¦ (((π΄ + π΅)βπ) / (!βπ))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (expβ(π΄ + π΅)) = ((expβπ΄) Β· (expβπ΅))) | ||
Theorem | efadd 15910 | 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 15911* | 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 15912 | Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.) |
β’ (π΄ β β β ((expβπ΄) Β· (expβ-π΄)) = 1) | ||
Theorem | efne0 15913 | 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 15914 | The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.) |
β’ (π΄ β β β (expβ-π΄) = (1 / (expβπ΄))) | ||
Theorem | eff2 15915 | The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) |
β’ exp:ββΆ(β β {0}) | ||
Theorem | efsub 15916 | Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (expβ(π΄ β π΅)) = ((expβπ΄) / (expβπ΅))) | ||
Theorem | efexp 15917 | 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 15918 | Value of the exponential function for integers. Special case of efval 15896. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ (π β β€ β (expβπ) = (eβπ)) | ||
Theorem | efgt0 15919 | 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 15920 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (expβπ΄) β β+) | ||
Theorem | rpefcld 15921 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (expβπ΄) β β+) | ||
Theorem | eftlcvg 15922* | The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ ((π΄ β β β§ π β β0) β seqπ( + , πΉ) β dom β ) | ||
Theorem | eftlcl 15923* | 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 15924* | 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 15925* | 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 15926* | 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 15927* | 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 15928 | 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 15929* | 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 15930 | 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 15931 | 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 15932 | 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 15933 | 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 15934 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β€ π΅ β (expβπ΄) β€ (expβπ΅))) | ||
Theorem | reef11 15935 | 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 15936 | 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 15937 | 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 15938 | 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 15939 | 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 15940 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ sin:ββΆβ | ||
Theorem | cosf 15941 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ cos:ββΆβ | ||
Theorem | sincl 15942 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | coscl 15943 | 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 15944 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) = ((sinβπ΄) / (cosβπ΄))) | ||
Theorem | tancl 15945 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | sincld 15946 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | coscld 15947 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | tancld 15948 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | tanval2 15949 | 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 15950 | 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 15951 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | recosval 15952 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | efi4p 15953* | 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 15954* | 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 15955* | 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 15956 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | recoscl 15957 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | retancl 15958 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | resincld 15959 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | recoscld 15960 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | retancld 15961 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | sinneg 15962 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβ-π΄) = -(sinβπ΄)) | ||
Theorem | cosneg 15963 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβ-π΄) = (cosβπ΄)) | ||
Theorem | tanneg 15964 | 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 15965 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
β’ (sinβ0) = 0 | ||
Theorem | cos0 15966 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
β’ (cosβ0) = 1 | ||
Theorem | tan0 15967 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
β’ (tanβ0) = 0 | ||
Theorem | efival 15968 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) | ||
Theorem | efmival 15969 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
β’ (π΄ β β β (expβ(-i Β· π΄)) = ((cosβπ΄) β (i Β· (sinβπ΄)))) | ||
Theorem | sinhval 15970 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((sinβ(i Β· π΄)) / i) = (((expβπ΄) β (expβ-π΄)) / 2)) | ||
Theorem | coshval 15971 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) = (((expβπ΄) + (expβ-π΄)) / 2)) | ||
Theorem | resinhcl 15972 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((sinβ(i Β· π΄)) / i) β β) | ||
Theorem | rpcoshcl 15973 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) β β+) | ||
Theorem | recoshcl 15974 | The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) β β) | ||
Theorem | retanhcl 15975 | The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((tanβ(i Β· π΄)) / i) β β) | ||
Theorem | tanhlt1 15976 | The hyperbolic tangent of a real number is upper bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((tanβ(i Β· π΄)) / i) < 1) | ||
Theorem | tanhbnd 15977 | The hyperbolic tangent of a real number is bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((tanβ(i Β· π΄)) / i) β (-1(,)1)) | ||
Theorem | efeul 15978 | Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.) |
β’ (π΄ β β β (expβπ΄) = ((expβ(ββπ΄)) Β· ((cosβ(ββπ΄)) + (i Β· (sinβ(ββπ΄)))))) | ||
Theorem | efieq 15979 | The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β ((expβ(i Β· π΄)) = (expβ(i Β· π΅)) β ((cosβπ΄) = (cosβπ΅) β§ (sinβπ΄) = (sinβπ΅)))) | ||
Theorem | sinadd 15980 | Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (sinβ(π΄ + π΅)) = (((sinβπ΄) Β· (cosβπ΅)) + ((cosβπ΄) Β· (sinβπ΅)))) | ||
Theorem | cosadd 15981 | Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (cosβ(π΄ + π΅)) = (((cosβπ΄) Β· (cosβπ΅)) β ((sinβπ΄) Β· (sinβπ΅)))) | ||
Theorem | tanaddlem 15982 | A useful intermediate step in tanadd 15983 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (((π΄ β β β§ π΅ β β) β§ ((cosβπ΄) β 0 β§ (cosβπ΅) β 0)) β ((cosβ(π΄ + π΅)) β 0 β ((tanβπ΄) Β· (tanβπ΅)) β 1)) | ||
Theorem | tanadd 15983 | Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (((π΄ β β β§ π΅ β β) β§ ((cosβπ΄) β 0 β§ (cosβπ΅) β 0 β§ (cosβ(π΄ + π΅)) β 0)) β (tanβ(π΄ + π΅)) = (((tanβπ΄) + (tanβπ΅)) / (1 β ((tanβπ΄) Β· (tanβπ΅))))) | ||
Theorem | sinsub 15984 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (sinβ(π΄ β π΅)) = (((sinβπ΄) Β· (cosβπ΅)) β ((cosβπ΄) Β· (sinβπ΅)))) | ||
Theorem | cossub 15985 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (cosβ(π΄ β π΅)) = (((cosβπ΄) Β· (cosβπ΅)) + ((sinβπ΄) Β· (sinβπ΅)))) | ||
Theorem | addsin 15986 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) + (sinβπ΅)) = (2 Β· ((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) | ||
Theorem | subsin 15987 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) β (sinβπ΅)) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) | ||
Theorem | sinmul 15988 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 15981 and cossub 15985. (Contributed by David A. Wheeler, 26-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (sinβπ΅)) = (((cosβ(π΄ β π΅)) β (cosβ(π΄ + π΅))) / 2)) | ||
Theorem | cosmul 15989 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 15981 and cossub 15985. (Contributed by David A. Wheeler, 26-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΄) Β· (cosβπ΅)) = (((cosβ(π΄ β π΅)) + (cosβ(π΄ + π΅))) / 2)) | ||
Theorem | addcos 15990 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΄) + (cosβπ΅)) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) | ||
Theorem | subcos 15991 | Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΅) β (cosβπ΄)) = (2 Β· ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) | ||
Theorem | sincossq 15992 | Sine squared plus cosine squared is 1. Equation 17 of [Gleason] p. 311. Note that this holds for non-real arguments, even though individually each term is unbounded. (Contributed by NM, 15-Jan-2006.) |
β’ (π΄ β β β (((sinβπ΄)β2) + ((cosβπ΄)β2)) = 1) | ||
Theorem | sin2t 15993 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
β’ (π΄ β β β (sinβ(2 Β· π΄)) = (2 Β· ((sinβπ΄) Β· (cosβπ΄)))) | ||
Theorem | cos2t 15994 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ(2 Β· π΄)) = ((2 Β· ((cosβπ΄)β2)) β 1)) | ||
Theorem | cos2tsin 15995 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
β’ (π΄ β β β (cosβ(2 Β· π΄)) = (1 β (2 Β· ((sinβπ΄)β2)))) | ||
Theorem | sinbnd 15996 | The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
β’ (π΄ β β β (-1 β€ (sinβπ΄) β§ (sinβπ΄) β€ 1)) | ||
Theorem | cosbnd 15997 | The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
β’ (π΄ β β β (-1 β€ (cosβπ΄) β§ (cosβπ΄) β€ 1)) | ||
Theorem | sinbnd2 15998 | The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
β’ (π΄ β β β (sinβπ΄) β (-1[,]1)) | ||
Theorem | cosbnd2 15999 | The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
β’ (π΄ β β β (cosβπ΄) β (-1[,]1)) | ||
Theorem | ef01bndlem 16000* | Lemma for sin01bnd 16001 and cos01bnd 16002. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β (0(,]1) β (absβΞ£π β (β€β₯β4)(πΉβπ)) < ((π΄β4) / 6)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |