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	efadd 12201	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 12202	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 12203	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 12204	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 12203 (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 12205	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 12206	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 12207	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 12208	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 12209	Value of the exponential function for integers. Special case of efval 12187. 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 12210	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 12211	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 12212	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 12213*	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 12214*	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 12215*	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 12216*	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 12217*	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 12218*	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 12219	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 12220*	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 12221	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 12222	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 12223	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 12224	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 12225	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 12226	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 12227	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 12228	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 12229	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 12230	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 12231	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 12232	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 12233	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 12234	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 12235	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 12236	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( sin ` A ) e. CC )
Theorem	coscld 12237	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( cos ` A ) e. CC )
Theorem	tanclapd 12238	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 12239	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 12240	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 12241	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 12242	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 12243*	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 12244*	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 12245*	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 12246	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( sin ` A ) e. RR )
Theorem	recoscl 12247	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( cos ` A ) e. RR )
Theorem	retanclap 12248	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 12249	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( sin ` A ) e. RR )
Theorem	recoscld 12250	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( cos ` A ) e. RR )
Theorem	retanclapd 12251	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 12252	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 12253	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 12254	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 12255	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
|- ( sin ` 0 ) = 0
Theorem	cos0 12256	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|- ( cos ` 0 ) = 1
Theorem	tan0 12257	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
|- ( tan ` 0 ) = 0
Theorem	efival 12258	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 12259	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 12260	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 12261	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 12262	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 12263	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 12264	A useful intermediate step in tanaddap 12265 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 12265	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 12266	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 12267	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 12268	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 12269	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 12270	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 12263 and cossub 12267. (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 12271	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 12263 and cossub 12267. (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 12272	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 12273	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 12274	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 12275	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 12276	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 12277	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 12278	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 12279	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 12280	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 12281	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 12282*	Lemma for sin01bnd 12283 and cos01bnd 12284. (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 12283	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 12284	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 12285	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( ( 1 / 3 ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 2 / 3 ) )
Theorem	cos2bnd 12286	Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( -u ( 7 / 9 ) < ( cos ` 2 ) /\ ( cos ` 2 ) < -u ( 1 / 9 ) )
Theorem	sinltxirr 12287*	The sine of a positive irrational number is less than its argument. Here irrational means apart from any rational number. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( ( A e. RR+ /\ A. q e. QQ A # q ) -> ( sin ` A ) < A )
Theorem	sin01gt0 12288	The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Wolf Lammen, 25-Sep-2020.)
|- ( A e. ( 0 (,] 1 ) -> 0 < ( sin ` A ) )
Theorem	cos01gt0 12289	The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( A e. ( 0 (,] 1 ) -> 0 < ( cos ` A ) )
Theorem	sin02gt0 12290	The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` A ) )
Theorem	sincos1sgn 12291	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) )
Theorem	sincos2sgn 12292	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
Theorem	sin4lt0 12293	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( sin ` 4 ) < 0
Theorem	cos12dec 12294	Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.)
|- ( ( A e. ( 1 [,] 2 ) /\ B e. ( 1 [,] 2 ) /\ A < B ) -> ( cos ` B ) < ( cos ` A ) )
Theorem	absefi 12295	The absolute value of the exponential of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.)
|- ( A e. RR -> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 )
Theorem	absef 12296	The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007.)
|- ( A e. CC -> ( abs ` ( exp ` A ) ) = ( exp ` ( Re ` A ) ) )
Theorem	absefib 12297	A complex number is real iff the exponential of its product with _i has absolute value one. (Contributed by NM, 21-Aug-2008.)
|- ( A e. CC -> ( A e. RR <-> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 ) )
Theorem	efieq1re 12298	A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.)
|- ( ( A e. CC /\ ( exp ` ( _i x. A ) ) = 1 ) -> A e. RR )
Theorem	demoivre 12299	De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 12300 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.)
|- ( ( A e. CC /\ N e. ZZ ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
Theorem	demoivreALT 12300	Alternate proof of demoivre 12299. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )