| Metamath
Proof Explorer Theorem List (p. 267 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ellogrn 26601 | Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
| ⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)) | ||
| Theorem | dflog2 26602 | 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 26603 | 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.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ran log) | ||
| Theorem | logrncn 26604 | The range of the natural logarithm function is a subset of the complex numbers. (Contributed by Mario Carneiro, 13-May-2014.) |
| ⊢ (𝐴 ∈ ran log → 𝐴 ∈ ℂ) | ||
| Theorem | eff1o2 26605 | 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→(ℂ ∖ {0}) | ||
| Theorem | logf1o 26606 | The natural logarithm function maps the nonzero complex numbers one-to-one onto its range. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log | ||
| Theorem | dfrelog 26607 | The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ (log ↾ ℝ+) = ◡(exp ↾ ℝ) | ||
| Theorem | relogf1o 26608 | The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ (log ↾ ℝ+):ℝ+–1-1-onto→ℝ | ||
| Theorem | logrncl 26609 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log) | ||
| Theorem | logcl 26610 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | ||
| Theorem | logimcl 26611 | Closure of the imaginary part of the logarithm function. (Contributed by Mario Carneiro, 23-Sep-2014.) (Revised by Mario Carneiro, 1-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-π < (ℑ‘(log‘𝐴)) ∧ (ℑ‘(log‘𝐴)) ≤ π)) | ||
| Theorem | logcld 26612 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 26610. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) | ||
| Theorem | logimcld 26613 | The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 26611. Compare logimclad 26614. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π)) | ||
| Theorem | logimclad 26614 | The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 26613. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π)) | ||
| Theorem | abslogimle 26615 | The imaginary part of the logarithm function has absolute value less than pi. (Contributed by Mario Carneiro, 3-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘(ℑ‘(log‘𝐴))) ≤ π) | ||
| Theorem | logrnaddcl 26616 | The range of the natural logarithm is closed under addition with reals. (Contributed by Mario Carneiro, 3-Apr-2015.) |
| ⊢ ((𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ran log) | ||
| Theorem | relogcl 26617 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ) | ||
| Theorem | eflog 26618 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴) | ||
| Theorem | logeq0im1 26619 | If the logarithm of a number is 0, the number must be 1. (Contributed by David A. Wheeler, 22-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (log‘𝐴) = 0) → 𝐴 = 1) | ||
| Theorem | logccne0 26620 | The logarithm isn't 0 if its argument isn't 0 or 1. (Contributed by David A. Wheeler, 17-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (log‘𝐴) ≠ 0) | ||
| Theorem | logne0 26621 | 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.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≠ 1) → (log‘𝐴) ≠ 0) | ||
| Theorem | reeflog 26622 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴) | ||
| Theorem | logef 26623 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴) | ||
| Theorem | relogef 26624 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴) | ||
| Theorem | logeftb 26625 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
| Theorem | relogeftb 26626 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
| Theorem | log1 26627 | 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 26628 | 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 | logi 26629 | The natural logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
| ⊢ (log‘i) = (i · (π / 2)) | ||
| Theorem | logneg 26630 | The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014.) (Revised by Mario Carneiro, 3-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ+ → (log‘-𝐴) = ((log‘𝐴) + (i · π))) | ||
| Theorem | logm1 26631 | The natural logarithm of negative 1. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
| ⊢ (log‘-1) = (i · π) | ||
| Theorem | lognegb 26632 | 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.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-𝐴 ∈ ℝ+ ↔ (ℑ‘(log‘𝐴)) = π)) | ||
| Theorem | relogoprlem 26633 | Lemma for relogmul 26634 and relogdiv 26635. 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‘𝐴) ∈ ℂ ∧ (log‘𝐵) ∈ ℂ) → (exp‘((log‘𝐴)𝐹(log‘𝐵))) = ((exp‘(log‘𝐴))𝐺(exp‘(log‘𝐵)))) & ⊢ (((log‘𝐴) ∈ ℝ ∧ (log‘𝐵) ∈ ℝ) → ((log‘𝐴)𝐹(log‘𝐵)) ∈ ℝ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴𝐺𝐵)) = ((log‘𝐴)𝐹(log‘𝐵))) | ||
| Theorem | relogmul 26634 | 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.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
| Theorem | relogdiv 26635 | 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.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
| Theorem | explog 26636 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
| Theorem | reexplog 26637 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
| Theorem | relogexp 26638 | 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.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (log‘(𝐴↑𝑁)) = (𝑁 · (log‘𝐴))) | ||
| Theorem | relog 26639 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | ||
| Theorem | relogiso 26640 | 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 ↾ ℝ+) Isom < , < (ℝ+, ℝ) | ||
| Theorem | reloggim 26641 | 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 ℝ+) ⇒ ⊢ (log ↾ ℝ+) ∈ (𝑃 GrpIso ℝfld) | ||
| Theorem | logltb 26642 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵))) | ||
| Theorem | logfac 26643* | The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015.) |
| ⊢ (𝑁 ∈ ℕ0 → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘)) | ||
| Theorem | eflogeq 26644* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) · 𝑛)))) | ||
| Theorem | logleb 26645 | Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
| Theorem | rplogcl 26646 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+) | ||
| Theorem | logge0 26647 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴)) | ||
| Theorem | logcj 26648 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≠ 0) → (log‘(∗‘𝐴)) = (∗‘(log‘𝐴))) | ||
| Theorem | efiarg 26649 | The exponential of the "arg" function ℑ ∘ log. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | ||
| Theorem | cosargd 26650 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 26649. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (cos‘(ℑ‘(log‘𝑋))) = ((ℜ‘𝑋) / (abs‘𝑋))) | ||
| Theorem | cosarg0d 26651 | The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → ((cos‘(ℑ‘(log‘𝑋))) = 0 ↔ (ℜ‘𝑋) = 0)) | ||
| Theorem | argregt0 26652 | Closure of the argument of a complex number with positive real part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (-(π / 2)(,)(π / 2))) | ||
| Theorem | argrege0 26653 | Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ (ℜ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (-(π / 2)[,](π / 2))) | ||
| Theorem | argimgt0 26654 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π)) | ||
| Theorem | argimlt0 26655 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0)) | ||
| Theorem | logimul 26656 | Multiplying a number by i increases the logarithm of the number by iπ / 2. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ (ℜ‘𝐴)) → (log‘(i · 𝐴)) = ((log‘𝐴) + (i · (π / 2)))) | ||
| Theorem | logneg2 26657 | The logarithm of the negative of a number with positive imaginary part is i · π less than the original. (Compare logneg 26630.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (log‘-𝐴) = ((log‘𝐴) − (i · π))) | ||
| Theorem | logmul2 26658 | Generalization of relogmul 26634 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
| Theorem | logdiv2 26659 | Generalization of relogdiv 26635 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
| Theorem | abslogle 26660 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘(log‘𝐴)) ≤ ((abs‘(log‘(abs‘𝐴))) + π)) | ||
| Theorem | tanarg 26661 | The basic relation between the "arg" function ℑ ∘ log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (tan‘(ℑ‘(log‘𝐴))) = ((ℑ‘𝐴) / (ℜ‘𝐴))) | ||
| Theorem | logdivlti 26662 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) | ||
| Theorem | logdivlt 26663 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ e ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ e ≤ 𝐵)) → (𝐴 < 𝐵 ↔ ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴))) | ||
| Theorem | logdivle 26664 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 3-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ e ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ e ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐵) / 𝐵) ≤ ((log‘𝐴) / 𝐴))) | ||
| Theorem | relogcld 26665 | Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ) | ||
| Theorem | reeflogd 26666 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴) | ||
| Theorem | relogmuld 26667 | 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.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
| Theorem | relogdivd 26668 | 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.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
| Theorem | logled 26669 | Natural logarithm preserves ≤. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
| Theorem | relogefd 26670 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(exp‘𝐴)) = 𝐴) | ||
| Theorem | rplogcld 26671 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+) | ||
| Theorem | logge0d 26672 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (log‘𝐴)) | ||
| Theorem | logge0b 26673 | The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.) |
| ⊢ (𝐴 ∈ ℝ+ → (0 ≤ (log‘𝐴) ↔ 1 ≤ 𝐴)) | ||
| Theorem | loggt0b 26674 | The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.) |
| ⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴)) | ||
| Theorem | logle1b 26675 | 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.) |
| ⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) ≤ 1 ↔ 𝐴 ≤ e)) | ||
| Theorem | loglt1b 26676 | The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020.) |
| ⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e)) | ||
| Theorem | divlogrlim 26677 | The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 | ||
| Theorem | logno1 26678 | The logarithm function is not eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 30-May-2016.) |
| ⊢ ¬ (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) | ||
| Theorem | dvrelog 26679 | The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) | ||
| Theorem | relogcn 26680 | The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (log ↾ ℝ+) ∈ (ℝ+–cn→ℝ) | ||
| Theorem | ellogdm 26681 | Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))) | ||
| Theorem | logdmn0 26682 | A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0) | ||
| Theorem | logdmnrp 26683 | A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → ¬ -𝐴 ∈ ℝ+) | ||
| Theorem | logdmss 26684 | The continuity domain of log is a subset of the regular domain of log. (Contributed by Mario Carneiro, 1-Mar-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ 𝐷 ⊆ (ℂ ∖ {0}) | ||
| Theorem | logcnlem2 26685 | Lemma for logcn 26689. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ∈ ℝ+) | ||
| Theorem | logcnlem3 26686 | Lemma for logcn 26689. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)) | ||
| Theorem | logcnlem4 26687 | Lemma for logcn 26689. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) < 𝑅) | ||
| Theorem | logcnlem5 26688* | Lemma for logcn 26689. (Contributed by Mario Carneiro, 18-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ) | ||
| Theorem | logcn 26689 | The logarithm function is continuous away from the branch cut at negative reals. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (log ↾ 𝐷) ∈ (𝐷–cn→ℂ) | ||
| Theorem | dvloglem 26690 | Lemma for dvlog 26693. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂfld) | ||
| Theorem | logdmopn 26691 | The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ 𝐷 ∈ (TopOpen‘ℂfld) | ||
| Theorem | logf1o2 26692 | 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.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (log ↾ 𝐷):𝐷–1-1-onto→(◡ℑ “ (-π(,)π)) | ||
| Theorem | dvlog 26693* | The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
| Theorem | dvlog2lem 26694 | Lemma for dvlog2 26695. (Contributed by Mario Carneiro, 1-Mar-2015.) |
| ⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ 𝑆 ⊆ (ℂ ∖ (-∞(,]0)) | ||
| Theorem | dvlog2 26695* | The derivative of the complex logarithm function on the open unit ball centered at 1, a sometimes easier region to work with than the ℂ ∖ (-∞, 0] of dvlog 26693. (Contributed by Mario Carneiro, 1-Mar-2015.) |
| ⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (ℂ D (log ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / 𝑥)) | ||
| Theorem | advlog 26696 | The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) | ||
| Theorem | advlogexp 26697* | The antiderivative of a power of the logarithm. (Set 𝐴 = 1 and multiply by (-1)↑𝑁 · 𝑁! to get the antiderivative of log(𝑥)↑𝑁 itself.) (Contributed by Mario Carneiro, 22-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) | ||
| Theorem | efopnlem1 26698 | Lemma for efopn 26700. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
| ⊢ (((𝑅 ∈ ℝ+ ∧ 𝑅 < π) ∧ 𝐴 ∈ (0(ball‘(abs ∘ − ))𝑅)) → (abs‘(ℑ‘𝐴)) < π) | ||
| Theorem | efopnlem2 26699 | Lemma for efopn 26700. (Contributed by Mario Carneiro, 2-May-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝑅 ∈ ℝ+ ∧ 𝑅 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽) | ||
| Theorem | efopn 26700 | The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ 𝐽 → (exp “ 𝑆) ∈ 𝐽) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |