P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resinf1o 22901	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 22902	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 22903.) (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 22903	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 22904	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 22905	( -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 22906*	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 22907*	Lemma for efif1o 22911. (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 22908*	Lemma for efif1o 22911. (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 22909*	Lemma for efif1o 22911. (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 22910*	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 22911*	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 22912*	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 22913*	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 22914	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 22915*	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 22916*	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 22917	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 22918	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 22919	The quotient group R/Z is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.)
|- R = (RRfld /.s (RRfld ~QG ZZ ) )   =>    |- R e. Grp
14.3.4  The natural logarithm on complex numbers
Syntax	clog 22920	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 22921	Extend class notation with the complex power function.
class ^c
Definition	df-log 22922	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 22923*	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 22924	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 22925	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 22926	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 22927	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 22928	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 22929	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 22930	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 22931	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 22932	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 22933	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 22934	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 22935	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 22936	The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 22934. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( log ` X ) e. CC )
Theorem	logimcld 22937	The imaginary part of the logarithm is in ( -u pi (,] pi ). Deduction form of logimcl 22935. Compare logimclad 22938. (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 22938	The imaginary part of the logarithm is in ( -u pi (,] pi ). Alternate form of logimcld 22937. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( Im ` ( log ` X ) ) e. ( -u pi (,] pi ) )
Theorem	abslogimle 22939	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 22940	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 22941	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 22942	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 22943	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 22944	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 22945	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 22946	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 22947	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 22948	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 22949	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 22950	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 ) ) )
Theorem	logm1 22951	The natural logarithm of negative 1. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.)
|- ( log ` -u 1 ) = ( _i x. pi )
Theorem	lognegb 22952	If a number has imaginary part equal to pi, then it is on the negative real axis and vice-versa. (Contributed by Mario Carneiro, 23-Sep-2014.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = pi ) )
Theorem	relogoprlem 22953	Lemma for relogmul 22954 and relogdiv 22955. Remark of [Cohen] p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2"). (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) F ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) )   &    |- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) F ( log ` B ) ) e. RR )   =>    |- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A G B ) ) = ( ( log ` A ) F ( log ` B ) ) )
Theorem	relogmul 22954	The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	relogdiv 22955	The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	explog 22956	Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
Theorem	reexplog 22957	Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
Theorem	relogexp 22958	The natural logarithm of positive A raised to an integer power. Property 4 of [Cohen] p. 301-302, restricted to natural logarithms and integer powers N. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( A ^ N ) ) = ( N x. ( log ` A ) ) )
Theorem	relog 22959	Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) = ( log ` ( abs ` A ) ) )
Theorem	relogiso 22960	The natural logarithm function on positive reals determines an isomorphism from the positive reals onto the reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( log |` RR+ ) Isom < , < ( RR+ , RR )
Theorem	reloggim 22961	The natural logarithm is a group isomorphism from the group of positive reals under multiplication to the group of reals under addition. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.)
|- P = ( (mulGrp ` ℂfld ) ↾s RR+ )   =>    |- ( log |` RR+ ) e. ( P GrpIso RRfld )
Theorem	logltb 22962	The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )
Theorem	logfac 22963*	The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( N e. NN0 -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )
Theorem	eflogeq 22964*	Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( exp ` A ) = B <-> E. n e. ZZ A = ( ( log ` B ) + ( ( _i x. ( 2 x. pi ) ) x. n ) ) ) )
Theorem	logne0 22965	Logarithm of a non-1 number is not zero and thus suitable as a divisor. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( A e. RR+ /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
Theorem	logleb 22966	Natural logarithm preserves <_. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
Theorem	rplogcl 22967	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )
Theorem	logge0 22968	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 1 <_ A ) -> 0 <_ ( log ` A ) )
Theorem	logcj 22969	The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. CC /\ ( Im ` A ) =/= 0 ) -> ( log ` ( * ` A ) ) = ( * ` ( log ` A ) ) )
Theorem	efiarg 22970	The exponential of the "arg" function Im o. log. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
Theorem	cosargd 22971	The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 22970. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( Re ` X ) / ( abs ` X ) ) )
Theorem	cosarg0d 22972	The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( ( cos ` ( Im ` ( log ` X ) ) ) = 0 <-> ( Re ` X ) = 0 ) )
Theorem	argregt0 22973	Closure of the argument of a complex number with positive real part. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. CC /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
Theorem	argrege0 22974	Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) )
Theorem	argimgt0 22975	Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( Im ` ( log ` A ) ) e. ( 0 (,) pi ) )
Theorem	argimlt0 22976	Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( Im ` ( log ` A ) ) e. ( -u pi (,) 0 ) )
Theorem	logimul 22977	Multiplying a number by _i increases the logarithm of the number by _i pi / 2. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( log ` ( _i x. A ) ) = ( ( log ` A ) + ( _i x. ( pi / 2 ) ) ) )
Theorem	logneg2 22978	The logarithm of the negative of a number with positive imaginary part is _i x. pi less than the original. (Compare logneg 22950.) (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` -u A ) = ( ( log ` A ) - ( _i x. pi ) ) )
Theorem	logmul2 22979	Generalization of relogmul 22954 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	logdiv2 22980	Generalization of relogdiv 22955 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	abslogle 22981	Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` A ) ) <_ ( ( abs ` ( log ` ( abs ` A ) ) ) + pi ) )
Theorem	tanarg 22982	The basic relation between the "arg" function Im o. log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( tan ` ( Im ` ( log ` A ) ) ) = ( ( Im ` A ) / ( Re ` A ) ) )
Theorem	logdivlti 22983	The log x / x function is strictly decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) )
Theorem	logdivlt 22984	The log x / x function is strictly decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A < B <-> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )
Theorem	logdivle 22985	The log x / x function is strictly decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 3-May-2016.)
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A <_ B <-> ( ( log ` B ) / B ) <_ ( ( log ` A ) / A ) ) )
Theorem	relogcld 22986	Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( log ` A ) e. RR )
Theorem	reeflogd 22987	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( exp ` ( log ` A ) ) = A )
Theorem	relogmuld 22988	The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	relogdivd 22989	The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	logled 22990	Natural logarithm preserves <_. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
Theorem	relogefd 22991	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( log ` ( exp ` A ) ) = A )
Theorem	rplogcld 22992	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 < A )   =>    |- ( ph -> ( log ` A ) e. RR+ )
Theorem	logge0d 22993	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> 0 <_ ( log ` A ) )
Theorem	divlogrlim 22994	The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
Theorem	logno1 22995	The logarithm function is not eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 30-May-2016.)
|- -. ( x e. RR+ |-> ( log ` x ) ) e. O(1)
Theorem	dvrelog 22996	The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
Theorem	relogcn 22997	The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- ( log |` RR+ ) e. ( RR+ -cn-> RR )
Theorem	ellogdm 22998	Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )
Theorem	logdmn0 22999	A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( A e. D -> A =/= 0 )
Theorem	logdmnrp 23000	A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( A e. D -> -. -u A e. RR+ )