P. 266 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26501-26600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abelthlem1 26501*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
Theorem	abelthlem2 26502*	Lemma for abelth 26511. The peculiar region 𝑆, known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing 1. Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    ⇒   ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
Theorem	abelthlem3 26503*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ )
Theorem	abelthlem4 26504*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
Theorem	abelthlem5 26505*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )
Theorem	abelthlem6 26506*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
Theorem	abelthlem7a 26507*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    ⇒   ⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
Theorem	abelthlem7 26508*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)    &   ⊢ (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))    ⇒   ⊢ (𝜑 → (abs‘(𝐹‘𝑋)) < ((𝑀 + 1) · 𝑅))
Theorem	abelthlem8 26509*	Lemma for abelth 26511. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))
Theorem	abelthlem9 26510*	Lemma for abelth 26511. By adjusting the constant term, we can assume that the entire series converges to 0. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))
Theorem	abelth 26511*	Abel's theorem. If the power series Σ𝑛 ∈ ℕ0𝐴(𝑛)(𝑥↑𝑛) is convergent at 1, then it is equal to the limit from "below", along a Stolz angle 𝑆 (note that the 𝑀 = 1 case of a Stolz angle is the real line [0, 1]). (Continuity on 𝑆 ∖ {1} follows more generally from psercn 26496.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	abelth2 26512*	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 26513	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 26514	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 26515	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 26516*	Lemma for reeff1o 26517. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 26517	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 26518	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 26519	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 26520	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 26521	Lemma for pire 26526, pigt2lt4 26524 and sinpi 26525. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	pilem2 26522	Lemma for pire 26526, pigt2lt4 26524 and sinpi 26525. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ (2(,)4))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (sin‘𝐴) = 0)    &   ⊢ (𝜑 → (sin‘𝐵) = 0)    ⇒   ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)
Theorem	pilem3 26523	Lemma for pire 26526, pigt2lt4 26524 and sinpi 26525. 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 26524	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 26525	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 26526	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	2pire 26527	(2 · π) is a real number. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · π) ∈ ℝ
Theorem	picn 26528	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	2picn 26529	(2 · π) is a complex number. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · π) ∈ ℂ
Theorem	pipos 26530	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pige0 26531	π is nonnegative. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 ≤ π
Theorem	pine0 26532	π is nonzero. (Contributed by SN, 25-Apr-2025.)
⊢ π ≠ 0
Theorem	pirp 26533	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 26534	-π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 26535	Lemma for sinhalfpi 26540 and coshalfpi 26541. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 26536	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 26537	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ
Theorem	neghalfpirx 26538	-π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ*
Theorem	pidiv2halves 26539	Adding π / 2 to itself gives π. See 2halves 12449. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ((π / 2) + (π / 2)) = π
Theorem	sinhalfpi 26540	The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(π / 2)) = 1
Theorem	coshalfpi 26541	The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(π / 2)) = 0
Theorem	cosneghalfpi 26542	The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
⊢ (cos‘-(π / 2)) = 0
Theorem	efhalfpi 26543	The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (π / 2))) = i
Theorem	cospi 26544	The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘π) = -1
Theorem	efipi 26545	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 26546	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ ((exp‘(i · π)) + 1) = 0
Theorem	sin2pi 26547	The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(2 · π)) = 0
Theorem	cos2pi 26548	The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(2 · π)) = 1
Theorem	ef2pi 26549	The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (2 · π))) = 1
Theorem	ef2kpi 26550	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 26551	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 26552	Lemma for sinper 26553 and cosper 26554. (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 26553	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴))
Theorem	cosper 26554	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴))
Theorem	sin2kpi 26555	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 26556	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 26557	Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴))
Theorem	cos2pim 26558	Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴))
Theorem	sinmpi 26559	Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴))
Theorem	cosmpi 26560	Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴))
Theorem	sinppi 26561	Sine of a number plus π. (Contributed by NM, 10-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴))
Theorem	cosppi 26562	Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴))
Theorem	efimpi 26563	The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴)))
Theorem	sinhalfpip 26564	The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴))
Theorem	sinhalfpim 26565	The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
Theorem	coshalfpip 26566	The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴))
Theorem	coshalfpim 26567	The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴))
Theorem	ptolemy 26568	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 16214, 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 26569	Lemma for sincosq1sgn 26570. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴))
Theorem	sincosq1sgn 26570	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 26571	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 26572	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 26573	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 26574	Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq0negpitopi 26575	Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)}))
Theorem	tanrpcl 26576	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
Theorem	tangtx 26577	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 26578	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 26579	The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴))
Theorem	sinq12ge0 26580	The sine of a number between 0 and π is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (0[,]π) → 0 ≤ (sin‘𝐴))
Theorem	sinq34lt0t 26581	The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0)
Theorem	cosq14gt0 26582	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 26583	The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.)
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴))
Theorem	sincosq1eq 26584	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 26585	The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2)))
Theorem	tan4thpi 26586	The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) (Proof shortened by SN, 2-Sep-2025.)
⊢ (tan‘(π / 4)) = 1
Theorem	tan4thpiOLD 26587	Obsolete version of tan4thpi 26586 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 26588	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 26589	The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
Theorem	pigt3 26590	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	pige3 26591	π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ 3 ≤ π
Theorem	pige3ALT 26592	Alternate proof of pige3 26591. 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 26593	The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴)))
Theorem	sinkpi 26594	The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0)
Theorem	coskpi 26595	The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)
Theorem	sineq0 26596	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 26597	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 26598	Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.)
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1)
Theorem	cosq34lt1 26599	Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.)
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1)
Theorem	efeq1 26600	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 · π))) ∈ ℤ))