![]() |
Metamath
Proof Explorer Theorem List (p. 263 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uc1pdeg 26201 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶) → (𝐷‘𝐹) ∈ ℕ0) | ||
Theorem | uc1pldg 26202 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈) | ||
Theorem | mon1pldg 26203 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = (deg1‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 ) | ||
Theorem | mon1puc1p 26204 | Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀) → 𝑋 ∈ 𝐶) | ||
Theorem | uc1pmon1p 26205 | Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶) → ((𝐴‘(𝐼‘((coe1‘𝑋)‘(𝐷‘𝑋)))) · 𝑋) ∈ 𝑀) | ||
Theorem | deg1submon1p 26206 | The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (Monic1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝑂) & ⊢ (𝜑 → (𝐷‘𝐹) = 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑂) & ⊢ (𝜑 → (𝐷‘𝐺) = 𝑋) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) < 𝑋) | ||
Theorem | mon1pid 26207 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ (𝐷‘ 1 ) = 0)) | ||
Theorem | q1pval 26208* | Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) | ||
Theorem | q1peqb 26209 | Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑋 ∈ 𝐵 ∧ (𝐷‘(𝐹 − (𝑋 · 𝐺))) < (𝐷‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑋)) | ||
Theorem | q1pcl 26210 | Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) | ||
Theorem | r1pval 26211 | Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) | ||
Theorem | r1pcl 26212 | Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝐸𝐺) ∈ 𝐵) | ||
Theorem | r1pdeglt 26213 | The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐷‘(𝐹𝐸𝐺)) < (𝐷‘𝐺)) | ||
Theorem | r1pid 26214 | Express the original polynomial 𝐹 as 𝐹 = (𝑞 · 𝐺) + 𝑟 using the quotient and remainder functions for 𝑞 and 𝑟. (Contributed by Mario Carneiro, 5-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ + = (+g‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐹 = (((𝐹𝑄𝐺) · 𝐺) + (𝐹𝐸𝐺))) | ||
Theorem | r1pid2 26215 | Identity law for polynomial remainder operation: it leaves a polynomial 𝐴 unchanged iff the degree of 𝐴 is less than the degree of the divisor 𝐵. (Contributed by Thierry Arnoux, 2-Apr-2025.) Generalize to domains. (Revised by SN, 21-Jun-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑁) ⇒ ⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵))) | ||
Theorem | dvdsq1p 26216 | Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ ∥ = (∥r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) | ||
Theorem | dvdsr1p 26217 | Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ ∥ = (∥r‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐸 = (rem1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ (𝐹𝐸𝐺) = 0 )) | ||
Theorem | ply1remlem 26218 | A term of the form 𝑥 − 𝑁 is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ 𝑈 = (Monic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝜑 → (𝐺 ∈ 𝑈 ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ { 0 }) = {𝑁})) | ||
Theorem | ply1rem 26219 | The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 16576). 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). (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐸 = (rem1p‘𝑅) ⇒ ⊢ (𝜑 → (𝐹𝐸𝐺) = (𝐴‘((𝑂‘𝐹)‘𝑁))) | ||
Theorem | facth1 26220 | The factor theorem and its converse. A polynomial 𝐹 has a root at 𝐴 iff 𝐺 = 𝑥 − 𝐴 is a factor of 𝐹. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑁)) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ ∥ = (∥r‘𝑃) ⇒ ⊢ (𝜑 → (𝐺 ∥ 𝐹 ↔ ((𝑂‘𝐹)‘𝑁) = 0 )) | ||
Theorem | fta1glem1 26221 | Lemma for fta1g 26223. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) | ||
Theorem | fta1glem2 26222* | Lemma for fta1g 26223. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) & ⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) ⇒ ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) | ||
Theorem | fta1g 26223 | The one-sided fundamental theorem of algebra. A polynomial of degree 𝑛 has at most 𝑛 roots. Unlike the real fundamental theorem fta 27137, which is only true in ℂ and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) ⇒ ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) | ||
Theorem | fta1blem 26224 | Lemma for fta1b 26225. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊) & ⊢ (𝜑 → 𝑀 ≠ 𝑊) & ⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋)))) ⇒ ⊢ (𝜑 → 𝑁 = 𝑊) | ||
Theorem | fta1b 26225* | The assumption that 𝑅 be a domain in fta1g 26223 is necessary. Here we show that the statement is strong enough to prove that 𝑅 is a domain. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀𝑓 ∈ (𝐵 ∖ { 0 })(♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) | ||
Theorem | idomrootle 26226* | No element of an integral domain can have more than 𝑁 𝑁-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (♯‘{𝑦 ∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁) | ||
Theorem | drnguc1p 26227 | Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐶) | ||
Theorem | ig1peu 26228* | There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) | ||
Theorem | ig1pval 26229* | Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))) | ||
Theorem | ig1pval2 26230 | Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐺‘{ 0 }) = 0 ) | ||
Theorem | ig1pval3 26231 | Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐺‘𝐼) ∈ 𝐼 ∧ (𝐺‘𝐼) ∈ 𝑀 ∧ (𝐷‘(𝐺‘𝐼)) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) | ||
Theorem | ig1pcl 26232 | The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) ∈ 𝐼) | ||
Theorem | ig1pdvds 26233 | The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ ∥ = (∥r‘𝑃) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼) → (𝐺‘𝐼) ∥ 𝑋) | ||
Theorem | ig1prsp 26234 | Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑃) & ⊢ 𝐾 = (RSpan‘𝑃) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈) → 𝐼 = (𝐾‘{(𝐺‘𝐼)})) | ||
Theorem | ply1lpir 26235 | The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ DivRing → 𝑃 ∈ LPIR) | ||
Theorem | ply1pid 26236 | The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Field → 𝑃 ∈ PID) | ||
Syntax | cply 26237 | Extend class notation to include the set of complex polynomials. |
class Poly | ||
Syntax | cidp 26238 | Extend class notation to include the identity polynomial. |
class Xp | ||
Syntax | ccoe 26239 | Extend class notation to include the coefficient function on polynomials. |
class coeff | ||
Syntax | cdgr 26240 | Extend class notation to include the degree function on polynomials. |
class deg | ||
Definition | df-ply 26241* | Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}) | ||
Definition | df-idp 26242 | Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ Xp = ( I ↾ ℂ) | ||
Definition | df-coe 26243* | Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | ||
Definition | df-dgr 26244 | Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )) | ||
Theorem | plyco0 26245* | Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))) | ||
Theorem | plyval 26246* | Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}) | ||
Theorem | plybss 26247 | Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) | ||
Theorem | elply 26248* | Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | ||
Theorem | elply2 26249* | The coefficient function can be assumed to have zeroes outside 0...𝑛. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | ||
Theorem | plyun0 26250 | The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (Poly‘(𝑆 ∪ {0})) = (Poly‘𝑆) | ||
Theorem | plyf 26251 | A polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) | ||
Theorem | plyss 26252 | The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇)) | ||
Theorem | plyssc 26253 | Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ) | ||
Theorem | elplyr 26254* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝐴:ℕ0⟶𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) | ||
Theorem | elplyd 26255* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) | ||
Theorem | ply1termlem 26256* | Lemma for ply1term 26257. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) | ||
Theorem | ply1term 26257* | A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) | ||
Theorem | plypow 26258* | A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑁)) ∈ (Poly‘𝑆)) | ||
Theorem | plyconst 26259 | A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆) → (ℂ × {𝐴}) ∈ (Poly‘𝑆)) | ||
Theorem | ne0p 26260 | A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝐹‘𝐴) ≠ 0) → 𝐹 ≠ 0𝑝) | ||
Theorem | ply0 26261 | The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝑆 ⊆ ℂ → 0𝑝 ∈ (Poly‘𝑆)) | ||
Theorem | plyid 26262 | The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆) → Xp ∈ (Poly‘𝑆)) | ||
Theorem | plyeq0lem 26263* | Lemma for plyeq0 26264. If 𝐴 is the coefficient function for a nonzero polynomial such that 𝑃(𝑧) = Σ𝑘 ∈ ℕ0𝐴(𝑘) · 𝑧↑𝑘 = 0 for every 𝑧 ∈ ℂ and 𝐴(𝑀) is the nonzero leading coefficient, then the function 𝐹(𝑧) = 𝑃(𝑧) / 𝑧↑𝑀 is a sum of powers of 1 / 𝑧, and so the limit of this function as 𝑧 ⇝ +∞ is the constant term, 𝐴(𝑀). But 𝐹(𝑧) = 0 everywhere, so this limit is also equal to zero so that 𝐴(𝑀) = 0, a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ 𝑀 = sup((◡𝐴 “ (𝑆 ∖ {0})), ℝ, < ) & ⊢ (𝜑 → (◡𝐴 “ (𝑆 ∖ {0})) ≠ ∅) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | plyeq0 26264* | If a polynomial is zero at every point (or even just zero at the positive integers), then all the coefficients must be zero. This is the basis for the method of equating coefficients of equal polynomials, and ensures that df-coe 26243 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → 𝐴 = (ℕ0 × {0})) | ||
Theorem | plypf1 26265 | Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.) (Proof shortened by AV, 29-Sep-2019.) |
⊢ 𝑅 = (ℂfld ↾s 𝑆) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (Base‘𝑃) & ⊢ 𝐸 = (eval1‘ℂfld) ⇒ ⊢ (𝑆 ∈ (SubRing‘ℂfld) → (Poly‘𝑆) = (𝐸 “ 𝐴)) | ||
Theorem | plyaddlem1 26266* | Derive the coefficient function for the sum of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...if(𝑀 ≤ 𝑁, 𝑁, 𝑀))(((𝐴 ∘f + 𝐵)‘𝑘) · (𝑧↑𝑘)))) | ||
Theorem | plymullem1 26267* | Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)))) | ||
Theorem | plyaddlem 26268* | Lemma for plyadd 26270. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plymullem 26269* | Lemma for plymul 26271. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plyadd 26270* | The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plymul 26271* | The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plysub 26272* | The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) & ⊢ (𝜑 → -1 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plyaddcl 26273 | The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ)) | ||
Theorem | plymulcl 26274 | The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · 𝐺) ∈ (Poly‘ℂ)) | ||
Theorem | plysubcl 26275 | The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f − 𝐺) ∈ (Poly‘ℂ)) | ||
Theorem | coeval 26276* | Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | ||
Theorem | coeeulem 26277* | Lemma for coeeu 26278. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m ℕ0)) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ↑m ℕ0)) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | coeeu 26278* | Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃!𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | ||
Theorem | coelem 26279* | Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → ((coeff‘𝐹) ∈ (ℂ ↑m ℕ0) ∧ ∃𝑛 ∈ ℕ0 (((coeff‘𝐹) “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)))))) | ||
Theorem | coeeq 26280* | If 𝐴 satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → (coeff‘𝐹) = 𝐴) | ||
Theorem | dgrval 26281 | Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) = sup((◡𝐴 “ (ℂ ∖ {0})), ℕ0, < )) | ||
Theorem | dgrlem 26282* | Lemma for dgrcl 26286 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) | ||
Theorem | coef 26283 | The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) | ||
Theorem | coef2 26284 | The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ0⟶𝑆) | ||
Theorem | coef3 26285 | The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) | ||
Theorem | dgrcl 26286 | The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0) | ||
Theorem | dgrub 26287 | If the 𝑀-th coefficient of 𝐹 is nonzero, then the degree of 𝐹 is at least 𝑀. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴‘𝑀) ≠ 0) → 𝑀 ≤ 𝑁) | ||
Theorem | dgrub2 26288 | All the coefficients above the degree of 𝐹 are zero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) | ||
Theorem | dgrlb 26289 | If all the coefficients above 𝑀 are zero, then the degree of 𝐹 is at most 𝑀. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ ℕ0 ∧ (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) → 𝑁 ≤ 𝑀) | ||
Theorem | coeidlem 26290* | Lemma for coeid 26291. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) | ||
Theorem | coeid 26291* | Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) | ||
Theorem | coeid2 26292* | Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑋↑𝑘))) | ||
Theorem | coeid3 26293* | Reconstruct a polynomial as an explicit sum of the coefficient function up to at least the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑋) = Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑋↑𝑘))) | ||
Theorem | plyco 26294* | The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | coeeq2 26295* | Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → (coeff‘𝐹) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ≤ 𝑁, 𝐴, 0))) | ||
Theorem | dgrle 26296* | Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → (deg‘𝐹) ≤ 𝑁) | ||
Theorem | dgreq 26297* | If the highest term in a polynomial expression is nonzero, then the polynomial's degree is completely determined. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → (𝐴‘𝑁) ≠ 0) ⇒ ⊢ (𝜑 → (deg‘𝐹) = 𝑁) | ||
Theorem | 0dgr 26298 | A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (deg‘(ℂ × {𝐴})) = 0) | ||
Theorem | 0dgrb 26299 | A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) | ||
Theorem | dgrnznn 26300 | A nonzero polynomial with a root has positive degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
⊢ (((𝑃 ∈ (Poly‘𝑆) ∧ 𝑃 ≠ 0𝑝) ∧ (𝐴 ∈ ℂ ∧ (𝑃‘𝐴) = 0)) → (deg‘𝑃) ∈ ℕ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |