Theorem List for Intuitionistic Logic Explorer - 11701-11800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | efval 11701* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
    
             |
|
Theorem | esum 11702 |
Value of Euler's constant = 2.71828.... (Contributed by Steve
Rodriguez, 5-Mar-2006.)
|
        |
|
Theorem | eff 11703 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
     |
|
Theorem | efcl 11704 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
    
  |
|
Theorem | efval2 11705* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|

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

           
  
      |
|
Theorem | efcvgfsum 11707* |
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.)
|

                        |
|
Theorem | reefcl 11708 |
The exponential function is real if its argument is real. (Contributed
by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
    
  |
|
Theorem | reefcld 11709 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | ere 11710 |
Euler's constant =
2.71828... is a real number. (Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
 |
|
Theorem | ege2le3 11711 |
Euler's constant =
2.71828... is bounded by 2 and 3.
(Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
         
        
  |
|
Theorem | ef0 11712 |
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.)
|
     |
|
Theorem | efcj 11713 |
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.)
|
                   |
|
Theorem | efaddlem 11714* |
Lemma for efadd 11715 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|

          
                                                 |
|
Theorem | efadd 11715 |
Sum of exponents law for exponential function. (Contributed by NM,
10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
      
              |
|
Theorem | efcan 11716 |
Cancellation law for exponential function. Equation 27 of [Rudin] p. 164.
(Contributed by NM, 13-Jan-2006.)
|
           
  |
|
Theorem | efap0 11717 |
The exponential of a complex number is apart from zero. (Contributed by
Jim Kingdon, 12-Dec-2022.)
|
     #   |
|
Theorem | efne0 11718 |
The exponential of a complex number is nonzero. Corollary 15-4.3 of
[Gleason] p. 309. The same result also
holds with not equal replaced by
apart, as seen at efap0 11717 (which will be more useful in most
contexts).
(Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
       |
|
Theorem | efneg 11719 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
     
        |
|
Theorem | eff2 11720 |
The exponential function maps the complex numbers to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
         |
|
Theorem | efsub 11721 |
Difference of exponents law for exponential function. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
                     |
|
Theorem | efexp 11722 |
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.)
|
                   |
|
Theorem | efzval 11723 |
Value of the exponential function for integers. Special case of efval 11701.
Equation 30 of [Rudin] p. 164. (Contributed
by Steve Rodriguez,
15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
    
      |
|
Theorem | efgt0 11724 |
The exponential of a real number is greater than 0. (Contributed by Paul
Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
       |
|
Theorem | rpefcl 11725 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 10-Nov-2013.)
|
    
  |
|
Theorem | rpefcld 11726 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | eftlcvg 11727* |
The tail series of the exponential function are convergent.
(Contributed by Mario Carneiro, 29-Apr-2014.)
|

                  |
|
Theorem | eftlcl 11728* |
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.)
|

                          |
|
Theorem | reeftlcl 11729* |
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.)
|

                          |
|
Theorem | eftlub 11730* |
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.)
|

          
                                                                  
                      |
|
Theorem | efsep 11731* |
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.)
|

          
          
                                              |
|
Theorem | effsumlt 11732* |
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.)
|

           
                |
|
Theorem | eft0val 11733 |
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.)
|
             |
|
Theorem | ef4p 11734* |
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.)
|

           
   
         
                      |
|
Theorem | efgt1p2 11735 |
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.)
|
        
 
      |
|
Theorem | efgt1p 11736 |
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.)
|
         |
|
Theorem | efgt1 11737 |
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.)
|

      |
|
Theorem | efltim 11738 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
20-Dec-2022.)
|
               |
|
Theorem | reef11 11739 |
The exponential function on real numbers is one-to-one. (Contributed by
NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.)
|
               |
|
Theorem | reeff1 11740 |
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 11741 |
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 11742 |
Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised
by Mario Carneiro, 10-Nov-2013.)
|
    
                     |
|
Theorem | cosval 11743 |
Value of the cosine function. (Contributed by NM, 14-Mar-2005.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
    
                   |
|
Theorem | sinf 11744 |
Domain and codomain of the sine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
     |
|
Theorem | cosf 11745 |
Domain and codomain of the cosine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
     |
|
Theorem | sincl 11746 |
Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised
by Mario Carneiro, 30-Apr-2014.)
|
    
  |
|
Theorem | coscl 11747 |
Closure of the cosine function with a complex argument. (Contributed by
NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
    
  |
|
Theorem | tanvalap 11748 |
Value of the tangent function. (Contributed by Mario Carneiro,
14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.)
|
      #                  |
|
Theorem | tanclap 11749 |
The closure of the tangent function with a complex argument. (Contributed
by David A. Wheeler, 15-Mar-2014.) (Revised by Jim Kingdon,
21-Dec-2022.)
|
      #        |
|
Theorem | sincld 11750 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | coscld 11751 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | tanclapd 11752 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
|
       #         |
|
Theorem | tanval2ap 11753 |
Express the tangent function directly in terms of . (Contributed
by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon,
22-Dec-2022.)
|
      #             
                            |
|
Theorem | tanval3ap 11754 |
Express the tangent function directly in terms of . (Contributed
by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon,
22-Dec-2022.)
|
            #                                |
|
Theorem | resinval 11755 |
The sine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
    
            |
|
Theorem | recosval 11756 |
The cosine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
    
            |
|
Theorem | efi4p 11757* |
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.)
|

                               
    
                 |
