P. 264 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26301-26400   *Has distinct variable group(s)

Type	Label	Description
Statement
14.2.2  Uniform convergence
Syntax	culm 26301	Extend class notation to include the uniform convergence predicate.
class ⇝𝑢
Definition	df-ulm 26302*	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 15413. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ ⇝𝑢 = (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)})
Theorem	ulmrel 26303	The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ Rel (⇝𝑢‘𝑆)
Theorem	ulmscl 26304	Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V)
Theorem	ulmval 26305*	Express the predicate: The sequence of functions 𝐹 converges uniformly to 𝐺 on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
Theorem	ulmcl 26306	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ)
Theorem	ulmf 26307*	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆))
Theorem	ulmpm 26308	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐹 ∈ ((ℂ ↑m 𝑆) ↑pm ℤ))
Theorem	ulmf2 26309	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
Theorem	ulm2 26310*	Simplify ulmval 26305 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)    &   ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	ulmi 26311*	The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶)
Theorem	ulmclm 26312*	A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘))    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴))
Theorem	ulmres 26313	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 26314*	Lemma for ulmshft 26315. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺))
Theorem	ulmshft 26315*	A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺))
Theorem	ulm0 26316	Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺)
Theorem	ulmuni 26317	A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.)
⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻)
Theorem	ulmdm 26318	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 26319*	Lemma for ulmcau 26320 and ulmcau2 26321: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 15281. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥))
Theorem	ulmcau 26320*	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 26321 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥))
Theorem	ulmcau2 26321*	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 26322*	A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇))
Theorem	ulmbdd 26323*	A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥)
Theorem	ulmcn 26324	A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ))    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ))
Theorem	ulmdvlem1 26325*	Lemma for ulmdv 26328. (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 26326*	Lemma for ulmdv 26328. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋)
Theorem	ulmdvlem3 26327*	Lemma for ulmdv 26328. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧))
Theorem	ulmdv 26328*	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 26329*	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 26330*	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 26331	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 25585.) (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶MblFn)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	iblulm 26332	A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐿1)
Theorem	itgulm 26333*	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 26334*	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 26335*	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 26336*	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 26337*	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 26338*	Lemma for radcnvlt1 26343, radcnvle 26345. 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 26339*	Lemma for radcnvlt1 26343, radcnvle 26345. 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 26340*	Lemma for radcnvlt1 26343, radcnvle 26345. 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 26341*	Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    ⇒   ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
Theorem	radcnvcl 26342*	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 26343*	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 26344*	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 26345*	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 26346*	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 26347*	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 26348*	Since by pserulm 26347 the series converges uniformly, it is also continuous by ulmcn 26324. (Contributed by Mario Carneiro, 3-Mar-2015.) Avoid ax-mulf 11108. (Revised by GG, 16-Mar-2025.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 < 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	psercn2OLD 26349*	Obsolete version of psercn2 26348 as of 16-Apr-2025. (Contributed by Mario Carneiro, 3-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 < 𝑅)    &   ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))
Theorem	psercnlem2 26350*	Lemma for psercn 26352. (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 26351*	Lemma for psercn 26352. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < )    &   ⊢ 𝑆 = (◡abs “ (0[,)𝑅))    &   ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅))
Theorem	psercn 26352*	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 26353*	Lemma for pserdv 26355. (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 26354*	Lemma for pserdv 26355. (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 26355*	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 26356*	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 26357*	Lemma for abelth 26367. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
Theorem	abelthlem2 26358*	Lemma for abelth 26367. 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 26359*	Lemma for abelth 26367. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ )
Theorem	abelthlem4 26360*	Lemma for abelth 26367. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
Theorem	abelthlem5 26361*	Lemma for abelth 26367. (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 26362*	Lemma for abelth 26367. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1}))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))
Theorem	abelthlem7a 26363*	Lemma for abelth 26367. (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 26364*	Lemma for abelth 26367. (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 26365*	Lemma for abelth 26367. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑀)    &   ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))    &   ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0)    ⇒   ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))
Theorem	abelthlem9 26366*	Lemma for abelth 26367. 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 26367*	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 26352.) (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 26368*	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 26369	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ exp ∈ (ℂ–cn→ℂ)
Theorem	sincn 26370	Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ sin ∈ (ℂ–cn→ℂ)
Theorem	coscn 26371	Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.)
⊢ cos ∈ (ℂ–cn→ℂ)
Theorem	reeff1olem 26372*	Lemma for reeff1o 26373. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)
Theorem	reeff1o 26373	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 26374	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 26375	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 26376	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 26377	Lemma for pire 26382, pigt2lt4 26380 and sinpi 26381. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
Theorem	pilem2 26378	Lemma for pire 26382, pigt2lt4 26380 and sinpi 26381. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ (2(,)4))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (sin‘𝐴) = 0)    &   ⊢ (𝜑 → (sin‘𝐵) = 0)    ⇒   ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)
Theorem	pilem3 26379	Lemma for pire 26382, pigt2lt4 26380 and sinpi 26381. 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 26380	π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (2 < π ∧ π < 4)
Theorem	sinpi 26381	The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘π) = 0
Theorem	pire 26382	π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ π ∈ ℝ
Theorem	picn 26383	π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ π ∈ ℂ
Theorem	pipos 26384	π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ 0 < π
Theorem	pine0 26385	π is nonzero. (Contributed by SN, 25-Apr-2025.)
⊢ π ≠ 0
Theorem	pirp 26386	π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ π ∈ ℝ+
Theorem	negpicn 26387	-π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -π ∈ ℂ
Theorem	sinhalfpilem 26388	Lemma for sinhalfpi 26393 and coshalfpi 26394. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0)
Theorem	halfpire 26389	π / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
⊢ (π / 2) ∈ ℝ
Theorem	neghalfpire 26390	-π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ
Theorem	neghalfpirx 26391	-π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -(π / 2) ∈ ℝ*
Theorem	pidiv2halves 26392	Adding π / 2 to itself gives π. See 2halves 12360. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ((π / 2) + (π / 2)) = π
Theorem	sinhalfpi 26393	The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(π / 2)) = 1
Theorem	coshalfpi 26394	The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘(π / 2)) = 0
Theorem	cosneghalfpi 26395	The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
⊢ (cos‘-(π / 2)) = 0
Theorem	efhalfpi 26396	The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.)
⊢ (exp‘(i · (π / 2))) = i
Theorem	cospi 26397	The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (cos‘π) = -1
Theorem	efipi 26398	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 26399	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ ((exp‘(i · π)) + 1) = 0
Theorem	sin2pi 26400	The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
⊢ (sin‘(2 · π)) = 0