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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sincos6thpi 25101 | The sine and cosine of π / 6. (Contributed by Paul Chapman, 25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.) |
⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2)) | ||
Theorem | sincos3rdpi 25102 | The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2)) | ||
Theorem | pigt3 25103 | π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ 3 < π | ||
Theorem | pige3 25104 | π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ 3 ≤ π | ||
Theorem | pige3ALT 25105 | Alternate proof of pige3 25104. 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 25106 | The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴))) | ||
Theorem | sinkpi 25107 | The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0) | ||
Theorem | coskpi 25108 | The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1) | ||
Theorem | sineq0 25109 | 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 25110 | 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 25111 | Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | cosq34lt1 25112 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | efeq1 25113 | 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 25114 | 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 25115 | Lemma for cosord 25116. (Contributed by Mario Carneiro, 10-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) | ||
Theorem | cosord 25116 | 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 25117 | 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 25118 | 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 25119 | 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 25120 | 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 25121 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 25122.) (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 25122 | 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 25123 | 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 25124 | The interval (-π(,]π) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (-π(,]π) ⊆ ℝ | ||
Theorem | efgh 25125* | 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 25126* | Lemma for efif1o 25130. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) | ||
Theorem | efif1olem2 25127* | Lemma for efif1o 25130. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ) | ||
Theorem | efif1olem3 25128* | Lemma for efif1o 25130. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) | ||
Theorem | efif1olem4 25129* | 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 25130* | 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 25131* | 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 25132* | 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 25133 | 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 25134* | 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 25135* | 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 25136 | 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 25137 | 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 25138 | Extend class notation with the natural logarithm function on complex numbers. |
class log | ||
Syntax | ccxp 25139 | Extend class notation with the complex power function. |
class ↑𝑐 | ||
Definition | df-log 25140 | 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 25141* | 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 25142 | 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 25143 | Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π)) | ||
Theorem | dflog2 25144 | 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 25145 | 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 25146 | 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 25147 | 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 25148 | 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 25149 | 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 25150 | 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 25151 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log) | ||
Theorem | logcl 25152 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ) | ||
Theorem | logimcl 25153 | 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 25154 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 25152. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (log‘𝑋) ∈ ℂ) | ||
Theorem | logimcld 25155 | The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 25153. Compare logimclad 25156. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π)) | ||
Theorem | logimclad 25156 | The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 25155. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π)) | ||
Theorem | abslogimle 25157 | 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 25158 | 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 25159 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ) | ||
Theorem | eflog 25160 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logeq0im1 25161 | 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 25162 | 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 25163 | 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 25164 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | logef 25165 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | relogef 25166 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | logeftb 25167 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | relogeftb 25168 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴)) | ||
Theorem | log1 25169 | 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 25170 | 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 25171 | 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 25172 | 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 25173 | 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 25174 | Lemma for relogmul 25175 and relogdiv 25176. 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 25175 | 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 25176 | 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 25177 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | reexplog 25178 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴)))) | ||
Theorem | relogexp 25179 | 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 25180 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴))) | ||
Theorem | relogiso 25181 | 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 25182 | 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 25183 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵))) | ||
Theorem | logfac 25184* | 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 25185* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) · 𝑛)))) | ||
Theorem | logleb 25186 | Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | rplogcl 25187 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0 25188 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴)) | ||
Theorem | logcj 25189 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≠ 0) → (log‘(∗‘𝐴)) = (∗‘(log‘𝐴))) | ||
Theorem | efiarg 25190 | The exponential of the "arg" function ℑ ∘ log. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) | ||
Theorem | cosargd 25191 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 25190. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (cos‘(ℑ‘(log‘𝑋))) = ((ℜ‘𝑋) / (abs‘𝑋))) | ||
Theorem | cosarg0d 25192 | 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 25193 | 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 25194 | 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 25195 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π)) | ||
Theorem | argimlt0 25196 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0)) | ||
Theorem | logimul 25197 | 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 25198 | The logarithm of the negative of a number with positive imaginary part is i · π less than the original. (Compare logneg 25171.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (log‘-𝐴) = ((log‘𝐴) − (i · π))) | ||
Theorem | logmul2 25199 | Generalization of relogmul 25175 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
Theorem | logdiv2 25200 | Generalization of relogdiv 25176 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |