Home | Metamath
Proof Explorer Theorem List (p. 237 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvfsum2 23601* | The reverse of dvfsumrlim 23598, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.) |
⊢ 𝑆 = (𝑇(,)+∞) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ*) & ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ≤ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑈) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸) ⇒ ⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸) | ||
Theorem | ftc1lem1 23602* | Lemma for ftc1a 23604 and ftc1 23609. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) | ||
Theorem | ftc1lem2 23603* | Lemma for ftc1 23609. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) | ||
Theorem | ftc1a 23604* | The Fundamental Theorem of Calculus, part one. The function 𝐺 formed by varying the right endpoint of an integral of 𝐹 is continuous if 𝐹 is integrable. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) | ||
Theorem | ftc1lem3 23605* | Lemma for ftc1 23609. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) | ||
Theorem | ftc1lem4 23606* | Lemma for ftc1 23609. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑌 − 𝐶)) < 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝐶))) < 𝐸) | ||
Theorem | ftc1lem5 23607* | Lemma for ftc1 23609. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) | ||
Theorem | ftc1lem6 23608* | Lemma for ftc1 23609. (Contributed by Mario Carneiro, 14-Aug-2014.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐻 limℂ 𝐶)) | ||
Theorem | ftc1 23609* | The Fundamental Theorem of Calculus, part one. The function formed by varying the right endpoint of an integral is differentiable at 𝐶 with derivative 𝐹(𝐶) if the original function is continuous at 𝐶. This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) & ⊢ 𝐽 = (𝐿 ↾t ℝ) & ⊢ 𝐾 = (𝐿 ↾t 𝐷) & ⊢ 𝐿 = (TopOpen‘ℂfld) ⇒ ⊢ (𝜑 → 𝐶(ℝ D 𝐺)(𝐹‘𝐶)) | ||
Theorem | ftc1cn 23610* | Strengthen the assumptions of ftc1 23609 to when the function 𝐹 is continuous on the entire interval (𝐴, 𝐵); in this case we can calculate D 𝐺 exactly. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) ⇒ ⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) | ||
Theorem | ftc2 23611* | The Fundamental Theorem of Calculus, part two. If 𝐹 is a function continuous on [𝐴, 𝐵] and continuously differentiable on (𝐴, 𝐵), then the integral of the derivative of 𝐹 is equal to 𝐹(𝐵) − 𝐹(𝐴). This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
Theorem | ftc2ditglem 23612* | Lemma for ftc2ditg 23613. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
Theorem | ftc2ditg 23613* | Directed integral analogue of ftc2 23611. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
Theorem | itgparts 23614* | Integration by parts. If 𝐵(𝑥) is the derivative of 𝐴(𝑥) and 𝐷(𝑥) is the derivative of 𝐶(𝑥), and 𝐸 = (𝐴 · 𝐵)(𝑋) and 𝐹 = (𝐴 · 𝐵)(𝑌), then under suitable integrability and differentiability assumptions, the integral of 𝐴 · 𝐷 from 𝑋 to 𝑌 is equal to 𝐹 − 𝐸 minus the integral of 𝐵 · 𝐶. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶) ∈ ((𝑋[,]𝑌)–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ ((𝑋(,)𝑌)–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 · 𝐷)) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐵 · 𝐶)) ∈ 𝐿1) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐶)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝐴 · 𝐶) = 𝐸) & ⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝐴 · 𝐶) = 𝐹) ⇒ ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐴 · 𝐷) d𝑥 = ((𝐹 − 𝐸) − ∫(𝑋(,)𝑌)(𝐵 · 𝐶) d𝑥)) | ||
Theorem | itgsubstlem 23615* | Lemma for itgsubst 23616. (Contributed by Mario Carneiro, 12-Sep-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ*) & ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1)) & ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) & ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) & ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) ⇒ ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) | ||
Theorem | itgsubst 23616* | Integration by 𝑢-substitution. If 𝐴(𝑥) is a continuous, differentiable function from [𝑋, 𝑌] to (𝑍, 𝑊), whose derivative is continuous and integrable, and 𝐶(𝑢) is a continuous function on (𝑍, 𝑊), then the integral of 𝐶(𝑢) from 𝐾 = 𝐴(𝑋) to 𝐿 = 𝐴(𝑌) is equal to the integral of 𝐶(𝐴(𝑥)) D 𝐴(𝑥) from 𝑋 to 𝑌. In this part of the proof we discharge the assumptions in itgsubstlem 23615, which use the fact that (𝑍, 𝑊) is open to shrink the interval a little to (𝑀, 𝑁) where 𝑍 < 𝑀 < 𝑁 < 𝑊- this is possible because 𝐴(𝑥) is a continuous function on a closed interval, so its range is in fact a closed interval, and we have some wiggle room on the edges. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ*) & ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1)) & ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) & ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) & ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) ⇒ ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) | ||
Syntax | cmdg 23617 | Multivariate polynomial degree. |
class mDeg | ||
Syntax | cdg1 23618 | Univariate polynomial degree. |
class deg1 | ||
Definition | df-mdeg 23619* | Define the degree of a polynomial. Note (SO): as an experiment I am using a definition which makes the degree of the zero polynomial -∞, contrary to the convention used in df-dgr 23751. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ mDeg = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ sup(ran (ℎ ∈ (𝑓 supp (0g‘𝑟)) ↦ (ℂfld Σg ℎ)), ℝ*, < ))) | ||
Definition | df-deg1 23620 | Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ deg1 = (𝑟 ∈ V ↦ (1𝑜 mDeg 𝑟)) | ||
Theorem | reldmmdeg 23621 | Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ Rel dom mDeg | ||
Theorem | tdeglem1 23622* | Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐻:𝐴⟶ℕ0) | ||
Theorem | tdeglem3 23623* | Additivity of the total degree helper function. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐻‘(𝑋 ∘𝑓 + 𝑌)) = ((𝐻‘𝑋) + (𝐻‘𝑌))) | ||
Theorem | tdeglem4 23624* | There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝐻‘𝑋) = 0 ↔ 𝑋 = (𝐼 × {0}))) | ||
Theorem | tdeglem2 23625 | Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ (ℎ ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (ℎ‘∅)) = (ℎ ∈ (ℕ0 ↑𝑚 1𝑜) ↦ (ℂfld Σg ℎ)) | ||
Theorem | mdegfval 23626* | Value of the multivariate degree function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ 𝐷 = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*, < )) | ||
Theorem | mdegval 23627* | Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*, < )) | ||
Theorem | mdegleb 23628* | Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 ))) | ||
Theorem | mdeglt 23629* | If there is an upper limit on the degree of a polynomial that is lower than the degree of some exponent bag, then that exponent bag is unrepresented in the polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → (𝐷‘𝐹) < (𝐻‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = 0 ) | ||
Theorem | mdegldg 23630* | A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ)) & ⊢ 𝑌 = (0g‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹))) | ||
Theorem | mdegxrcl 23631 | Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*) | ||
Theorem | mdegxrf 23632 | Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ 𝐷:𝐵⟶ℝ* | ||
Theorem | mdegcl 23633 | Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞})) | ||
Theorem | mdeg0 23634 | Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (𝐷‘ 0 ) = -∞) | ||
Theorem | mdegnn0cl 23635 | Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0) | ||
Theorem | degltlem1 23636 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < 𝑌 ↔ 𝑋 ≤ (𝑌 − 1))) | ||
Theorem | degltp1le 23637 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < (𝑌 + 1) ↔ 𝑋 ≤ 𝑌)) | ||
Theorem | mdegaddle 23638 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) | ||
Theorem | mdegvscale 23639 | The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺)) | ||
Theorem | mdegvsca 23640 | The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐸) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = (𝐷‘𝐺)) | ||
Theorem | mdegle0 23641 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐴 = (algSc‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))))) | ||
Theorem | mdegmullem 23642* | Lemma for mdegmulle2 23643. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) & ⊢ 𝐴 = {𝑎 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld Σg 𝑏)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
Theorem | mdegmulle2 23643 | The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (𝐼 mPoly 𝑅) & ⊢ 𝐷 = (𝐼 mDeg 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
Theorem | deg1fval 23644 | Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ 𝐷 = (1𝑜 mDeg 𝑅) | ||
Theorem | deg1xrf 23645 | Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ 𝐷:𝐵⟶ℝ* | ||
Theorem | deg1xrcl 23646 | Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*) | ||
Theorem | deg1cl 23647 | Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞})) | ||
Theorem | mdegpropd 23648* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (𝐼 mDeg 𝑅) = (𝐼 mDeg 𝑆)) | ||
Theorem | deg1fvi 23649 | Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ ( deg1 ‘𝑅) = ( deg1 ‘( I ‘𝑅)) | ||
Theorem | deg1propd 23650* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → ( deg1 ‘𝑅) = ( deg1 ‘𝑆)) | ||
Theorem | deg1z 23651 | Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐷‘ 0 ) = -∞) | ||
Theorem | deg1nn0cl 23652 | Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0) | ||
Theorem | deg1n0ima 23653 | Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ (𝑅 ∈ Ring → (𝐷 “ (𝐵 ∖ { 0 })) ⊆ ℕ0) | ||
Theorem | deg1nn0clb 23654 | A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → (𝐹 ≠ 0 ↔ (𝐷‘𝐹) ∈ ℕ0)) | ||
Theorem | deg1lt0 23655 | A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) < 0 ↔ 𝐹 = 0 )) | ||
Theorem | deg1ldg 23656 | A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑌 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐴‘(𝐷‘𝐹)) ≠ 𝑌) | ||
Theorem | deg1ldgn 23657 | An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑌 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℕ0) & ⊢ (𝜑 → (𝐴‘𝑋) = 𝑌) ⇒ ⊢ (𝜑 → (𝐷‘𝐹) ≠ 𝑋) | ||
Theorem | deg1ldgdomn 23658 | A nonzero univariate polynomial over a domain always has a nonzero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐴‘(𝐷‘𝐹)) ∈ 𝐸) | ||
Theorem | deg1leb 23659* | Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ ℕ0 (𝐺 < 𝑥 → (𝐴‘𝑥) = 0 ))) | ||
Theorem | deg1val 23660 | Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Jul-2019.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐴 supp 0 ), ℝ*, < )) | ||
Theorem | deg1lt 23661 | If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ (𝐷‘𝐹) < 𝐺) → (𝐴‘𝐺) = 0 ) | ||
Theorem | deg1ge 23662 | Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (coe1‘𝐹) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℕ0 ∧ (𝐴‘𝐺) ≠ 0 ) → 𝐺 ≤ (𝐷‘𝐹)) | ||
Theorem | coe1mul3 23663 | The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ ∙ = (.r‘𝑌) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐼) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐽) ⇒ ⊢ (𝜑 → ((coe1‘(𝐹 ∙ 𝐺))‘(𝐼 + 𝐽)) = (((coe1‘𝐹)‘𝐼) · ((coe1‘𝐺)‘𝐽))) | ||
Theorem | coe1mul4 23664 | Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ ∙ = (.r‘𝑌) & ⊢ · = (.r‘𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 0 = (0g‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) ⇒ ⊢ (𝜑 → ((coe1‘(𝐹 ∙ 𝐺))‘((𝐷‘𝐹) + (𝐷‘𝐺))) = (((coe1‘𝐹)‘(𝐷‘𝐹)) · ((coe1‘𝐺)‘(𝐷‘𝐺)))) | ||
Theorem | deg1addle 23665 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) | ||
Theorem | deg1addle2 23666 | If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℝ*) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐿) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐿) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ 𝐿) | ||
Theorem | deg1add 23667 | Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐺) < (𝐷‘𝐹)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) = (𝐷‘𝐹)) | ||
Theorem | deg1vscale 23668 | The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺)) | ||
Theorem | deg1vsca 23669 | The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐸) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = (𝐷‘𝐺)) | ||
Theorem | deg1invg 23670 | The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑁 = (invg‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝑁‘𝐹)) = (𝐷‘𝐹)) | ||
Theorem | deg1suble 23671 | The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) | ||
Theorem | deg1sub 23672 | Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐺) < (𝐷‘𝐹)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) = (𝐷‘𝐹)) | ||
Theorem | deg1mulle2 23673 | Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) | ||
Theorem | deg1sublt 23674 | Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ (𝜑 → 𝐿 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐿) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐿) & ⊢ 𝐴 = (coe1‘𝐹) & ⊢ 𝐶 = (coe1‘𝐺) & ⊢ (𝜑 → ((coe1‘𝐹)‘𝐿) = ((coe1‘𝐺)‘𝐿)) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 − 𝐺)) < 𝐿) | ||
Theorem | deg1le0 23675 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵) → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘((coe1‘𝐹)‘0)))) | ||
Theorem | deg1sclle 23676 | A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐷‘(𝐴‘𝐹)) ≤ 0) | ||
Theorem | deg1scl 23677 | A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → (𝐷‘(𝐴‘𝐹)) = 0) | ||
Theorem | deg1mul2 23678 | Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ≠ 0 ) & ⊢ (𝜑 → ((coe1‘𝐹)‘(𝐷‘𝐹)) ∈ 𝐸) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = ((𝐷‘𝐹) + (𝐷‘𝐺))) | ||
Theorem | deg1mul3 23679 | Degree of multiplication of a polynomial on the left by a nonzero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Jul-2019.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (RLReg‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐸 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) = (𝐷‘𝐺)) | ||
Theorem | deg1mul3le 23680 | Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) ≤ (𝐷‘𝐺)) | ||
Theorem | deg1tmle 23681 | Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) ≤ 𝐹) | ||
Theorem | deg1tm 23682 | Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝐶 ∈ 𝐾 ∧ 𝐶 ≠ 0 ) ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) = 𝐹) | ||
Theorem | deg1pwle 23683 | Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) ≤ 𝐹) | ||
Theorem | deg1pw 23684 | Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑁 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝑁) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) = 𝐹) | ||
Theorem | ply1nz 23685 | Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing) | ||
Theorem | ply1nzb 23686 | Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ 𝑃 ∈ NzRing)) | ||
Theorem | ply1domn 23687 | Corollary of deg1mul2 23678: the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn → 𝑃 ∈ Domn) | ||
Theorem | ply1idom 23688 | The ring of univariate polynomials over an integral domain is itself an integral domain. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (𝑅 ∈ IDomn → 𝑃 ∈ IDomn) | ||
Syntax | cmn1 23689 | Monic polynomials. |
class Monic1p | ||
Syntax | cuc1p 23690 | Unitic polynomials. |
class Unic1p | ||
Syntax | cq1p 23691 | Univariate polynomial quotient. |
class quot1p | ||
Syntax | cr1p 23692 | Univariate polynomial remainder. |
class rem1p | ||
Syntax | cig1p 23693 | Univariate polynomial ideal generator. |
class idlGen1p | ||
Definition | df-mon1 23694* | Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟))}) | ||
Definition | df-uc1p 23695* | Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 23701. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))}) | ||
Definition | df-q1p 23696* | Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 23701. We actually use the reversed version for better harmony with our divisibility df-dvdsr 18464. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 (( deg1 ‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < (( deg1 ‘𝑟)‘𝑔)))) | ||
Definition | df-r1p 23697* | Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
⊢ rem1p = (𝑟 ∈ V ↦ ⦋(Base‘(Poly1‘𝑟)) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓(-g‘(Poly1‘𝑟))((𝑓(quot1p‘𝑟)𝑔)(.r‘(Poly1‘𝑟))𝑔)))) | ||
Definition | df-ig1p 23698* | Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
⊢ idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 = {(0g‘(Poly1‘𝑟))}, (0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖ {(0g‘(Poly1‘𝑟))})), ℝ, < ))))) | ||
Theorem | ply1divmo 23699* | Uniqueness of a quotient in a polynomial division. For polynomials 𝐹, 𝐺 such that 𝐺 ≠ 0 and the leading coefficient of 𝐺 is not a zero divisor, there is at most one polynomial 𝑞 which satisfies 𝐹 = (𝐺 · 𝑞) + 𝑟 where the degree of 𝑟 is less than the degree of 𝐺. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) & ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝐸) & ⊢ 𝐸 = (RLReg‘𝑅) ⇒ ⊢ (𝜑 → ∃*𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) | ||
Theorem | ply1divex 23700* | Lemma for ply1divalg 23701: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ≠ 0 ) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝐾) & ⊢ (𝜑 → (((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) = 1 ) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |