HomeTheorem List (p. 138 of 368)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 138 of 368) | < 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-25499) |
Hilbert Space Explorer
(25500-27024) |
Users' Mathboxes
(27025-36800) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | efgt1p2 13701 | 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.) |
           
  | ||
| Theorem | efgt1p 13702 | 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.) |
| | ||
| Theorem | efgt1 13703 | 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.) |
|
| ||
| Theorem | eflt 13704 | The exponential function on the reals is strictly monotonic. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 17-Jul-2014.) |
 ![/\](wedge.gif "/\"){kind=small}   | ||
| Theorem | efle 13705 | The exponential function on the reals is strictly monotonic. (Contributed by Mario Carneiro, 11-Mar-2014.) |
 | ||
| Theorem | reef11 13706 | The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Mario Carneiro, 11-Mar-2014.) |
 | ||
| Theorem | reeff1 13707 | 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.) |
   | ||
| Theorem | eflegeo 13708 | The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.) |
     | ||
| Theorem | sinval 13709 | Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
 
   | ||
| Theorem | cosval 13710 | Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
| ||
| Theorem | sinf 13711 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
 | ||
| Theorem | cosf 13712 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| | ||
| Theorem | sincl 13713 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | coscl 13714 | Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | tanval 13715 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) |
  | ||
| Theorem | tancl 13716 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
| | ||
| Theorem | sincld 13717 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| | ||
| Theorem | coscld 13718 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| | ||
| Theorem | tancld 13719 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
| | ||
| Theorem | tanval2 13720 |
Express the tangent function directly in terms of . (Contributed
by Mario Carneiro, 25-Feb-2015.)
|
|
| ||
| Theorem | tanval3 13721 |
Express the tangent function directly in terms of . (Contributed
by Mario Carneiro, 25-Feb-2015.)
|
| | ||
| Theorem | resinval 13722 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
 | ||
| Theorem | recosval 13723 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
 | ||
| Theorem | efi4p 13724* | 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.) |
  
 
     | ||
| Theorem | resin4p 13725* | 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.) |
|
| ||
| Theorem | recos4p 13726* | 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.) |
|
| ||
| Theorem | resincl 13727 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | recoscl 13728 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | retancl 13729 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
| | ||
| Theorem | resincld 13730 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| | ||
| Theorem | recoscld 13731 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| | ||
| Theorem | retancld 13732 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
| | ||
| Theorem | sinneg 13733 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | cosneg 13734 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
|
| ||
| Theorem | tanneg 13735 | The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.) |
| | ||
| Theorem | sin0 13736 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
| | ||
| Theorem | cos0 13737 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
| | ||
| Theorem | tan0 13738 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
| | ||
| Theorem | efival 13739 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
| | ||
| Theorem | efmival 13740 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
| | ||
| Theorem | sinhval 13741 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| | ||
| Theorem | coshval 13742 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
|
| ||
| Theorem | resinhcl 13743 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| | ||
| Theorem | rpcoshcl 13744 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| | ||
| Theorem | recoshcl 13745 | The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| | ||
| Theorem | retanhcl 13746 | The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| | ||
| Theorem | tanhlt1 13747 |
The hyperbolic tangent of a real number is upper bounded by .
(Contributed by Mario Carneiro, 4-Apr-2015.)
|
| | ||
| Theorem | tanhbnd 13748 |
The hyperbolic tangent of a real number is bounded by .
(Contributed by Mario Carneiro, 4-Apr-2015.)
|
 | ||
