Home | Metamath
Proof Explorer Theorem List (p. 252 of 450) | < 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: | Metamath Proof Explorer
(1-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sincos3rdpi 25101 | The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2)) | ||
Theorem | pigt3 25102 | π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ 3 < π | ||
Theorem | pige3 25103 | π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ 3 ≤ π | ||
Theorem | pige3ALT 25104 | Alternate proof of pige3 25103. This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2π. We translate this to algebra by looking at the function e↑(i𝑥) as 𝑥 goes from 0 to π / 3; it moves at unit speed and travels distance 1, hence 1 ≤ π / 3. (Contributed by Mario Carneiro, 21-May-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 3 ≤ π | ||
Theorem | abssinper 25105 | The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴))) | ||
Theorem | sinkpi 25106 | The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0) | ||
Theorem | coskpi 25107 | The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1) | ||
Theorem | sineq0 25108 | A complex number whose sine is zero is an integer multiple of π. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / π) ∈ ℤ)) | ||
Theorem | coseq1 25109 | A complex number whose cosine is one is an integer multiple of 2π. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) = 1 ↔ (𝐴 / (2 · π)) ∈ ℤ)) | ||
Theorem | cos02pilt1 25110 | Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | cosq34lt1 25111 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | efeq1 25112 | A complex number whose exponential is one is an integer multiple of 2πi. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) = 1 ↔ (𝐴 / (i · (2 · π))) ∈ ℤ)) | ||
Theorem | cosne0 25113 | The cosine function has no zeroes within the vertical strip of the complex plane between real part -π / 2 and π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0) | ||
Theorem | cosordlem 25114 | Lemma for cosord 25115. (Contributed by Mario Carneiro, 10-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) | ||
Theorem | cosord 25115 | Cosine is decreasing over the closed interval from 0 to π. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ (0[,]π) ∧ 𝐵 ∈ (0[,]π)) → (𝐴 < 𝐵 ↔ (cos‘𝐵) < (cos‘𝐴))) | ||
Theorem | cos11 25116 | Cosine is one-to-one over the closed interval from 0 to π. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ (0[,]π) ∧ 𝐵 ∈ (0[,]π)) → (𝐴 = 𝐵 ↔ (cos‘𝐴) = (cos‘𝐵))) | ||
Theorem | sinord 25117 | Sine is increasing over the closed interval from -(π / 2) to (π / 2). (Contributed by Mario Carneiro, 29-Jul-2014.) |
⊢ ((𝐴 ∈ (-(π / 2)[,](π / 2)) ∧ 𝐵 ∈ (-(π / 2)[,](π / 2))) → (𝐴 < 𝐵 ↔ (sin‘𝐴) < (sin‘𝐵))) | ||
Theorem | recosf1o 25118 | The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (cos ↾ (0[,]π)):(0[,]π)–1-1-onto→(-1[,]1) | ||
Theorem | resinf1o 25119 | The sine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (sin ↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) | ||
Theorem | tanord1 25120 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 25121.) (Contributed by Mario Carneiro, 29-Jul-2014.) Revised to replace an OLD theorem. (Revised by Wolf Lammen, 20-Sep-2020.) |
⊢ ((𝐴 ∈ (0[,)(π / 2)) ∧ 𝐵 ∈ (0[,)(π / 2))) → (𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵))) | ||
Theorem | tanord 25121 | The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ (-(π / 2)(,)(π / 2)) ∧ 𝐵 ∈ (-(π / 2)(,)(π / 2))) → (𝐴 < 𝐵 ↔ (tan‘𝐴) < (tan‘𝐵))) | ||
Theorem | tanregt0 25122 | The real part of the tangent of a complex number with real part in the open interval (0(,)(π / 2)) is positive. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴))) | ||
Theorem | negpitopissre 25123 | The interval (-π(,]π) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (-π(,]π) ⊆ ℝ | ||
Theorem | efgh 25124* | The exponential function of a scaled complex number is a group homomorphism from the group of complex numbers under addition to the set of complex numbers under multiplication. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 11-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (exp‘(𝐴 · 𝑥))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝑋 ∈ (SubGrp‘ℂfld)) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐹‘(𝐵 + 𝐶)) = ((𝐹‘𝐵) · (𝐹‘𝐶))) | ||
Theorem | efif1olem1 25125* | Lemma for efif1o 25129. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) | ||
Theorem | efif1olem2 25126* | Lemma for efif1o 25129. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ) | ||
Theorem | efif1olem3 25127* | Lemma for efif1o 25129. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) | ||
Theorem | efif1olem4 25128* | 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 25129* | 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 25130* | 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 25131* | 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 25132 | 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 25133* | 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 25134* | 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 25135 | 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 25136 | 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 25137 | Extend class notation with the natural logarithm function on complex numbers. |
class log | ||
Syntax | ccxp 25138 | Extend class notation with the complex power function. |
class ↑𝑐 | ||
Definition | df-log 25139 | 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 25140* | 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 25141 | 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 25142 | Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)) | ||
Theorem | dflog2 25143 | 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 25144 | 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 25145 | 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 25146 | 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 25147 | 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 25148 | 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 25149 | 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 25150 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log) | ||
Theorem | logcl 25151 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | ||
Theorem | logimcl 25152 | 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 25153 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 25151. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) | ||
Theorem | logimcld 25154 | The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 25152. Compare logimclad 25155. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π)) | ||
Theorem | logimclad 25155 | The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 25154. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π)) | ||
Theorem | abslogimle 25156 | 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 25157 | 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 25158 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ) | ||
Theorem | eflog 25159 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logeq0im1 25160 | 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 25161 | 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 25162 | 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 25163 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logef 25164 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | relogef 25165 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | logeftb 25166 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | relogeftb 25167 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | log1 25168 | 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 25169 | 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 25170 | 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 25171 | 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 25172 | 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 25173 | Lemma for relogmul 25174 and relogdiv 25175. 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 25174 | 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 25175 | 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 25176 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | reexplog 25177 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | relogexp 25178 | 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 25179 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | ||
Theorem | relogiso 25180 | 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 25181 | 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 25182 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵))) | ||
Theorem | logfac 25183* | 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 25184* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) · 𝑛)))) | ||
Theorem | logleb 25185 | Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | rplogcl 25186 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0 25187 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴)) | ||
Theorem | logcj 25188 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≠ 0) → (log‘(∗‘𝐴)) = (∗‘(log‘𝐴))) | ||
Theorem | efiarg 25189 | The exponential of the "arg" function ℑ ∘ log. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | ||
Theorem | cosargd 25190 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 25189. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (cos‘(ℑ‘(log‘𝑋))) = ((ℜ‘𝑋) / (abs‘𝑋))) | ||
Theorem | cosarg0d 25191 | 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 25192 | 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 25193 | 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 25194 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π)) | ||
Theorem | argimlt0 25195 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0)) | ||
Theorem | logimul 25196 | 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 25197 | The logarithm of the negative of a number with positive imaginary part is i · π less than the original. (Compare logneg 25170.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (log‘-𝐴) = ((log‘𝐴) − (i · π))) | ||
Theorem | logmul2 25198 | Generalization of relogmul 25174 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
Theorem | logdiv2 25199 | Generalization of relogdiv 25175 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
Theorem | abslogle 25200 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘(log‘𝐴)) ≤ ((abs‘(log‘(abs‘𝐴))) + π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |