Type | Label | Description |
Statement |
|
Theorem | prodsn 11601* |
A product of a singleton is the term. (Contributed by Scott Fenton,
14-Dec-2017.)
|
           |
|
Theorem | fprod1 11602* |
A finite product of only one term is the term itself. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
             |
|
Theorem | climprod1 11603 |
The limit of a product over one. (Contributed by Scott Fenton,
15-Dec-2017.)
|
         
   
  |
|
Theorem | fprodsplitdc 11604* |
Split a finite product into two parts. New proofs should use
fprodsplit 11605 which is the same but with one fewer
hypothesis.
(Contributed by Scott Fenton, 16-Dec-2017.)
(New usage is discouraged.)
|
            DECID         
    |
|
Theorem | fprodsplit 11605* |
Split a finite product into two parts. (Contributed by Scott Fenton,
16-Dec-2017.)
|
                 
    |
|
Theorem | fprodm1 11606* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 16-Dec-2017.)
|
            
 
       
            |
|
Theorem | fprod1p 11607* |
Separate out the first term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
            
 
       
            |
|
Theorem | fprodp1 11608* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 24-Dec-2017.)
|
           
      
      
    
        |
|
Theorem | fprodm1s 11609* |
Separate out the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
            
       
           ![]_ ]_](_urbrack.gif)    |
|
Theorem | fprodp1s 11610* |
Multiply in the last term in a finite product. (Contributed by Scott
Fenton, 27-Dec-2017.)
|
           
         
    
       
 ![]_ ]_](_urbrack.gif)    |
|
Theorem | prodsns 11611* |
A product of the singleton is the term. (Contributed by Scott Fenton,
25-Dec-2017.)
|
    ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   |
|
Theorem | fprodunsn 11612* |
Multiply in an additional term in a finite product. See also
fprodsplitsn 11641 which is the same but with a   hypothesis in
place of the distinct variable condition between and .
(Contributed by Jim Kingdon, 16-Aug-2024.)
|
                
           |
|
Theorem | fprodcl2lem 11613* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|
    
 
      
        |
|
Theorem | fprodcllem 11614* |
Finite product closure lemma. (Contributed by Scott Fenton,
14-Dec-2017.)
|
    
 
      
        |
|
Theorem | fprodcl 11615* |
Closure of a finite product of complex numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
       
  |
|
Theorem | fprodrecl 11616* |
Closure of a finite product of real numbers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
       
  |
|
Theorem | fprodzcl 11617* |
Closure of a finite product of integers. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
       
  |
|
Theorem | fprodnncl 11618* |
Closure of a finite product of positive integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
       
  |
|
Theorem | fprodrpcl 11619* |
Closure of a finite product of positive reals. (Contributed by Scott
Fenton, 14-Dec-2017.)
|
       
  |
|
Theorem | fprodnn0cl 11620* |
Closure of a finite product of nonnegative integers. (Contributed by
Scott Fenton, 14-Dec-2017.)
|
       
  |
|
Theorem | fprodcllemf 11621* |
Finite product closure lemma. A version of fprodcllem 11614 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
      
 
      
        |
|
Theorem | fprodreclf 11622* |
Closure of a finite product of real numbers. A version of fprodrecl 11616
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
     
      |
|
Theorem | fprodfac 11623* |
Factorial using product notation. (Contributed by Scott Fenton,
15-Dec-2017.)
|
             |
|
Theorem | fprodabs 11624* |
The absolute value of a finite product. (Contributed by Scott Fenton,
25-Dec-2017.)
|
       
                         |
|
Theorem | fprodeq0 11625* |
Any finite product containing a zero term is itself zero. (Contributed
by Scott Fenton, 27-Dec-2017.)
|
       
            
     
  |
|
Theorem | fprodshft 11626* |
Shift the index of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
            
           
      
     |
|
Theorem | fprodrev 11627* |
Reversal of a finite product. (Contributed by Scott Fenton,
5-Jan-2018.)
|
            
   
       
      
     |
|
Theorem | fprodconst 11628* |
The product of constant terms ( is not free in ).
(Contributed by Scott Fenton, 12-Jan-2018.)
|
   
   ♯     |
|
Theorem | fprodap0 11629* |
A finite product of nonzero terms is nonzero. (Contributed by Scott
Fenton, 15-Jan-2018.)
|
       
 #    #   |
|
Theorem | fprod2dlemstep 11630* |
Lemma for fprod2d 11631- induction step. (Contributed by Scott
Fenton,
30-Jan-2018.)
|
        
    
 
   
        
 
               

            |
|
Theorem | fprod2d 11631* |
Write a double product as a product over a two-dimensional region.
Compare fsum2d 11443. (Contributed by Scott Fenton,
30-Jan-2018.)
|
        
    
 
   

       |
|
Theorem | fprodxp 11632* |
Combine two products into a single product over the cartesian product.
(Contributed by Scott Fenton, 1-Feb-2018.)
|
           
 
   
      |
|
Theorem | fprodcnv 11633* |
Transform a product region using the converse operation. (Contributed
by Scott Fenton, 1-Feb-2018.)
|
        
               |
