P. 123 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12201-12300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fprodclf 12201*	Closure of a finite product of complex numbers. A version of fprodcl 12173 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 12202*	A finite product of terms apart from zero is apart from zero. A version of fprodap0 12187 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 12203*	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 12204*	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 12205*	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 12206*	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 12207*	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 12208	Extend class notation to include the exponential function.
class exp
Syntax	ceu 12209	Extend class notation to include Euler's constant _e = 2.71828....
class _e
Syntax	csin 12210	Extend class notation to include the sine function.
class sin
Syntax	ccos 12211	Extend class notation to include the cosine function.
class cos
Syntax	ctan 12212	Extend class notation to include the tangent function.
class tan
Syntax	cpi 12213	Extend class notation to include the constant pi, pi = 3.14159....
class pi
Definition	df-ef 12214*	Define the exponential function. Its value at the complex number A is ( exp ` A ) and is called the "exponential of A"; see efval 12227. (Contributed by NM, 14-Mar-2005.)
|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
Definition	df-e 12215	Define Euler's constant _e = 2.71828.... (Contributed by NM, 14-Mar-2005.)
|- _e = ( exp ` 1 )
Definition	df-sin 12216	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 12217	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 12218	Define the tangent function. We define it this way for cmpt 4150, 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 12219	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 12220	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 12221	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 12222	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 12223*	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 12224*	Lemma for efcl 12230. The series that defines the exponential function converges. The ratio test cvgratgt0 12099 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 12225*	Lemma for efcl 12230. 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 12226*	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 12227*	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 12228	Value of Euler's constant _e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
|- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )
Theorem	eff 12229	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 12230	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 12231*	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 12232*	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 12233*	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 12234	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 12235	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 12236	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 12237	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 12238	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 12239	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 12240*	Lemma for efadd 12241 (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 12241	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 12242	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 12243	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 12244	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 12243 (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 12245	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 12246	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 12247	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 12248	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 12249	Value of the exponential function for integers. Special case of efval 12227. 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 12250	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 12251	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 12252	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 12253*	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 12254*	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 12255*	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 12256*	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 12257*	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 12258*	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 12259	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 12260*	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 12261	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 12262	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 12263	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 12264	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 12265	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 12266	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 12267	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 12268	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 12269	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 12270	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 12271	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 12272	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 12273	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 12274	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 12275	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 )
Theorem	sincld 12276	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( sin ` A ) e. CC )
Theorem	coscld 12277	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( cos ` A ) e. CC )
Theorem	tanclapd 12278	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( cos ` A ) # 0 )   =>    |- ( ph -> ( tan ` A ) e. CC )
Theorem	tanval2ap 12279	Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.)
|- ( ( A e. CC /\ ( cos ` A ) # 0 ) -> ( tan ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
Theorem	tanval3ap 12280	Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.)
|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) # 0 ) -> ( tan ` A ) = ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) )
Theorem	resinval 12281	The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( sin ` A ) = ( Im ` ( exp ` ( _i x. A ) ) ) )
Theorem	recosval 12282	The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( cos ` A ) = ( Re ` ( exp ` ( _i x. A ) ) ) )
Theorem	efi4p 12283*	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.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
Theorem	resin4p 12284*	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.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. RR -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
Theorem	recos4p 12285*	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.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. RR -> ( cos ` A ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
Theorem	resincl 12286	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( sin ` A ) e. RR )
Theorem	recoscl 12287	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( cos ` A ) e. RR )
Theorem	retanclap 12288	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
|- ( ( A e. RR /\ ( cos ` A ) # 0 ) -> ( tan ` A ) e. RR )
Theorem	resincld 12289	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( sin ` A ) e. RR )
Theorem	recoscld 12290	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( cos ` A ) e. RR )
Theorem	retanclapd 12291	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> ( cos ` A ) # 0 )   =>    |- ( ph -> ( tan ` A ) e. RR )
Theorem	sinneg 12292	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
Theorem	cosneg 12293	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
Theorem	tannegap 12294	The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.)
|- ( ( A e. CC /\ ( cos ` A ) # 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )
Theorem	sin0 12295	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
|- ( sin ` 0 ) = 0
Theorem	cos0 12296	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|- ( cos ` 0 ) = 1
Theorem	tan0 12297	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
|- ( tan ` 0 ) = 0
Theorem	efival 12298	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
Theorem	efmival 12299	The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)
|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
Theorem	efeul 12300	Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)
|- ( A e. CC -> ( exp ` A ) = ( ( exp ` ( Re ` A ) ) x. ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) ) )