![]() |
Metamath
Proof Explorer Theorem List (p. 247 of 437) | < 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: | ![]() (1-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mbfulm 24601 | A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim 23876.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶MblFn) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
Theorem | iblulm 24602 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐿1) | ||
Theorem | itgulm 24603* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) ⇝ ∫𝑆(𝐺‘𝑥) d𝑥) | ||
Theorem | itgulm2 24604* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ 𝐿1) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ∈ 𝐿1 ∧ (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥)) | ||
Theorem | pserval 24605* | Value of the function 𝐺 that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) ⇒ ⊢ (𝑋 ∈ ℂ → (𝐺‘𝑋) = (𝑚 ∈ ℕ0 ↦ ((𝐴‘𝑚) · (𝑋↑𝑚)))) | ||
Theorem | pserval2 24606* | Value of the function 𝐺 that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) ⇒ ⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑁) = ((𝐴‘𝑁) · (𝑋↑𝑁))) | ||
Theorem | psergf 24607* | The sequence of terms in the infinite sequence defining a power series for fixed 𝑋. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ) | ||
Theorem | radcnvlem1 24608* | Lemma for radcnvlt1 24613, radcnvle 24615. If 𝑋 is a point closer to zero than 𝑌 and the power series converges at 𝑌, then it converges absolutely at 𝑋, even if the terms in the sequence are multiplied by 𝑛. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌)) & ⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ ) & ⊢ 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) ⇒ ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ ) | ||
Theorem | radcnvlem2 24609* | Lemma for radcnvlt1 24613, radcnvle 24615. If 𝑋 is a point closer to zero than 𝑌 and the power series converges at 𝑌, then it converges absolutely at 𝑋. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌)) & ⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ) | ||
Theorem | radcnvlem3 24610* | Lemma for radcnvlt1 24613, radcnvle 24615. If 𝑋 is a point closer to zero than 𝑌 and the power series converges at 𝑌, then it converges at 𝑋. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌)) & ⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) | ||
Theorem | radcnv0 24611* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) ⇒ ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) | ||
Theorem | radcnvcl 24612* | The radius of convergence 𝑅 of an infinite series is a nonnegative extended real number. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ⇒ ⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) | ||
Theorem | radcnvlt1 24613* | If 𝑋 is within the open disk of radius 𝑅 centered at zero, then the infinite series converges absolutely at 𝑋, and also converges when the series is multiplied by 𝑛. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < 𝑅) & ⊢ 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) ⇒ ⊢ (𝜑 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ )) | ||
Theorem | radcnvlt2 24614* | If 𝑋 is within the open disk of radius 𝑅 centered at zero, then the infinite series converges at 𝑋. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < 𝑅) ⇒ ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) | ||
Theorem | radcnvle 24615* | If 𝑋 is a convergent point of the infinite series, then 𝑋 is within the closed disk of radius 𝑅 centered at zero. Or, by contraposition, the series diverges at any point strictly more than 𝑅 from the origin. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅) | ||
Theorem | dvradcnv 24616* | The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is at least as large as the radius of convergence of 𝐺. (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < 𝑅) ⇒ ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ ) | ||
Theorem | pserulm 24617* | If 𝑆 is a region contained in a circle of radius 𝑀 < 𝑅, then the sequence of partial sums of the infinite series converges uniformly on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) ⇒ ⊢ (𝜑 → 𝐻(⇝𝑢‘𝑆)𝐹) | ||
Theorem | psercn2 24618* | Since by pserulm 24617 the series converges uniformly, it is also continuous by ulmcn 24594. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
Theorem | psercnlem2 24619* | Lemma for psercn 24621. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ (◡abs “ (0[,]𝑀)) ∧ (◡abs “ (0[,]𝑀)) ⊆ 𝑆)) | ||
Theorem | psercnlem1 24620* | Lemma for psercn 24621. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) | ||
Theorem | psercn 24621* | An infinite series converges to a continuous function on the open disk of radius 𝑅, where 𝑅 is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
Theorem | pserdvlem1 24622* | Lemma for pserdv 24624. (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 24623* | Lemma for pserdv 24624. (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 24624* | 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 24625* | 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 24626* | Lemma for abelth 24636. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) | ||
Theorem | abelthlem2 24627* | Lemma for abelth 24636. 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 24628* | Lemma for abelth 24636. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | abelthlem4 24629* | Lemma for abelth 24636. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) | ||
Theorem | abelthlem5 24630* | Lemma for abelth 24636. (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 24631* | Lemma for abelth 24636. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | ||
Theorem | abelthlem7a 24632* | Lemma for abelth 24636. (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 24633* | Lemma for abelth 24636. (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 24634* | Lemma for abelth 24636. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) | ||
Theorem | abelthlem9 24635* | Lemma for abelth 24636. 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 24636* | 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 24621.) (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 24637* | 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 24638 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
⊢ exp ∈ (ℂ–cn→ℂ) | ||
Theorem | sincn 24639 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ sin ∈ (ℂ–cn→ℂ) | ||
Theorem | coscn 24640 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ cos ∈ (ℂ–cn→ℂ) | ||
Theorem | reeff1olem 24641* | Lemma for reeff1o 24642. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) | ||
Theorem | reeff1o 24642 | 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 24643 | 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 24644 | 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 24645 | 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 24646 | Lemma for pire 24652, pigt2lt4 24650 and sinpi 24651. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0)) | ||
Theorem | pilem2 24647 | Lemma for pire 24652, pigt2lt4 24650 and sinpi 24651. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ (2(,)4)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (sin‘𝐴) = 0) & ⊢ (𝜑 → (sin‘𝐵) = 0) ⇒ ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵) | ||
Theorem | pilem3 24648 | Lemma for pire 24652, pigt2lt4 24650 and sinpi 24651. 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 | pilem3OLD 24649 | Obsolete proof of pilem3 24648 as of 30-Jun-2022. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0) | ||
Theorem | pigt2lt4 24650 | π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ (2 < π ∧ π < 4) | ||
Theorem | sinpi 24651 | The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘π) = 0 | ||
Theorem | pire 24652 | π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ π ∈ ℝ | ||
Theorem | picn 24653 | π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ π ∈ ℂ | ||
Theorem | pipos 24654 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ 0 < π | ||
Theorem | pirp 24655 | π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ π ∈ ℝ+ | ||
Theorem | negpicn 24656 | -π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -π ∈ ℂ | ||
Theorem | sinhalfpilem 24657 | Lemma for sinhalfpi 24662 and coshalfpi 24663. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0) | ||
Theorem | halfpire 24658 | π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (π / 2) ∈ ℝ | ||
Theorem | neghalfpire 24659 | -π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ | ||
Theorem | neghalfpirx 24660 | -π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ* | ||
Theorem | pidiv2halves 24661 | Adding π / 2 to itself gives π. See 2halves 11614. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ((π / 2) + (π / 2)) = π | ||
Theorem | sinhalfpi 24662 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(π / 2)) = 1 | ||
Theorem | coshalfpi 24663 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(π / 2)) = 0 | ||
Theorem | cosneghalfpi 24664 | The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (cos‘-(π / 2)) = 0 | ||
Theorem | efhalfpi 24665 | The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (π / 2))) = i | ||
Theorem | cospi 24666 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘π) = -1 | ||
Theorem | efipi 24667 | 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 24668 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ ((exp‘(i · π)) + 1) = 0 | ||
Theorem | sin2pi 24669 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(2 · π)) = 0 | ||
Theorem | cos2pi 24670 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(2 · π)) = 1 | ||
Theorem | ef2pi 24671 | The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (2 · π))) = 1 | ||
Theorem | ef2kpi 24672 | 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 24673 | 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 24674 | Lemma for sinper 24675 and cosper 24676. (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 24675 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴)) | ||
Theorem | cosper 24676 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴)) | ||
Theorem | sin2kpi 24677 | 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 24678 | 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 24679 | Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴)) | ||
Theorem | cos2pim 24680 | Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinmpi 24681 | Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴)) | ||
Theorem | cosmpi 24682 | Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴)) | ||
Theorem | sinppi 24683 | Sine of a number plus π. (Contributed by NM, 10-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) | ||
Theorem | cosppi 24684 | Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) | ||
Theorem | efimpi 24685 | The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴))) | ||
Theorem | sinhalfpip 24686 | The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinhalfpim 24687 | The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | coshalfpip 24688 | The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴)) | ||
Theorem | coshalfpim 24689 | The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴)) | ||
Theorem | ptolemy 24690 | 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 15308, 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 24691 | Lemma for sincosq1sgn 24692. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴)) | ||
Theorem | sincosq1sgn 24692 | 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 24693 | 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 24694 | 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 24695 | 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 24696 | Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) | ||
Theorem | coseq0negpitopi 24697 | Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)})) | ||
Theorem | tanrpcl 24698 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) |
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+) | ||
Theorem | tangtx 24699 | 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 24700 | 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‘𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |