P. 265 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26401-26500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sin2pim 26401	Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴))
Theorem	cos2pim 26402	Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴))
Theorem	sinmpi 26403	Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴))
Theorem	cosmpi 26404	Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴))
Theorem	sinppi 26405	Sine of a number plus π. (Contributed by NM, 10-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴))
Theorem	cosppi 26406	Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴))
Theorem	efimpi 26407	The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴)))
Theorem	sinhalfpip 26408	The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴))
Theorem	sinhalfpim 26409	The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
Theorem	coshalfpip 26410	The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴))
Theorem	coshalfpim 26411	The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴))
Theorem	ptolemy 26412	Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 16147, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = π) → (((sin‘𝐴) · (sin‘𝐵)) + ((sin‘𝐶) · (sin‘𝐷))) = ((sin‘(𝐵 + 𝐶)) · (sin‘(𝐴 + 𝐶))))
Theorem	sincosq1lem 26413	Lemma for sincosq1sgn 26414. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴))
Theorem	sincosq1sgn 26414	The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
Theorem	sincosq2sgn 26415	The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ((π / 2)(,)π) → (0 < (sin‘𝐴) ∧ (cos‘𝐴) < 0))
Theorem	sincosq3sgn 26416	The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ (π(,)(3 · (π / 2))) → ((sin‘𝐴) < 0 ∧ (cos‘𝐴) < 0))
Theorem	sincosq4sgn 26417	The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ((3 · (π / 2))(,)(2 · π)) → ((sin‘𝐴) < 0 ∧ 0 < (cos‘𝐴)))
Theorem	coseq00topi 26418	Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq0negpitopi 26419	Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)}))
Theorem	tanrpcl 26420	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
Theorem	tangtx 26421	The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 < (tan‘𝐴))
Theorem	tanabsge 26422	The tangent function is greater than or equal to its argument in absolute value. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ (𝐴 ∈ (-(π / 2)(,)(π / 2)) → (abs‘𝐴) ≤ (abs‘(tan‘𝐴)))
Theorem	sinq12gt0 26423	The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴))
Theorem	sinq12ge0 26424	The sine of a number between 0 and π is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (0[,]π) → 0 ≤ (sin‘𝐴))
Theorem	sinq34lt0t 26425	The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0)
Theorem	cosq14gt0 26426	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 26427	The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴))
Theorem	sincosq1eq 26428	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 26429	The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2)))
Theorem	tan4thpi 26430	The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) (Proof shortened by SN, 2-Sep-2025.)
⊢ (tan‘(π / 4)) = 1
Theorem	tan4thpiOLD 26431	Obsolete version of tan4thpi 26430 as of 2-Sep-2025. (Contributed by Mario Carneiro, 5-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (tan‘(π / 4)) = 1
Theorem	sincos6thpi 26432	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 26433	The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
Theorem	pigt3 26434	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	pige3 26435	π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ 3 ≤ π
Theorem	pige3ALT 26436	Alternate proof of pige3 26435. 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 26437	The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴)))
Theorem	sinkpi 26438	The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0)
Theorem	coskpi 26439	The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)
Theorem	sineq0 26440	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 26441	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 26442	Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.)
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1)
Theorem	cosq34lt1 26443	Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.)
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1)
Theorem	efeq1 26444	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 26445	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 26446	Lemma for cosord 26447. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝜑 → 𝐴 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴))
Theorem	cosord 26447	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	cos0pilt1 26448	Cosine is between minus one and one on the open interval between zero and π. (Contributed by Jim Kingdon, 7-May-2024.)
⊢ (𝐴 ∈ (0(,)π) → (cos‘𝐴) ∈ (-1(,)1))
Theorem	cos11 26449	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 26450	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 26451	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 26452	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 26453	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 26454.) (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 26454	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 26455	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 26456	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 26457*	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 26458*	Lemma for efif1o 26462. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π))
Theorem	efif1olem2 26459*	Lemma for efif1o 26462. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ)
Theorem	efif1olem3 26460*	Lemma for efif1o 26462. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤)))    &   ⊢ 𝐶 = (◡abs “ {1})    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
Theorem	efif1olem4 26461*	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 26462*	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 26463*	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 26464*	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 26465	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 26466*	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 26467*	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 26468	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 26469	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 26470	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 26471	Extend class notation with the complex power function.
class ↑𝑐
Definition	df-log 26472	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 26473*	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 26474	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 26475	Write out the property 𝐴 ∈ ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ran log ↔ (𝐴 ∈ ℂ ∧ -π < (ℑ‘𝐴) ∧ (ℑ‘𝐴) ≤ π))
Theorem	dflog2 26476	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 26477	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 26478	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 26479	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 26480	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 26481	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 26482	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 26483	Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ran log)
Theorem	logcl 26484	Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈ ℂ)
Theorem	logimcl 26485	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 26486	The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 26484. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (log‘𝑋) ∈ ℂ)
Theorem	logimcld 26487	The imaginary part of the logarithm is in (-π(,]π). Deduction form of logimcl 26485. Compare logimclad 26488. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (-π < (ℑ‘(log‘𝑋)) ∧ (ℑ‘(log‘𝑋)) ≤ π))
Theorem	logimclad 26488	The imaginary part of the logarithm is in (-π(,]π). Alternate form of logimcld 26487. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (ℑ‘(log‘𝑋)) ∈ (-π(,]π))
Theorem	abslogimle 26489	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 26490	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 26491	Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
Theorem	eflog 26492	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
Theorem	logeq0im1 26493	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 26494	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 26495	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 26496	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴)
Theorem	logef 26497	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ (𝐴 ∈ ran log → (log‘(exp‘𝐴)) = 𝐴)
Theorem	relogef 26498	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴)
Theorem	logeftb 26499	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴))
Theorem	relogeftb 26500	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴))