![]() |
Metamath
Proof Explorer Theorem List (p. 267 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efif1olem4 26601* | The exponential function of an imaginary number maps any interval of length 2π one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.) |
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝐶 = (◡abs “ {1}) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) & ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ) & ⊢ 𝑆 = (sin ↾ (-(π / 2)[,](π / 2))) ⇒ ⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝐶) | ||
Theorem | efif1o 26602* | The exponential function of an imaginary number maps any open-below, closed-above interval of length 2π one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝐶 = (◡abs “ {1}) & ⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ (𝐴 ∈ ℝ → 𝐹:𝐷–1-1-onto→𝐶) | ||
Theorem | efifo 26603* | The exponential function of an imaginary number maps the reals onto the unit circle. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℝ ↦ (exp‘(i · 𝑧))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ 𝐹:ℝ–onto→𝐶 | ||
Theorem | eff1olem 26604* | The exponential function maps the set 𝑆, of complex numbers with imaginary part in a real interval of length 2 · π, one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.) |
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝑆 = (◡ℑ “ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) & ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ) ⇒ ⊢ (𝜑 → (exp ↾ 𝑆):𝑆–1-1-onto→(ℂ ∖ {0})) | ||
Theorem | eff1o 26605 | The exponential function maps the set 𝑆, of complex numbers with imaginary part in the closed-above, open-below interval from -π to π one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
⊢ 𝑆 = (◡ℑ “ (-π(,]π)) ⇒ ⊢ (exp ↾ 𝑆):𝑆–1-1-onto→(ℂ ∖ {0}) | ||
Theorem | efabl 26606* | 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.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) & ⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s ran 𝐹) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (SubGrp‘ℂfld)) ⇒ ⊢ (𝜑 → 𝐺 ∈ Abel) | ||
Theorem | efsubm 26607* | 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.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) & ⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s ran 𝐹) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (SubGrp‘ℂfld)) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (SubMnd‘(mulGrp‘ℂfld))) | ||
Theorem | circgrp 26608 | The circle group 𝑇 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.) |
⊢ 𝐶 = (◡abs “ {1}) & ⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s 𝐶) ⇒ ⊢ 𝑇 ∈ Abel | ||
Theorem | circsubm 26609 | The circle group 𝑇 is a submonoid of the multiplicative group of ℂfld. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝐶 = (◡abs “ {1}) & ⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s 𝐶) ⇒ ⊢ 𝐶 ∈ (SubMnd‘(mulGrp‘ℂfld)) | ||
Syntax | clog 26610 | Extend class notation with the natural logarithm function on complex numbers. |
class log | ||
Syntax | ccxp 26611 | Extend class notation with the complex power function. |
class ↑𝑐 | ||
Definition | df-log 26612 | 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 ↾ (◡ℑ “ (-π(,]π))) | ||
Definition | df-cxp 26613* | Define the power function on complex numbers. Note that the value of this function when 𝑥 = 0 and (ℜ‘𝑦) ≤ 0, 𝑦 ≠ 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ↑𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))) | ||
Theorem | logrn 26614 | The range of the natural logarithm function, also the principal domain of the exponential function. This allows 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 = (◡ℑ “ (-π(,]π)) | ||
Theorem | ellogrn 26615 | Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)) | ||
Theorem | dflog2 26616 | 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 26617 | 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 26618 | 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 26619 | 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 26620 | 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 26621 | 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 26622 | 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 26623 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log) | ||
Theorem | logcl 26624 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | ||
Theorem | logimcl 26625 | 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 26626 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 26624. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) | ||
Theorem | logimcld 26627 | The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 26625. Compare logimclad 26628. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π)) | ||
Theorem | logimclad 26628 | The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 26627. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π)) | ||
Theorem | abslogimle 26629 | 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 26630 | 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 26631 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ) | ||
Theorem | eflog 26632 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logeq0im1 26633 | 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 26634 | 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 26635 | 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 26636 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logef 26637 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | relogef 26638 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | logeftb 26639 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | relogeftb 26640 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | log1 26641 | 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 26642 | 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 26643 | The natural logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
⊢ (log‘i) = (i · (π / 2)) | ||
Theorem | logneg 26644 | 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 26645 | 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 26646 | 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 26647 | Lemma for relogmul 26648 and relogdiv 26649. 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 26648 | 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 26649 | 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 26650 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | reexplog 26651 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | relogexp 26652 | 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 26653 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | ||
Theorem | relogiso 26654 | 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 26655 | 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 26656 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵))) | ||
Theorem | logfac 26657* | 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 26658* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) · 𝑛)))) | ||
Theorem | logleb 26659 | Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | rplogcl 26660 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0 26661 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴)) | ||
Theorem | logcj 26662 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≠ 0) → (log‘(∗‘𝐴)) = (∗‘(log‘𝐴))) | ||
Theorem | efiarg 26663 | The exponential of the "arg" function ℑ ∘ log. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | ||
Theorem | cosargd 26664 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 26663. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (cos‘(ℑ‘(log‘𝑋))) = ((ℜ‘𝑋) / (abs‘𝑋))) | ||
Theorem | cosarg0d 26665 | 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 26666 | 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 26667 | 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 26668 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π)) | ||
Theorem | argimlt0 26669 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0)) | ||
Theorem | logimul 26670 | 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 26671 | The logarithm of the negative of a number with positive imaginary part is i · π less than the original. (Compare logneg 26644.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (log‘-𝐴) = ((log‘𝐴) − (i · π))) | ||
Theorem | logmul2 26672 | Generalization of relogmul 26648 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
Theorem | logdiv2 26673 | Generalization of relogdiv 26649 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
Theorem | abslogle 26674 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘(log‘𝐴)) ≤ ((abs‘(log‘(abs‘𝐴))) + π)) | ||
Theorem | tanarg 26675 | The basic relation between the "arg" function ℑ ∘ log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (tan‘(ℑ‘(log‘𝐴))) = ((ℑ‘𝐴) / (ℜ‘𝐴))) | ||
Theorem | logdivlti 26676 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) | ||
Theorem | logdivlt 26677 | 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 26678 | 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 26679 | Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ) | ||
Theorem | reeflogd 26680 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | relogmuld 26681 | 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 26682 | 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 26683 | Natural logarithm preserves ≤. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | relogefd 26684 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | rplogcld 26685 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0d 26686 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (log‘𝐴)) | ||
Theorem | logge0b 26687 | 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 26688 | 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 26689 | 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 26690 | 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 26691 | The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 | ||
Theorem | logno1 26692 | 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 26693 | The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) | ||
Theorem | relogcn 26694 | The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (log ↾ ℝ+) ∈ (ℝ+–cn→ℝ) | ||
Theorem | ellogdm 26695 | Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))) | ||
Theorem | logdmn0 26696 | A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0) | ||
Theorem | logdmnrp 26697 | A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → ¬ -𝐴 ∈ ℝ+) | ||
Theorem | logdmss 26698 | 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 26699 | Lemma for logcn 26703. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ∈ ℝ+) | ||
Theorem | logcnlem3 26700 | Lemma for logcn 26703. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |