![]() |
Metamath
Proof Explorer Theorem List (p. 250 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | plyrem 24901 | The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 15881). If a polynomial 𝐹 is divided by the linear factor 𝑥 − 𝐴, the remainder is equal to 𝐹(𝐴), the evaluation of the polynomial at 𝐴 (interpreted as a constant polynomial). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝐺 = (Xp ∘f − (ℂ × {𝐴})) & ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · (𝐹 quot 𝐺))) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 = (ℂ × {(𝐹‘𝐴)})) | ||
Theorem | facth 24902 | The factor theorem. If a polynomial 𝐹 has a root at 𝐴, then 𝐺 = 𝑥 − 𝐴 is a factor of 𝐹 (and the other factor is 𝐹 quot 𝐺). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝐺 = (Xp ∘f − (ℂ × {𝐴})) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0) → 𝐹 = (𝐺 ∘f · (𝐹 quot 𝐺))) | ||
Theorem | fta1lem 24903* | Lemma for fta1 24904. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝑅 = (◡𝐹 “ {0}) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℂ) ∖ {0𝑝})) & ⊢ (𝜑 → (deg‘𝐹) = (𝐷 + 1)) & ⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {0})) & ⊢ (𝜑 → ∀𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝})((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧ (♯‘(◡𝑔 “ {0})) ≤ (deg‘𝑔)))) ⇒ ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹))) | ||
Theorem | fta1 24904 | The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg(𝐹) roots. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝑅 = (◡𝐹 “ {0}) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹))) | ||
Theorem | quotcan 24905 | Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝐻 = (𝐹 ∘f · 𝐺) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐻 quot 𝐺) = 𝐹) | ||
Theorem | vieta1lem1 24906* | Lemma for vieta1 24908. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ 𝑅 = (◡𝐹 “ {0}) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → (♯‘𝑅) = 𝑁) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → (𝐷 + 1) = 𝑁) & ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))) & ⊢ 𝑄 = (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄))) | ||
Theorem | vieta1lem2 24907* | Lemma for vieta1 24908: inductive step. Let 𝑧 be a root of 𝐹. Then 𝐹 = (Xp − 𝑧) · 𝑄 for some 𝑄 by the factor theorem, and 𝑄 is a degree- 𝐷 polynomial, so by the induction hypothesis Σ𝑥 ∈ (◡𝑄 “ 0)𝑥 = -(coeff‘𝑄)‘(𝐷 − 1) / (coeff‘𝑄)‘𝐷, so Σ𝑥 ∈ 𝑅𝑥 = 𝑧 − (coeff‘𝑄)‘ (𝐷 − 1) / (coeff‘𝑄)‘𝐷. Now the coefficients of 𝐹 are 𝐴‘(𝐷 + 1) = (coeff‘𝑄)‘𝐷 and 𝐴‘𝐷 = Σ𝑘 ∈ (0...𝐷)(coeff‘Xp − 𝑧)‘𝑘 · (coeff‘𝑄) ‘(𝐷 − 𝑘), which works out to -𝑧 · (coeff‘𝑄)‘𝐷 + (coeff‘𝑄)‘(𝐷 − 1), so putting it all together we have Σ𝑥 ∈ 𝑅𝑥 = -𝐴‘𝐷 / 𝐴‘(𝐷 + 1) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ 𝑅 = (◡𝐹 “ {0}) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → (♯‘𝑅) = 𝑁) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → (𝐷 + 1) = 𝑁) & ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))) & ⊢ 𝑄 = (𝐹 quot (Xp ∘f − (ℂ × {𝑧}))) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁))) | ||
Theorem | vieta1 24908* | The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas). If a polynomial of degree 𝑁 has 𝑁 distinct roots, then the sum over these roots can be calculated as -𝐴(𝑁 − 1) / 𝐴(𝑁). (If the roots are not distinct, then this formula is still true but must double-count some of the roots according to their multiplicities.) (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ 𝑅 = (◡𝐹 “ {0}) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → (♯‘𝑅) = 𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁))) | ||
Theorem | plyexmo 24909* | An infinite set of values can be extended to a polynomial in at most one way. (Contributed by Stefan O'Rear, 14-Nov-2014.) |
⊢ ((𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin) → ∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹)) | ||
Syntax | caa 24910 | Extend class notation to include the set of algebraic numbers. |
class 𝔸 | ||
Definition | df-aa 24911 | Define the set of algebraic numbers. An algebraic number is a root of a nonzero polynomial over the integers. Here we construct it as the union of all kernels (preimages of {0}) of all polynomials in (Poly‘ℤ), except the zero polynomial 0𝑝. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝔸 = ∪ 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(◡𝑓 “ {0}) | ||
Theorem | elaa 24912* | Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) | ||
Theorem | aacn 24913 | An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ) | ||
Theorem | aasscn 24914 | The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ 𝔸 ⊆ ℂ | ||
Theorem | elqaalem1 24915* | Lemma for elqaa 24918. 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 24916* | Lemma for elqaa 24918. (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 24917* | Lemma for elqaa 24918. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝})) & ⊢ (𝜑 → (𝐹‘𝐴) = 0) & ⊢ 𝐵 = (coeff‘𝐹) & ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) & ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝔸) | ||
Theorem | elqaa 24918* | 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 24912 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 24919 | Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ 𝔸) | ||
Theorem | qssaa 24920 | The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ ℚ ⊆ 𝔸 | ||
Theorem | iaa 24921 | The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ i ∈ 𝔸 | ||
Theorem | aareccl 24922 | The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ 𝔸) | ||
Theorem | aacjcl 24923 | The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝐴 ∈ 𝔸 → (∗‘𝐴) ∈ 𝔸) | ||
Theorem | aannenlem1 24924* | Lemma for aannen 24927. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) ⇒ ⊢ (𝐴 ∈ ℕ0 → (𝐻‘𝐴) ∈ Fin) | ||
Theorem | aannenlem2 24925* | Lemma for aannen 24927. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) ⇒ ⊢ 𝔸 = ∪ ran 𝐻 | ||
Theorem | aannenlem3 24926* | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0}) ⇒ ⊢ 𝔸 ≈ ℕ | ||
Theorem | aannen 24927 | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝔸 ≈ ℕ | ||
Theorem | aalioulem1 24928 | Lemma for aaliou 24934. 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 24929* | Lemma for aaliou 24934. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) | ||
Theorem | aalioulem3 24930* | Lemma for aaliou 24934. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (𝐹‘𝐴) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟)))) | ||
Theorem | aalioulem4 24931* | Lemma for aaliou 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (𝐹‘𝐴) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (((𝐹‘(𝑝 / 𝑞)) ≠ 0 ∧ (abs‘(𝐴 − (𝑝 / 𝑞))) ≤ 1) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) | ||
Theorem | aalioulem5 24932* | Lemma for aaliou 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (𝐹‘𝐴) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) ≠ 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) | ||
Theorem | aalioulem6 24933* | Lemma for aaliou 24934. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (𝐹‘𝐴) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) | ||
Theorem | aaliou 24934* | 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 24935* | Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐵) < 1) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) ⇒ ⊢ (𝜑 → seq𝐴( + , 𝐹) ⇝ (𝐶 / (1 − 𝐵))) | ||
Theorem | aaliou2 24936* | Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐴 ∈ (𝔸 ∩ ℝ) → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) | ||
Theorem | aaliou2b 24937* | Liouville's approximation theorem extended to complex 𝐴. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
⊢ (𝐴 ∈ 𝔸 → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) | ||
Theorem | aaliou3lem1 24938* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴)))) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ) | ||
Theorem | aaliou3lem2 24939* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴)))) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵))) | ||
Theorem | aaliou3lem3 24940* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴)))) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) ⇒ ⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴))))) | ||
Theorem | aaliou3lem8 24941* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℕ (2 · (2↑-(!‘(𝑥 + 1)))) ≤ (𝐵 / ((2↑(!‘𝑥))↑𝐴))) | ||
Theorem | aaliou3lem4 24942* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ 𝐿 ∈ ℝ | ||
Theorem | aaliou3lem5 24943* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ (𝐴 ∈ ℕ → (𝐻‘𝐴) ∈ ℝ) | ||
Theorem | aaliou3lem6 24944* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) ∈ ℤ) | ||
Theorem | aaliou3lem7 24945* | Lemma for aaliou3 24947. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝐴))) ≤ (2 · (2↑-(!‘(𝐴 + 1)))))) | ||
Theorem | aaliou3lem9 24946* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ ¬ 𝐿 ∈ 𝔸 | ||
Theorem | aaliou3 24947 | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.) |
⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸 | ||
Syntax | ctayl 24948 | Taylor polynomial of a function. |
class Tayl | ||
Syntax | cana 24949 | The class of analytic functions. |
class Ana | ||
Definition | df-tayl 24950* | 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 24951* | 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 24952* | Lemma for taylfval 24954. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) ⇒ ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ) | ||
Theorem | taylfvallem 24953* | Lemma for taylfval 24954. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ℂ) → (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))) ⊆ ℂ) | ||
Theorem | taylfval 24954* |
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 24960 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 24955* | 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 24956* | 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 24957* | 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 24958* | Lemma for taylpfval 24960 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) | ||
Theorem | taylplem2 24959* | Lemma for taylpfval 24960 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) ⇒ ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ) | ||
Theorem | taylpfval 24960* | 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 24961 | 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 24962* | Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) & ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑇‘𝑋) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘))) | ||
Theorem | taylply2 24963* | The Taylor polynomial is a polynomial of degree (at most) 𝑁. This version of taylply 24964 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 24964 | 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 24965 | 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 24966 | 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 24967 | 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 24968* | Lemma for taylth 24970. 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 24970 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 24969* | Lemma for taylth 24970. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵) & ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁)) & ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵)) ⇒ ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵)) | ||
Theorem | taylth 24970* | 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ℂ 𝐵)) | ||
Syntax | culm 24971 | Extend class notation to include the uniform convergence predicate. |
class ⇝𝑢 | ||
Definition | df-ulm 24972* | 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 14837. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ ⇝𝑢 = (𝑠 ∈ V ↦ {〈𝑓, 𝑦〉 ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)}) | ||
Theorem | ulmrel 24973 | The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ Rel (⇝𝑢‘𝑆) | ||
Theorem | ulmscl 24974 | Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) | ||
Theorem | ulmval 24975* | Express the predicate: The sequence of functions 𝐹 converges uniformly to 𝐺 on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) | ||
Theorem | ulmcl 24976 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) | ||
Theorem | ulmf 24977* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑m 𝑆)) | ||
Theorem | ulmpm 24978 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐹 ∈ ((ℂ ↑m 𝑆) ↑pm ℤ)) | ||
Theorem | ulmf2 24979 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | ||
Theorem | ulm2 24980* | Simplify ulmval 24975 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
Theorem | ulmi 24981* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶) | ||
Theorem | ulmclm 24982* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴)) | ||
Theorem | ulmres 24983 | 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 24984* | Lemma for ulmshft 24985. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
Theorem | ulmshft 24985* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
Theorem | ulm0 24986 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺) | ||
Theorem | ulmuni 24987 | A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻) | ||
Theorem | ulmdm 24988 | 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 24989* | Lemma for ulmcau 24990 and ulmcau2 24991: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 14707. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) | ||
Theorem | ulmcau 24990* | 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 24991 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) | ||
Theorem | ulmcau2 24991* | 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 24992* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇)) | ||
Theorem | ulmbdd 24993* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥) | ||
Theorem | ulmcn 24994 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ)) | ||
Theorem | ulmdvlem1 24995* | Lemma for ulmdv 24998. (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 24996* | Lemma for ulmdv 24998. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋) | ||
Theorem | ulmdvlem3 24997* | Lemma for ulmdv 24998. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧)) | ||
Theorem | ulmdv 24998* | 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 24999* | 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 25000* | 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‘(𝑇‘𝑧)) ≤ 𝑥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |