Home | Metamath
Proof Explorer Theorem List (p. 244 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | clog 24301 | Extend class notation with the natural logarithm function on complex numbers. |
Syntax | ccxp 24302 | Extend class notation with the complex power function. |
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.) |
Definition | df-cxp 24304* | Define the power function on complex numbers. Note that the value of this function when and should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014.) |
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 . (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
Theorem | ellogrn 24306 | Write out the property explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
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.) |
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.) |
Theorem | logrncn 24309 | The range of the natural logarithm function is a subset of the complex numbers. (Contributed by Mario Carneiro, 13-May-2014.) |
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.) |
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.) |
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.) |
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.) |
Theorem | logrncl 24314 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
Theorem | logcl 24315 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
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.) |
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.) |
Theorem | logimcld 24318 | The imaginary part of the logarithm is in . Deduction form of logimcl 24316. Compare logimclad 24319. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | logimclad 24319 | The imaginary part of the logarithm is in . Alternate form of logimcld 24318. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | abslogimle 24320 | The imaginary part of the logarithm function has absolute value less than pi. (Contributed by Mario Carneiro, 3-Jul-2017.) |
Theorem | logrnaddcl 24321 | The range of the natural logarithm is closed under addition with reals. (Contributed by Mario Carneiro, 3-Apr-2015.) |
Theorem | relogcl 24322 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | eflog 24323 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
Theorem | logeq0im1 24324 | If the logarithm of a number is 0, the number must be 1. (Contributed by David A. Wheeler, 22-Jul-2017.) |
Theorem | logccne0 24325 | The logarithm isn't 0 if its argument isn't 0 or 1. (Contributed by David A. Wheeler, 17-Jul-2017.) |
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.) |
Theorem | reeflog 24327 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | logef 24328 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
Theorem | relogef 24329 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | logeftb 24330 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
Theorem | relogeftb 24331 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | log1 24332 | The natural logarithm of . One case of Property 1a of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | loge 24333 | The natural logarithm of . One case of Property 1b of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
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.) |
Theorem | logm1 24335 | The natural logarithm of negative . (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
Theorem | lognegb 24336 | If a number has imaginary part equal to , then it is on the negative real axis and vice-versa. (Contributed by Mario Carneiro, 23-Sep-2014.) |
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.) |
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.) |
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.) |
Theorem | explog 24340 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
Theorem | reexplog 24341 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | relogexp 24342 | The natural logarithm of positive raised to an integer power. Property 4 of [Cohen] p. 301-302, restricted to natural logarithms and integer powers . (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | relog 24343 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
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.) |
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.) |
mulGrpℂfld ↾s GrpIso RRfld | ||
Theorem | logltb 24346 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Theorem | logfac 24347* | The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015.) |
Theorem | eflogeq 24348* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
Theorem | logleb 24349 | Natural logarithm preserves . (Contributed by Stefan O'Rear, 19-Sep-2014.) |
Theorem | rplogcl 24350 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
Theorem | logge0 24351 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | logcj 24352 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | efiarg 24353 | The exponential of the "arg" function . (Contributed by Mario Carneiro, 25-Feb-2015.) |
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.) |
Theorem | cosarg0d 24355 | The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | argregt0 24356 | Closure of the argument of a complex number with positive real part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | argrege0 24357 | Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015.) |
Theorem | argimgt0 24358 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | argimlt0 24359 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | logimul 24360 | Multiplying a number by increases the logarithm of the number by . (Contributed by Mario Carneiro, 4-Apr-2015.) |
Theorem | logneg2 24361 | The logarithm of the negative of a number with positive imaginary part is less than the original. (Compare logneg 24334.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
Theorem | logmul2 24362 | Generalization of relogmul 24338 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
Theorem | logdiv2 24363 | Generalization of relogdiv 24339 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
Theorem | abslogle 24364 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
Theorem | tanarg 24365 | The basic relation between the "arg" function and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | logdivlti 24366 | The function is strictly decreasing on the reals greater than . (Contributed by Mario Carneiro, 14-Mar-2014.) |
Theorem | logdivlt 24367 | The function is strictly decreasing on the reals greater than . (Contributed by Mario Carneiro, 14-Mar-2014.) |
Theorem | logdivle 24368 | The function is strictly decreasing on the reals greater than . (Contributed by Mario Carneiro, 3-May-2016.) |
Theorem | relogcld 24369 | Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | reeflogd 24370 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
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.) |
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.) |
Theorem | logled 24373 | Natural logarithm preserves . (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | relogefd 24374 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | rplogcld 24375 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | logge0d 24376 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
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.) |
Theorem | loggt0b 24378 | The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.) |
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.) |
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.) |
Theorem | divlogrlim 24381 | The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.) |
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.) |
Theorem | dvrelog 24383 | The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | relogcn 24384 | The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.) |
Theorem | ellogdm 24385 | Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.) |
Theorem | logdmn0 24386 | A number in the continuous domain of is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.) |
Theorem | logdmnrp 24387 | A number in the continuous domain of is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.) |
Theorem | logdmss 24388 | The continuity domain of is a subset of the regular domain of . (Contributed by Mario Carneiro, 1-Mar-2015.) |
Theorem | logcnlem2 24389 | Lemma for logcn 24393. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | logcnlem3 24390 | Lemma for logcn 24393. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | logcnlem4 24391 | Lemma for logcn 24393. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | logcnlem5 24392* | Lemma for logcn 24393. (Contributed by Mario Carneiro, 18-Feb-2015.) |
Theorem | logcn 24393 | The logarithm function is continuous away from the branch cut at negative reals. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | dvloglem 24394 | Lemma for dvlog 24397. (Contributed by Mario Carneiro, 24-Feb-2015.) |
ℂfld | ||
Theorem | logdmopn 24395 | The "continuous domain" of is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
ℂfld | ||
Theorem | logf1o2 24396 | The logarithm maps its continuous domain bijectively onto the set of numbers with imaginary part . The negative reals are mapped to the numbers with imaginary part equal to . (Contributed by Mario Carneiro, 2-May-2015.) |
Theorem | dvlog 24397* | The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.) |
Theorem | dvlog2lem 24398 | Lemma for dvlog2 24399. (Contributed by Mario Carneiro, 1-Mar-2015.) |
Theorem | dvlog2 24399* | The derivative of the complex logarithm function on the open unit ball centered at , a sometimes easier region to work with than the of dvlog 24397. (Contributed by Mario Carneiro, 1-Mar-2015.) |
Theorem | advlog 24400 | The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |