P. 249 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24801-24900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sinq34lt0t 24801	The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0)
Theorem	cosq14gt0 24802	The cosine of a number strictly between -π / 2 and π / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ (𝐴 ∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘𝐴))
Theorem	cosq14ge0 24803	The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴))
Theorem	sincosq1eq 24804	Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐴 + 𝐵) = 1) → (sin‘(𝐴 · (π / 2))) = (cos‘(𝐵 · (π / 2))))
Theorem	sincos4thpi 24805	The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2)))
Theorem	tan4thpi 24806	The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (tan‘(π / 4)) = 1
Theorem	sincos6thpi 24807	The sine and cosine of π / 6. (Contributed by Paul Chapman, 25-Jan-2008.) Replace OLD theorem. (Revised by Wolf Lammen, 24-Sep-2020.)
⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2))
Theorem	sincos3rdpi 24808	The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
Theorem	pigt3 24809	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	pige3 24810	π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ 3 ≤ π
Theorem	pige3ALT 24811	Alternate proof of pige3 24810. 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 24812	The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴)))
Theorem	sinkpi 24813	The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0)
Theorem	coskpi 24814	The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)
Theorem	sineq0 24815	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 24816	A complex number whose cosine is one is an integer multiple of 2π. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) = 1 ↔ (𝐴 / (2 · π)) ∈ ℤ))
Theorem	efeq1 24817	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 24818	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 24819	Lemma for cosord 24820. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝜑 → 𝐴 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴))
Theorem	cosord 24820	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 24821	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 24822	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 24823	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 24824	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 24825	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 24826.) (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 24826	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 24827	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 24828	The interval (-π(,]π) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
⊢ (-π(,]π) ⊆ ℝ
14.3.3  Mapping of the exponential function
Theorem	efgh 24829*	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 24830*	Lemma for efif1o 24834. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π))
Theorem	efif1olem2 24831*	Lemma for efif1o 24834. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ)
Theorem	efif1olem3 24832*	Lemma for efif1o 24834. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤)))    &   ⊢ 𝐶 = (◡abs “ {1})    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
Theorem	efif1olem4 24833*	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 24834*	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 24835*	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 24836*	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 24837	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 24838*	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 24839*	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 24840	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 24841	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))
14.3.4  The natural logarithm on complex numbers
Syntax	clog 24842	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 24843	Extend class notation with the complex power function.
class ↑𝑐
Definition	df-log 24844	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 24845*	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 24846	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 24847	Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))
Theorem	dflog2 24848	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 24849	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 24850	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 24851	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 24852	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 24853	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 24854	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 24855	Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log)
Theorem	logcl 24856	Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ)
Theorem	logimcl 24857	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 24858	The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 24856. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (log‘𝑋) ∈ ℂ)
Theorem	logimcld 24859	The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 24857. Compare logimclad 24860. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π))
Theorem	logimclad 24860	The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 24859. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π))
Theorem	abslogimle 24861	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 24862	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 24863	Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
Theorem	eflog 24864	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
Theorem	logeq0im1 24865	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 24866	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 24867	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 24868	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴)
Theorem	logef 24869	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴)
Theorem	relogef 24870	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴)
Theorem	logeftb 24871	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴))
Theorem	relogeftb 24872	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴))
Theorem	log1 24873	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 24874	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 24875	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 24876	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 24877	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 24878	Lemma for relogmul 24879 and relogdiv 24880. 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 24879	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 24880	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 24881	Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴))))
Theorem	reexplog 24882	Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴))))
Theorem	relogexp 24883	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 24884	Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (ℜ‘(log‘𝐴)) = (log‘(abs‘𝐴)))
Theorem	relogiso 24885	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 24886	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 24887	The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵)))
Theorem	logfac 24888*	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 24889*	Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) · 𝑛))))
Theorem	logleb 24890	Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵)))
Theorem	rplogcl 24891	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+)
Theorem	logge0 24892	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴))
Theorem	logcj 24893	The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≠ 0) → (log‘(∗‘𝐴)) = (∗‘(log‘𝐴)))
Theorem	efiarg 24894	The exponential of the "arg" function ℑ ∘ log. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴)))
Theorem	cosargd 24895	The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 24894. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (cos‘(ℑ‘(log‘𝑋))) = ((ℜ‘𝑋) / (abs‘𝑋)))
Theorem	cosarg0d 24896	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 24897	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 24898	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 24899	Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π))
Theorem	argimlt0 24900	Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0))