P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reefiso 23401	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
|- ( exp |` RR ) Isom < , < ( RR , RR+ )
Theorem	efcvx 23402	The exponential function on the reals is a strictly convex function. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( exp ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < ( ( T x. ( exp ` A ) ) + ( ( 1 - T ) x. ( exp ` B ) ) ) )
Theorem	reefgim 23403	The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.)
|- P = ( (mulGrp ` ℂfld ) ↾s RR+ )   =>    |- ( exp |` RR ) e. (RRfld GrpIso P )
14.3.2  Properties of pi = 3.14159...
Theorem	pilem1 23404	Lemma for pire 23411, pigt2lt4 23409 and sinpi 23410. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
Theorem	pilem2 23405	Lemma for pire 23411, pigt2lt4 23409 and sinpi 23410. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
|- ( ph -> A e. ( 2 (,) 4 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( sin ` A ) = 0 )   &    |- ( ph -> ( sin ` B ) = 0 )   &    |- ( ph -> pi < A )   =>    |- ( ph -> ( ( pi + A ) / 2 ) <_ B )
Theorem	pilem2OLD 23406	Lemma for pire 23411, pigt2lt4 23409 and sinpi 23410. (Contributed by Mario Carneiro, 12-Jun-2014.) Obsolete version of pilem2 23405 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A e. ( 2 (,) 4 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( sin ` A ) = 0 )   &    |- ( ph -> ( sin ` B ) = 0 )   &    |- ( ph -> pi < A )   =>    |- ( ph -> ( ( pi + A ) / 2 ) <_ B )
Theorem	pilem3 23407	Lemma for pire 23411, pigt2lt4 23409 and sinpi 23410. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pilem3OLD 23408	Lemma for pire 23411, pigt2lt4 23409 and sinpi 23410. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) Obsolete version of pilem3 23407 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
Theorem	pigt2lt4 23409	pi is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( 2 < pi /\ pi < 4 )
Theorem	sinpi 23410	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 23411	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 23412	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 23413	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 23414	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 23415	-u pi is a real number (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 23416	Lemma for sinhalfpi 23421 and coshalfpi 23422. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 23417	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 23418	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 23419	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 23420	Adding pi / 2 to itself is pi (common case). See 2halves 10848. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 23421	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 23422	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 23423	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 23424	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 23425	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 23426	The exponential of _i x. pi. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( exp ` ( _i x. pi ) ) = -u 1
Theorem	eulerid 23427	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( ( exp ` ( _i x. pi ) ) + 1 ) = 0
Theorem	sin2pi 23428	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 23429	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 23430	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 23431	The exponential of 2 K pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. pi ) ) x. K ) ) = 1 )
Theorem	efper 23432	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. pi ) ) x. K ) ) ) = ( exp ` A ) )
Theorem	sinperlem 23433	Lemma for sinper 23434 and cosper 23435. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )   &    |- ( ( A + ( K x. ( 2 x. pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) ) / D ) )   =>    |- ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( F ` A ) )
Theorem	sinper 23434	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( sin ` A ) )
Theorem	cosper 23435	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( cos ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( cos ` A ) )
Theorem	sin2kpi 23436	If K is an integer, the sine of 2 K pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( sin ` ( K x. ( 2 x. pi ) ) ) = 0 )
Theorem	cos2kpi 23437	If K is an integer, the cosine of 2 K pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( cos ` ( K x. ( 2 x. pi ) ) ) = 1 )
Theorem	sin2pim 23438	Sine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( ( 2 x. pi ) - A ) ) = -u ( sin ` A ) )
Theorem	cos2pim 23439	Cosine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( ( 2 x. pi ) - A ) ) = ( cos ` A ) )
Theorem	sinmpi 23440	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 23441	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 23442	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 23443	Cosine of a complex number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 23444	The exponential function of _i times a real number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( exp ` ( _i x. ( A - pi ) ) ) = -u ( exp ` ( _i x. A ) ) )
Theorem	sinhalfpip 23445	The sine of pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( sin ` ( ( pi / 2 ) + A ) ) = ( cos ` A ) )
Theorem	sinhalfpim 23446	The sine of pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( sin ` ( ( pi / 2 ) - A ) ) = ( cos ` A ) )
Theorem	coshalfpip 23447	The cosine of pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( ( pi / 2 ) + A ) ) = -u ( sin ` A ) )
Theorem	coshalfpim 23448	The cosine of pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( ( pi / 2 ) - A ) ) = ( sin ` A ) )
Theorem	ptolemy 23449	Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 14225, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ ( ( A + B ) + ( C + D ) ) = pi ) -> ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` C ) x. ( sin ` D ) ) ) = ( ( sin ` ( B + C ) ) x. ( sin ` ( A + C ) ) ) )
Theorem	sincosq1lem 23450	Lemma for sincosq1sgn 23451. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( ( A e. RR /\ 0 < A /\ A < ( pi / 2 ) ) -> 0 < ( sin ` A ) )
Theorem	sincosq1sgn 23451	The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
Theorem	sincosq2sgn 23452	The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( ( pi / 2 ) (,) pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )
Theorem	sincosq3sgn 23453	The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( pi (,) ( 3 x. ( pi / 2 ) ) ) -> ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) )
Theorem	sincosq4sgn 23454	The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( ( 3 x. ( pi / 2 ) ) (,) ( 2 x. pi ) ) -> ( ( sin ` A ) < 0 /\ 0 < ( cos ` A ) ) )
Theorem	coseq00topi 23455	Location of the zeroes of cosine in ( 0 [,] pi ). (Contributed by David Moews, 28-Feb-2017.)
|- ( A e. ( 0 [,] pi ) -> ( ( cos ` A ) = 0 <-> A = ( pi / 2 ) ) )
Theorem	coseq0negpitopi 23456	Location of the zeroes of cosine in ( -u pi (,] pi ). (Contributed by David Moews, 28-Feb-2017.)
|- ( A e. ( -u pi (,] pi ) -> ( ( cos ` A ) = 0 <-> A e. { ( pi / 2 ) , -u ( pi / 2 ) } ) )
Theorem	tanrpcl 23457	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> ( tan ` A ) e. RR+ )
Theorem	tangtx 23458	The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> A < ( tan ` A ) )
Theorem	tanabsge 23459	The tangent function is greater than or equal to its argument in absolute value. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( A e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) -> ( abs ` A ) <_ ( abs ` ( tan ` A ) ) )
Theorem	sinq12gt0 23460	The sine of a number strictly between 0 and pi is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. ( 0 (,) pi ) -> 0 < ( sin ` A ) )
Theorem	sinq12ge0 23461	The sine of a number between 0 and pi is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
|- ( A e. ( 0 [,] pi ) -> 0 <_ ( sin ` A ) )
Theorem	sinq34lt0t 23462	The sine of a number strictly between pi and 2 x. pi is negative. (Contributed by NM, 17-Aug-2008.)
|- ( A e. ( pi (,) ( 2 x. pi ) ) -> ( sin ` A ) < 0 )
Theorem	cosq14gt0 23463	The cosine of a number strictly between -u pi / 2 and pi / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( A e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) -> 0 < ( cos ` A ) )
Theorem	cosq14ge0 23464	The cosine of a number between -u pi / 2 and pi / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
|- ( A e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) -> 0 <_ ( cos ` A ) )
Theorem	sincosq1eq 23465	Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( sin ` ( A x. ( pi / 2 ) ) ) = ( cos ` ( B x. ( pi / 2 ) ) ) )
Theorem	sincos4thpi 23466	The sine and cosine of pi / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( sin ` ( pi / 4 ) ) = ( 1 / ( sqr ` 2 ) ) /\ ( cos ` ( pi / 4 ) ) = ( 1 / ( sqr ` 2 ) ) )
Theorem	tan4thpi 23467	The tangent of pi / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( tan ` ( pi / 4 ) ) = 1
Theorem	sincos6thpi 23468	The sine and cosine of pi / 6. (Contributed by Paul Chapman, 25-Jan-2008.) Replace OLD theorem. (Revised by Wolf Lammen, 24-Sep-2020.)
|- ( ( sin ` ( pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( pi / 6 ) ) = ( ( sqr ` 3 ) / 2 ) )
Theorem	sincos3rdpi 23469	The sine and cosine of pi / 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( ( sin ` ( pi / 3 ) ) = ( ( sqr ` 3 ) / 2 ) /\ ( cos ` ( pi / 3 ) ) = ( 1 / 2 ) )
Theorem	pige3 23470	pi is greater or equal to 3. This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2 pi. We translate this to algebra by looking at the function _e ^ ( _i x ) as x goes from 0 to pi / 3; it moves at unit speed and travels distance 1, hence 1 <_ pi / 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- 3 <_ pi
Theorem	abssinper 23471	The absolute value of sine has period pi. (Contributed by NM, 17-Aug-2008.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. pi ) ) ) ) = ( abs ` ( sin ` A ) ) )
Theorem	sinkpi 23472	The sine of an integer multiple of pi is 0. (Contributed by NM, 11-Aug-2008.)
|- ( K e. ZZ -> ( sin ` ( K x. pi ) ) = 0 )
Theorem	coskpi 23473	The absolute value of the cosine of an integer multiple of pi is 1. (Contributed by NM, 19-Aug-2008.)
|- ( K e. ZZ -> ( abs ` ( cos ` ( K x. pi ) ) ) = 1 )
Theorem	sineq0 23474	A complex number whose sine is zero is an integer multiple of pi. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( ( sin ` A ) = 0 <-> ( A / pi ) e. ZZ ) )
Theorem	coseq1 23475	A complex number whose cosine is one is an integer multiple of 2 pi. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. CC -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. pi ) ) e. ZZ ) )
Theorem	efeq1 23476	A complex number whose exponential is one is an integer multiple of 2 pi _i. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( ( exp ` A ) = 1 <-> ( A / ( _i x. ( 2 x. pi ) ) ) e. ZZ ) )
Theorem	cosne0 23477	The cosine function has no zeroes within the vertical strip of the complex plane between real part -u pi / 2 and pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( cos ` A ) =/= 0 )
Theorem	cosordlem 23478	Lemma for cosord 23479. (Contributed by Mario Carneiro, 10-May-2014.)
|- ( ph -> A e. ( 0 [,] pi ) )   &    |- ( ph -> B e. ( 0 [,] pi ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( cos ` B ) < ( cos ` A ) )
Theorem	cosord 23479	Cosine is decreasing over the closed interval from 0 to pi. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. ( 0 [,] pi ) /\ B e. ( 0 [,] pi ) ) -> ( A < B <-> ( cos ` B ) < ( cos ` A ) ) )
Theorem	cos11 23480	Cosine is one-to-one over the closed interval from 0 to pi. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. ( 0 [,] pi ) /\ B e. ( 0 [,] pi ) ) -> ( A = B <-> ( cos ` A ) = ( cos ` B ) ) )
Theorem	sinord 23481	Sine is increasing over the closed interval from -u ( pi / 2 ) to ( pi / 2 ). (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( ( A e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) /\ B e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) ) -> ( A < B <-> ( sin ` A ) < ( sin ` B ) ) )
Theorem	recosf1o 23482	The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( cos |` ( 0 [,] pi ) ) : ( 0 [,] pi ) -1-1-onto-> ( -u 1 [,] 1 )
Theorem	resinf1o 23483	The sine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( sin |` ( -u ( pi / 2 ) [,] ( pi / 2 ) ) ) : ( -u ( pi / 2 ) [,] ( pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )
Theorem	tanord1 23484	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 23485.) (Contributed by Mario Carneiro, 29-Jul-2014.) Revised to replace an OLD theorem. (Revised by Wolf Lammen, 20-Sep-2020.)
|- ( ( A e. ( 0 [,) ( pi / 2 ) ) /\ B e. ( 0 [,) ( pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )
Theorem	tanord 23485	The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( A e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) /\ B e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )
Theorem	tanregt0 23486	The positivity of tan ( A ) extends to complex numbers with the same real part. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) ( pi / 2 ) ) ) -> 0 < ( Re ` ( tan ` A ) ) )
Theorem	negpitopissre 23487	( -u pi (,] pi ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
|- ( -u pi (,] pi ) C_ RR
14.3.3  Mapping of the exponential function
Theorem	efgh 23488*	The exponential function of a scaled complex number is a group homomorphism from the group of complex numbers under addition to the set of complex numbers under multiplication. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 11-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.)
|- F = ( x e. X |-> ( exp ` ( A x. x ) ) )   =>    |- ( ( ( A e. CC /\ X e. (SubGrp ` ℂfld ) ) /\ B e. X /\ C e. X ) -> ( F ` ( B + C ) ) = ( ( F ` B ) x. ( F ` C ) ) )
Theorem	efif1olem1 23489*	Lemma for efif1o 23493. (Contributed by Mario Carneiro, 13-May-2014.)
|- D = ( A (,] ( A + ( 2 x. pi ) ) )   =>    |- ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. pi ) )
Theorem	efif1olem2 23490*	Lemma for efif1o 23493. (Contributed by Mario Carneiro, 13-May-2014.)
|- D = ( A (,] ( A + ( 2 x. pi ) ) )   =>    |- ( ( A e. RR /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. pi ) ) e. ZZ )
Theorem	efif1olem3 23491*	Lemma for efif1o 23493. (Contributed by Mario Carneiro, 8-May-2015.)
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )   &    |- C = ( `' abs " { 1 } )   =>    |- ( ( ph /\ x e. C ) -> ( Im ` ( sqr ` x ) ) e. ( -u 1 [,] 1 ) )
Theorem	efif1olem4 23492*	The exponential function of an imaginary number maps any interval of length 2 pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.)
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )   &    |- C = ( `' abs " { 1 } )   &    |- ( ph -> D C_ RR )   &    |- ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. pi ) )   &    |- ( ( ph /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. pi ) ) e. ZZ )   &    |- S = ( sin |` ( -u ( pi / 2 ) [,] ( pi / 2 ) ) )   =>    |- ( ph -> F : D -1-1-onto-> C )
Theorem	efif1o 23493*	The exponential function of an imaginary number maps any open-below, closed-above interval of length 2 pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Mario Carneiro, 13-May-2014.)
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )   &    |- C = ( `' abs " { 1 } )   &    |- D = ( A (,] ( A + ( 2 x. pi ) ) )   =>    |- ( A e. RR -> F : D -1-1-onto-> C )
Theorem	efifo 23494*	The exponential function of an imaginary number maps the reals onto the unit circle. (Contributed by Mario Carneiro, 13-May-2014.)
|- F = ( z e. RR |-> ( exp ` ( _i x. z ) ) )   &    |- C = ( `' abs " { 1 } )   =>    |- F : RR -onto-> C
Theorem	eff1olem 23495*	The exponential function maps the set S, of complex numbers with imaginary part in a real interval of length 2 x. pi, one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.)
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )   &    |- S = ( `' Im " D )   &    |- ( ph -> D C_ RR )   &    |- ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. pi ) )   &    |- ( ( ph /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. pi ) ) e. ZZ )   =>    |- ( ph -> ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } ) )
Theorem	eff1o 23496	The exponential function maps the set S, of complex numbers with imaginary part in the closed-above, open-below interval from -u pi to pi one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.)
|- S = ( `' Im " ( -u pi (,] pi ) )   =>    |- ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } )
Theorem	efabl 23497*	The image of a subgroup of the group +, under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.)
|- F = ( x e. X |-> ( exp ` ( A x. x ) ) )   &    |- G = ( (mulGrp ` ℂfld ) ↾s ran F )   &    |- ( ph -> A e. CC )   &    |- ( ph -> X e. (SubGrp ` ℂfld ) )   =>    |- ( ph -> G e. Abel )
Theorem	efsubm 23498*	The image of a subgroup of the group +, under the exponential function of a scaled complex number is a submonoid of the multiplicative group of ℂfld. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- F = ( x e. X |-> ( exp ` ( A x. x ) ) )   &    |- G = ( (mulGrp ` ℂfld ) ↾s ran F )   &    |- ( ph -> A e. CC )   &    |- ( ph -> X e. (SubGrp ` ℂfld ) )   =>    |- ( ph -> ran F e. (SubMnd ` (mulGrp ` ℂfld ) ) )
Theorem	circgrp 23499	The circle group T is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by Mario Carneiro, 13-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.)
|- C = ( `' abs " { 1 } )   &    |- T = ( (mulGrp ` ℂfld ) ↾s C )   =>    |- T e. Abel
Theorem	circsubm 23500	The circle group T is a submonoid of the multiplicative group of ℂfld. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- C = ( `' abs " { 1 } )   &    |- T = ( (mulGrp ` ℂfld ) ↾s C )   =>    |- C e. (SubMnd ` (mulGrp ` ℂfld ) )