P. 266 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26501-26600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dgrcolem2 26501*	Lemma for dgrco 26502. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 = (𝐷 + 1))    &   ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((deg‘𝑓) ≤ 𝐷 → (deg‘(𝑓 ∘ 𝐺)) = ((deg‘𝑓) · 𝑁)))    ⇒   ⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁))
Theorem	dgrco 26502	The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → (deg‘(𝐹 ∘ 𝐺)) = (𝑀 · 𝑁))
Theorem	plycjlem 26503*	Lemma for plycj 26504 and coecj 26505. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))
Theorem	plycj 26504*	The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on (∗‘𝑧) independently of 𝑧.) (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∗‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
Theorem	coecj 26505	Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐺) = (∗ ∘ 𝐴))
Theorem	plycjOLD 26506*	Obsolete version of plycj 26504 as of 22-Sep-2025. The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on (∗‘𝑧) independently of 𝑧.) (Contributed by Mario Carneiro, 24-Jul-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∗‘𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
Theorem	coecjOLD 26507	Obsolete version of coecj 26505 as of 22-Sep-2025. Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   ⊢ 𝐴 = (coeff‘𝐹)    ⇒   ⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐺) = (∗ ∘ 𝐴))
Theorem	plyrecj 26508	A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 𝐴 ∈ ℂ) → (∗‘(𝐹‘𝐴)) = (𝐹‘(∗‘𝐴)))
Theorem	plymul0or 26509	Polynomial multiplication has no zero divisors. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((𝐹 ∘f · 𝐺) = 0𝑝 ↔ (𝐹 = 0𝑝 ∨ 𝐺 = 0𝑝)))
Theorem	ofmulrt 26510	The set of roots of a product is the union of the roots of the terms. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → (◡(𝐹 ∘f · 𝐺) “ {0}) = ((◡𝐹 “ {0}) ∪ (◡𝐺 “ {0})))
Theorem	plymul02 26511	Product of a polynomial with the zero polynomial. (Contributed by Thierry Arnoux, 26-Sep-2018.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (0𝑝 ∘f · 𝐹) = 0𝑝)
Theorem	plyn0mulidp 26512*	Coefficients of a non-zero polynomial multiplied by the identity polynomial. (Contributed by Thierry Arnoux, 25-Sep-2018.)
⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹 ∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
Theorem	plymulidp 26513*	Coefficients of a polynomial multiplied by the identity polynomial. (Contributed by Thierry Arnoux, 25-Sep-2018.)
⊢ (𝐹 ∈ (Poly‘ℝ) → (coeff‘(𝐹 ∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
Theorem	plyreres 26514	Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐹 ∈ (Poly‘ℝ) → (𝐹 ↾ ℝ):ℝ⟶ℝ)
Theorem	dvply1 26515*	Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))))    &   ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)    &   ⊢ 𝐵 = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (ℂ D 𝐹) = 𝐺)
Theorem	dvply2g 26516	The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) Avoid ax-mulf 11207. (Revised by GG, 30-Apr-2025.)
⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆))
Theorem	dvply2 26517	The derivative of a polynomial is a polynomial. (Contributed by Stefan O'Rear, 14-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
⊢ (𝐹 ∈ (Poly‘𝑆) → (ℂ D 𝐹) ∈ (Poly‘ℂ))
Theorem	dvnply2 26518	Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝑆 ∈ (SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) → ((ℂ D𝑛 𝐹)‘𝑁) ∈ (Poly‘𝑆))
Theorem	dvnply 26519	Polynomials have polynomials as derivatives of all orders. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑁 ∈ ℕ0) → ((ℂ D𝑛 𝐹)‘𝑁) ∈ (Poly‘ℂ))
Theorem	plycpn 26520	Polynomials are smooth. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈ ∩ ran (𝓑C𝑛‘ℂ))
14.1.4  The division algorithm for polynomials
Syntax	cquot 26521	Extend class notation to include the quotient of a polynomial division.
class quot
Definition	df-quot 26522*	Define the quotient function on polynomials. This is the 𝑞 of the expression 𝑓 = 𝑔 · 𝑞 + 𝑟 in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (℩𝑞 ∈ (Poly‘ℂ)[(𝑓 ∘f − (𝑔 ∘f · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
Theorem	quotval 26523*	Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) = (℩𝑞 ∈ (Poly‘ℂ)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
Theorem	plydivlem1 26524*	Lemma for plydivalg 26530. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 0 ∈ 𝑆)
Theorem	plydivlem2 26525*	Lemma for plydivalg 26530. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    ⇒   ⊢ ((𝜑 ∧ 𝑞 ∈ (Poly‘𝑆)) → 𝑅 ∈ (Poly‘𝑆))
Theorem	plydivlem3 26526*	Lemma for plydivex 26528. Base case of induction. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    &   ⊢ (𝜑 → (𝐹 = 0𝑝 ∨ ((deg‘𝐹) − (deg‘𝐺)) < 0))    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))
Theorem	plydivlem4 26527*	Lemma for plydivex 26528. Induction step. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑀 − 𝑁) = 𝐷)    &   ⊢ (𝜑 → 𝐹 ≠ 0𝑝)    &   ⊢ 𝑈 = (𝑓 ∘f − (𝐺 ∘f · 𝑝))    &   ⊢ 𝐻 = (𝑧 ∈ ℂ ↦ (((𝐴‘𝑀) / (𝐵‘𝑁)) · (𝑧↑𝐷)))    &   ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘𝑆)((𝑓 = 0𝑝 ∨ ((deg‘𝑓) − 𝑁) < 𝐷) → ∃𝑝 ∈ (Poly‘𝑆)(𝑈 = 0𝑝 ∨ (deg‘𝑈) < 𝑁)))    &   ⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝐵 = (coeff‘𝐺)    &   ⊢ 𝑀 = (deg‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐺)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < 𝑁))
Theorem	plydivex 26528*	Lemma for plydivalg 26530. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))
Theorem	plydiveu 26529*	Lemma for plydivalg 26530. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    &   ⊢ (𝜑 → 𝑞 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))    &   ⊢ 𝑇 = (𝐹 ∘f − (𝐺 ∘f · 𝑝))    &   ⊢ (𝜑 → 𝑝 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → (𝑇 = 0𝑝 ∨ (deg‘𝑇) < (deg‘𝐺)))    ⇒   ⊢ (𝜑 → 𝑝 = 𝑞)
Theorem	plydivalg 26530*	The division algorithm on polynomials over a subfield 𝑆 of the complex numbers. If 𝐹 and 𝐺 ≠ 0 are polynomials over 𝑆, then there is a unique quotient polynomial 𝑞 such that the remainder 𝐹 − 𝐺 · 𝑞 is either zero or has degree less than 𝐺. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · 𝑞))    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ (Poly‘𝑆)(𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))
Theorem	quotlem 26531*	Lemma for properties of the polynomial quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · (𝐹 quot 𝐺)))    ⇒   ⊢ (𝜑 → ((𝐹 quot 𝐺) ∈ (Poly‘𝑆) ∧ (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺))))
Theorem	quotcl 26532*	The quotient of two polynomials in a field 𝑆 is also in the field. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ 𝑆)    &   ⊢ (𝜑 → -1 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → 𝐺 ≠ 0𝑝)    ⇒   ⊢ (𝜑 → (𝐹 quot 𝐺) ∈ (Poly‘𝑆))
Theorem	quotcl2 26533	Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐹 quot 𝐺) ∈ (Poly‘ℂ))
Theorem	quotdgr 26534	Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · (𝐹 quot 𝐺)))    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝑅 = 0𝑝 ∨ (deg‘𝑅) < (deg‘𝐺)))
Theorem	plyremlem 26535	Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐺 = (Xp ∘f − (ℂ × {𝐴}))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐺 ∈ (Poly‘ℂ) ∧ (deg‘𝐺) = 1 ∧ (◡𝐺 “ {0}) = {𝐴}))
Theorem	plyrem 26536	The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 16637). If a polynomial 𝐹 is divided by the linear factor 𝑥 − 𝐴, the remainder is equal to 𝐹(𝐴), the evaluation of the polynomial at 𝐴 (interpreted as a constant polynomial). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐺 = (Xp ∘f − (ℂ × {𝐴}))    &   ⊢ 𝑅 = (𝐹 ∘f − (𝐺 ∘f · (𝐹 quot 𝐺)))    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ) → 𝑅 = (ℂ × {(𝐹‘𝐴)}))
Theorem	facth 26537	The factor theorem. If a polynomial 𝐹 has a root at 𝐴, then 𝐺 = 𝑥 − 𝐴 is a factor of 𝐹 (and the other factor is 𝐹 quot 𝐺). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐺 = (Xp ∘f − (ℂ × {𝐴}))    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐴 ∈ ℂ ∧ (𝐹‘𝐴) = 0) → 𝐹 = (𝐺 ∘f · (𝐹 quot 𝐺)))
Theorem	fta1lem 26538*	Lemma for fta1 26539. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝑅 = (◡𝐹 “ {0})    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℂ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (deg‘𝐹) = (𝐷 + 1))    &   ⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {0}))    &   ⊢ (𝜑 → ∀𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝})((deg‘𝑔) = 𝐷 → ((◡𝑔 “ {0}) ∈ Fin ∧ (♯‘(◡𝑔 “ {0})) ≤ (deg‘𝑔))))    ⇒   ⊢ (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
Theorem	fta1 26539	The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg(𝐹) roots. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝑅 = (◡𝐹 “ {0})    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
Theorem	quotcan 26540	Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014.)
⊢ 𝐻 = (𝐹 ∘f · 𝐺)    ⇒   ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆) ∧ 𝐺 ≠ 0𝑝) → (𝐻 quot 𝐺) = 𝐹)
Theorem	vieta1lem1 26541*	Lemma for vieta1 26543. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝑅 = (◡𝐹 “ {0})    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → (♯‘𝑅) = 𝑁)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → (𝐷 + 1) = 𝑁)    &   ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))    &   ⊢ 𝑄 = (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))    ⇒   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
Theorem	vieta1lem2 26542*	Lemma for vieta1 26543: inductive step. Let 𝑧 be a root of 𝐹. Then 𝐹 = (Xp − 𝑧) · 𝑄 for some 𝑄 by the factor theorem, and 𝑄 is a degree- 𝐷 polynomial, so by the induction hypothesis Σ𝑥 ∈ (◡𝑄 “ 0)𝑥 = -(coeff‘𝑄)‘(𝐷 − 1) / (coeff‘𝑄)‘𝐷, so Σ𝑥 ∈ 𝑅𝑥 = 𝑧 − (coeff‘𝑄)‘ (𝐷 − 1) / (coeff‘𝑄)‘𝐷. Now the coefficients of 𝐹 are 𝐴‘(𝐷 + 1) = (coeff‘𝑄)‘𝐷 and 𝐴‘𝐷 = Σ𝑘 ∈ (0...𝐷)(coeff‘Xp − 𝑧)‘𝑘 · (coeff‘𝑄) ‘(𝐷 − 𝑘), which works out to -𝑧 · (coeff‘𝑄)‘𝐷 + (coeff‘𝑄)‘(𝐷 − 1), so putting it all together we have Σ𝑥 ∈ 𝑅𝑥 = -𝐴‘𝐷 / 𝐴‘(𝐷 + 1) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝑅 = (◡𝐹 “ {0})    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → (♯‘𝑅) = 𝑁)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → (𝐷 + 1) = 𝑁)    &   ⊢ (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(◡𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (◡𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))    &   ⊢ 𝑄 = (𝐹 quot (Xp ∘f − (ℂ × {𝑧})))    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
Theorem	vieta1 26543*	The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas). If a polynomial of degree 𝑁 has 𝑁 distinct roots, then the sum over these roots can be calculated as -𝐴(𝑁 − 1) / 𝐴(𝑁). (If the roots are not distinct, then this formula is still true but must double-count some of the roots according to their multiplicities.) See also vieta 34077 for the case of polynomials over a generic ring. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ 𝐴 = (coeff‘𝐹)    &   ⊢ 𝑁 = (deg‘𝐹)    &   ⊢ 𝑅 = (◡𝐹 “ {0})    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   ⊢ (𝜑 → (♯‘𝑅) = 𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴‘𝑁)))
Theorem	plyexmo 26544*	An infinite set of values can be extended to a polynomial in at most one way. (Contributed by Stefan O'Rear, 14-Nov-2014.)
⊢ ((𝐷 ⊆ ℂ ∧ ¬ 𝐷 ∈ Fin) → ∃*𝑝(𝑝 ∈ (Poly‘𝑆) ∧ (𝑝 ↾ 𝐷) = 𝐹))
14.1.5  Algebraic numbers
Syntax	caa 26545	Extend class notation to include the set of algebraic numbers.
class 𝔸
Definition	df-aa 26546	Define the set of algebraic numbers. An algebraic number is a root of a nonzero polynomial over the integers. Here we construct it as the union of all kernels (preimages of {0}) of all polynomials in (Poly‘ℤ), except the zero polynomial 0𝑝. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ 𝔸 = ∪ 𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(◡𝑓 “ {0})
Theorem	elaa 26547*	Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014.)
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0))
Theorem	aacn 26548	An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ)
Theorem	aasscn 26549	The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ 𝔸 ⊆ ℂ
Theorem	elqaalem1 26550*	Lemma for elqaa 26553. The function 𝑁 represents the denominators of the rational coefficients 𝐵. By multiplying them all together to make 𝑅, we get a number big enough to clear all the denominators and make 𝑅 · 𝐹 an integer polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    &   ⊢ 𝐵 = (coeff‘𝐹)    &   ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))    &   ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ ℕ0) → ((𝑁‘𝐾) ∈ ℕ ∧ ((𝐵‘𝐾) · (𝑁‘𝐾)) ∈ ℤ))
Theorem	elqaalem2 26551*	Lemma for elqaa 26553. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    &   ⊢ 𝐵 = (coeff‘𝐹)    &   ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))    &   ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))    &   ⊢ 𝑃 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 · 𝑦) mod (𝑁‘𝐾)))    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ (0...(deg‘𝐹))) → (𝑅 mod (𝑁‘𝐾)) = 0)
Theorem	elqaalem3 26552*	Lemma for elqaa 26553. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ((Poly‘ℚ) ∖ {0𝑝}))    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    &   ⊢ 𝐵 = (coeff‘𝐹)    &   ⊢ 𝑁 = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ ((𝐵‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < ))    &   ⊢ 𝑅 = (seq0( · , 𝑁)‘(deg‘𝐹))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝔸)
Theorem	elqaa 26553*	The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa 26547 are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof shortened by AV, 3-Oct-2020.)
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0))
Theorem	qaa 26554	Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ 𝔸)
Theorem	qssaa 26555	The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ ℚ ⊆ 𝔸
Theorem	0aa 26556	Zero is algebraic. (Contributed by Ender Ting, 21-Jul-2026.)
⊢ 0 ∈ 𝔸
Theorem	1aa 26557	One is algebraic. (Contributed by Ender Ting, 21-Jul-2026.)
⊢ 1 ∈ 𝔸
Theorem	iaa 26558	The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ i ∈ 𝔸
Theorem	aareccl 26559	The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ 𝔸)
Theorem	aacjcl 26560	The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝐴 ∈ 𝔸 → (∗‘𝐴) ∈ 𝔸)
Theorem	aannenlem1 26561*	Lemma for aannen 26564. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})    ⇒   ⊢ (𝐴 ∈ ℕ0 → (𝐻‘𝐴) ∈ Fin)
Theorem	aannenlem2 26562*	Lemma for aannen 26564. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})    ⇒   ⊢ 𝔸 = ∪ ran 𝐻
Theorem	aannenlem3 26563*	The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐻 = (𝑎 ∈ ℕ0 ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ0 (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})    ⇒   ⊢ 𝔸 ≈ ℕ
Theorem	aannen 26564	The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝔸 ≈ ℕ
14.1.6  Liouville's approximation theorem
Theorem	aalioulem1 26565	Lemma for aaliou 26571. An integer polynomial cannot inflate the denominator of a rational by more than its degree. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑋 ∈ ℤ)    &   ⊢ (𝜑 → 𝑌 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐹‘(𝑋 / 𝑌)) · (𝑌↑(deg‘𝐹))) ∈ ℤ)
Theorem	aalioulem2 26566*	Lemma for aaliou 26571. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Theorem	aalioulem3 26567*	Lemma for aaliou 26571. (Contributed by Stefan O'Rear, 15-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((abs‘(𝐴 − 𝑟)) ≤ 1 → (𝑥 · (abs‘(𝐹‘𝑟))) ≤ (abs‘(𝐴 − 𝑟))))
Theorem	aalioulem4 26568*	Lemma for aaliou 26571. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (((𝐹‘(𝑝 / 𝑞)) ≠ 0 ∧ (abs‘(𝐴 − (𝑝 / 𝑞))) ≤ 1) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Theorem	aalioulem5 26569*	Lemma for aaliou 26571. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) ≠ 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Theorem	aalioulem6 26570*	Lemma for aaliou 26571. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	aaliou 26571*	Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial 𝐹 in integer coefficients, is not approximable beyond order 𝑁 = deg(𝐹) by rational numbers. In this form, it also applies to rational numbers themselves, which are not well approximable by other rational numbers. This is Metamath 100 proof #18. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝑁 = (deg‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝐹‘𝐴) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	geolim3 26572*	Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐵) < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝐹 = (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))    ⇒   ⊢ (𝜑 → seq𝐴( + , 𝐹) ⇝ (𝐶 / (1 − 𝐵)))
Theorem	aaliou2 26573*	Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝔸 ∩ ℝ) → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	aaliou2b 26574*	Liouville's approximation theorem extended to complex 𝐴. (Contributed by Stefan O'Rear, 20-Nov-2014.)
⊢ (𝐴 ∈ 𝔸 → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))
Theorem	aaliou3lem1 26575*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ)
Theorem	aaliou3lem2 26576*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵)))
Theorem	aaliou3lem3 26577*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴))))    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    ⇒   ⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴)))))
Theorem	aaliou3lem8 26578*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 20-Nov-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℕ (2 · (2↑-(!‘(𝑥 + 1)))) ≤ (𝐵 / ((2↑(!‘𝑥))↑𝐴)))
Theorem	aaliou3lem4 26579*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ 𝐿 ∈ ℝ
Theorem	aaliou3lem5 26580*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ (𝐴 ∈ ℕ → (𝐻‘𝐴) ∈ ℝ)
Theorem	aaliou3lem6 26581*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) ∈ ℤ)
Theorem	aaliou3lem7 26582*	Lemma for aaliou3 26584. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝐴))) ≤ (2 · (2↑-(!‘(𝐴 + 1))))))
Theorem	aaliou3lem9 26583*	Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.)
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))    &   ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)    &   ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))    ⇒   ⊢ ¬ 𝐿 ∈ 𝔸
Theorem	aaliou3 26584	Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.)
⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸
Theorem	aaliou3r 26585	The sum presented above is convergent, which means that the "Liouville number" is indeed real. (Contributed by Ender Ting, 21-Jul-2026.)
⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∈ ℝ
14.2  Sequences and series
14.2.1  Taylor polynomials and Taylor's theorem
Syntax	ctayl 26586	Taylor polynomial of a function.
class Tayl
Syntax	cana 26587	The class of analytic functions.
class Ana
Definition	df-tayl 26588*	Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ0 ∪ {+∞}) should be replaced by 𝑛 ∈ ℕ0*. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))
Definition	df-ana 26589*	Define the set of analytic functions, which are functions such that the Taylor series of the function at each point converges to the function in some neighborhood of the point. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
Theorem	taylfvallem1 26590*	Lemma for taylfval 26592. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    ⇒   ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ)
Theorem	taylfvallem 26591*	Lemma for taylfval 26592. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ℂ) → (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))) ⊆ ℂ)
Theorem	taylfval 26592*	Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: 𝑆 is the base set with respect to evaluate the derivatives (generally ℝ or ℂ), 𝐹 is the function we are approximating, at point 𝐵, to order 𝑁. The result is a polynomial function of 𝑥. This "extended" version of taylpfval 26598 additionally handles the case 𝑁 = +∞, in which case this is not a polynomial but an infinite series, the Taylor series of the function. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))
Theorem	eltayl 26593*	Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝑇𝑌 ↔ (𝑋 ∈ ℂ ∧ 𝑌 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))))))
Theorem	taylf 26594*	The Taylor series defines a function on a subset of the complex numbers. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ)
Theorem	tayl0 26595*	The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))
Theorem	taylplem1 26596*	Lemma for taylpfval 26598 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
Theorem	taylplem2 26597*	Lemma for taylpfval 26598 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    ⇒   ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ)
Theorem	taylpfval 26598*	Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: 𝑆 is the base set with respect to evaluate the derivatives (generally ℝ or ℂ), 𝐹 is the function we are approximating, at point 𝐵, to order 𝑁. The result is a polynomial function of 𝑥. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))
Theorem	taylpf 26599	The Taylor polynomial is a function on the complex numbers (even if the base set of the original function is the reals). (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    ⇒   ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
Theorem	taylpval 26600*	Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁))    &   ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑇‘𝑋) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))