|
Theorem | fprodcom2fi 11634* |
Interchange order of multiplication. Note that    and
   are not necessarily constant expressions. (Contributed by
Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
|
     
                
 
   
    |
|
Theorem | fprodcom 11635* |
Interchange product order. (Contributed by Scott Fenton,
2-Feb-2018.)
|
     
  
        |
|
Theorem | fprod0diagfz 11636* |
Two ways to express "the product of     over the
triangular
region , ,
. Compare
fisum0diag 11449. (Contributed by Scott Fenton, 2-Feb-2018.)
|
      
                                          |
|
Theorem | fprodrec 11637* |
The finite product of reciprocals is the reciprocal of the product.
(Contributed by Jim Kingdon, 28-Aug-2024.)
|
       
 #     

    |
|
Theorem | fproddivap 11638* |
The quotient of two finite products. (Contributed by Scott Fenton,
15-Jan-2018.)
|
       
     #            |
|
Theorem | fproddivapf 11639* |
The quotient of two finite products. A version of fproddivap 11638 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
     
       
 #     
  
   |
|
Theorem | fprodsplitf 11640* |
Split a finite product into two parts. A version of fprodsplit 11605 using
bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
                   
    |
|
Theorem | fprodsplitsn 11641* |
Separate out a term in a finite product. See also fprodunsn 11612 which is
the same but with a distinct variable condition in place of
  . (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
              
           
   |
|
Theorem | fprodsplit1f 11642* |
Separate out a term in a finite product. (Contributed by Glauco
Siliprandi, 5-Apr-2020.)
|
               
              |
|
Theorem | fprodclf 11643* |
Closure of a finite product of complex numbers. A version of fprodcl 11615
using bound-variable hypotheses instead of distinct variable conditions.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
     
      |
|
Theorem | fprodap0f 11644* |
A finite product of terms apart from zero is apart from zero. A version
of fprodap0 11629 using bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
(Revised by Jim Kingdon, 30-Aug-2024.)
|
     
     #    #   |
|
Theorem | fprodge0 11645* |
If all the terms of a finite product are nonnegative, so is the product.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
     
    
 
   |
|
Theorem | fprodeq0g 11646* |
Any finite product containing a zero term is itself zero. (Contributed
by Glauco Siliprandi, 5-Apr-2020.)
|
     
     
      |
|
Theorem | fprodge1 11647* |
If all of the terms of a finite product are greater than or equal to
, so is the
product. (Contributed by Glauco Siliprandi,
5-Apr-2020.)
|
     
    
 
   |
|
Theorem | fprodle 11648* |
If all the terms of two finite products are nonnegative and compare, so
do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
     
    
       
      |
|
Theorem | fprodmodd 11649* |
If all factors of two finite products are equal modulo , the
products are equal modulo . (Contributed by AV, 7-Jul-2021.)
|
       
     
           
   |
|
4.9 Elementary trigonometry
|
|
4.9.1 The exponential, sine, and cosine
functions
|
|
Syntax | ce 11650 |
Extend class notation to include the exponential function.
|
 |
|
Syntax | ceu 11651 |
Extend class notation to include Euler's constant = 2.71828....
|
 |
|
Syntax | csin 11652 |
Extend class notation to include the sine function.
|
 |
|
Syntax | ccos 11653 |
Extend class notation to include the cosine function.
|
 |
|
Syntax | ctan 11654 |
Extend class notation to include the tangent function.
|
 |
|
Syntax | cpi 11655 |
Extend class notation to include the constant pi, = 3.14159....
|
 |
|
Definition | df-ef 11656* |
Define the exponential function. Its value at the complex number
is     and is called the "exponential of "; see
efval 11669. (Contributed by NM, 14-Mar-2005.)
|
              |
|
Definition | df-e 11657 |
Define Euler's constant = 2.71828.... (Contributed by NM,
14-Mar-2005.)
|
     |
|
Definition | df-sin 11658 |
Define the sine function. (Contributed by NM, 14-Mar-2005.)
|
                      |
|
Definition | df-cos 11659 |
Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|
                    |
|
Definition | df-tan 11660 |
Define the tangent function. We define it this way for cmpt 4065,
which
requires the form   .
(Contributed by Mario
Carneiro, 14-Mar-2014.)
|
                      |
|
Definition | df-pi 11661 |
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 11662 |
Closure of a term in the series expansion of the exponential function.
(Contributed by Paul Chapman, 11-Sep-2007.)
|
               |
|
Theorem | reeftcl 11663 |
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 11664 |
The absolute value of a term in the series expansion of the exponential
function. (Contributed by Paul Chapman, 23-Nov-2007.)
|
                                 |
|
Theorem | eftvalcn 11665* |
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 11666* |
Lemma for efcl 11672. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11541 is used to show convergence.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|

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

           
    |
|
Theorem | ef0lem 11668* |
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 11669* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
    
             |
|
Theorem | esum 11670 |
Value of Euler's constant = 2.71828.... (Contributed by Steve
Rodriguez, 5-Mar-2006.)
|
        |
|
Theorem | eff 11671 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
     |
|
Theorem | efcl 11672 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
    
  |
|
Theorem | efval2 11673* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|

           
   
       |
|
Theorem | efcvg 11674* |
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 11675* |
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 11676 |
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 11677 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | ere 11678 |
Euler's constant =
2.71828... is a real number. (Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
 |
|
Theorem | ege2le3 11679 |
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 11680 |
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 11681 |
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 11682* |
Lemma for efadd 11683 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|

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

                  |
|
Theorem | eftlcl 11696* |
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 11697* |
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 11698* |
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 11699* |
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 11700* |
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.)
|

           
                |