Home | Metamath
Proof Explorer Theorem List (p. 250 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ulmi 24901* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶) | ||
Theorem | ulmclm 24902* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴)) | ||
Theorem | ulmres 24903 | 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 24904* | Lemma for ulmshft 24905. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
Theorem | ulmshft 24905* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
Theorem | ulm0 24906 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺) | ||
Theorem | ulmuni 24907 | A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻) | ||
Theorem | ulmdm 24908 | 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 24909* | Lemma for ulmcau 24910 and ulmcau2 24911: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 14703. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) | ||
Theorem | ulmcau 24910* | 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 24911 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) | ||
Theorem | ulmcau2 24911* | 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 24912* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇)) | ||
Theorem | ulmbdd 24913* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥) | ||
Theorem | ulmcn 24914 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ)) | ||
Theorem | ulmdvlem1 24915* | Lemma for ulmdv 24918. (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 24916* | Lemma for ulmdv 24918. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋) | ||
Theorem | ulmdvlem3 24917* | Lemma for ulmdv 24918. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧)) | ||
Theorem | ulmdv 24918* | 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 24919* | 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 24920* | 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 24921 | 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 24196.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶MblFn) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
Theorem | iblulm 24922 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐿1) | ||
Theorem | itgulm 24923* | 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 24924* | 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 24925* | 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 24926* | 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 24927* | 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 24928* | Lemma for radcnvlt1 24933, radcnvle 24935. 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 24929* | Lemma for radcnvlt1 24933, radcnvle 24935. 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 24930* | Lemma for radcnvlt1 24933, radcnvle 24935. 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 24931* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) ⇒ ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) | ||
Theorem | radcnvcl 24932* | 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 24933* | 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 24934* | 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 24935* | 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 24936* | 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 24937* | 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 24938* | Since by pserulm 24937 the series converges uniformly, it is also continuous by ulmcn 24914. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
Theorem | psercnlem2 24939* | Lemma for psercn 24941. (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 24940* | Lemma for psercn 24941. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) | ||
Theorem | psercn 24941* | 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 24942* | Lemma for pserdv 24944. (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 24943* | Lemma for pserdv 24944. (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 24944* | 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 24945* | 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 24946* | Lemma for abelth 24956. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) | ||
Theorem | abelthlem2 24947* | Lemma for abelth 24956. 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 24948* | Lemma for abelth 24956. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | abelthlem4 24949* | Lemma for abelth 24956. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) | ||
Theorem | abelthlem5 24950* | Lemma for abelth 24956. (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 24951* | Lemma for abelth 24956. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | ||
Theorem | abelthlem7a 24952* | Lemma for abelth 24956. (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 24953* | Lemma for abelth 24956. (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 24954* | Lemma for abelth 24956. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) | ||
Theorem | abelthlem9 24955* | Lemma for abelth 24956. 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 24956* | 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 24941.) (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 24957* | 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 24958 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
⊢ exp ∈ (ℂ–cn→ℂ) | ||
Theorem | sincn 24959 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ sin ∈ (ℂ–cn→ℂ) | ||
Theorem | coscn 24960 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ cos ∈ (ℂ–cn→ℂ) | ||
Theorem | reeff1olem 24961* | Lemma for reeff1o 24962. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) | ||
Theorem | reeff1o 24962 | 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 24963 | 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 24964 | 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 24965 | 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 24966 | Lemma for pire 24971, pigt2lt4 24969 and sinpi 24970. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0)) | ||
Theorem | pilem2 24967 | Lemma for pire 24971, pigt2lt4 24969 and sinpi 24970. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ (2(,)4)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (sin‘𝐴) = 0) & ⊢ (𝜑 → (sin‘𝐵) = 0) ⇒ ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵) | ||
Theorem | pilem3 24968 | Lemma for pire 24971, pigt2lt4 24969 and sinpi 24970. 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 24969 | π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ (2 < π ∧ π < 4) | ||
Theorem | sinpi 24970 | The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘π) = 0 | ||
Theorem | pire 24971 | π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ π ∈ ℝ | ||
Theorem | picn 24972 | π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ π ∈ ℂ | ||
Theorem | pipos 24973 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ 0 < π | ||
Theorem | pirp 24974 | π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ π ∈ ℝ+ | ||
Theorem | negpicn 24975 | -π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -π ∈ ℂ | ||
Theorem | sinhalfpilem 24976 | Lemma for sinhalfpi 24981 and coshalfpi 24982. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0) | ||
Theorem | halfpire 24977 | π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (π / 2) ∈ ℝ | ||
Theorem | neghalfpire 24978 | -π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ | ||
Theorem | neghalfpirx 24979 | -π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ* | ||
Theorem | pidiv2halves 24980 | Adding π / 2 to itself gives π. See 2halves 11853. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ((π / 2) + (π / 2)) = π | ||
Theorem | sinhalfpi 24981 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(π / 2)) = 1 | ||
Theorem | coshalfpi 24982 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(π / 2)) = 0 | ||
Theorem | cosneghalfpi 24983 | The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (cos‘-(π / 2)) = 0 | ||
Theorem | efhalfpi 24984 | The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (π / 2))) = i | ||
Theorem | cospi 24985 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘π) = -1 | ||
Theorem | efipi 24986 | 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 24987 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ ((exp‘(i · π)) + 1) = 0 | ||
Theorem | sin2pi 24988 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(2 · π)) = 0 | ||
Theorem | cos2pi 24989 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(2 · π)) = 1 | ||
Theorem | ef2pi 24990 | The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (2 · π))) = 1 | ||
Theorem | ef2kpi 24991 | 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 24992 | 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 24993 | Lemma for sinper 24994 and cosper 24995. (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 24994 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴)) | ||
Theorem | cosper 24995 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴)) | ||
Theorem | sin2kpi 24996 | 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 24997 | 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 24998 | Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴)) | ||
Theorem | cos2pim 24999 | Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinmpi 25000 | Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |