Home | Metamath
Proof Explorer Theorem List (p. 251 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-28679) |
Hilbert Space Explorer
(28680-30202) |
Users' Mathboxes
(30203-44991) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pserdvlem1 25001* | Lemma for pserdv 25003. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅)) | ||
Theorem | pserdvlem2 25002* | Lemma for pserdv 25003. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) & ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) | ||
Theorem | pserdv 25003* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) & ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) | ||
Theorem | pserdv2 25004* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) & ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ ((𝑘 · (𝐴‘𝑘)) · (𝑦↑(𝑘 − 1))))) | ||
Theorem | abelthlem1 25005* | Lemma for abelth 25015. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) | ||
Theorem | abelthlem2 25006* | Lemma for abelth 25015. 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 25007* | Lemma for abelth 25015. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | abelthlem4 25008* | Lemma for abelth 25015. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) | ||
Theorem | abelthlem5 25009* | Lemma for abelth 25015. (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 25010* | Lemma for abelth 25015. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | ||
Theorem | abelthlem7a 25011* | Lemma for abelth 25015. (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 25012* | Lemma for abelth 25015. (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 25013* | Lemma for abelth 25015. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) | ||
Theorem | abelthlem9 25014* | Lemma for abelth 25015. 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 25015* | 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 25000.) (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 25016* | 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→ℂ)) | ||
Theorem | efcn 25017 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
⊢ exp ∈ (ℂ–cn→ℂ) | ||
Theorem | sincn 25018 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ sin ∈ (ℂ–cn→ℂ) | ||
Theorem | coscn 25019 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ cos ∈ (ℂ–cn→ℂ) | ||
Theorem | reeff1olem 25020* | Lemma for reeff1o 25021. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) | ||
Theorem | reeff1o 25021 | 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 25022 | 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 25023 | 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 25024 | 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 𝑃) | ||
Theorem | pilem1 25025 | Lemma for pire 25030, pigt2lt4 25028 and sinpi 25029. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0)) | ||
Theorem | pilem2 25026 | Lemma for pire 25030, pigt2lt4 25028 and sinpi 25029. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ (2(,)4)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (sin‘𝐴) = 0) & ⊢ (𝜑 → (sin‘𝐵) = 0) ⇒ ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵) | ||
Theorem | pilem3 25027 | Lemma for pire 25030, pigt2lt4 25028 and sinpi 25029. 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 25028 | π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ (2 < π ∧ π < 4) | ||
Theorem | sinpi 25029 | The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘π) = 0 | ||
Theorem | pire 25030 | π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ π ∈ ℝ | ||
Theorem | picn 25031 | π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ π ∈ ℂ | ||
Theorem | pipos 25032 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ 0 < π | ||
Theorem | pirp 25033 | π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ π ∈ ℝ+ | ||
Theorem | negpicn 25034 | -π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -π ∈ ℂ | ||
Theorem | sinhalfpilem 25035 | Lemma for sinhalfpi 25040 and coshalfpi 25041. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0) | ||
Theorem | halfpire 25036 | π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (π / 2) ∈ ℝ | ||
Theorem | neghalfpire 25037 | -π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ | ||
Theorem | neghalfpirx 25038 | -π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ* | ||
Theorem | pidiv2halves 25039 | Adding π / 2 to itself gives π. See 2halves 11852. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ((π / 2) + (π / 2)) = π | ||
Theorem | sinhalfpi 25040 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(π / 2)) = 1 | ||
Theorem | coshalfpi 25041 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(π / 2)) = 0 | ||
Theorem | cosneghalfpi 25042 | The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (cos‘-(π / 2)) = 0 | ||
Theorem | efhalfpi 25043 | The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (π / 2))) = i | ||
Theorem | cospi 25044 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘π) = -1 | ||
Theorem | efipi 25045 | 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 25046 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ ((exp‘(i · π)) + 1) = 0 | ||
Theorem | sin2pi 25047 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(2 · π)) = 0 | ||
Theorem | cos2pi 25048 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(2 · π)) = 1 | ||
Theorem | ef2pi 25049 | The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (2 · π))) = 1 | ||
Theorem | ef2kpi 25050 | 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 25051 | 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 25052 | Lemma for sinper 25053 and cosper 25054. (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 25053 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴)) | ||
Theorem | cosper 25054 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴)) | ||
Theorem | sin2kpi 25055 | 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 25056 | 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 25057 | Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴)) | ||
Theorem | cos2pim 25058 | Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinmpi 25059 | Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴)) | ||
Theorem | cosmpi 25060 | Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴)) | ||
Theorem | sinppi 25061 | Sine of a number plus π. (Contributed by NM, 10-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) | ||
Theorem | cosppi 25062 | Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) | ||
Theorem | efimpi 25063 | The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴))) | ||
Theorem | sinhalfpip 25064 | The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinhalfpim 25065 | The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | coshalfpip 25066 | The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴)) | ||
Theorem | coshalfpim 25067 | The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴)) | ||
Theorem | ptolemy 25068 | 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 15510, 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 25069 | Lemma for sincosq1sgn 25070. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴)) | ||
Theorem | sincosq1sgn 25070 | 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 25071 | 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 25072 | 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 25073 | 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 25074 | Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) | ||
Theorem | coseq0negpitopi 25075 | Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)})) | ||
Theorem | tanrpcl 25076 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) |
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+) | ||
Theorem | tangtx 25077 | 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 25078 | 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 25079 | The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴)) | ||
Theorem | sinq12ge0 25080 | The sine of a number between 0 and π is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ (𝐴 ∈ (0[,]π) → 0 ≤ (sin‘𝐴)) | ||
Theorem | sinq34lt0t 25081 | The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0) | ||
Theorem | cosq14gt0 25082 | 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 25083 | The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴)) | ||
Theorem | sincosq1eq 25084 | 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 25085 | The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.) |
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2))) | ||
Theorem | tan4thpi 25086 | The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (tan‘(π / 4)) = 1 | ||
Theorem | sincos6thpi 25087 | 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 25088 | The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2)) | ||
Theorem | pigt3 25089 | π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ 3 < π | ||
Theorem | pige3 25090 | π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ 3 ≤ π | ||
Theorem | pige3ALT 25091 | Alternate proof of pige3 25090. 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 25092 | The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴))) | ||
Theorem | sinkpi 25093 | The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0) | ||
Theorem | coskpi 25094 | The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1) | ||
Theorem | sineq0 25095 | 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 25096 | 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 25097 | Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | cosq34lt1 25098 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | efeq1 25099 | 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 25100 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |