![]() |
Metamath
Proof Explorer Theorem List (p. 261 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uc1pcl 26001 | Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ∈ 𝐵) | ||
Theorem | mon1pcl 26002 | Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ∈ 𝐵) | ||
Theorem | uc1pn0 26003 | Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → 𝐹 ≠ 0 ) | ||
Theorem | mon1pn0 26004 | Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → 𝐹 ≠ 0 ) | ||
Theorem | uc1pdeg 26005 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐶) → (𝐷‘𝐹) ∈ ℕ0) | ||
Theorem | uc1pldg 26006 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐶 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝑈) | ||
Theorem | mon1pldg 26007 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝑀 → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1 ) | ||
Theorem | mon1puc1p 26008 | Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐶 = (Unic1p‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀) → 𝑋 ∈ 𝐶) | ||
Theorem | uc1pmon1p 26009 | 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 26010 | 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 | q1pval 26011* | Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝑄𝐺) = (℩𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 · 𝐺))) < (𝐷‘𝐺))) | ||
Theorem | q1peqb 26012 | Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑋 ∈ 𝐵 ∧ (𝐷‘(𝐹 − (𝑋 · 𝐺))) < (𝐷‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑋)) | ||
Theorem | q1pcl 26013 | Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑄 = (quot1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) | ||
Theorem | r1pval 26014 | Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑄 = (quot1p‘𝑅) & ⊢ · = (.r‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹𝐸𝐺) = (𝐹 − ((𝐹𝑄𝐺) · 𝐺))) | ||
Theorem | r1pcl 26015 | Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Unic1p‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝐸𝐺) ∈ 𝐵) | ||
Theorem | r1pdeglt 26016 | 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 26017 | 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 | dvdsq1p 26018 | 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 26019 | 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 26020 | 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 26021 | The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 16482). 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 26022 | 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 26023 | Lemma for fta1g 26025. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) | ||
Theorem | fta1glem2 26024* | Lemma for fta1g 26025. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) & ⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) & ⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) ⇒ ⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) | ||
Theorem | fta1g 26025 | The one-sided fundamental theorem of algebra. A polynomial of degree 𝑛 has at most 𝑛 roots. Unlike the real fundamental theorem fta 26928, 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 26026 | Lemma for fta1b 26027. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑂 = (eval1‘𝑅) & ⊢ 𝑊 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑀 ∈ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ 𝐾) & ⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊) & ⊢ (𝜑 → 𝑀 ≠ 𝑊) & ⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋)))) ⇒ ⊢ (𝜑 → 𝑁 = 𝑊) | ||
Theorem | fta1b 26027* | The assumption that 𝑅 be a domain in fta1g 26025 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 | drnguc1p 26028 | 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 26029* | 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 26030* | 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 26031 | 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 26032 | 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 26033 | 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 26034 | 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 26035 | 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 26036 | 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 26037 | The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Field → 𝑃 ∈ PID) | ||
Syntax | cply 26038 | Extend class notation to include the set of complex polynomials. |
class Poly | ||
Syntax | cidp 26039 | Extend class notation to include the identity polynomial. |
class Xp | ||
Syntax | ccoe 26040 | Extend class notation to include the coefficient function on polynomials. |
class coeff | ||
Syntax | cdgr 26041 | Extend class notation to include the degree function on polynomials. |
class deg | ||
Definition | df-ply 26042* | 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 26043 | Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ Xp = ( I ↾ ℂ) | ||
Definition | df-coe 26044* | 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 26045 | Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )) | ||
Theorem | plyco0 26046* | 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 26047* | Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}) | ||
Theorem | plybss 26048 | Reverse closure of the parameter 𝑆 of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) | ||
Theorem | elply 26049* | Definition of a polynomial with coefficients in 𝑆. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) | ||
Theorem | elply2 26050* | 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 26051 | 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 26052 | The polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) | ||
Theorem | plyss 26053 | The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇)) | ||
Theorem | plyssc 26054 | Every polynomial ring is contained in the ring of polynomials over ℂ. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (Poly‘𝑆) ⊆ (Poly‘ℂ) | ||
Theorem | elplyr 26055* | 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 26056* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) | ||
Theorem | ply1termlem 26057* | Lemma for ply1term 26058. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(if(𝑘 = 𝑁, 𝐴, 0) · (𝑧↑𝑘)))) | ||
Theorem | ply1term 26058* | A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ 𝐹 = (𝑧 ∈ ℂ ↦ (𝐴 · (𝑧↑𝑁))) ⇒ ⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) | ||
Theorem | plypow 26059* | A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑𝑁)) ∈ (Poly‘𝑆)) | ||
Theorem | plyconst 26060 | A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 𝐴 ∈ 𝑆) → (ℂ × {𝐴}) ∈ (Poly‘𝑆)) | ||
Theorem | ne0p 26061 | A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝐹‘𝐴) ≠ 0) → 𝐹 ≠ 0𝑝) | ||
Theorem | ply0 26062 | The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ (𝑆 ⊆ ℂ → 0𝑝 ∈ (Poly‘𝑆)) | ||
Theorem | plyid 26063 | The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
⊢ ((𝑆 ⊆ ℂ ∧ 1 ∈ 𝑆) → Xp ∈ (Poly‘𝑆)) | ||
Theorem | plyeq0lem 26064* | Lemma for plyeq0 26065. 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 26065* | 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 26044 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 0𝑝 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → 𝐴 = (ℕ0 × {0})) | ||
Theorem | plypf1 26066 | 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 26067* | 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 26068* | 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 26069* | Lemma for plyadd 26071. (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 26070* | Lemma for plymul 26072. (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 26071* | The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plymul 26072* | The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plysub 26073* | The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) & ⊢ (𝜑 → -1 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (Poly‘𝑆)) | ||
Theorem | plyaddcl 26074 | The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f + 𝐺) ∈ (Poly‘ℂ)) | ||
Theorem | plymulcl 26075 | The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f · 𝐺) ∈ (Poly‘ℂ)) | ||
Theorem | plysubcl 26076 | The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘f − 𝐺) ∈ (Poly‘ℂ)) | ||
Theorem | coeval 26077* | Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹) = (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) | ||
Theorem | coeeulem 26078* | Lemma for coeeu 26079. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (ℂ ↑m ℕ0)) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ↑m ℕ0)) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | coeeu 26079* | 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 26080* | 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 26081* | 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 26082 | Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) = sup((◡𝐴 “ (ℂ ∖ {0})), ℕ0, < )) | ||
Theorem | dgrlem 26083* | Lemma for dgrcl 26087 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) | ||
Theorem | coef 26084 | The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) | ||
Theorem | coef2 26085 | The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → 𝐴:ℕ0⟶𝑆) | ||
Theorem | coef3 26086 | The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) | ||
Theorem | dgrcl 26087 | The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ0) | ||
Theorem | dgrub 26088 | 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 26089 | All the coefficients above the degree of 𝐹 are zero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) ⇒ ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0}) | ||
Theorem | dgrlb 26090 | 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 26091* | Lemma for coeid 26092. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ 𝐴 = (coeff‘𝐹) & ⊢ 𝑁 = (deg‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ((𝑆 ∪ {0}) ↑m ℕ0)) & ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑀 + 1))) = {0}) & ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐵‘𝑘) · (𝑧↑𝑘)))) ⇒ ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) | ||
Theorem | coeid 26092* | 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 26093* | 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 26094* | 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 26095* | 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 26096* | 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 26097* | 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 26098* | 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 26099 | A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (deg‘(ℂ × {𝐴})) = 0) | ||
Theorem | 0dgrb 26100 | A function has degree zero iff it is a constant function. (Contributed by Mario Carneiro, 23-Jul-2014.) |
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |