Theorem List for Intuitionistic Logic Explorer - 11201-11300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | csin 11201 |
Extend class notation to include the sine function.
|
 |
|
Syntax | ccos 11202 |
Extend class notation to include the cosine function.
|
 |
|
Syntax | ctan 11203 |
Extend class notation to include the tangent function.
|
 |
|
Syntax | cpi 11204 |
Extend class notation to include the constant pi, = 3.14159....
|
 |
|
Definition | df-ef 11205* |
Define the exponential function. Its value at the complex number
is     and is called the "exponential of "; see
efval 11218. (Contributed by NM, 14-Mar-2005.)
|
              |
|
Definition | df-e 11206 |
Define Euler's constant = 2.71828.... (Contributed by NM,
14-Mar-2005.)
|
     |
|
Definition | df-sin 11207 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
                      |
|
Definition | df-cos 11208 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
                    |
|
Definition | df-tan 11209 |
Define the tangent function. We define it this way for cmpt 3949,
which
requires the form   .
(Contributed by Mario
Carneiro, 14-Mar-2014.)
|
                      |
|
Definition | df-pi 11210 |
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             |
|
Theorem | eftcl 11211 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
               |
|
Theorem | reeftcl 11212 |
The terms of the series expansion of the exponential function at a real
number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|
               |
|
Theorem | eftabs 11213 |
The absolute value of a term in the series expansion of the exponential
function. (Contributed by Paul Chapman, 23-Nov-2007.)
|
                                 |
|
Theorem | eftvalcn 11214* |
The value of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
8-Dec-2022.)
|

                 
            |
|
Theorem | efcllemp 11215* |
Lemma for efcl 11221. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11194 is used to show convergence.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|

           
         
 
  
 |
|
Theorem | efcllem 11216* |
Lemma for efcl 11221. The series that defines the exponential
function
converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|

           
    |
|
Theorem | ef0lem 11217* |
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.)
|

           
  
  |
|
Theorem | efval 11218* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
    
             |
|
Theorem | esum 11219 |
Value of Euler's constant = 2.71828.... (Contributed by Steve
Rodriguez, 5-Mar-2006.)
|
        |
|
Theorem | eff 11220 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
     |
|
Theorem | efcl 11221 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
    
  |
|
Theorem | efval2 11222* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|

           
   
       |
|
Theorem | efcvg 11223* |
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 11224* |
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 11225 |
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 11226 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | ere 11227 |
Euler's constant =
2.71828... is a real number. (Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
 |
|
Theorem | ege2le3 11228 |
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 11229 |
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 11230 |
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 11231* |
Lemma for efadd 11232 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|

          
                                                 |
|
Theorem | efadd 11232 |
Sum of exponents law for exponential function. (Contributed by NM,
10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
      
              |
|
Theorem | efcan 11233 |
Cancellation law for exponential function. Equation 27 of [Rudin] p. 164.
(Contributed by NM, 13-Jan-2006.)
|
           
  |
|
Theorem | efap0 11234 |
The exponential of a complex number is apart from zero. (Contributed by
Jim Kingdon, 12-Dec-2022.)
|
     #   |
|
Theorem | efne0 11235 |
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 11234 (which will be more useful in most
contexts).
(Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
       |
|
Theorem | efneg 11236 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
     
        |
|
Theorem | eff2 11237 |
The exponential function maps the complex numbers to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
         |
|
Theorem | efsub 11238 |
Difference of exponents law for exponential function. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
                     |
|
Theorem | efexp 11239 |
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 11240 |
Value of the exponential function for integers. Special case of efval 11218.
Equation 30 of [Rudin] p. 164. (Contributed
by Steve Rodriguez,
15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
    
      |
|
Theorem | efgt0 11241 |
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 11242 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 10-Nov-2013.)
|
    
  |
|
Theorem | rpefcld 11243 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | eftlcvg 11244* |
The tail series of the exponential function are convergent.
(Contributed by Mario Carneiro, 29-Apr-2014.)
|

                  |
|
Theorem | eftlcl 11245* |
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 11246* |
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 11247* |
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 11248* |
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 11249* |
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 11250 |
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 11251* |
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 11252 |
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 11253 |
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 11254 |
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 11255 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
20-Dec-2022.)
|
               |
|
Theorem | efler 11256 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 20-Dec-2022.)
|
               |
|
Theorem | reef11 11257 |
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 11258 |
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 11259 |
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 11260 |
Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised
by Mario Carneiro, 10-Nov-2013.)
|
    
                     |
|
Theorem | cosval 11261 |
Value of the cosine function. (Contributed by NM, 14-Mar-2005.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
    
                   |
|
Theorem | sinf 11262 |
Domain and codomain of the sine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
     |
|
Theorem | cosf 11263 |
Domain and codomain of the cosine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
     |
|
Theorem | sincl 11264 |
Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised
by Mario Carneiro, 30-Apr-2014.)
|
    
  |
|
Theorem | coscl 11265 |
Closure of the cosine function with a complex argument. (Contributed by
NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
    
  |
|
Theorem | tanvalap 11266 |
Value of the tangent function. (Contributed by Mario Carneiro,
14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.)
|
      #                  |
|
Theorem | tanclap 11267 |
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 11268 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | coscld 11269 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | tanclapd 11270 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
|
       #         |
|
Theorem | tanval2ap 11271 |
Express the tangent function directly in terms of . (Contributed
by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon,
22-Dec-2022.)
|
      #             
                            |
|
Theorem | tanval3ap 11272 |
Express the tangent function directly in terms of . (Contributed
by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon,
22-Dec-2022.)
|
            #                                |
|
Theorem | resinval 11273 |
The sine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
    
            |
|
Theorem | recosval 11274 |
The cosine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
    
            |
|
Theorem | efi4p 11275* |
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 11276* |
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 11277* |
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 11278 |
The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
    
  |
|
Theorem | recoscl 11279 |
The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
    
  |
|
Theorem | retanclap 11280 |
The closure of the tangent function with a real argument. (Contributed by
David A. Wheeler, 15-Mar-2014.)
|
      #        |
|
Theorem | resincld 11281 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | recoscld 11282 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
         |
|
Theorem | retanclapd 11283 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.)
|
       #         |
|
Theorem | sinneg 11284 |
The sine of a negative is the negative of the sine. (Contributed by NM,
30-Apr-2005.)
|
     
       |
|
Theorem | cosneg 11285 |
The cosines of a number and its negative are the same. (Contributed by
NM, 30-Apr-2005.)
|
     
      |
|
Theorem | tannegap 11286 |
The tangent of a negative is the negative of the tangent. (Contributed by
David A. Wheeler, 23-Mar-2014.)
|
      #              |
|
Theorem | sin0 11287 |
Value of the sine function at 0. (Contributed by Steve Rodriguez,
14-Mar-2005.)
|
     |
|
Theorem | cos0 11288 |
Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|
     |
|
Theorem | tan0 11289 |
The value of the tangent function at zero is zero. (Contributed by David
A. Wheeler, 16-Mar-2014.)
|
     |
|
Theorem | efival 11290 |
The exponential function in terms of sine and cosine. (Contributed by NM,
30-Apr-2005.)
|
                     |
|
Theorem | efmival 11291 |
The exponential function in terms of sine and cosine. (Contributed by NM,
14-Jan-2006.)
|
                      |
|
Theorem | efeul 11292 |
Eulerian representation of the complex exponential. (Suggested by Jeff
Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)
|
    
                                |
|
Theorem | efieq 11293 |
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 11294 |
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 11295 |
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 11296 |
A useful intermediate step in tanaddap 11297 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 11297 |
Addition formula for tangent. (Contributed by Mario Carneiro,
4-Apr-2015.)
|
         #     #
      #
 
     
     
                    |
|
Theorem | sinsub 11298 |
Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                   
             |
|
Theorem | cossub 11299 |
Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                   
             |
|
Theorem | addsin 11300 |
Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
                                   |