P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sin2pi 22601	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 22602	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 22603	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 22604	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 22605	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 22606	Lemma for sinper 22607 and cosper 22608. (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 22607	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 22608	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 22609	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 22610	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 22611	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 22612	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 22613	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 22614	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 22615	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 22616	Cosine of a complex number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 22617	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 22618	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 22619	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 22620	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 22621	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 22622	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 13764, 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 22623	Lemma for sincosq1sgn 22624. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( ( A e. RR /\ 0 < A /\ A < ( pi / 2 ) ) -> 0 < ( sin ` A ) )
Theorem	sincosq1sgn 22624	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 22625	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 22626	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 22627	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 22628	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 22629	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 22630	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 22631	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 22632	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 22633	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 22634	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 22635	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 22636	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 22637	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 22638	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 22639	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 22640	The tangent of pi / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( tan ` ( pi / 4 ) ) = 1
Theorem	sincos6thpi 22641	The sine and cosine of pi / 6. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( sin ` ( pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( pi / 6 ) ) = ( ( sqr ` 3 ) / 2 ) )
Theorem	sincos3rdpi 22642	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 22643	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 22644	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 22645	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 22646	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 22647	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 22648	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 22649	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 22650	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 22651	Lemma for cosord 22652. (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 22652	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 22653	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 22654	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 22655	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 22656	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 22657	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 22658.) (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( ( A e. ( 0 [,) ( pi / 2 ) ) /\ B e. ( 0 [,) ( pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )
Theorem	tanord 22658	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 22659	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 22660	( -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 22661*	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.)
|- F = ( x e. CC |-> ( exp ` ( A x. x ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( F ` ( B + C ) ) = ( ( F ` B ) x. ( F ` C ) ) )
Theorem	efif1olem1 22662*	Lemma for efif1o 22666. (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 22663*	Lemma for efif1o 22666. (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 22664*	Lemma for efif1o 22666. (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 22665*	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 22666*	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 22667*	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 22668*	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 22669	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 } )
14.3.4  The natural logarithm on complex numbers
Syntax	clog 22670	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 22671	Extend class notation with the complex power function.
class ^c
Definition	df-log 22672	Define the natural logarithm function on complex numbers. See http://en.wikipedia.org/wiki/Natural_logarithm ("The natural logarithm function can also be defined as the inverse function of the exponential function"). (Contributed by Paul Chapman, 21-Apr-2008.)
|- log = `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
Definition	df-cxp 22673*	Define the power function on complex numbers. Note that the value of this function when x = 0 and ( Re ` y ) <_ 0 , y =/= 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ^c = ( x e. CC , y e. CC |-> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) )
Theorem	logrn 22674	The range of the natural logarithm function, also the principal domain of the exponential function. This allows us to write the longer class expression as simply ran log. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.)
|- ran log = ( `' Im " ( -u pi (,] pi ) )
Theorem	ellogrn 22675	Write out the property A e. ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. ran log <-> ( A e. CC /\ -u pi < ( Im ` A ) /\ ( Im ` A ) <_ pi ) )
Theorem	dflog2 22676	The natural logarithm function in terms of the exponential function restricted to its principal domain. (Contributed by Paul Chapman, 21-Apr-2008.)
|- log = `' ( exp |` ran log )
Theorem	relogrn 22677	The range of the natural logarithm function includes the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 1-Apr-2015.)
|- ( A e. RR -> A e. ran log )
Theorem	logrncn 22678	The range of the natural logarithm function is a subset of the complex numbers. (Contributed by Mario Carneiro, 13-May-2014.)
|- ( A e. ran log -> A e. CC )
Theorem	eff1o2 22679	The exponential function restricted to its principal domain maps one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.)
|- ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } )
Theorem	logf1o 22680	The natural logarithm function maps the nonzero complex numbers one-to-one onto its range. (Contributed by Paul Chapman, 21-Apr-2008.)
|- log : ( CC \ { 0 } ) -1-1-onto-> ran log
Theorem	dfrelog 22681	The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( log |` RR+ ) = `' ( exp |` RR )
Theorem	relogf1o 22682	The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR
Theorem	logrncl 22683	Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )
Theorem	logcl 22684	Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
Theorem	logimcl 22685	Closure of the imaginary part of the logarithm function. (Contributed by Mario Carneiro, 23-Sep-2014.) (Revised by Mario Carneiro, 1-Apr-2015.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( -u pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ pi ) )
Theorem	logcld 22686	The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 22684. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( log ` X ) e. CC )
Theorem	logimcld 22687	The imaginary part of the logarithm is in ( -u pi (,] pi ). Deduction form of logimcl 22685. Compare logimclad 22688. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( -u pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ pi ) )
Theorem	logimclad 22688	The imaginary part of the logarithm is in ( -u pi (,] pi ). Alternate form of logimcld 22687. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( Im ` ( log ` X ) ) e. ( -u pi (,] pi ) )
Theorem	abslogimle 22689	The imaginary part of the logarithm function has absolute value less than pi. (Contributed by Mario Carneiro, 3-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( Im ` ( log ` A ) ) ) <_ pi )
Theorem	logrnaddcl 22690	The range of the natural logarithm is closed under addition with reals. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ( A e. ran log /\ B e. RR ) -> ( A + B ) e. ran log )
Theorem	relogcl 22691	Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR+ -> ( log ` A ) e. RR )
Theorem	eflog 22692	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
Theorem	reeflog 22693	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
Theorem	logef 22694	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( A e. ran log -> ( log ` ( exp ` A ) ) = A )
Theorem	relogef 22695	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR -> ( log ` ( exp ` A ) ) = A )
Theorem	logeftb 22696	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. ran log ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
Theorem	relogeftb 22697	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
Theorem	log1 22698	The natural logarithm of 1. One case of Property 1a of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( log ` 1 ) = 0
Theorem	loge 22699	The natural logarithm of _e. One case of Property 1b of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( log ` _e ) = 1
Theorem	logneg 22700	The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014.) (Revised by Mario Carneiro, 3-Apr-2015.)
|- ( A e. RR+ -> ( log ` -u A ) = ( ( log ` A ) + ( _i x. pi ) ) )