P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fprodssdc 11901*	Change the index set to a subset in a finite sum. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> A. j e. B DECID j e. A )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )
Theorem	fprodmul 11902*	The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   =>    |- ( ph -> prod_ k e. A ( B x. C ) = ( prod_ k e. A B x. prod_ k e. A C ) )
Theorem	prodsnf 11903*	A product of a singleton is the term. A version of prodsn 11904 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/_ k B   &    |- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )
Theorem	prodsn 11904*	A product of a singleton is the term. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> prod_ k e. { M } A = B )
Theorem	fprod1 11905*	A finite product of only one term is the term itself. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( k = M -> A = B )   =>    |- ( ( M e. ZZ /\ B e. CC ) -> prod_ k e. ( M ... M ) A = B )
Theorem	climprod1 11906	The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )
Theorem	fprodsplitdc 11907*	Split a finite product into two parts. New proofs should use fprodsplit 11908 which is the same but with one fewer hypothesis. (Contributed by Scott Fenton, 16-Dec-2017.) (New usage is discouraged.)
|- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> A. j e. U DECID j e. A )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )
Theorem	fprodsplit 11908*	Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )
Theorem	fprodm1 11909*	Separate out the last term in a finite product. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = N -> A = B )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. B ) )
Theorem	fprod1p 11910*	Separate out the first term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   &    |- ( k = M -> A = B )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( B x. prod_ k e. ( ( M + 1 ) ... N ) A ) )
Theorem	fprodp1 11911*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   &    |- ( k = ( N + 1 ) -> A = B )   =>    |- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. B ) )
Theorem	fprodm1s 11912*	Separate out the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )   =>    |- ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. [_ N / k ]_ A ) )
Theorem	fprodp1s 11913*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   =>    |- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. [_ ( N + 1 ) / k ]_ A ) )
Theorem	prodsns 11914*	A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017.)
|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> prod_ k e. { M } A = [_ M / k ]_ A )
Theorem	fprodunsn 11915*	Multiply in an additional term in a finite product. See also fprodsplitsn 11944 which is the same but with a F/ k ph hypothesis in place of the distinct variable condition between ph and k. (Contributed by Jim Kingdon, 16-Aug-2024.)
|- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( k = B -> C = D )   =>    |- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )
Theorem	fprodcl2lem 11916*	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> prod_ k e. A B e. S )
Theorem	fprodcllem 11917*	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> 1 e. S )   =>    |- ( ph -> prod_ k e. A B e. S )
Theorem	fprodcl 11918*	Closure of a finite product of complex numbers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B e. CC )
Theorem	fprodrecl 11919*	Closure of a finite product of real numbers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> prod_ k e. A B e. RR )
Theorem	fprodzcl 11920*	Closure of a finite product of integers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ZZ )   =>    |- ( ph -> prod_ k e. A B e. ZZ )
Theorem	fprodnncl 11921*	Closure of a finite product of positive integers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. NN )   =>    |- ( ph -> prod_ k e. A B e. NN )
Theorem	fprodrpcl 11922*	Closure of a finite product of positive reals. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR+ )   =>    |- ( ph -> prod_ k e. A B e. RR+ )
Theorem	fprodnn0cl 11923*	Closure of a finite product of nonnegative integers. (Contributed by Scott Fenton, 14-Dec-2017.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. NN0 )   =>    |- ( ph -> prod_ k e. A B e. NN0 )
Theorem	fprodcllemf 11924*	Finite product closure lemma. A version of fprodcllem 11917 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> 1 e. S )   =>    |- ( ph -> prod_ k e. A B e. S )
Theorem	fprodreclf 11925*	Closure of a finite product of real numbers. A version of fprodrecl 11919 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> prod_ k e. A B e. RR )
Theorem	fprodfac 11926*	Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
Theorem	fprodabs 11927*	The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   =>    |- ( ph -> ( abs ` prod_ k e. ( M ... N ) A ) = prod_ k e. ( M ... N ) ( abs ` A ) )
Theorem	fprodeq0 11928*	Any finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ( ph /\ k = N ) -> A = 0 )   =>    |- ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( M ... K ) A = 0 )
Theorem	fprodshft 11929*	Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( k - K ) -> A = B )   =>    |- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( M + K ) ... ( N + K ) ) B )
Theorem	fprodrev 11930*	Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( K - k ) -> A = B )   =>    |- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( K - N ) ... ( K - M ) ) B )
Theorem	fprodconst 11931*	The product of constant terms ( k is not free in B). (Contributed by Scott Fenton, 12-Jan-2018.)
|- ( ( A e. Fin /\ B e. CC ) -> prod_ k e. A B = ( B ^ (♯ ` A ) ) )
Theorem	fprodap0 11932*	A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A B # 0 )
Theorem	fprod2dlemstep 11933*	Lemma for fprod2d 11934- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   &    |- ( ph -> -. y e. x )   &    |- ( ph -> ( x u. { y } ) C_ A )   &    |- ( ph -> x e. Fin )   &    |- ( ps <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )   =>    |- ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
Theorem	fprod2d 11934*	Write a double product as a product over a two-dimensional region. Compare fsum2d 11746. (Contributed by Scott Fenton, 30-Jan-2018.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D )
Theorem	fprodxp 11935*	Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. ( A X. B ) D )
Theorem	fprodcnv 11936*	Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018.)
|- ( x = <. j , k >. -> B = D )   &    |- ( y = <. k , j >. -> C = D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> Rel A )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> prod_ x e. A B = prod_ y e. `' A C )
Theorem	fprodcom2fi 11937*	Interchange order of multiplication. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ k e. C ) -> D e. Fin )   &    |- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B E = prod_ k e. C prod_ j e. D E )
Theorem	fprodcom 11938*	Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ k e. B prod_ j e. A C )
Theorem	fprod0diagfz 11939*	Two ways to express "the product of A ( j , k ) over the triangular region M <_ j, M <_ k, j + k <_ N. Compare fisum0diag 11752. (Contributed by Scott Fenton, 2-Feb-2018.)
|- ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> prod_ j e. ( 0 ... N ) prod_ k e. ( 0 ... ( N - j ) ) A = prod_ k e. ( 0 ... N ) prod_ j e. ( 0 ... ( N - k ) ) A )
Theorem	fprodrec 11940*	The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A ( 1 / B ) = ( 1 / prod_ k e. A B ) )
Theorem	fproddivap 11941*	The quotient of two finite products. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> C # 0 )   =>    |- ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) )
Theorem	fproddivapf 11942*	The quotient of two finite products. A version of fproddivap 11941 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> C # 0 )   =>    |- ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) )
Theorem	fprodsplitf 11943*	Split a finite product into two parts. A version of fprodsplit 11908 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )
Theorem	fprodsplitsn 11944*	Separate out a term in a finite product. See also fprodunsn 11915 which is the same but with a distinct variable condition in place of F/ k ph. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( k = B -> C = D )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )
Theorem	fprodsplit1f 11945*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> F/_ k D )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ k = C ) -> B = D )   =>    |- ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )
Theorem	fprodclf 11946*	Closure of a finite product of complex numbers. A version of fprodcl 11918 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B e. CC )
Theorem	fprodap0f 11947*	A finite product of terms apart from zero is apart from zero. A version of fprodap0 11932 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A B # 0 )
Theorem	fprodge0 11948*	If all the terms of a finite product are nonnegative, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   =>    |- ( ph -> 0 <_ prod_ k e. A B )
Theorem	fprodeq0g 11949*	Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ k = C ) -> B = 0 )   =>    |- ( ph -> prod_ k e. A B = 0 )
Theorem	fprodge1 11950*	If all of the terms of a finite product are greater than or equal to 1, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 1 <_ B )   =>    |- ( ph -> 1 <_ prod_ k e. A B )
Theorem	fprodle 11951*	If all the terms of two finite products are nonnegative and compare, so do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   &    |- ( ( ph /\ k e. A ) -> C e. RR )   &    |- ( ( ph /\ k e. A ) -> B <_ C )   =>    |- ( ph -> prod_ k e. A B <_ prod_ k e. A C )
Theorem	fprodmodd 11952*	If all factors of two finite products are equal modulo M, the products are equal modulo M. (Contributed by AV, 7-Jul-2021.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ZZ )   &    |- ( ( ph /\ k e. A ) -> C e. ZZ )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ k e. A ) -> ( B mod M ) = ( C mod M ) )   =>    |- ( ph -> ( prod_ k e. A B mod M ) = ( prod_ k e. A C mod M ) )
4.10  Elementary trigonometry
4.10.1  The exponential, sine, and cosine functions
Syntax	ce 11953	Extend class notation to include the exponential function.
class exp
Syntax	ceu 11954	Extend class notation to include Euler's constant _e = 2.71828....
class _e
Syntax	csin 11955	Extend class notation to include the sine function.
class sin
Syntax	ccos 11956	Extend class notation to include the cosine function.
class cos
Syntax	ctan 11957	Extend class notation to include the tangent function.
class tan
Syntax	cpi 11958	Extend class notation to include the constant pi, pi = 3.14159....
class pi
Definition	df-ef 11959*	Define the exponential function. Its value at the complex number A is ( exp ` A ) and is called the "exponential of A"; see efval 11972. (Contributed by NM, 14-Mar-2005.)
|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
Definition	df-e 11960	Define Euler's constant _e = 2.71828.... (Contributed by NM, 14-Mar-2005.)
|- _e = ( exp ` 1 )
Definition	df-sin 11961	Define the sine function. (Contributed by NM, 14-Mar-2005.)
|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
Definition	df-cos 11962	Define the cosine function. (Contributed by NM, 14-Mar-2005.)
|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
Definition	df-tan 11963	Define the tangent function. We define it this way for cmpt 4105, which requires the form ( x e. A |-> B ). (Contributed by Mario Carneiro, 14-Mar-2014.)
|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
Definition	df-pi 11964	Define the constant pi, pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.)
|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
Theorem	eftcl 11965	Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)
|- ( ( A e. CC /\ K e. NN0 ) -> ( ( A ^ K ) / ( ! ` K ) ) e. CC )
Theorem	reeftcl 11966	The terms of the series expansion of the exponential function at a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|- ( ( A e. RR /\ K e. NN0 ) -> ( ( A ^ K ) / ( ! ` K ) ) e. RR )
Theorem	eftabs 11967	The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.)
|- ( ( A e. CC /\ K e. NN0 ) -> ( abs ` ( ( A ^ K ) / ( ! ` K ) ) ) = ( ( ( abs ` A ) ^ K ) / ( ! ` K ) ) )
Theorem	eftvalcn 11968*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( ( A e. CC /\ N e. NN0 ) -> ( F ` N ) = ( ( A ^ N ) / ( ! ` N ) ) )
Theorem	efcllemp 11969*	Lemma for efcl 11975. The series that defines the exponential function converges. The ratio test cvgratgt0 11844 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 8-Dec-2022.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> K e. NN )   &    |- ( ph -> ( 2 x. ( abs ` A ) ) < K )   =>    |- ( ph -> seq 0 ( + , F ) e. dom ~~> )
Theorem	efcllem 11970*	Lemma for efcl 11975. The series that defines the exponential function converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 8-Dec-2022.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )
Theorem	ef0lem 11971*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A = 0 -> seq 0 ( + , F ) ~~> 1 )
Theorem	efval 11972*	Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
Theorem	esum 11973	Value of Euler's constant _e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
|- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )
Theorem	eff 11974	Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
|- exp : CC --> CC
Theorem	efcl 11975	Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( A e. CC -> ( exp ` A ) e. CC )
Theorem	efval2 11976*	Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( F ` k ) )
Theorem	efcvg 11977*	The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> seq 0 ( + , F ) ~~> ( exp ` A ) )
Theorem	efcvgfsum 11978*	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.)
|- F = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ^ k ) / ( ! ` k ) ) )   =>    |- ( A e. CC -> F ~~> ( exp ` A ) )
Theorem	reefcl 11979	The exponential function is real if its argument is real. (Contributed by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- ( A e. RR -> ( exp ` A ) e. RR )
Theorem	reefcld 11980	The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( exp ` A ) e. RR )
Theorem	ere 11981	Euler's constant _e = 2.71828... is a real number. (Contributed by NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|- _e e. RR
Theorem	ege2le3 11982	Euler's constant _e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
|- F = ( n e. NN |-> ( 2 x. ( ( 1 / 2 ) ^ n ) ) )   &    |- G = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )   =>    |- ( 2 <_ _e /\ _e <_ 3 )
Theorem	ef0 11983	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.)
|- ( exp ` 0 ) = 1
Theorem	efcj 11984	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.)
|- ( A e. CC -> ( exp ` ( * ` A ) ) = ( * ` ( exp ` A ) ) )
Theorem	efaddlem 11985*	Lemma for efadd 11986 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   &    |- G = ( n e. NN0 |-> ( ( B ^ n ) / ( ! ` n ) ) )   &    |- H = ( n e. NN0 |-> ( ( ( A + B ) ^ n ) / ( ! ` n ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )
Theorem	efadd 11986	Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )
Theorem	efcan 11987	Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)
|- ( A e. CC -> ( ( exp ` A ) x. ( exp ` -u A ) ) = 1 )
Theorem	efap0 11988	The exponential of a complex number is apart from zero. (Contributed by Jim Kingdon, 12-Dec-2022.)
|- ( A e. CC -> ( exp ` A ) # 0 )
Theorem	efne0 11989	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 11988 (which will be more useful in most contexts). (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 29-Apr-2014.)
|- ( A e. CC -> ( exp ` A ) =/= 0 )
Theorem	efneg 11990	The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( exp ` -u A ) = ( 1 / ( exp ` A ) ) )
Theorem	eff2 11991	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|- exp : CC --> ( CC \ { 0 } )
Theorem	efsub 11992	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) )
Theorem	efexp 11993	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.)
|- ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( N x. A ) ) = ( ( exp ` A ) ^ N ) )
Theorem	efzval 11994	Value of the exponential function for integers. Special case of efval 11972. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- ( N e. ZZ -> ( exp ` N ) = ( _e ^ N ) )
Theorem	efgt0 11995	The exponential of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. RR -> 0 < ( exp ` A ) )
Theorem	rpefcl 11996	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.)
|- ( A e. RR -> ( exp ` A ) e. RR+ )
Theorem	rpefcld 11997	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( exp ` A ) e. RR+ )
Theorem	eftlcvg 11998*	The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )
Theorem	eftlcl 11999*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( ( A e. CC /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. CC )
Theorem	reeftlcl 12000*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( ( A e. RR /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. RR )