P. 243 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24201-24300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reeff1o 24201	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( exp |` RR ) : RR -1-1-onto-> RR+
Theorem	reefiso 24202	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 24203	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 24204	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 24205	Lemma for pire 24210, pigt2lt4 24208 and sinpi 24209. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
Theorem	pilem2 24206	Lemma for pire 24210, pigt2lt4 24208 and sinpi 24209. (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	pilem3 24207	Lemma for pire 24210, pigt2lt4 24208 and sinpi 24209. 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	pigt2lt4 24208	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 24209	The sine of pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` pi ) = 0
Theorem	pire 24210	pi is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
|- pi e. RR
Theorem	picn 24211	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 24212	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 24213	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 24214	-u pi is a real number (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 24215	Lemma for sinhalfpi 24220 and coshalfpi 24221. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 24216	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 24217	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 24218	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 24219	Adding pi / 2 to itself is pi (common case). See 2halves 11260. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 24220	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 24221	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 24222	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 24223	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 24224	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 24225	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 24226	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 24227	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 24228	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 24229	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 24230	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 24231	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 24232	Lemma for sinper 24233 and cosper 24234. (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 24233	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 24234	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 24235	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 24236	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 24237	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 24238	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 24239	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 24240	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 24241	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 24242	Cosine of a complex number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 24243	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 24244	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 24245	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 24246	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 24247	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 24248	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 14902, 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 24249	Lemma for sincosq1sgn 24250. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( ( A e. RR /\ 0 < A /\ A < ( pi / 2 ) ) -> 0 < ( sin ` A ) )
Theorem	sincosq1sgn 24250	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 24251	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 24252	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 24253	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 24254	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 24255	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 24256	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 24257	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 24258	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 24259	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 24260	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 24261	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 24262	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 24263	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 24264	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 24265	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 24266	The tangent of pi / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( tan ` ( pi / 4 ) ) = 1
Theorem	sincos6thpi 24267	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 24268	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 24269	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 24270	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 24271	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 24272	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 24273	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 24274	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 24275	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 24276	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 24277	Lemma for cosord 24278. (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 24278	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 24279	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 24280	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 24281	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 24282	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 24283	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 24284.) (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 24284	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 24285	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 24286	( -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 24287*	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 24288*	Lemma for efif1o 24292. (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 24289*	Lemma for efif1o 24292. (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 24290*	Lemma for efif1o 24292. (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 24291*	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 24292*	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 24293*	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 24294*	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 24295	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 24296*	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 24297*	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 24298	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 24299	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 ) )
Theorem	rzgrp 24300	The quotient group R/Z is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- R = (RRfld /.s (RRfld ~QG ZZ ) )   =>    |- R e. Grp