| Theorem | efeul 13749 | Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.) |
|
| ||
| Theorem | efieq 13750 | The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.) |
|
| ||
| Theorem | sinadd 13751 | Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | cosadd 13752 | Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | tanaddlem 13753 | A useful intermediate step in tanadd 13754 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) |
|
| ||
| Theorem | tanadd 13754 | Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.) |
|
| ||
| Theorem | sinsub 13755 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
|
| ||
| Theorem | cossub 13756 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
|
| ||
| Theorem | addsin 13757 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
| | ||
| Theorem | subsin 13758 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
| | ||
| Theorem | sinmul 13759 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 13752 and cossub 13756. (Contributed by David A. Wheeler, 26-May-2015.) |
| | ||
| Theorem | cosmul 13760 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 13752 and cossub 13756. (Contributed by David A. Wheeler, 26-May-2015.) |
| | ||
| Theorem | addcos 13761 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
| | ||
| Theorem | subcos 13762 | Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.) |
| | ||
| Theorem | sincossq 13763 | 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.) |
| | ||
| Theorem | sin2t 13764 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
| | ||
| Theorem | cos2t 13765 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
| | ||
| Theorem | cos2tsin 13766 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
| | ||
| Theorem | sinbnd 13767 | The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
| | ||
| Theorem | cosbnd 13768 | The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
| | ||
| Theorem | sinbnd2 13769 | The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
![[,]](_icc.gif "[,]"){kind=small} | ||
| Theorem | cosbnd2 13770 | The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
|
| ||
| Theorem | ef01bndlem 13771* | Lemma for sin01bnd 13772 and cos01bnd 13773. (Contributed by Paul Chapman, 19-Jan-2008.) |
![(,]](_ioc.gif "(,]"){kind=small} 
| ||
| Theorem | sin01bnd 13772 | Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| | ||
| Theorem | cos01bnd 13773 | Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | cos1bnd 13774 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
| | ||
| Theorem | cos2bnd 13775 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
  | ||
| Theorem | sinltx 13776 | The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014.) |
| | ||
| Theorem | sin01gt0 13777 | The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
|
| ||
| Theorem | cos01gt0 13778 | The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
|
| ||
| Theorem | sin02gt0 13779 | The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
|
| ||
| Theorem | sincos1sgn 13780 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
| | ||
| Theorem | sincos2sgn 13781 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
| | ||
| Theorem | sin4lt0 13782 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
|
| ||
| Theorem | absefi 13783 | The absolute value of the exponential function of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.) |
| | ||
| Theorem | absef 13784 | The absolute value of the exponential function is the exponential function of the real part. (Contributed by Paul Chapman, 13-Sep-2007.) |
| | ||
| Theorem | absefib 13785 | A number is real iff its imaginary exponential has absolute value one. (Contributed by NM, 21-Aug-2008.) |
| | ||
| Theorem | efieq1re 13786 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
|
| ||
| Theorem | demoivre 13787 | De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 13788 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
 
| ||
| Theorem | demoivreALT 13788 | Alternate proof of demoivre 13787. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
|
| ||
| Theorem | eirrlem 13789* | Lemma for eirr 13790. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
     | ||
| Theorem | eirr 13790 |
is irrational.
(Contributed by Paul Chapman, 9-Feb-2008.)
(Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
  | ||
| Theorem | egt2lt3 13791 |
Euler's constant =
2.71828... is bounded by 2 and 3. (Contributed
by NM, 28-Nov-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
|
| ||
| Theorem | epos 13792 |
Euler's constant is
greater than 0. (Contributed by Jeff Hankins,
22-Nov-2008.)
|
| | ||
| Theorem | epr 13793 |
Euler's constant is
a positive real. (Contributed by Jeff Hankins,
22-Nov-2008.)
|
| | ||
| Theorem | xpnnen 13794 | The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
  | ||
| Theorem | xpnnenOLD 13795 |
The Cartesian product of the set of positive integers with itself is
equinumerous to the set of positive integers. The key idea is to use
nn0opth2 12309 to show that the mapping from positive
integers  and
 to is one-to-one. (Contributed by NM,
1-Aug-2004.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
| | ||
| Theorem | xpomenOLD 13796 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133 (which proves this with a direct, but longer, proof; ours uses instead the Schroeder-Bernstein Theorem sbth 7629 in xpnnen 13794). (Contributed by NM, 23-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
 | ||
| Theorem | znnenlem 13797 | Lemma for znnen 13798. (Contributed by NM, 31-Jul-2004.) |
| ||
| Theorem | znnen 13798 | The set of integers and the set of positive integers are equinumerous. Exercise 1 of [Gleason] p. 140. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.) |
|
| ||
| Theorem | qnnen 13799 |
The rational numbers are countable. This proof does not use the Axiom
of Choice, even though it uses an onto function, because the base set
is
numerable. Exercise 2 of [Enderton] p. 133.
For
purposes of the Metamath 100 list, we are considering Mario Carneiro's
revision as the date this proof was completed. This is Metamath 100
proof #3. (Contributed by NM, 31-Jul-2004.) (Revised by Mario
Carneiro, 3-Mar-2013.)
|
|
| ||
| Theorem | rpnnen2lem1 13800* | Lemma for rpnnen2 13811. (Contributed by Mario Carneiro, 13-May-2013.) |
  
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |