P. 118 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11701-11800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	efval 11701*	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 11702	Value of Euler's constant _e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
|- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )
Theorem	eff 11703	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 11704	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 11705*	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 11706*	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 11707*	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 11708	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 11709	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 11710	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 11711	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 11712	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 11713	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 11714*	Lemma for efadd 11715 (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 11715	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 11716	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 11717	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 11718	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 11717 (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 11719	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 11720	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 11721	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 11722	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 11723	Value of the exponential function for integers. Special case of efval 11701. 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 11724	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 11725	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 11726	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 11727*	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 11728*	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 11729*	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 11730*	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 11731*	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 11732*	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 11733	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 11734*	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 11735	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 11736	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 11737	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 11738	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 11739	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 11740	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 11741	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 11742	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 11743	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 11744	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 11745	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 11746	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 11747	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 11748	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 11749	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 11750	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( sin ` A ) e. CC )
Theorem	coscld 11751	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( cos ` A ) e. CC )
Theorem	tanclapd 11752	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 11753	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 11754	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 11755	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 11756	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 11757*	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 11758*	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 11759*	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 11760	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( sin ` A ) e. RR )
Theorem	recoscl 11761	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( cos ` A ) e. RR )
Theorem	retanclap 11762	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 11763	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( sin ` A ) e. RR )
Theorem	recoscld 11764	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( cos ` A ) e. RR )
Theorem	retanclapd 11765	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 11766	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 11767	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 11768	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 11769	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
|- ( sin ` 0 ) = 0
Theorem	cos0 11770	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|- ( cos ` 0 ) = 1
Theorem	tan0 11771	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
|- ( tan ` 0 ) = 0
Theorem	efival 11772	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 11773	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 11774	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 ) ) ) ) ) )
Theorem	efieq 11775	The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` ( _i x. A ) ) = ( exp ` ( _i x. B ) ) <-> ( ( cos ` A ) = ( cos ` B ) /\ ( sin ` A ) = ( sin ` B ) ) ) )
Theorem	sinadd 11776	Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A + B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( sin ` B ) ) ) )
Theorem	cosadd 11777	Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )
Theorem	tanaddaplem 11778	A useful intermediate step in tanaddap 11779 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) (Revised by Jim Kingdon, 25-Dec-2022.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) # 0 /\ ( cos ` B ) # 0 ) ) -> ( ( cos ` ( A + B ) ) # 0 <-> ( ( tan ` A ) x. ( tan ` B ) ) # 1 ) )
Theorem	tanaddap 11779	Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) # 0 /\ ( cos ` B ) # 0 /\ ( cos ` ( A + B ) ) # 0 ) ) -> ( tan ` ( A + B ) ) = ( ( ( tan ` A ) + ( tan ` B ) ) / ( 1 - ( ( tan ` A ) x. ( tan ` B ) ) ) ) )
Theorem	sinsub 11780	Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A - B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) )
Theorem	cossub 11781	Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A - B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
Theorem	addsin 11782	Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) + ( sin ` B ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	subsin 11783	Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) - ( sin ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	sinmul 11784	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 11777 and cossub 11781. (Contributed by David A. Wheeler, 26-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) = ( ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) / 2 ) )
Theorem	cosmul 11785	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 11777 and cossub 11781. (Contributed by David A. Wheeler, 26-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) / 2 ) )
Theorem	addcos 11786	Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) + ( cos ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	subcos 11787	Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` B ) - ( cos ` A ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	sincossq 11788	Sine squared plus cosine squared is 1. Equation 17 of [Gleason] p. 311. Note that this holds for non-real arguments, even though individually each term is unbounded. (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
Theorem	sin2t 11789	Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.)
|- ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )
Theorem	cos2t 11790	Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )
Theorem	cos2tsin 11791	Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.)
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
Theorem	sinbnd 11792	The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( -u 1 <_ ( sin ` A ) /\ ( sin ` A ) <_ 1 ) )
Theorem	cosbnd 11793	The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
Theorem	sinbnd2 11794	The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. RR -> ( sin ` A ) e. ( -u 1 [,] 1 ) )
Theorem	cosbnd2 11795	The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. RR -> ( cos ` A ) e. ( -u 1 [,] 1 ) )
Theorem	ef01bndlem 11796*	Lemma for sin01bnd 11797 and cos01bnd 11798. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) < ( ( A ^ 4 ) / 6 ) )
Theorem	sin01bnd 11797	Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )
Theorem	cos01bnd 11798	Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )
Theorem	cos1bnd 11799	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( ( 1 / 3 ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 2 / 3 ) )
Theorem	cos2bnd 11800	Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( -u ( 7 / 9 ) < ( cos ` 2 ) /\ ( cos ` 2 ) < -u ( 1 / 9 ) )