![]() |
Metamath
Proof Explorer Theorem List (p. 242 of 424) | < 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-27159) |
![]() (27160-28684) |
![]() (28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efsubm 24101* | 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 24102 | 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 24103 | 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)) | ||
Theorem | rzgrp 24104 | The quotient group R/Z is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑅 = (ℝfld /s (ℝfld ~QG ℤ)) ⇒ ⊢ 𝑅 ∈ Grp | ||
Syntax | clog 24105 | Extend class notation with the natural logarithm function on complex numbers. |
class log | ||
Syntax | ccxp 24106 | Extend class notation with the complex power function. |
class ↑𝑐 | ||
Definition | df-log 24107 | 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"). To obtain a function, only the principle value of the multivalued inverses of the exponential function, i.e. the inverse whose imaginary part lies in the interval (-pi, pi], see https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ log = ◡(exp ↾ (◡ℑ “ (-π(,]π))) | ||
Definition | df-cxp 24108* | 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 24109 | 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 = (◡ℑ “ (-π(,]π)) | ||
Theorem | ellogrn 24110 | Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)) | ||
Theorem | dflog2 24111 | 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 24112 | 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 24113 | 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 24114 | 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 24115 | 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 24116 | 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 24117 | 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 24118 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log) | ||
Theorem | logcl 24119 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | ||
Theorem | logimcl 24120 | 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 24121 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 24119. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) | ||
Theorem | logimcld 24122 | The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 24120. Compare logimclad 24123. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π)) | ||
Theorem | logimclad 24123 | The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 24122. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π)) | ||
Theorem | abslogimle 24124 | 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 24125 | 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 24126 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ) | ||
Theorem | eflog 24127 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logeq0im1 24128 | 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 24129 | 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 24130 | 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 24131 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logef 24132 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | relogef 24133 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | logeftb 24134 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | relogeftb 24135 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | log1 24136 | 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 24137 | 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 24138 | 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 24139 | 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 24140 | 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 24141 | Lemma for relogmul 24142 and relogdiv 24143. 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 24142 | 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 24143 | 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 24144 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | reexplog 24145 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | relogexp 24146 | 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 24147 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | ||
Theorem | relogiso 24148 | 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 24149 | 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 24150 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵))) | ||
Theorem | logfac 24151* | 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 24152* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) · 𝑛)))) | ||
Theorem | logleb 24153 | Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | rplogcl 24154 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0 24155 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴)) | ||
Theorem | logcj 24156 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≠ 0) → (log‘(∗‘𝐴)) = (∗‘(log‘𝐴))) | ||
Theorem | efiarg 24157 | The exponential of the "arg" function ℑ ∘ log. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | ||
Theorem | cosargd 24158 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 24157. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (cos‘(ℑ‘(log‘𝑋))) = ((ℜ‘𝑋) / (abs‘𝑋))) | ||
Theorem | cosarg0d 24159 | 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 24160 | 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 24161 | 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 24162 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π)) | ||
Theorem | argimlt0 24163 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0)) | ||
Theorem | logimul 24164 | 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 24165 | The logarithm of the negative of a number with positive imaginary part is i · π less than the original. (Compare logneg 24138.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (log‘-𝐴) = ((log‘𝐴) − (i · π))) | ||
Theorem | logmul2 24166 | Generalization of relogmul 24142 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
Theorem | logdiv2 24167 | Generalization of relogdiv 24143 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
Theorem | abslogle 24168 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘(log‘𝐴)) ≤ ((abs‘(log‘(abs‘𝐴))) + π)) | ||
Theorem | tanarg 24169 | The basic relation between the "arg" function ℑ ∘ log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (tan‘(ℑ‘(log‘𝐴))) = ((ℑ‘𝐴) / (ℜ‘𝐴))) | ||
Theorem | logdivlti 24170 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) | ||
Theorem | logdivlt 24171 | 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 24172 | 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 24173 | Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ) | ||
Theorem | reeflogd 24174 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | relogmuld 24175 | 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 24176 | 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 24177 | Natural logarithm preserves ≤. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | relogefd 24178 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | rplogcld 24179 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0d 24180 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (log‘𝐴)) | ||
Theorem | divlogrlim 24181 | The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 | ||
Theorem | logno1 24182 | 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 24183 | The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) | ||
Theorem | relogcn 24184 | The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (log ↾ ℝ+) ∈ (ℝ+–cn→ℝ) | ||
Theorem | ellogdm 24185 | Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))) | ||
Theorem | logdmn0 24186 | A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0) | ||
Theorem | logdmnrp 24187 | A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → ¬ -𝐴 ∈ ℝ+) | ||
Theorem | logdmss 24188 | 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 24189 | Lemma for logcn 24193. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ∈ ℝ+) | ||
Theorem | logcnlem3 24190 | Lemma for logcn 24193. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)) | ||
Theorem | logcnlem4 24191 | Lemma for logcn 24193. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) < 𝑅) | ||
Theorem | logcnlem5 24192* | Lemma for logcn 24193. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ) | ||
Theorem | logcn 24193 | 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 24194 | Lemma for dvlog 24197. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂfld) | ||
Theorem | logdmopn 24195 | The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ 𝐷 ∈ (TopOpen‘ℂfld) | ||
Theorem | logf1o2 24196 | 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 24197* | The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
Theorem | dvlog2lem 24198 | Lemma for dvlog2 24199. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ 𝑆 ⊆ (ℂ ∖ (-∞(,]0)) | ||
Theorem | dvlog2 24199* | 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 24197. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (ℂ D (log ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / 𝑥)) | ||
Theorem | advlog 24200 | The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |