P. 125 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12401-12500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fprodnncl 12401*	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 12402*	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 12403*	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 12404*	Finite product closure lemma. A version of fprodcllem 12397 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 12405*	Closure of a finite product of real numbers. A version of fprodrecl 12399 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 12406*	Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
Theorem	fprodabs 12407*	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 12408*	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 12409*	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 12410*	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 12411*	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 12412*	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 12413*	Lemma for fprod2d 12414- 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 12414*	Write a double product as a product over a two-dimensional region. Compare fsum2d 12226. (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 12415*	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 12416*	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 12417*	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 12418*	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 12419*	Two ways to express "the product of A ( j , k ) over the triangular region M <_ j, M <_ k, j + k <_ N. Compare fisum0diag 12232. (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 12420*	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 12421*	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 12422*	The quotient of two finite products. A version of fproddivap 12421 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 12423*	Split a finite product into two parts. A version of fprodsplit 12388 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 12424*	Separate out a term in a finite product. See also fprodunsn 12395 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 12425*	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 12426*	Closure of a finite product of complex numbers. A version of fprodcl 12398 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 12427*	A finite product of terms apart from zero is apart from zero. A version of fprodap0 12412 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 12428*	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 12429*	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 12430*	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 12431*	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 12432*	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 12433	Extend class notation to include the exponential function.
class exp
Syntax	ceu 12434	Extend class notation to include Euler's constant _e = 2.71828....
class _e
Syntax	csin 12435	Extend class notation to include the sine function.
class sin
Syntax	ccos 12436	Extend class notation to include the cosine function.
class cos
Syntax	ctan 12437	Extend class notation to include the tangent function.
class tan
Syntax	cpi 12438	Extend class notation to include the constant pi, pi = 3.14159....
class pi
Definition	df-ef 12439*	Define the exponential function. Its value at the complex number A is ( exp ` A ) and is called the "exponential of A"; see efval 12452. (Contributed by NM, 14-Mar-2005.)
|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
Definition	df-e 12440	Define Euler's constant _e = 2.71828.... (Contributed by NM, 14-Mar-2005.)
|- _e = ( exp ` 1 )
Definition	df-sin 12441	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 12442	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 12443	Define the tangent function. We define it this way for cmpt 4193, 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 12444	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 12445	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 12446	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 12447	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 12448*	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 12449*	Lemma for efcl 12455. The series that defines the exponential function converges. The ratio test cvgratgt0 12324 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 12450*	Lemma for efcl 12455. 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 12451*	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 12452*	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 12453	Value of Euler's constant _e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
|- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )
Theorem	eff 12454	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 12455	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 12456*	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 12457*	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 12458*	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 12459	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 12460	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 12461	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 12462	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 12463	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 12464	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 12465*	Lemma for efadd 12466 (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 12466	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 12467	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 12468	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 12469	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 12468 (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 12470	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 12471	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 12472	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 12473	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 12474	Value of the exponential function for integers. Special case of efval 12452. 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 12475	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 12476	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 12477	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 12478*	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 12479*	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 12480*	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 )
Theorem	eftlub 12481*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   &    |- G = ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) )   &    |- H = ( n e. NN0 |-> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ n ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) <_ 1 )   =>    |- ( ph -> ( abs ` sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) <_ ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )
Theorem	efsep 12482*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   &    |- N = ( M + 1 )   &    |- M e. NN0   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( exp ` A ) = ( B + sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) )   &    |- ( ph -> ( B + ( ( A ^ M ) / ( ! ` M ) ) ) = D )   =>    |- ( ph -> ( exp ` A ) = ( D + sum_ k e. ( ZZ>= ` N ) ( F ` k ) ) )
Theorem	effsumlt 12483*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( seq 0 ( + , F ) ` N ) < ( exp ` A ) )
Theorem	eft0val 12484	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.)
|- ( A e. CC -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = 1 )
Theorem	ef4p 12485*	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.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> ( exp ` A ) = ( ( ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) + ( ( A ^ 3 ) / 6 ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
Theorem	efgt1p2 12486	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.)
|- ( A e. RR+ -> ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) < ( exp ` A ) )
Theorem	efgt1p 12487	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.)
|- ( A e. RR+ -> ( 1 + A ) < ( exp ` A ) )
Theorem	efgt1 12488	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.)
|- ( A e. RR+ -> 1 < ( exp ` A ) )
Theorem	efltim 12489	The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 20-Dec-2022.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> ( exp ` A ) < ( exp ` B ) ) )
Theorem	reef11 12490	The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` A ) = ( exp ` B ) <-> A = B ) )
Theorem	reeff1 12491	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.)
|- ( exp |` RR ) : RR -1-1-> RR+
Theorem	eflegeo 12492	The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A < 1 )   =>    |- ( ph -> ( exp ` A ) <_ ( 1 / ( 1 - A ) ) )
Theorem	sinval 12493	Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
Theorem	cosval 12494	Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
Theorem	sinf 12495	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- sin : CC --> CC
Theorem	cosf 12496	Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- cos : CC --> CC
Theorem	sincl 12497	Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. CC -> ( sin ` A ) e. CC )
Theorem	coscl 12498	Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. CC -> ( cos ` A ) e. CC )
Theorem	tanvalap 12499	Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.)
|- ( ( A e. CC /\ ( cos ` A ) # 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
Theorem	tanclap 12500	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.)
|- ( ( A e. CC /\ ( cos ` A ) # 0 ) -> ( tan ` A ) e. CC )