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

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

       |
|
Theorem | fprodxp 11634* |
Combine two products into a single product over the cartesian product.
(Contributed by Scott Fenton, 1-Feb-2018.)
|
           
 
   
      |
|
Theorem | fprodcnv 11635* |
Transform a product region using the converse operation. (Contributed
by Scott Fenton, 1-Feb-2018.)
|
        
               |
|
Theorem | fprodcom2fi 11636* |
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 11637* |
Interchange product order. (Contributed by Scott Fenton,
2-Feb-2018.)
|
     
  
        |
|
Theorem | fprod0diagfz 11638* |
Two ways to express "the product of     over the
triangular
region , ,
. Compare
fisum0diag 11451. (Contributed by Scott Fenton, 2-Feb-2018.)
|
      
                                          |
|
Theorem | fprodrec 11639* |
The finite product of reciprocals is the reciprocal of the product.
(Contributed by Jim Kingdon, 28-Aug-2024.)
|
       
 #     

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

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

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

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

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

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

          
                                                                  
                      |