|
Theorem | resin4p 11758* |
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 11759* |
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 11760 |
The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
    
  |
|
Theorem | recoscl 11761 |
The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
    
  |
|
Theorem | retanclap 11762 |
The closure of the tangent function with a real argument. (Contributed by
David A. Wheeler, 15-Mar-2014.)
|
      #        |
|
Theorem | resincld 11763 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | recoscld 11764 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | retanclapd 11765 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.)
|
       #         |
|
Theorem | sinneg 11766 |
The sine of a negative is the negative of the sine. (Contributed by NM,
30-Apr-2005.)
|
     
       |
|
Theorem | cosneg 11767 |
The cosines of a number and its negative are the same. (Contributed by
NM, 30-Apr-2005.)
|
     
      |
|
Theorem | tannegap 11768 |
The tangent of a negative is the negative of the tangent. (Contributed by
David A. Wheeler, 23-Mar-2014.)
|
      #              |
|
Theorem | sin0 11769 |
Value of the sine function at 0. (Contributed by Steve Rodriguez,
14-Mar-2005.)
|
     |
|
Theorem | cos0 11770 |
Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|
     |
|
Theorem | tan0 11771 |
The value of the tangent function at zero is zero. (Contributed by David
A. Wheeler, 16-Mar-2014.)
|
     |
|
Theorem | efival 11772 |
The exponential function in terms of sine and cosine. (Contributed by NM,
30-Apr-2005.)
|
                     |
|
Theorem | efmival 11773 |
The exponential function in terms of sine and cosine. (Contributed by NM,
14-Jan-2006.)
|
                      |
|
Theorem | efeul 11774 |
Eulerian representation of the complex exponential. (Suggested by Jeff
Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)
|
    
                                |
|
Theorem | efieq 11775 |
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 11776 |
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 11777 |
Addition formula for cosine. Equation 15 of [Gleason] p. 310.
(Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro,
30-Apr-2014.)
|
      
            
             |
|
Theorem | tanaddaplem 11778 |
A useful intermediate step in tanaddap 11779 when showing that the addition of
tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.)
(Revised by Jim Kingdon, 25-Dec-2022.)
|
         #     #       
  #           #    |
|
Theorem | tanaddap 11779 |
Addition formula for tangent. (Contributed by Mario Carneiro,
4-Apr-2015.)
|
         #     #
      #
 
     
     
                    |
|
Theorem | sinsub 11780 |
Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                   
             |
|
Theorem | cossub 11781 |
Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                   
             |
|
Theorem | addsin 11782 |
Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                                   |
|
Theorem | subsin 11783 |
Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                                   |
|
Theorem | sinmul 11784 |
Product of sines can be rewritten as half the difference of certain
cosines. This follows from cosadd 11777 and cossub 11781. (Contributed by David
A. Wheeler, 26-May-2015.)
|
                               |
|
Theorem | cosmul 11785 |
Product of cosines can be rewritten as half the sum of certain cosines.
This follows from cosadd 11777 and cossub 11781. (Contributed by David A.
Wheeler, 26-May-2015.)
|
                               |
|
Theorem | addcos 11786 |
Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                                   |
|
Theorem | subcos 11787 |
Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
(Revised by Mario Carneiro, 10-May-2014.)
|
                                   |
|
Theorem | sincossq 11788 |
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 11789 |
Double-angle formula for sine. (Contributed by Paul Chapman,
17-Jan-2008.)
|
                     |
|
Theorem | cos2t 11790 |
Double-angle formula for cosine. (Contributed by Paul Chapman,
24-Jan-2008.)
|
                     |
|
Theorem | cos2tsin 11791 |
Double-angle formula for cosine in terms of sine. (Contributed by NM,
12-Sep-2008.)
|
                     |
|
Theorem | sinbnd 11792 |
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 11793 |
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 11794 |
The sine of a real number is in the closed interval from -1 to 1.
(Contributed by Mario Carneiro, 12-May-2014.)
|
    
   ![[,] [,]](_icc.gif)    |
|
Theorem | cosbnd2 11795 |
The cosine of a real number is in the closed interval from -1 to 1.
(Contributed by Mario Carneiro, 12-May-2014.)
|
    
   ![[,] [,]](_icc.gif)    |
|
Theorem | ef01bndlem 11796* |
Lemma for sin01bnd 11797 and cos01bnd 11798. (Contributed by Paul Chapman,
19-Jan-2008.)
|

                ![(,] (,]](_ioc.gif)                    
   |
|
Theorem | sin01bnd 11797 |
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.)
|
   ![(,] (,]](_ioc.gif)                      |
|
Theorem | cos01bnd 11798 |
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.)
|
   ![(,] (,]](_ioc.gif)         
                
     |
|
Theorem | cos1bnd 11799 |
Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|
               |
|
Theorem | cos2bnd 11800 |
Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|
                 |