P. 244 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24301-24400   *Has distinct variable group(s)

Type	Label	Description
Statement
14.3.4  The natural logarithm on complex numbers
Syntax	clog 24301	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 24302	Extend class notation with the complex power function.
class ^c
Definition	df-log 24303	Define the natural logarithm function on complex numbers. It is defined as the principal value, that is, the inverse of the exponential whose imaginary part lies in the interval (-pi, pi]. See http://en.wikipedia.org/wiki/Natural_logarithm and https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Paul Chapman, 21-Apr-2008.)
|- log = `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
Definition	df-cxp 24304*	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 24305	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 24306	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 24307	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 24308	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 24309	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 24310	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 24311	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 24312	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 24313	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 24314	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 24315	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 24316	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 24317	The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 24315. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( log ` X ) e. CC )
Theorem	logimcld 24318	The imaginary part of the logarithm is in ( -u pi (,] pi ). Deduction form of logimcl 24316. Compare logimclad 24319. (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 24319	The imaginary part of the logarithm is in ( -u pi (,] pi ). Alternate form of logimcld 24318. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> X e. CC )   &    |- ( ph -> X =/= 0 )   =>    |- ( ph -> ( Im ` ( log ` X ) ) e. ( -u pi (,] pi ) )
Theorem	abslogimle 24320	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 24321	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 24322	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 24323	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	logeq0im1 24324	If the logarithm of a number is 0, the number must be 1. (Contributed by David A. Wheeler, 22-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 /\ ( log ` A ) = 0 ) -> A = 1 )
Theorem	logccne0 24325	The logarithm isn't 0 if its argument isn't 0 or 1. (Contributed by David A. Wheeler, 17-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
Theorem	logne0 24326	Logarithm of a non-1 positive real number is not zero and thus suitable as a divisor. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Proof shortened by AV, 14-Jun-2020.)
|- ( ( A e. RR+ /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
Theorem	reeflog 24327	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 24328	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 24329	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 24330	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 24331	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 24332	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 24333	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 24334	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 24335	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 24336	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 24337	Lemma for relogmul 24338 and relogdiv 24339. 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 24338	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 24339	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 24340	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 24341	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 24342	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 24343	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 24344	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 24345	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 24346	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 24347*	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 24348*	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	logleb 24349	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 24350	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 24351	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 24352	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 24353	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 24354	The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 24353. (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 24355	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 24356	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 24357	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 24358	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 24359	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 24360	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 24361	The logarithm of the negative of a number with positive imaginary part is _i x. pi less than the original. (Compare logneg 24334.) (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ( A e. CC /\ 0 < ( Im ` A ) ) -> ( log ` -u A ) = ( ( log ` A ) - ( _i x. pi ) ) )
Theorem	logmul2 24362	Generalization of relogmul 24338 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 24363	Generalization of relogdiv 24339 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 24364	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 24365	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 24366	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 24367	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 24368	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 24369	Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( log ` A ) e. RR )
Theorem	reeflogd 24370	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 24371	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 24372	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 24373	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 24374	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 24375	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 24376	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	logge0b 24377	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( 0 <_ ( log ` A ) <-> 1 <_ A ) )
Theorem	loggt0b 24378	The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( 0 < ( log ` A ) <-> 1 < A ) )
Theorem	logle1b 24379	The logarithm of a number is less than or equal to 1 iff the number is less than or equal to Euler's constant. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( ( log ` A ) <_ 1 <-> A <_ _e ) )
Theorem	loglt1b 24380	The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( ( log ` A ) < 1 <-> A < _e ) )
Theorem	divlogrlim 24381	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 24382	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 24383	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 24384	The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- ( log |` RR+ ) e. ( RR+ -cn-> RR )
Theorem	ellogdm 24385	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 24386	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 24387	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+ )
Theorem	logdmss 24388	The continuity domain of log is a subset of the regular domain of log. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- D C_ ( CC \ { 0 } )
Theorem	logcnlem2 24389	Lemma for logcn 24393. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) )   &    |- T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) )   &    |- ( ph -> A e. D )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> if ( S <_ T , S , T ) e. RR+ )
Theorem	logcnlem3 24390	Lemma for logcn 24393. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) )   &    |- T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) )   &    |- ( ph -> A e. D )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> B e. D )   &    |- ( ph -> ( abs ` ( A - B ) ) < if ( S <_ T , S , T ) )   =>    |- ( ph -> ( -u pi < ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) /\ ( ( Im ` ( log ` B ) ) - ( Im ` ( log ` A ) ) ) <_ pi ) )
Theorem	logcnlem4 24391	Lemma for logcn 24393. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) )   &    |- T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) )   &    |- ( ph -> A e. D )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> B e. D )   &    |- ( ph -> ( abs ` ( A - B ) ) < if ( S <_ T , S , T ) )   =>    |- ( ph -> ( abs ` ( ( Im ` ( log ` A ) ) - ( Im ` ( log ` B ) ) ) ) < R )
Theorem	logcnlem5 24392*	Lemma for logcn 24393. (Contributed by Mario Carneiro, 18-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> RR )
Theorem	logcn 24393	The logarithm function is continuous away from the branch cut at negative reals. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( log |` D ) e. ( D -cn-> CC )
Theorem	dvloglem 24394	Lemma for dvlog 24397. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( log " D ) e. ( TopOpen ` ℂfld )
Theorem	logdmopn 24395	The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- D e. ( TopOpen ` ℂfld )
Theorem	logf1o2 24396	The logarithm maps its continuous domain bijectively onto the set of numbers with imaginary part -u pi < Im ( z ) < pi. The negative reals are mapped to the numbers with imaginary part equal to pi. (Contributed by Mario Carneiro, 2-May-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( log |` D ) : D -1-1-onto-> ( `' Im " ( -u pi (,) pi ) )
Theorem	dvlog 24397*	The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( CC _D ( log |` D ) ) = ( x e. D |-> ( 1 / x ) )
Theorem	dvlog2lem 24398	Lemma for dvlog2 24399. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- S = ( 1 ( ball ` ( abs o. - ) ) 1 )   =>    |- S C_ ( CC \ ( -oo (,] 0 ) )
Theorem	dvlog2 24399*	The derivative of the complex logarithm function on the open unit ball centered at 1, a sometimes easier region to work with than the CC \ ( -oo , 0 ] of dvlog 24397. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- S = ( 1 ( ball ` ( abs o. - ) ) 1 )   =>    |- ( CC _D ( log |` S ) ) = ( x e. S |-> ( 1 / x ) )
Theorem	advlog 24400	The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) )