P. 338 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33701-33800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fldextfld2 33701	A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field)
Theorem	fldextsubrg 33702	Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝑈 = (Base‘𝐹)    ⇒   ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸))
Theorem	fldextress 33703	Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹)))
Theorem	brfinext 33704	The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0))
Theorem	extdgval 33705	Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
Theorem	fldextsralvec 33706	The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
Theorem	extdgcl 33707	Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*)
Theorem	extdggt0 33708	Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹))
Theorem	fldexttr 33709	Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾)
Theorem	fldextid 33710	The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹)
Theorem	extdgid 33711	A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.)
⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1)
Theorem	fldsdrgfldext 33712	A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐺 = (𝐹 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → 𝐹/FldExt𝐺)
Theorem	fldsdrgfldext2 33713	A sub-sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐺 = (𝐹 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹))    &   ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐺))    &   ⊢ 𝐻 = (𝐹 ↾s 𝐵)    ⇒   ⊢ (𝜑 → 𝐺/FldExt𝐻)
Theorem	extdgmul 33714	The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, the degree of the extension 𝐸/FldExt𝐾 is the product of the degrees of the extensions 𝐸/FldExt𝐹 and 𝐹/FldExt𝐾. Proposition 1.2 of [Lang], p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → (𝐸[:]𝐾) = ((𝐸[:]𝐹) ·e (𝐹[:]𝐾)))
Theorem	finexttrb 33715	The extension 𝐸 of 𝐾 is finite if and only if 𝐸 is finite over 𝐹 and 𝐹 is finite over 𝐾. Corollary 1.3 of [Lang] , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → (𝐸/FinExt𝐾 ↔ (𝐸/FinExt𝐹 ∧ 𝐹/FinExt𝐾)))
Theorem	extdg1id 33716	If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)
Theorem	extdg1b 33717	The degree of the extension 𝐸/FldExt𝐹 is 1 iff 𝐸 and 𝐹 are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → ((𝐸[:]𝐹) = 1 ↔ 𝐸 = 𝐹))
Theorem	fldgenfldext 33718	A subfield 𝐹 extended with a set 𝐴 forms a field extension. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ 𝐴)))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐿/FldExt𝐾)
Theorem	fldextchr 33719	The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → (chr‘𝐹) = (chr‘𝐸))
Theorem	evls1fldgencl 33720	Closure of the subring polynomial evaluation in the field extention. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
Theorem	ccfldsrarelvec 33721	The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
Theorem	ccfldextdgrr 33722	The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ (ℂfld[:]ℝfld) = 2
Theorem	fldextrspunlsplem 33723*	Lemma for fldextrspunlsp 33724: First direction. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝑃:𝐻⟶𝐺)    &   ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))    &   ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
Theorem	fldextrspunlsp 33724	Lemma for fldextrspunfld 33726. The subring generated by the union of two field extensions 𝐺 and 𝐻 is the vector sub- 𝐺 space generated by a basis 𝐵 of 𝐻. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵))
Theorem	fldextrspunlem1 33725	Lemma for fldextrspunfld 33726. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    ⇒   ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
Theorem	fldextrspunfld 33726	The ring generated by the union of two field extensions is a field. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    ⇒   ⊢ (𝜑 → 𝐸 ∈ Field)
Theorem	fldextrspunlem2 33727	Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐿 fldGen (𝐺 ∪ 𝐻)))
Theorem	fldextrspundgle 33728	Inequality involving the degree of two different field extensions 𝐼 and 𝐽 of a same field 𝐹. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    ⇒   ⊢ (𝜑 → (𝐸[:]𝐼) ≤ (𝐽[:]𝐾))
Theorem	fldextrspundglemul 33729	Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾 of the same field 𝐾, 𝐽 / 𝐾 being finite, and the composiste field 𝐸 = 𝐼𝐽, the degree of the extension of the composite field 𝐸 / 𝐾 is at most the product of the field extension degrees of 𝐼 / 𝐾 and 𝐽 / 𝐾. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    ⇒   ⊢ (𝜑 → (𝐸[:]𝐾) ≤ ((𝐼[:]𝐾) ·e (𝐽[:]𝐾)))
Theorem	fldextrspundgdvdslem 33730	Lemma for fldextrspundgdvds 33731. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0)
Theorem	fldextrspundgdvds 33731	Given two finite extensions 𝐼 / 𝐾 and 𝐽 / 𝐾 of the same field 𝐾, the degree of the extension 𝐼 / 𝐾 divides the degree of the extension 𝐸 / 𝐾, 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐼[:]𝐾) ∥ (𝐸[:]𝐾))
Theorem	fldext2rspun 33732*	Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾, 𝐼 / 𝐾 being a quadratic extension, and the degree of 𝐽 / 𝐾 being a power of 2, the degree of the extension 𝐸 / 𝐾 is a power of 2 , 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐼[:]𝐾) = 2)    &   ⊢ (𝜑 → (𝐽[:]𝐾) = (2↑𝑁))    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐸[:]𝐾) = (2↑𝑛))
21.3.11.1  Algebraic numbers
Syntax	cirng 33733	Integral subring of a ring.
class IntgRing
Definition	df-irng 33734*	Define the subring of elements of a ring 𝑟 integral over a subset 𝑠. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Thierry Arnoux, 28-Jan-2025.)
⊢ IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)}))
Theorem	irngval 33735*	The elements of a field 𝑅 integral over a subset 𝑆. In the case of a subfield, those are the algebraic numbers over the field 𝑆 within the field 𝑅. That is, the numbers 𝑋 which are roots of monic polynomials 𝑃(𝑋) with coefficients in 𝑆. (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 IntgRing 𝑆) = ∪ 𝑓 ∈ (Monic1p‘𝑈)(◡(𝑂‘𝑓) “ { 0 }))
Theorem	elirng 33736*	Property for an element 𝑋 of a field 𝑅 to be integral over a subring 𝑆. (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑅 IntgRing 𝑆) ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑋) = 0 )))
Theorem	irngss 33737	All elements of a subring 𝑆 are integral over 𝑆. This is only true in the case of a nonzero ring, since there are no integral elements in a zero ring (see 0ringirng 33739). (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆))
Theorem	irngssv 33738	An integral element is an element of the base set. (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 IntgRing 𝑆) ⊆ 𝐵)
Theorem	0ringirng 33739	A zero ring 𝑅 has no integral elements. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → ¬ 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝑅 IntgRing 𝑆) = ∅)
Theorem	irngnzply1lem 33740	In the case of a field 𝐸, a root 𝑋 of some nonzero polynomial 𝑃 with coefficients in a subfield 𝐹 is integral over 𝐹. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝑃 ∈ dom 𝑂)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑍)    &   ⊢ (𝜑 → ((𝑂‘𝑃)‘𝑋) = 0 )    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
Theorem	irngnzply1 33741*	In the case of a field 𝐸, the roots of nonzero polynomials 𝑝 with coefficients in a subfield 𝐹 are exactly the integral elements over 𝐹. Roots of nonzero polynomials are called algebraic numbers, so this shows that in the case of a field, elements integral over 𝐹 are exactly the algebraic numbers. In this formula, dom 𝑂 represents the polynomials, and 𝑍 the zero polynomial. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    ⇒   ⊢ (𝜑 → (𝐸 IntgRing 𝐹) = ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }))
21.3.11.2  Minimal polynomials
Syntax	cminply 33742	Extend class notation with the minimal polynomial builder function.
class minPoly
Definition	df-minply 33743*	Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025.)
⊢ minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})))
Theorem	ply1annidllem 33744*	Write the set 𝑄 of polynomials annihilating an element 𝐴 as the kernel of the ring homomorphism 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐹 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))    ⇒   ⊢ (𝜑 → 𝑄 = (◡𝐹 “ { 0 }))
Theorem	ply1annidl 33745*	The set 𝑄 of polynomials annihilating an element 𝐴 forms an ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    ⇒   ⊢ (𝜑 → 𝑄 ∈ (LIdeal‘𝑃))
Theorem	ply1annnr 33746*	The set 𝑄 of polynomials annihilating an element 𝐴 is not the whole polynomial ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 𝑈)
Theorem	ply1annig1p 33747*	The ideal 𝑄 of polynomials annihilating an element 𝐴 is generated by the ideal's canonical generator. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐾 = (RSpan‘𝑃)    &   ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → 𝑄 = (𝐾‘{(𝐺‘𝑄)}))
Theorem	minplyval 33748*	Expand the value of the minimal polynomial (𝑀‘𝐴) for a given element 𝐴. It is defined as the unique monic polynomial of minimal degree which annihilates 𝐴. By ply1annig1p 33747, that polynomial generates the ideal of the annihilators of 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐾 = (RSpan‘𝑃)    &   ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = (𝐺‘𝑄))
Theorem	minplycl 33749*	The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐾 = (RSpan‘𝑃)    &   ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃))
Theorem	ply1annprmidl 33750*	The set 𝑄 of polynomials annihilating an element 𝐴 is a prime ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    ⇒   ⊢ (𝜑 → 𝑄 ∈ (PrmIdeal‘𝑃))
Theorem	minplymindeg 33751	The minimal polynomial of 𝐴 is minimal among the nonzero annihilators of 𝐴 with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝐷 = (deg1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → ((𝑂‘𝐻)‘𝐴) = 0 )    &   ⊢ (𝜑 → 𝐻 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐻 ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ≤ (𝐷‘𝐻))
Theorem	minplyann 33752	The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 )
Theorem	minplyirredlem 33753	Lemma for minplyirred 33754. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    &   ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴))    &   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸))    &   ⊢ (𝜑 → 𝐺 ≠ 𝑍)    &   ⊢ (𝜑 → 𝐻 ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃))
Theorem	minplyirred 33754	A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃))
Theorem	irngnminplynz 33755	Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)
Theorem	minplym1p 33756	A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	irredminply 33757	An irreducible, monic, annihilating polynomial is the minimal polynomial. (Contributed by Thierry Arnoux, 27-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = 0 )    &   ⊢ (𝜑 → 𝐺 ∈ (Irred‘𝑃))    &   ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘(𝐸 ↾s 𝐹)))    ⇒   ⊢ (𝜑 → 𝐺 = (𝑀‘𝐴))
Theorem	algextdeglem1 33758	Lemma for algextdeg 33766. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
Theorem	algextdeglem2 33759*	Lemma for algextdeg 33766. Both the ring of polynomials 𝑃 and the field 𝐿 generated by 𝐾 and the algebraic element 𝐴 can be considered as modules over the elements of 𝐹. Then, the evaluation map 𝐺, mapping polynomials to their evaluation at 𝐴, is a module homomorphism between those modules. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
Theorem	algextdeglem3 33760*	Lemma for algextdeg 33766. The quotient 𝑃 / 𝑍 of the vector space 𝑃 of polynomials by the subspace 𝑍 of polynomials annihilating 𝐴 is itself a vector space. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → 𝑄 ∈ LVec)
Theorem	algextdeglem4 33761*	Lemma for algextdeg 33766. By lmhmqusker 33445, the surjective module homomorphism 𝐺 described in algextdeglem2 33759 induces an isomorphism with the quotient space. Therefore, the dimension of that quotient space 𝑃 / 𝑍 is the degree of the algebraic field extension. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))
Theorem	algextdeglem5 33762*	Lemma for algextdeg 33766. The subspace 𝑍 of annihilators of 𝐴 is a principal ideal generated by the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{(𝑀‘𝐴)}))
Theorem	algextdeglem6 33763*	Lemma for algextdeg 33766. By r1pquslmic 33631, the univariate polynomial remainder ring (𝐻 “s 𝑃) is isomorphic with the quotient ring 𝑄. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    &   ⊢ 𝑅 = (rem1p‘𝐾)    &   ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))    ⇒   ⊢ (𝜑 → (dim‘𝑄) = (dim‘(𝐻 “s 𝑃)))
Theorem	algextdeglem7 33764*	Lemma for algextdeg 33766. The polynomials 𝑋 of lower degree than the minimal polynomial are left unchanged when taking the remainder of the division by that minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    &   ⊢ 𝑅 = (rem1p‘𝐾)    &   ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))    &   ⊢ 𝑇 = (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑇 ↔ (𝐻‘𝑋) = 𝑋))
Theorem	algextdeglem8 33765*	Lemma for algextdeg 33766. The dimension of the univariate polynomial remainder ring (𝐻 “s 𝑃) is the degree of the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    &   ⊢ 𝑅 = (rem1p‘𝐾)    &   ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))    &   ⊢ 𝑇 = (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴))))    ⇒   ⊢ (𝜑 → (dim‘(𝐻 “s 𝑃)) = (𝐷‘(𝑀‘𝐴)))
Theorem	algextdeg 33766	The degree of an algebraic field extension (noted [𝐿:𝐾]) is the degree of the minimal polynomial 𝑀(𝐴), whereas 𝐿 is the field generated by 𝐾 and the algebraic element 𝐴. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿[:]𝐾) = (𝐷‘(𝑀‘𝐴)))
21.3.11.3  Quadratic Field Extensions
Theorem	rtelextdg2lem 33767	Lemma for rtelextdg2 33768: If an element 𝑋 is a solution of a quadratic equation, then the degree of its field extension is at most 2. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝑋})))    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑉 = (Base‘𝐸)    &   ⊢ · = (.r‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐹)    &   ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )    &   ⊢ 𝑌 = (var1‘𝐾)    &   ⊢ ⊕ = (+g‘𝑃)    &   ⊢ ⊗ = (.r‘𝑃)    &   ⊢ ∧ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑈 = (algSc‘𝑃)    &   ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))    ⇒   ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)
Theorem	rtelextdg2 33768	If an element 𝑋 is a solution of a quadratic equation, then it is either in the base field, or the degree of its field extension is exactly 2. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝑋})))    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑉 = (Base‘𝐸)    &   ⊢ · = (.r‘𝐸)    &   ⊢ + = (+g‘𝐸)    &   ⊢ ↑ = (.g‘(mulGrp‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐹)    &   ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2))
21.3.11.4  Towers of quadratic extentions
Theorem	fldext2chn 33769*	In a non-empty chain 𝑇 of quadratic field extensions, the degree of the final extension is always a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐸 = (𝑊 ↾s 𝑒)    &   ⊢ 𝐹 = (𝑊 ↾s 𝑓)    &   ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}    &   ⊢ (𝜑 → 𝑇 ∈ ( < Chain(SubDRing‘𝑊)))    &   ⊢ (𝜑 → 𝑊 ∈ Field)    &   ⊢ (𝜑 → (𝑊 ↾s (𝑇‘0)) = 𝑄)    &   ⊢ (𝜑 → (𝑊 ↾s (lastS‘𝑇)) = 𝐿)    &   ⊢ (𝜑 → 0 < (♯‘𝑇))    ⇒   ⊢ (𝜑 → (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)))
21.3.12  Constructible Numbers This section defines the set of constructible points as complex numbers which can be drawn starting from two points (we take 0 and 1), and taking intersections of circles and lines. This construction is useful for proving the impossibility of doubling the cube ( * imp2cube ), and of angle trisection ( * imp3ang )
Syntax	cconstr 33770	Extend class notation with the set of constructible points.
class Constr
Definition	df-constr 33771*	Define the set of geometrically constructible points, by recursively adding the line-line, line-circle and circle-circle intersections constructions using points in a previous iteration. (Contributed by Saveliy Skresanov, 19-Jan-2025.)
⊢ Constr = ∪ (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) “ ω)
Theorem	constrrtll 33772	In the construction of constructible numbers, line-line intersections are solutions of linear equations, and can therefore be completely constructed. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → 𝑋 = (𝐶 + (𝑅 · (𝐷 − 𝐶))))    &   ⊢ (𝜑 → (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ 0)    &   ⊢ 𝑁 = (𝐴 + (((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵 − 𝐴)))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑁)
Theorem	constrrtlc1 33773	In the construction of constructible numbers, line-circle intersections are roots of a quadratic equation, non-degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) = (abs‘(𝐸 − 𝐹)))    &   ⊢ 𝑄 = (((∗‘𝐵) − (∗‘𝐴)) / (𝐵 − 𝐴))    &   ⊢ 𝑀 = (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄)    &   ⊢ 𝑁 = (-((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸 − 𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) / 𝑄)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0 ∧ 𝑄 ≠ 0))
Theorem	constrrtlc2 33774	In the construction of constructible numbers, line-circle intersections are one of the original points, in a degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) = (abs‘(𝐸 − 𝐹)))    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = 𝐴)
Theorem	constrrtcclem 33775	In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. Case of non-degenerate circles. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐷)    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))    &   ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))    &   ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))    &   ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))    &   ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ≠ 𝐹)    ⇒   ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
Theorem	constrrtcc 33776	In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐷)    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))    &   ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶)))    &   ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹)))    &   ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴)))    &   ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴)))    ⇒   ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0)
Theorem	isconstr 33777*	Property of being a constructible number. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    ⇒   ⊢ (𝐴 ∈ Constr ↔ ∃𝑚 ∈ ω 𝐴 ∈ (𝐶‘𝑚))
Theorem	constr0 33778	The first step of the construction of constructible numbers is the pair {0, 1}. In this theorem and the following, we use (𝐶‘𝑁) for the 𝑁-th intermediate iteration of the constructible number. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    ⇒   ⊢ (𝐶‘∅) = {0, 1}
Theorem	constrsuc 33779*	Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    &   ⊢ 𝑆 = (𝐶‘𝑁)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐶‘suc 𝑁) ↔ (𝑋 ∈ ℂ ∧ (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 ∃𝑑 ∈ 𝑆 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 ∃𝑒 ∈ 𝑆 ∃𝑓 ∈ 𝑆 ∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 ∃𝑑 ∈ 𝑆 ∃𝑒 ∈ 𝑆 ∃𝑓 ∈ 𝑆 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))))
Theorem	constrlim 33780*	Limit step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ 𝑉)    &   ⊢ (𝜑 → Lim 𝑁)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) = ∪ 𝑛 ∈ 𝑁 (𝐶‘𝑛))
Theorem	constrsscn 33781*	Closure of the constructible points in the complex numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) ⊆ ℂ)
Theorem	constrsslem 33782*	Lemma for constrss 33784. This lemma requires the additional condition that 0 is the constructible number; that condition is removed in constrss 33784. (Proposed by Saveliy Skresanov, 23-JUn-2025.) (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    &   ⊢ (𝜑 → 0 ∈ (𝐶‘𝑁))    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (𝐶‘suc 𝑁))
Theorem	constr01 33783*	0 and 1 are in all steps of the construction of constructible points. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    ⇒   ⊢ (𝜑 → {0, 1} ⊆ (𝐶‘𝑁))
Theorem	constrss 33784*	Constructed points are in the next generation constructed points. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (𝐶‘suc 𝑁))
Theorem	constrmon 33785*	The construction of constructible numbers is monotonous, i.e. if the ordinal 𝑀 is less than the ordinal 𝑁, which is denoted by 𝑀 ∈ 𝑁, then the 𝑀-th step of the constructible numbers is included in the 𝑁-th step. (Contributed by Thierry Arnoux, 1-Jul-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    ⇒   ⊢ (𝜑 → (𝐶‘𝑀) ⊆ (𝐶‘𝑁))
Theorem	constrconj 33786*	If a point 𝑋 of the complex plane is constructible, so is its conjugate (∗‘𝑋). (Proposed by Saveliy Skresanov, 25-Jun-2025.) (Contributed by Thierry Arnoux, 1-Jul-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶‘𝑁))    ⇒   ⊢ (𝜑 → (∗‘𝑋) ∈ (𝐶‘𝑁))
Theorem	constrfin 33787*	Each step of the construction of constructible numbers is finite. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin)
Theorem	constrelextdg2 33788*	If the 𝑁-th step (𝐶‘𝑁) of the construction of constuctible numbers is included in a subfield 𝐹 of the complex numbers, then any element 𝑋 of the next step (𝐶‘suc 𝑁) is either in 𝐹 or in a quadratic extension of 𝐹. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ 𝐾 = (ℂfld ↾s 𝐹)    &   ⊢ 𝐿 = (ℂfld ↾s (ℂfld fldGen (𝐹 ∪ {𝑋})))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘ℂfld))    &   ⊢ (𝜑 → 𝑁 ∈ On)    &   ⊢ (𝜑 → (𝐶‘𝑁) ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐶‘suc 𝑁))    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2))
Theorem	constrextdg2lem 33789*	Lemma for constrextdg2 33790 (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ 𝐸 = (ℂfld ↾s 𝑒)    &   ⊢ 𝐹 = (ℂfld ↾s 𝑓)    &   ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑅 ∈ ( < Chain(SubDRing‘ℂfld)))    &   ⊢ (𝜑 → (𝑅‘0) = ℚ)    &   ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (lastS‘𝑅))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ ( < Chain(SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑁) ⊆ (lastS‘𝑣)))
Theorem	constrextdg2 33790*	Any step (𝐶‘𝑁) of the construction of constructible numbers is contained in the last field of a tower of quadratic field extensions starting with ℚ. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ 𝐸 = (ℂfld ↾s 𝑒)    &   ⊢ 𝐹 = (ℂfld ↾s 𝑓)    &   ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}    &   ⊢ (𝜑 → 𝑁 ∈ ω)    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ ( < Chain(SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣)))
21.3.12.1  Impossible constructions
Theorem	2sqr3minply 33791	The polynomial ((𝑋↑3) − 2) is the minimal polynomial for (2↑𝑐(1 / 3)) over ℚ, and its degree is 3. (Contributed by Thierry Arnoux, 14-Jun-2025.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ − = (-g‘𝑃)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑃 = (Poly1‘𝑄)    &   ⊢ 𝐾 = (algSc‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑄)    &   ⊢ 𝐷 = (deg1‘𝑄)    &   ⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2))    &   ⊢ 𝐴 = (2↑𝑐(1 / 3))    &   ⊢ 𝑀 = (ℂfld minPoly ℚ)    ⇒   ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)
21.3.13  Matrices
21.3.13.1  Submatrices
Syntax	csmat 33792	Syntax for a function generating submatrices.
class subMat1
Definition	df-smat 33793*	Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...𝑀) × (1...𝑁)) into a new index in ((1...(𝑀 − 1)) × (1...(𝑁 − 1))). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 22583. (Contributed by Thierry Arnoux, 18-Aug-2020.)
⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
Theorem	smatfval 33794*	Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)))
Theorem	smatrcl 33795	Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    ⇒   ⊢ (𝜑 → 𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))))
Theorem	smatlem 33796	Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋)    &   ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌)    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌))
Theorem	smattl 33797	Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽))
Theorem	smattr 33798	Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽))
Theorem	smatbl 33799	Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1)))
Theorem	smatbr 33800	Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1)))