P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aasscn 24901	The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ 𝔸 ⊆ ℂ
Theorem	elqaalem1 24902*	Lemma for elqaa 24905. The function 𝑁 represents the denominators of the rational coefficients 𝐵. By multiplying them all together to make 𝑅, we get a number big enough to clear all the denominators and make 𝑅 · 𝐹 an integer polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    &   ⊢ 𝐵 = (coeff‘𝐹)    &   ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))    &   ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → ((𝑁‘𝐾) ∈ ℕ ∧ ((𝐵‘𝐾) · (𝑁‘𝐾)) ∈ ℤ))
Theorem	elqaalem2 24903*	Lemma for elqaa 24905. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    &   ⊢ 𝐵 = (coeff‘𝐹)    &   ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))    &   ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))    &   ⊢ 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝐾)))    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁‘𝐾)) = 0)
Theorem	elqaalem3 24904*	Lemma for elqaa 24905. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    &   ⊢ 𝐵 = (coeff‘𝐹)    &   ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))    &   ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝔸)
Theorem	elqaa 24905*	The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa 24899 are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof shortened by AV, 3-Oct-2020.)
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0))
Theorem	qaa 24906	Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ 𝔸)
Theorem	qssaa 24907	The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ ℚ ⊆ 𝔸
Theorem	iaa 24908	The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ i ∈ 𝔸
Theorem	aareccl 24909	The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ 𝔸)
Theorem	aacjcl 24910	The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝐴 ∈ 𝔸 → (∗‘𝐴) ∈ 𝔸)
Theorem	aannenlem1 24911*	Lemma for aannen 24914. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})    ⇒   ⊢ (𝐴 ∈ ℕ0 → (𝐻‘𝐴) ∈ Fin)
Theorem	aannenlem2 24912*	Lemma for aannen 24914. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})    ⇒   ⊢ 𝔸 = ∪ ran 𝐻
Theorem	aannenlem3 24913*	The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})    ⇒   ⊢ 𝔸 ≈ ℕ
Theorem	aannen 24914	The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝔸 ≈ ℕ
14.1.6  Liouville's approximation theorem
Theorem	aalioulem1 24915	Lemma for aaliou 24921. An integer polynomial cannot inflate the denominator of a rational by more than its degree. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑋 ∈ ℤ)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐹‘(𝑋 / 𝑌)) · (𝑌↑(deg‘𝐹))) ∈ ℤ)
Theorem	aalioulem2 24916*	Lemma for aaliou 24921. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Theorem	aalioulem3 24917*	Lemma for aaliou 24921. (Contributed by Stefan O'Rear, 15-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))
Theorem	aalioulem4 24918*	Lemma for aaliou 24921. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (((𝐹‘(𝑝 / 𝑞)) ≠ 0 ∧ (abs‘(𝐴 − (𝑝 / 𝑞))) ≤ 1) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Theorem	aalioulem5 24919*	Lemma for aaliou 24921. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) ≠ 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Theorem	aalioulem6 24920*	Lemma for aaliou 24921. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	aaliou 24921*	Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial 𝐹 in integer coefficients, is not approximable beyond order 𝑁 = deg(𝐹) by rational numbers. In this form, it also applies to rational numbers themselves, which are not well approximable by other rational numbers. This is Metamath 100 proof #18. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	geolim3 24922*	Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐵) < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))    ⇒   ⊢ (𝜑 → seq𝐴( + , 𝐹) ⇝ (𝐶 / (1 − 𝐵)))
Theorem	aaliou2 24923*	Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝔸 ∩ ℝ) → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	aaliou2b 24924*	Liouville's approximation theorem extended to complex 𝐴. (Contributed by Stefan O'Rear, 20-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	aaliou3lem1 24925*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ)
Theorem	aaliou3lem2 24926*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)))
Theorem	aaliou3lem3 24927*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    ⇒   ⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴)))))
Theorem	aaliou3lem8 24928*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 20-Nov-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℕ (2 · (2↑-(!‘(𝑥 + 1)))) ≤ (𝐵 / ((2↑(!‘𝑥))↑𝐴)))
Theorem	aaliou3lem4 24929*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ 𝐿 ∈ ℝ
Theorem	aaliou3lem5 24930*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ (𝐴 ∈ ℕ → (𝐻‘𝐴) ∈ ℝ)
Theorem	aaliou3lem6 24931*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) ∈ ℤ)
Theorem	aaliou3lem7 24932*	Lemma for aaliou3 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝐴))) ≤ (2 · (2↑-(!‘(𝐴 + 1))))))
Theorem	aaliou3lem9 24933*	Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ ¬ 𝐿 ∈ 𝔸
Theorem	aaliou3 24934	Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.)
⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸
14.2  Sequences and series
14.2.1  Taylor polynomials and Taylor's theorem
Syntax	ctayl 24935	Taylor polynomial of a function.
class Tayl
Syntax	cana 24936	The class of analytic functions.
class Ana
Definition	df-tayl 24937*	Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ0 ∪ {+∞}) should be replaced by 𝑛 ∈ ℕ0*. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))
Definition	df-ana 24938*	Define the set of analytic functions, which are functions such that the Taylor series of the function at each point converges to the function in some neighborhood of the point. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
Theorem	taylfvallem1 24939*	Lemma for taylfval 24941. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    ⇒   ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ)
Theorem	taylfvallem 24940*	Lemma for taylfval 24941. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ℂ) → (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))) ⊆ ℂ)
Theorem	taylfval 24941*	Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: 𝑆 is the base set with respect to evaluate the derivatives (generally ℝ or ℂ), 𝐹 is the function we are approximating, at point 𝐵, to order 𝑁. The result is a polynomial function of 𝑥. This "extended" version of taylpfval 24947 additionally handles the case 𝑁 = +∞, in which case this is not a polynomial but an infinite series, the Taylor series of the function. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))
Theorem	eltayl 24942*	Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑇𝑌 ↔ (𝑋 ∈ ℂ ∧ 𝑌 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))))))
Theorem	taylf 24943*	The Taylor series defines a function on a subset of the complex numbers. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ)
Theorem	tayl0 24944*	The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))
Theorem	taylplem1 24945*	Lemma for taylpfval 24947 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
Theorem	taylplem2 24946*	Lemma for taylpfval 24947 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    ⇒   ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ)
Theorem	taylpfval 24947*	Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: 𝑆 is the base set with respect to evaluate the derivatives (generally ℝ or ℂ), 𝐹 is the function we are approximating, at point 𝐵, to order 𝑁. The result is a polynomial function of 𝑥. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))
Theorem	taylpf 24948	The Taylor polynomial is a function on the complex numbers (even if the base set of the original function is the reals). (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
Theorem	taylpval 24949*	Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑇‘𝑋) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))
Theorem	taylply2 24950*	The Taylor polynomial is a polynomial of degree (at most) 𝑁. This version of taylply 24951 shows that the coefficients of 𝑇 are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑇 ∈ (Poly‘𝐷) ∧ (deg‘𝑇) ≤ 𝑁))
Theorem	taylply 24951	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 24952	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 24953	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 24954	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 24955*	Lemma for taylth 24957. 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 24957 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 24956*	Lemma for taylth 24957. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁))    &   ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵))    ⇒   ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))
Theorem	taylth 24957*	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 24958	Extend class notation to include the uniform convergence predicate.
class ⇝𝑢
Definition	df-ulm 24959*	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 14839. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ ⇝𝑢 = (𝑠 ∈ V ↦ {⟨𝑓, 𝑦⟩ ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)})
Theorem	ulmrel 24960	The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ Rel (⇝𝑢‘𝑆)
Theorem	ulmscl 24961	Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V)
Theorem	ulmval 24962*	Express the predicate: The sequence of functions 𝐹 converges uniformly to 𝐺 on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
Theorem	ulmcl 24963	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ)
Theorem	ulmf 24964*	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆))
Theorem	ulmpm 24965	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐹 ∈ ((ℂ ↑m 𝑆) ↑pm ℤ))
Theorem	ulmf2 24966	Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
Theorem	ulm2 24967*	Simplify ulmval 24962 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)    &   ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	ulmi 24968*	The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶)
Theorem	ulmclm 24969*	A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘))    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴))
Theorem	ulmres 24970	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 24971*	Lemma for ulmshft 24972. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺))
Theorem	ulmshft 24972*	A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺))
Theorem	ulm0 24973	Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)    ⇒   ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺)
Theorem	ulmuni 24974	A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.)
⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻)
Theorem	ulmdm 24975	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 24976*	Lemma for ulmcau 24977 and ulmcau2 24978: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 14709. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥))
Theorem	ulmcau 24977*	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 24978 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥))
Theorem	ulmcau2 24978*	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 24979*	A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇))
Theorem	ulmbdd 24980*	A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥)
Theorem	ulmcn 24981	A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ))    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ))
Theorem	ulmdvlem1 24982*	Lemma for ulmdv 24985. (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 24983*	Lemma for ulmdv 24985. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋)
Theorem	ulmdvlem3 24984*	Lemma for ulmdv 24985. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧))
Theorem	ulmdv 24985*	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 24986*	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 24987*	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 24988	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 24263.) (Contributed by Mario Carneiro, 18-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶MblFn)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	iblulm 24989	A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1)    &   ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺)    &   ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝐿1)
Theorem	itgulm 24990*	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 24991*	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 24992*	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 24993*	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 24994*	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 24995*	Lemma for radcnvlt1 25000, radcnvle 25002. 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 24996*	Lemma for radcnvlt1 25000, radcnvle 25002. 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 24997*	Lemma for radcnvlt1 25000, radcnvle 25002. 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 24998*	Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.)
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    ⇒   ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })
Theorem	radcnvcl 24999*	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 25000*	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 ⇝ ))