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	eftlub 12201*	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 12202*	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 12203*	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 12204	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 12205*	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 12206	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 12207	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 12208	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 12209	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 12210	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 12211	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 12212	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 12213	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 12214	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 12215	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 12216	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 12217	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 12218	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 12219	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 12220	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 12221	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( sin ` A ) e. CC )
Theorem	coscld 12222	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( cos ` A ) e. CC )
Theorem	tanclapd 12223	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 12224	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 12225	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 12226	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 12227	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 12228*	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 12229*	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 12230*	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 12231	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( sin ` A ) e. RR )
Theorem	recoscl 12232	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( cos ` A ) e. RR )
Theorem	retanclap 12233	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 12234	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( sin ` A ) e. RR )
Theorem	recoscld 12235	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( cos ` A ) e. RR )
Theorem	retanclapd 12236	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 12237	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 12238	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 12239	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 12240	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
|- ( sin ` 0 ) = 0
Theorem	cos0 12241	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|- ( cos ` 0 ) = 1
Theorem	tan0 12242	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
|- ( tan ` 0 ) = 0
Theorem	efival 12243	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 12244	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 12245	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 12246	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 12247	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 12248	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 12249	A useful intermediate step in tanaddap 12250 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 12250	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 12251	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 12252	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 12253	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 12254	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 12255	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 12248 and cossub 12252. (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 12256	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 12248 and cossub 12252. (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 12257	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 12258	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 12259	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 12260	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 12261	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 12262	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 12263	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 12264	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 12265	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 12266	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 12267*	Lemma for sin01bnd 12268 and cos01bnd 12269. (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 12268	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 12269	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 12270	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( ( 1 / 3 ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 2 / 3 ) )
Theorem	cos2bnd 12271	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 12272*	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 12273	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 12274	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 12275	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 12276	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) )
Theorem	sincos2sgn 12277	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
Theorem	sin4lt0 12278	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( sin ` 4 ) < 0
Theorem	cos12dec 12279	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 12280	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 12281	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 12282	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 12283	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 12284	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 12285 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 12285	Alternate proof of demoivre 12284. 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 ) ) ) ) )
4.10.1.1  The circle constant (tau = 2 pi)
Syntax	ctau 12286	Extend class notation to include the constant tau, tau = 6.28318....
class tau
Definition	df-tau 12287	Define the circle constant tau, tau = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including tau, a three-legged variant of pi, or 2 pi. Note the difference between this constant tau and the formula variable ta. Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.)
|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
4.10.2  _e is irrational
Theorem	eirraplem 12288*	Lemma for eirrap 12289. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.)
|- F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )   &    |- ( ph -> P e. ZZ )   &    |- ( ph -> Q e. NN )   =>    |- ( ph -> _e # ( P / Q ) )
Theorem	eirrap 12289	_e is irrational. That is, for any rational number, _e is apart from it. In the absence of excluded middle, we can distinguish between this and saying that _e is not rational, which is eirr 12290. (Contributed by Jim Kingdon, 6-Jan-2023.)
|- ( Q e. QQ -> _e # Q )
Theorem	eirr 12290	_e is not rational. In the absence of excluded middle, we can distinguish between this and saying that _e is irrational in the sense of being apart from any rational number, which is eirrap 12289. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.)
|- _e e/ QQ
Theorem	egt2lt3 12291	Euler's constant _e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.)
|- ( 2 < _e /\ _e < 3 )
Theorem	epos 12292	Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- 0 < _e
Theorem	epr 12293	Euler's constant _e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- _e e. RR+
Theorem	ene0 12294	_e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 0
Theorem	eap0 12295	_e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.)
|- _e # 0
Theorem	ene1 12296	_e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 1
Theorem	eap1 12297	_e is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.)
|- _e # 1
PART 5  ELEMENTARY NUMBER THEORY This part introduces elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.
5.1  Elementary properties of divisibility
5.1.1  The divides relation
Syntax	cdvds 12298	Extend the definition of a class to include the divides relation. See df-dvds 12299.
class ||
Definition	df-dvds 12299*	Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
Theorem	divides 12300*	Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 16094). As proven in dvdsval3 12302, M || N <-> ( N mod M ) = 0. See divides 12300 and dvdsval2 12301 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )