P. 248 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24701-24800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abelth2 24701*	Abel's theorem, restricted to the [0, 1] interval. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((0[,]1)–cn→ℂ))
14.3  Basic trigonometry
14.3.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 24702	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 24703	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 24704	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 24705*	Lemma for reeff1o 24706. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 24706	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ+
Theorem	reefiso 24707	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
⊢ (exp ↾ ℝ) Isom < , < (ℝ, ℝ+)
Theorem	efcvx 24708	The exponential function on the reals is a strictly convex function. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (exp‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < ((𝑇 · (exp‘𝐴)) + ((1 − 𝑇) · (exp‘𝐵))))
Theorem	reefgim 24709	The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑃 = ((mulGrp‘ℂfld) ↾s ℝ+)    ⇒   ⊢ (exp ↾ ℝ) ∈ (ℝfld GrpIso 𝑃)
14.3.2  Properties of pi = 3.14159...
Theorem	pilem1 24710	Lemma for pire 24715, pigt2lt4 24713 and sinpi 24714. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	pilem2 24711	Lemma for pire 24715, pigt2lt4 24713 and sinpi 24714. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ (2(,)4))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (sin‘𝐴) = 0)    &   ⊢ (𝜑 → (sin‘𝐵) = 0)    ⇒   ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)
Theorem	pilem3 24712	Lemma for pire 24715, pigt2lt4 24713 and sinpi 24714. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.) (Proof shortened by BJ, 30-Jun-2022.)
⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)
Theorem	pigt2lt4 24713	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 24714	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 24715	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	picn 24716	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	pipos 24717	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pirp 24718	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 24719	-π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 24720	Lemma for sinhalfpi 24725 and coshalfpi 24726. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 24721	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 24722	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ
Theorem	neghalfpirx 24723	-π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ*
Theorem	pidiv2halves 24724	Adding π / 2 to itself gives π. See 2halves 11702. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ((π / 2) + (π / 2)) = π
Theorem	sinhalfpi 24725	The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(π / 2)) = 1
Theorem	coshalfpi 24726	The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(π / 2)) = 0
Theorem	cosneghalfpi 24727	The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
⊢ (cos‘-(π / 2)) = 0
Theorem	efhalfpi 24728	The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (π / 2))) = i
Theorem	cospi 24729	The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘π) = -1
Theorem	efipi 24730	The exponential of i · π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (exp‘(i · π)) = -1
Theorem	eulerid 24731	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ ((exp‘(i · π)) + 1) = 0
Theorem	sin2pi 24732	The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(2 · π)) = 0
Theorem	cos2pi 24733	The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(2 · π)) = 1
Theorem	ef2pi 24734	The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (2 · π))) = 1
Theorem	ef2kpi 24735	If 𝐾 is an integer, then the exponential of 2𝐾πi is 1. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐾 ∈ ℤ → (exp‘((i · (2 · π)) · 𝐾)) = 1)
Theorem	efper 24736	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (exp‘(𝐴 + ((i · (2 · π)) · 𝐾))) = (exp‘𝐴))
Theorem	sinperlem 24737	Lemma for sinper 24738 and cosper 24739. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (𝐹‘𝐴) = (((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷))    &   ⊢ ((𝐴 + (𝐾 · (2 · π))) ∈ ℂ → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (((exp‘(i · (𝐴 + (𝐾 · (2 · π)))))𝑂(exp‘(-i · (𝐴 + (𝐾 · (2 · π)))))) / 𝐷))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (𝐹‘𝐴))
Theorem	sinper 24738	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴))
Theorem	cosper 24739	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴))
Theorem	sin2kpi 24740	If 𝐾 is an integer, then the sine of 2𝐾π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · (2 · π))) = 0)
Theorem	cos2kpi 24741	If 𝐾 is an integer, then the cosine of 2𝐾π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · (2 · π))) = 1)
Theorem	sin2pim 24742	Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴))
Theorem	cos2pim 24743	Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴))
Theorem	sinmpi 24744	Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴))
Theorem	cosmpi 24745	Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴))
Theorem	sinppi 24746	Sine of a number plus π. (Contributed by NM, 10-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴))
Theorem	cosppi 24747	Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴))
Theorem	efimpi 24748	The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴)))
Theorem	sinhalfpip 24749	The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴))
Theorem	sinhalfpim 24750	The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
Theorem	coshalfpip 24751	The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴))
Theorem	coshalfpim 24752	The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴))
Theorem	ptolemy 24753	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 15346, 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 24754	Lemma for sincosq1sgn 24755. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴))
Theorem	sincosq1sgn 24755	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 24756	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 24757	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 24758	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 24759	Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq0negpitopi 24760	Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)}))
Theorem	tanrpcl 24761	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
Theorem	tangtx 24762	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 24763	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 24764	The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴))
Theorem	sinq12ge0 24765	The sine of a number between 0 and π is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (0[,]π) → 0 ≤ (sin‘𝐴))
Theorem	sinq34lt0t 24766	The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0)
Theorem	cosq14gt0 24767	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 24768	The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴))
Theorem	sincosq1eq 24769	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 24770	The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2)))
Theorem	tan4thpi 24771	The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (tan‘(π / 4)) = 1
Theorem	sincos6thpi 24772	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 24773	The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
Theorem	pigt3 24774	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	pige3 24775	π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ 3 ≤ π
Theorem	pige3ALT 24776	Alternate proof of pige3 24775. 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 24777	The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴)))
Theorem	sinkpi 24778	The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0)
Theorem	coskpi 24779	The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)
Theorem	sineq0 24780	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 24781	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 24782	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 24783	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 24784	Lemma for cosord 24785. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝜑 → 𝐴 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴))
Theorem	cosord 24785	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 24786	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 24787	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 24788	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 24789	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 24790	The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 24791.) (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 24791	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 24792	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 24793	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 24794*	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 24795*	Lemma for efif1o 24799. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π))
Theorem	efif1olem2 24796*	Lemma for efif1o 24799. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ)
Theorem	efif1olem3 24797*	Lemma for efif1o 24799. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤)))    &   ⊢ 𝐶 = (◡abs “ {1})    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1))
Theorem	efif1olem4 24798*	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 24799*	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 24800*	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→𝐶