Home Metamath Proof ExplorerTheorem List (p. 128 of 329) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-22452) Hilbert Space Explorer (22453-23975) Users' Mathboxes (23976-32860)

Theorem List for Metamath Proof Explorer - 12701-12800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Definitiondf-ef 12701* Define the exponential function. (Contributed by NM, 14-Mar-2005.)

Definitiondf-e 12702 Define Euler's constant 2.71828.... (Contributed by NM, 14-Mar-2005.)

Definitiondf-sin 12703 Define the sine function. (Contributed by NM, 14-Mar-2005.)

Definitiondf-cos 12704 Define the cosine function. (Contributed by NM, 14-Mar-2005.)

Definitiondf-tan 12705 Define the tangent function. We define it this way for cmpt 4291, which requires the form . (Contributed by Mario Carneiro, 14-Mar-2014.)

Definitiondf-pi 12706 Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (We use the inverse of less-than, " ", to turn supremum into infimum; currently we don't have infimum defined separately.) (Contributed by Paul Chapman, 23-Jan-2008.)

Theoremeftcl 12707 Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)

Theoremreeftcl 12708 The terms of the series expansion of the exponential function of a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.)

Theoremeftabs 12709 The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.)

Theoremeftval 12710* 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.)

Theoremefcllem 12711* Lemma for efcl 12716. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 12691 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)

Theoremef0lem 12712* 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.)

Theoremefval 12713* Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)

Theoremesum 12714 Value of Euler's constant = 2.71828... (Contributed by Steve Rodriguez, 5-Mar-2006.)

Theoremeff 12715 Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)

Theoremefcl 12716 Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)

Theoremefval2 12717* Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)

Theoremefcvg 12718* The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro, 28-Apr-2014.)

Theoremefcvgfsum 12719* 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.)

Theoremreefcl 12720 The exponential function is real if its argument is real. (Contributed by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)

Theoremreefcld 12721 The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremere 12722 Euler's constant = 2.71828... is a real number. (Contributed by NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)

Theoremege2le3 12723 Lemma for egt2lt3 12836. (Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)

Theoremef0 12724 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.)

Theoremefcj 12725 Exponential function of a complex conjugate. Equation 3 of [Gleason] p. 308. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)

Theoremefadd 12727 Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)

Theoremefcan 12728 Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)

Theoremefne0 12729 The exponential function never vanishes. Corollary 15-4.3 of [Gleason] p. 309. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 29-Apr-2014.)

Theoremefneg 12730 Exponent of a negative number. (Contributed by Mario Carneiro, 10-May-2014.)

Theoremeff2 12731 The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)

Theoremefsub 12732 Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)

Theoremefexp 12733 Exponential function to 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.)

Theoremefzval 12734 Value of the exponential function for integers. Special case of efval 12713. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)

Theoremefgt0 12735 The exponential function of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremrpefcl 12736 The exponential function of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.)

Theoremrpefcld 12737 The exponential function of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremeftlcvg 12738* The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.)

Theoremeftlcl 12739* 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.)

Theoremreeftlcl 12740* 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.)

Theoremeftlub 12741* 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.)

Theoremefsep 12742* 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.)

Theoremeffsumlt 12743* The partial sums of the series expansion of the exponential function of 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.)

Theoremeft0val 12744 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.)

Theoremef4p 12745* 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.)

Theoremefgt1p2 12746 The exponential function of a positive real number is greater than the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014.)

Theoremefgt1p 12747 The exponential function 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.)

Theoremefgt1 12748 The exponential function of a positive real number is greater than 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremeflt 12749 The exponential function on the reals is strictly monotonic. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 17-Jul-2014.)

Theoremefle 12750 The exponential function on the reals is strictly monotonic. (Contributed by Mario Carneiro, 11-Mar-2014.)

Theoremreef11 12751 The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Mario Carneiro, 11-Mar-2014.)

Theoremreeff1 12752 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.)

Theoremeflegeo 12753 The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.)

Theoremsinval 12754 Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.)

Theoremcosval 12755 Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.)

Theoremsinf 12756 Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremcosf 12757 Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremsincl 12758 Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremcoscl 12759 Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremtanval 12760 Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.)

Theoremtancl 12761 The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.)

Theoremsincld 12762 Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremcoscld 12763 Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremtancld 12764 Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremtanval2 12765 Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.)

Theoremtanval3 12766 Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.)

Theoremresinval 12767 The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)

Theoremrecosval 12768 The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)

Theoremefi4p 12769* Separate out the first four terms of the infinite series expansion of the exponential function of an imaginary number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremresin4p 12770* 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.)

Theoremrecos4p 12771* 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.)

Theoremresincl 12772 The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)

Theoremrecoscl 12773 The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)

Theoremretancl 12774 The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)

Theoremresincld 12775 Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremrecoscld 12776 Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremretancld 12777 Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremsinneg 12778 The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)

Theoremcosneg 12779 The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)

Theoremtanneg 12780 The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.)

Theoremsin0 12781 Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)

Theoremcos0 12782 Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)

Theoremtan0 12783 The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)

Theoremefival 12784 The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)

Theoremefmival 12785 The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)

Theoremsinhval 12786 Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremcoshval 12787 Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremresinhcl 12788 The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremrpcoshcl 12789 The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremrecoshcl 12790 The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremretanhcl 12791 The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremtanhlt1 12792 The hyperbolic tangent of a real number is upper bounded by . (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremtanhbnd 12793 The hyperbolic tangent of a real number is bounded by . (Contributed by Mario Carneiro, 4-Apr-2015.)

Theoremefeul 12794 Eulerian representation of the complex exponential. (Suggested by Jeffrey Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)

Theoremefieq 12795 The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.)

Theoremsinadd 12796 Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremcosadd 12797 Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)

Theoremtanaddlem 12798 A useful intermediate step in tanadd 12799 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.)