P. 261 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26001-26100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ftc1lem3 26001*	Lemma for ftc1 26005. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
Theorem	ftc1lem4 26002*	Lemma for ftc1 26005. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶))    &   ⊢ 𝐽 = (𝐿 ↾t ℝ)    &   ⊢ 𝐾 = (𝐿 ↾t 𝐷)    &   ⊢ 𝐿 = (TopOpen‘ℂfld)    &   ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (abs‘(𝑌 − 𝐶)) < 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝐶))) < 𝐸)
Theorem	ftc1lem5 26003*	Lemma for ftc1 26005. (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 26004*	Lemma for ftc1 26005. (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 26005*	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 26006*	Strengthen the assumptions of ftc1 26005 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 26007*	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 26008*	Lemma for ftc2ditg 26009. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	ftc2ditg 26009*	Directed integral analogue of ftc2 26007. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))
Theorem	itgparts 26010*	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 26011*	Lemma for itgsubst 26012. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ*)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))    &   ⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))    &   ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))    &   ⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸)    &   ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾)    &   ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊))    &   ⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))    ⇒   ⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥)
Theorem	itgsubst 26012*	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 26011, 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 26013*	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 26014	Multivariate polynomial degree.
class mDeg
Syntax	cdg1 26015	Univariate polynomial degree.
class deg1
Definition	df-mdeg 26016*	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 26152. (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 26017	Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ deg1 = (𝑟 ∈ V ↦ (1o mDeg 𝑟))
Theorem	reldmmdeg 26018	Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ Rel dom mDeg
Theorem	tdeglem1 26019*	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	tdeglem3 26020*	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	tdeglem4 26021*	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	tdeglem2 26022	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 26023*	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 26024*	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 26025*	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 26026*	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 26027*	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 26028	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 26029	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 26030	Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞}))
Theorem	mdeg0 26031	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 26032	Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0)
Theorem	degltlem1 26033	Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < 𝑌 ↔ 𝑋 ≤ (𝑌 − 1)))
Theorem	degltp1le 26034	Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ ((𝑋 ∈ (ℕ0 ∪ {-∞}) ∧ 𝑌 ∈ ℤ) → (𝑋 < (𝑌 + 1) ↔ 𝑋 ≤ 𝑌))
Theorem	mdegaddle 26035	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 26036	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 26037	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 26038	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 26039*	Lemma for mdegmulle2 26040. (Contributed by Stefan O'Rear, 26-Mar-2015.)
⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐷 = (𝐼 mDeg 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽)    &   ⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾)    &   ⊢ 𝐴 = {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}    &   ⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld Σg 𝑏))    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾))
Theorem	mdegmulle2 26040	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 26041	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 26042	Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ 𝐷:𝐵⟶ℝ*
Theorem	deg1xrcl 26043	Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ ℝ*)
Theorem	deg1cl 26044	Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈ (ℕ0 ∪ {-∞}))
Theorem	mdegpropd 26045*	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 26046	Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ (deg1‘𝑅) = (deg1‘( I ‘𝑅))
Theorem	deg1propd 26047*	Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑆))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑆)𝑦))    ⇒   ⊢ (𝜑 → (deg1‘𝑅) = (deg1‘𝑆))
Theorem	deg1z 26048	Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝑅 ∈ Ring → (𝐷‘ 0 ) = -∞)
Theorem	deg1nn0cl 26049	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 26050	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 26051	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 26052	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 26053	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 26054	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 26055	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 26056*	Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐴 = (coe1‘𝐹)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 𝐺 ↔ ∀𝑥 ∈ ℕ0 (𝐺 < 𝑥 → (𝐴‘𝑥) = 0 )))
Theorem	deg1val 26057	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 26058	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 26059	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 26060	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 26061	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 26062	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 26063	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 26064	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 26065	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 26066	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 26067	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 26068	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 26069	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 26070	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 26071	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 26072	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 26073	A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐷‘(𝐴‘𝐹)) ≤ 0)
Theorem	deg1scl 26074	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 26075	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	deg1mul 26076	Degree of multiplication of two nonzero polynomials in a domain. (Contributed by metakunt, 6-May-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) = ((𝐷‘𝐹) + (𝐷‘𝐺)))
Theorem	deg1mul3 26077	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 26078	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 26079	Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝑃)    &   ⊢ 𝑁 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑁)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐶 · (𝐹 ↑ 𝑋))) ≤ 𝐹)
Theorem	deg1tm 26080	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 26081	Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝑃)    &   ⊢ ↑ = (.g‘𝑁)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) ≤ 𝐹)
Theorem	deg1pw 26082	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 26083	Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing)
Theorem	ply1nzb 26084	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 26085	Corollary of deg1mul2 26075: 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 26086	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 26087	Monic polynomials.
class Monic1p
Syntax	cuc1p 26088	Unitic polynomials.
class Unic1p
Syntax	cq1p 26089	Univariate polynomial quotient.
class quot1p
Syntax	cr1p 26090	Univariate polynomial remainder.
class rem1p
Syntax	cig1p 26091	Univariate polynomial ideal generator.
class idlGen1p
Definition	df-mon1 26092*	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 26093*	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 26099. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ Unic1p = (𝑟 ∈ V ↦ {𝑓 ∈ (Base‘(Poly1‘𝑟)) ∣ (𝑓 ≠ (0g‘(Poly1‘𝑟)) ∧ ((coe1‘𝑓)‘((deg1‘𝑟)‘𝑓)) ∈ (Unit‘𝑟))})
Definition	df-q1p 26094*	Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 26099. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20293. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ quot1p = (𝑟 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑝⦌⦋(Base‘𝑝) / 𝑏⦌(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (℩𝑞 ∈ 𝑏 ((deg1‘𝑟)‘(𝑓(-g‘𝑝)(𝑞(.r‘𝑝)𝑔))) < ((deg1‘𝑟)‘𝑔))))
Definition	df-r1p 26095*	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 26096*	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 26097*	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 26098*	Lemma for ply1divalg 26099: 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 )    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))
Theorem	ply1divalg 26099*	The division algorithm for univariate polynomials over a ring. For polynomials 𝐹, 𝐺 such that 𝐺 ≠ 0 and the leading coefficient of 𝐺 is a unit, there are unique polynomials 𝑞 and 𝑟 = 𝐹 − (𝐺 · 𝑞) such that the degree of 𝑟 is less than the degree of 𝐺. (Contributed by Stefan O'Rear, 27-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    &   ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝑈)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))
Theorem	ply1divalg2 26100*	Reverse the order of multiplication in ply1divalg 26099 via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ≠ 0 )    &   ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝑈)    &   ⊢ 𝑈 = (Unit‘𝑅)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝑞 ∙ 𝐺))) < (𝐷‘𝐺))