HomeTheorem List (p. 268 of 510)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 268 of 510) | < 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-31513) |
Hilbert Space Explorer
(31514-33036) |
Users' Mathboxes
(33037-50959) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ulmcl 26701 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
| ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) | ||
| Theorem | ulmf 26702* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
| ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆)) | ||
| Theorem | ulmpm 26703 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
| ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐹 ∈ ((ℂ ↑m 𝑆) ↑pm ℤ)) | ||
| Theorem | ulmf2 26704 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
| ⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | ||
| Theorem | ulm2 26705* | Simplify ulmval 26700 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
| Theorem | ulmi 26706* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶) | ||
| Theorem | ulmclm 26707* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴)) | ||
| Theorem | ulmres 26708 | A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ (𝐹 ↾ 𝑊)(⇝𝑢‘𝑆)𝐺)) | ||
| Theorem | ulmshftlem 26709* | Lemma for ulmshft 26710. (Contributed by Mario Carneiro, 24-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
| Theorem | ulmshft 26710* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
| Theorem | ulm0 26711 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺) | ||
| Theorem | ulmuni 26712 | A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
| ⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻) | ||
| Theorem | ulmdm 26713 | Two ways to express that a function has a limit. (The expression ((⇝𝑢‘𝑆)‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Mario Carneiro, 5-Jul-2017.) |
| ⊢ (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ 𝐹(⇝𝑢‘𝑆)((⇝𝑢‘𝑆)‘𝐹)) | ||
| Theorem | ulmcaulem 26714* | Lemma for ulmcau 26715 and ulmcau2 26716: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 15516. (Contributed by Mario Carneiro, 1-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) | ||
| Theorem | ulmcau 26715* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < 𝑥 there is a 𝑗 such that for all 𝑗 ≤ 𝑘 the functions 𝐹(𝑘) and 𝐹(𝑗) are uniformly within 𝑥 of each other on 𝑆. This is the four-quantifier version, see ulmcau2 26716 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) | ||
| Theorem | ulmcau2 26716* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < 𝑥 there is a 𝑗 such that for all 𝑗 ≤ 𝑘, 𝑚 the functions 𝐹(𝑘) and 𝐹(𝑚) are uniformly within 𝑥 of each other on 𝑆. (Contributed by Mario Carneiro, 1-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) | ||
| Theorem | ulmss 26717* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇)) | ||
| Theorem | ulmbdd 26718* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥) | ||
| Theorem | ulmcn 26719 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ)) | ||
| Theorem | ulmdvlem1 26720* | Lemma for ulmdv 26723. (Contributed by Mario Carneiro, 3-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊) & ⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈) & ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2)) & ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶) & ⊢ ((𝜑 ∧ 𝜓) → ((abs‘(𝑌 − 𝐶)) < 𝑊 → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅) | ||
| Theorem | ulmdvlem2 26721* | Lemma for ulmdv 26723. (Contributed by Mario Carneiro, 8-May-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋) | ||
| Theorem | ulmdvlem3 26722* | Lemma for ulmdv 26723. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧)) | ||
| Theorem | ulmdv 26723* | If 𝐹 is a sequence of differentiable functions on 𝑋 which converge pointwise to 𝐺, and the derivatives of 𝐹(𝑛) converge uniformly to 𝐻, then 𝐺 is differentiable with derivative 𝐻. (Contributed by Mario Carneiro, 27-Feb-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ (𝜑 → (𝑆 D 𝐺) = 𝐻) | ||
| Theorem | mtest 26724* | The Weierstrass M-test. If 𝐹 is a sequence of functions which are uniformly bounded by the convergent sequence 𝑀(𝑘), then the series generated by the sequence 𝐹 converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘)) & ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq𝑁( ∘f + , 𝐹) ∈ dom (⇝𝑢‘𝑆)) | ||
| Theorem | mtestbdd 26725* | Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
| ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘)) & ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑁( ∘f + , 𝐹)(⇝𝑢‘𝑆)𝑇) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝑇‘𝑧)) ≤ 𝑥) | ||
| Theorem | mbfulm 26726 | 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 25982.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶MblFn) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
| Theorem | iblulm 26727 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐿1) | ||
| Theorem | itgulm 26728* | 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 26729* | 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 26730* | 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 26731* | 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 26732* | 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 26733* | Lemma for radcnvlt1 26738, radcnvle 26740. 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 26734* | Lemma for radcnvlt1 26738, radcnvle 26740. 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 26735* | Lemma for radcnvlt1 26738, radcnvle 26740. 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 26736* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
| ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) ⇒ ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) | ||
| Theorem | radcnvcl 26737* | 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 26738* | 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 26739* | 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 26740* | 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 26741* | 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 26742* | 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 26743* | Since by pserulm 26742 the series converges uniformly, it is also continuous by ulmcn 26719. (Contributed by Mario Carneiro, 3-Mar-2015.) Avoid ax-mulf 11273. (Revised by GG, 16-Mar-2025.) |
| ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
| Theorem | psercnlem2 26744* | Lemma for psercn 26746. (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 26745* | Lemma for psercn 26746. (Contributed by Mario Carneiro, 18-Mar-2015.) |
| ⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) | ||
| Theorem | psercn 26746* | 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 26747* | Lemma for pserdv 26749. (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 26748* | Lemma for pserdv 26749. (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 26749* | 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 26750* | 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 26751* | Lemma for abelth 26761. (Contributed by Mario Carneiro, 1-Apr-2015.) |
| ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) | ||
| Theorem | abelthlem2 26752* | Lemma for abelth 26761. 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 26753* | Lemma for abelth 26761. (Contributed by Mario Carneiro, 31-Mar-2015.) |
| ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | ||
| Theorem | abelthlem4 26754* | Lemma for abelth 26761. (Contributed by Mario Carneiro, 31-Mar-2015.) |
| ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) | ||
| Theorem | abelthlem5 26755* | Lemma for abelth 26761. (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 26756* | Lemma for abelth 26761. (Contributed by Mario Carneiro, 2-Apr-2015.) |
| ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | ||
| Theorem | abelthlem7a 26757* | Lemma for abelth 26761. (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 26758* | Lemma for abelth 26761. (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 26759* | Lemma for abelth 26761. (Contributed by Mario Carneiro, 2-Apr-2015.) |
| ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) | ||
| Theorem | abelthlem9 26760* | Lemma for abelth 26761. 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 26761* | 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 26746.) (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 26762* | 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 26763 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
| ⊢ exp ∈ (ℂ–cn→ℂ) | ||
| Theorem | sincn 26764 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
| ⊢ sin ∈ (ℂ–cn→ℂ) | ||
| Theorem | coscn 26765 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
| ⊢ cos ∈ (ℂ–cn→ℂ) | ||
| Theorem | reeff1olem 26766* | Lemma for reeff1o 26767. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) | ||
| Theorem | reeff1o 26767 | 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 26768 | 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 26769 | 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 26770 | 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 26771 | Lemma for pire 26776, pigt2lt4 26774 and sinpi 26775. (Contributed by Mario Carneiro, 9-May-2014.) |
| ⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0)) | ||
| Theorem | pilem2 26772 | Lemma for pire 26776, pigt2lt4 26774 and sinpi 26775. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ (2(,)4)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (sin‘𝐴) = 0) & ⊢ (𝜑 → (sin‘𝐵) = 0) ⇒ ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵) | ||
| Theorem | pilem3 26773 | Lemma for pire 26776, pigt2lt4 26774 and sinpi 26775. 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 26774 | π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
| ⊢ (2 < π ∧ π < 4) | ||
| Theorem | sinpi 26775 | The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin‘π) = 0 | ||
| Theorem | pire 26776 | π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ π ∈ ℝ | ||
| Theorem | 2pire 26777 | (2 · π) is a real number. (Contributed by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ (2 · π) ∈ ℝ | ||
| Theorem | picn 26778 | π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
| ⊢ π ∈ ℂ | ||
| Theorem | 2picn 26779 | (2 · π) is a complex number. (Contributed by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ (2 · π) ∈ ℂ | ||
| Theorem | pipos 26780 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
| ⊢ 0 < π | ||
| Theorem | pige0 26781 | π is nonnegative. (Contributed by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 0 ≤ π | ||
| Theorem | pine0 26782 | π is nonzero. (Contributed by SN, 25-Apr-2025.) |
| ⊢ π ≠ 0 | ||
| Theorem | pirp 26783 | π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ π ∈ ℝ+ | ||
| Theorem | negpicn 26784 | -π is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -π ∈ ℂ | ||
| Theorem | sinhalfpilem 26785 | Lemma for sinhalfpi 26790 and coshalfpi 26791. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0) | ||
| Theorem | halfpire 26786 | π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (π / 2) ∈ ℝ | ||
| Theorem | neghalfpire 26787 | -π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -(π / 2) ∈ ℝ | ||
| Theorem | neghalfpirx 26788 | -π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -(π / 2) ∈ ℝ* | ||
| Theorem | pidiv2halves 26789 | Adding π / 2 to itself gives π. See 2halves 12557. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ ((π / 2) + (π / 2)) = π | ||
| Theorem | sinhalfpi 26790 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin‘(π / 2)) = 1 | ||
| Theorem | coshalfpi 26791 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos‘(π / 2)) = 0 | ||
| Theorem | cosneghalfpi 26792 | The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (cos‘-(π / 2)) = 0 | ||
| Theorem | efhalfpi 26793 | The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
| ⊢ (exp‘(i · (π / 2))) = i | ||
| Theorem | cospi 26794 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos‘π) = -1 | ||
| Theorem | efipi 26795 | 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 26796 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
| ⊢ ((exp‘(i · π)) + 1) = 0 | ||
| Theorem | sin2pi 26797 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin‘(2 · π)) = 0 | ||
| Theorem | cos2pi 26798 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos‘(2 · π)) = 1 | ||
| Theorem | ef2pi 26799 | The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
| ⊢ (exp‘(i · (2 · π))) = 1 | ||
| Theorem | ef2kpi 26800 | If 𝐾 is an integer, then the exponential of 2𝐾πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
| ⊢ (𝐾 ∈ ℤ → (exp‘((i · (2 · π)) · 𝐾)) = 1) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |