P. 252 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25101-25200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvfsumrlim2 25101*	Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if 𝑥 ∈ 𝑆 ↦ 𝐵 is a decreasing function with antiderivative 𝐴 converging to zero, then the difference between Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐵(𝑘) and ∫𝑢 ∈ (𝑀[,]𝑥)𝐵(𝑢) d𝑢 = 𝐴(𝑥) converges to a constant limit value, with the remainder term bounded by 𝐵(𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ≤ 𝑋)    ⇒   ⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (abs‘((𝐺‘𝑋) − 𝐿)) ≤ ⦋𝑋 / 𝑥⦌𝐵)
Theorem	dvfsumrlim3 25102*	Conjoin the statements of dvfsumrlim 25100 and dvfsumrlim2 25101. (This is useful as a target for lemmas, because the hypotheses to this theorem are complex, and we don't want to repeat ourselves.) (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝑆 = (𝑇(,)+∞)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1))    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))    &   ⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐸)    ⇒   ⊢ (𝜑 → (𝐺:𝑆⟶ℝ ∧ 𝐺 ∈ dom ⇝𝑟 ∧ ((𝐺 ⇝𝑟 𝐿 ∧ 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋) → (abs‘((𝐺‘𝑋) − 𝐿)) ≤ 𝐸)))
Theorem	dvfsum2 25103*	The reverse of dvfsumrlim 25100, 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 25104*	Lemma for ftc1a 25106 and ftc1 25111. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)
Theorem	ftc1lem2 25105*	Lemma for ftc1 25111. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)    ⇒   ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
Theorem	ftc1a 25106*	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 25107*	Lemma for ftc1 25111. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
Theorem	ftc1lem4 25108*	Lemma for ftc1 25111. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    &   ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑌 − 𝐶)) < 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝐶))) < 𝐸)
Theorem	ftc1lem5 25109*	Lemma for ftc1 25111. (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 25110*	Lemma for ftc1 25111. (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 25111*	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 25112*	Strengthen the assumptions of ftc1 25111 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 25113*	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 25114*	Lemma for ftc2ditg 25115. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	ftc2ditg 25115*	Directed integral analogue of ftc2 25113. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	itgparts 25116*	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 25117*	Lemma for itgsubst 25118. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ*)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))    &   ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))    ⇒   ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)
Theorem	itgsubst 25118*	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 25117, 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𝑥)
Theorem	itgpowd 25119*	The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1)))
PART 14  BASIC REAL AND COMPLEX FUNCTIONS
14.1  Polynomials
14.1.1  Polynomial degrees
Syntax	cmdg 25120	Multivariate polynomial degree.
class mDeg
Syntax	cdg1 25121	Univariate polynomial degree.
class deg1
Definition	df-mdeg 25122*	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 25257. (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 25123	Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ deg1 = (𝑟 ∈ V ↦ (1o mDeg 𝑟))
Theorem	reldmmdeg 25124	Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ Rel dom mDeg
Theorem	tdeglem1 25125*	Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove sethood antecedent. (Revised by SN, 7-Aug-2024.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ 𝐻:𝐴⟶ℕ0
Theorem	tdeglem1OLD 25126*	Obsolete version of tdeglem1 25125 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻:𝐴⟶ℕ0)
Theorem	tdeglem3 25127*	Additivity of the total degree helper function. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐻‘(𝑋 ∘f + 𝑌)) = ((𝐻‘𝑋) + (𝐻‘𝑌)))
Theorem	tdeglem3OLD 25128*	Obsolete version of tdeglem3 25127 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐻‘(𝑋 ∘f + 𝑌)) = ((𝐻‘𝑋) + (𝐻‘𝑌)))
Theorem	tdeglem4 25129*	There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ (𝑋 ∈ 𝐴 → ((𝐻‘𝑋) = 0 ↔ 𝑋 = (𝐼 × {0})))
Theorem	tdeglem4OLD 25130*	Obsolete version of tdeglem4 25129 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 29-Mar-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝐻‘𝑋) = 0 ↔ 𝑋 = (𝐼 × {0})))
Theorem	tdeglem2 25131	Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ (ℎ ∈ (ℕ0 ↑m 1o) ↦ (ℎ‘∅)) = (ℎ ∈ (ℕ0 ↑m 1o) ↦ (ℂfld Σg ℎ))
Theorem	mdegfval 25132*	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 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ 𝐷 = (𝑓 ∈ 𝐵 ↦ sup((𝐻 “ (𝑓 supp 0 )), ℝ*, < ))
Theorem	mdegval 25133*	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 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*, < ))
Theorem	mdegleb 25134*	Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐺 < (𝐻‘𝑥) → (𝐹‘𝑥) = 0 )))
Theorem	mdeglt 25135*	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 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐷‘𝐹) < (𝐻‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = 0 )
Theorem	mdegldg 25136*	A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = {𝑚 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑚 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld Σg ℎ))    &   ⊢ 𝑌 = (0g‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))
Theorem	mdegxrcl 25137	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 25138	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 25139	Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞}))
Theorem	mdeg0 25140	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 25141	Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0)
Theorem	degltlem1 25142	Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < 𝑌 ↔ 𝑋 ≤ (𝑌 − 1)))
Theorem	degltp1le 25143	Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < (𝑌 + 1) ↔ 𝑋 ≤ 𝑌))
Theorem	mdegaddle 25144	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 25145	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 25146	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 25147	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 25148*	Lemma for mdegmulle2 25149. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽)    &   ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾)    &   ⊢ 𝐴 = {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld Σg 𝑏))    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾))
Theorem	mdegmulle2 25149	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 25150	Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    ⇒   ⊢ 𝐷 = (1o mDeg 𝑅)
Theorem	deg1xrf 25151	Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ 𝐷:𝐵⟶ℝ*
Theorem	deg1xrcl 25152	Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*)
Theorem	deg1cl 25153	Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞}))
Theorem	mdegpropd 25154*	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 25155	Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ ( deg1 ‘𝑅) = ( deg1 ‘( I ‘𝑅))
Theorem	deg1propd 25156*	Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦))    ⇒   ⊢ (𝜑 → ( deg1 ‘𝑅) = ( deg1 ‘𝑆))
Theorem	deg1z 25157	Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐷‘ 0 ) = -∞)
Theorem	deg1nn0cl 25158	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 25159	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 25160	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 25161	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 25162	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 25163	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 25164	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 25165*	Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ ℕ0 (𝐺 < 𝑥 → (𝐴‘𝑥) = 0 )))
Theorem	deg1val 25166	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 25167	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 25168	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 25169	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 25170	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 25171	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 25172	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 25173	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 25174	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 25175	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 25176	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 25177	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 25178	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 25179	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 25180	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 25181	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 25182	A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐷‘(𝐴‘𝐹)) ≤ 0)
Theorem	deg1scl 25183	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 25184	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 25185	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 25186	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 25187	Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑁 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑁)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) ≤ 𝐹)
Theorem	deg1tm 25188	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 25189	Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑁)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) ≤ 𝐹)
Theorem	deg1pw 25190	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 25191	Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing)
Theorem	ply1nzb 25192	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 25193	Corollary of deg1mul2 25184: 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 25194	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)
14.1.2  The division algorithm for univariate polynomials
Syntax	cmn1 25195	Monic polynomials.
class Monic1p
Syntax	cuc1p 25196	Unitic polynomials.
class Unic1p
Syntax	cq1p 25197	Univariate polynomial quotient.
class quot1p
Syntax	cr1p 25198	Univariate polynomial remainder.
class rem1p
Syntax	cig1p 25199	Univariate polynomial ideal generator.
class idlGen1p
Definition	df-mon1 25200*	Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ Monic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘(( deg1 ‘𝑟)‘𝑓)) = (1r‘𝑟))})