P. 268 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26701-26800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	taylply2 26701*	The Taylor polynomial is a polynomial of degree (at most) 𝑁. This version of taylply 26702 shows that the coefficients of 𝑇 are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017.) Avoid ax-mulf 11284. (Revised by GG, 30-Apr-2025.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑇 ∈ (Poly‘𝐷) ∧ (deg‘𝑇) ≤ 𝑁))
Theorem	taylply 26702	The Taylor polynomial is a polynomial of degree (at most) 𝑁. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → (𝑇 ∈ (Poly‘ℂ) ∧ (deg‘𝑇) ≤ 𝑁))
Theorem	dvtaylp 26703	The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)))    ⇒   ⊢ (𝜑 → (ℂ D ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)) = (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵))
Theorem	dvntaylp 26704	The 𝑀-th derivative of the Taylor polynomial is the Taylor polynomial of the 𝑀-th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 𝑀)))    ⇒   ⊢ (𝜑 → ((ℂ D𝑛 ((𝑁 + 𝑀)(𝑆 Tayl 𝐹)𝐵))‘𝑀) = (𝑁(𝑆 Tayl ((𝑆 D𝑛 𝐹)‘𝑀))𝐵))
Theorem	dvntaylp0 26705	The first 𝑁 derivatives of the Taylor polynomial at 𝐵 match the derivatives of the function from which it is derived. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → (((ℂ D𝑛 𝑇)‘𝑀)‘𝐵) = (((𝑆 D𝑛 𝐹)‘𝑀)‘𝐵))
Theorem	taylthlem1 26706*	Lemma for taylth 26708. This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that 𝑆 = ℝ, we can only do this part generically, and for taylth 26708 itself we must restrict to ℝ. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    &   ⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))    &   ⊢ ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) limℂ 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) limℂ 𝐵))    ⇒   ⊢ (𝜑 → 0 ∈ (𝑅 limℂ 𝐵))
Theorem	taylthlem2 26707*	Lemma for taylth 26708. (Contributed by Mario Carneiro, 1-Jan-2017.) Avoid ax-mulf 11284. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁))    &   ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵))    ⇒   ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))
Theorem	taylth 26708*	Taylor's theorem. The Taylor polynomial of a 𝑁-times differentiable function is such that the error term goes to zero faster than (𝑥 − 𝐵)↑𝑁. This is Metamath 100 proof #35. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)    &   ⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))    ⇒   ⊢ (𝜑 → 0 ∈ (𝑅 limℂ 𝐵))
14.2.2  Uniform convergence
Syntax	culm 26709	Extend class notation to include the uniform convergence predicate.
class ⇝𝑢
Definition	df-ulm 26710*	Define the uniform convergence of a sequence of functions. Here 𝐹(⇝𝑢‘𝑆)𝐺 if 𝐹 is a sequence of functions 𝐹(𝑛), 𝑛 ∈ ℕ defined on 𝑆 and 𝐺 is a function on 𝑆, and for every 0 < 𝑥 there is a 𝑗 such that the functions 𝐹(𝑘) for 𝑗 ≤ 𝑘 are all uniformly within 𝑥 of 𝐺 on the domain 𝑆. Compare with df-clim 15661. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ ⇝𝑢 = (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)})
Theorem	ulmrel 26711	The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ Rel (⇝𝑢‘𝑆)
Theorem	ulmscl 26712	Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V)
Theorem	ulmval 26713*	Express the predicate: The sequence of functions 𝐹 converges uniformly to 𝐺 on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
Theorem	ulmcl 26714	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ)
Theorem	ulmf 26715*	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆))
Theorem	ulmpm 26716	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐹 ∈ ((ℂ ↑m 𝑆) ↑pm ℤ))
Theorem	ulmf2 26717	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
Theorem	ulm2 26718*	Simplify ulmval 26713 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)    &   ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	ulmi 26719*	The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶)
Theorem	ulmclm 26720*	A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘))    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴))
Theorem	ulmres 26721	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 26722*	Lemma for ulmshft 26723. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺))
Theorem	ulmshft 26723*	A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺))
Theorem	ulm0 26724	Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺)
Theorem	ulmuni 26725	A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.)
⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻)
Theorem	ulmdm 26726	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 26727*	Lemma for ulmcau 26728 and ulmcau2 26729: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 15529. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥))
Theorem	ulmcau 26728*	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 26729 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥))
Theorem	ulmcau2 26729*	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 26730*	A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇))
Theorem	ulmbdd 26731*	A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥)
Theorem	ulmcn 26732	A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ))    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ))
Theorem	ulmdvlem1 26733*	Lemma for ulmdv 26736. (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 26734*	Lemma for ulmdv 26736. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋)
Theorem	ulmdvlem3 26735*	Lemma for ulmdv 26736. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧))
Theorem	ulmdv 26736*	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 26737*	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 26738*	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 26739	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 25995.) (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶MblFn)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	iblulm 26740	A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐿1)
Theorem	itgulm 26741*	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 26742*	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𝑥))
14.2.3  Power series
Theorem	pserval 26743*	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 26744*	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 26745*	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 26746*	Lemma for radcnvlt1 26751, radcnvle 26753. 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 26747*	Lemma for radcnvlt1 26751, radcnvle 26753. 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 26748*	Lemma for radcnvlt1 26751, radcnvle 26753. 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 26749*	Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    ⇒   ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
Theorem	radcnvcl 26750*	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 26751*	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 26752*	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 26753*	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 26754*	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 26755*	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 26756*	Since by pserulm 26755 the series converges uniformly, it is also continuous by ulmcn 26732. (Contributed by Mario Carneiro, 3-Mar-2015.) Avoid ax-mulf 11284. (Revised by GG, 16-Mar-2025.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 < 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	psercnlem2 26757*	Lemma for psercn 26759. (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 26758*	Lemma for psercn 26759. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅))
Theorem	psercn 26759*	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 26760*	Lemma for pserdv 26762. (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 26761*	Lemma for pserdv 26762. (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 26762*	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 26763*	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 26764*	Lemma for abelth 26774. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
Theorem	abelthlem2 26765*	Lemma for abelth 26774. 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 26766*	Lemma for abelth 26774. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ )
Theorem	abelthlem4 26767*	Lemma for abelth 26774. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
Theorem	abelthlem5 26768*	Lemma for abelth 26774. (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 26769*	Lemma for abelth 26774. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
Theorem	abelthlem7a 26770*	Lemma for abelth 26774. (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 26771*	Lemma for abelth 26774. (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 26772*	Lemma for abelth 26774. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))
Theorem	abelthlem9 26773*	Lemma for abelth 26774. 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 26774*	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 26759.) (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 26775*	Abel's theorem, restricted to the [0, 1] interval. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((0[,]1)–cn→ℂ))
14.3  Basic trigonometry
14.3.1  The exponential, sine, and cosine functions (cont.)
Theorem	efcn 26776	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 26777	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 26778	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 26779*	Lemma for reeff1o 26780. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 26780	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 26781	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 26782	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 26783	The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑃 = ((mulGrp‘ℂfld) ↾s ℝ+)    ⇒   ⊢ (exp ↾ ℝ) ∈ (ℝfld GrpIso 𝑃)
14.3.2  Properties of pi = 3.14159...
Theorem	pilem1 26784	Lemma for pire 26789, pigt2lt4 26787 and sinpi 26788. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	pilem2 26785	Lemma for pire 26789, pigt2lt4 26787 and sinpi 26788. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ (2(,)4))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (sin‘𝐴) = 0)    &   ⊢ (𝜑 → (sin‘𝐵) = 0)    ⇒   ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)
Theorem	pilem3 26786	Lemma for pire 26789, pigt2lt4 26787 and sinpi 26788. 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 26787	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 26788	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 26789	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	2pire 26790	(2 · π) is a real number. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · π) ∈ ℝ
Theorem	picn 26791	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	2picn 26792	(2 · π) is a complex number. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · π) ∈ ℂ
Theorem	pipos 26793	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pige0 26794	π is nonnegative. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 ≤ π
Theorem	pine0 26795	π is nonzero. (Contributed by SN, 25-Apr-2025.)
⊢ π ≠ 0
Theorem	pirp 26796	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 26797	-π is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 26798	Lemma for sinhalfpi 26803 and coshalfpi 26804. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 26799	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 26800	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