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	extdg1b 33701	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 33702	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 33703	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 33704	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 33705	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 33706	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 33707*	Lemma for fldextrspunlsp 33708: 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 33708	Lemma for fldextrspunfld 33710. 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 33709	Lemma for fldextrspunfld 33710. 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 33710	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 33711	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 33712	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 33713	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 33714	Lemma for fldextrspundgdvds 33715. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0)
Theorem	fldextrspundgdvds 33715	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 33716*	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 33717	Integral subring of a ring.
class IntgRing
Definition	df-irng 33718*	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 33719*	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 33720*	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 33721	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 33723). (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆))
Theorem	irngssv 33722	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 33723	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 33724	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 33725*	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 }))
Theorem	extdgfialglem1 33726*	Lemma for extdgfialg 33728. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ 𝑍 = (0g‘𝐸)    &   ⊢ · = (.r‘𝐸)    &   ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))
Theorem	extdgfialglem2 33727*	Lemma for extdgfialg 33728. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ 𝑍 = (0g‘𝐸)    &   ⊢ · = (.r‘𝐸)    &   ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)    &   ⊢ (𝜑 → 𝐴 finSupp 𝑍)    &   ⊢ (𝜑 → (𝐸 Σg (𝐴 ∘f · 𝐺)) = 𝑍)    &   ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
Theorem	extdgfialg 33728	A finite field extension 𝐸 / 𝐹 is algebraic. Part of the proof of Proposition 1.1 of [Lang], p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐸 IntgRing 𝐹) = 𝐵)
21.3.11.2  Algebraic extensions
Syntax	calgext 33729	Syntax for the algebraic field extension relation.
class /AlgExt
Definition	df-algext 33730*	Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒))}
Theorem	bralgext 33731	Express the fact that a field extension 𝐸 / 𝐹 is algebraic. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸/AlgExt𝐹 ↔ (𝐸/FldExt𝐹 ∧ (𝐸 IntgRing 𝐶) = 𝐵)))
Theorem	finextalg 33732	A finite field extension is algebraic. Proposition 1.1 of [Lang], p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐸/FinExt𝐹)    ⇒   ⊢ (𝜑 → 𝐸/AlgExt𝐹)
21.3.11.3  Minimal polynomials
Syntax	cminply 33733	Extend class notation with the minimal polynomial builder function.
class minPoly
Definition	df-minply 33734*	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 33735*	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 33736*	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 33737*	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 33738*	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 33739*	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 33738, 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 33740*	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 33741*	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 33742	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 33743	The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 )
Theorem	minplyirredlem 33744	Lemma for minplyirred 33745. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    &   ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴))    &   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸))    &   ⊢ (𝜑 → 𝐺 ≠ 𝑍)    &   ⊢ (𝜑 → 𝐻 ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃))
Theorem	minplyirred 33745	A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃))
Theorem	irngnminplynz 33746	Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)
Theorem	minplym1p 33747	A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	minplynzm1p 33748	If a minimal polynomial is nonzero, then it is monic. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	minplyelirng 33749	If the minimial polynomial 𝐹 of an element 𝑋 of a field 𝑅 has nonnegative degree, then 𝑋 is integral. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (𝑅 minPoly 𝑆)    &   ⊢ 𝐷 = (deg1‘(𝑅 ↾s 𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑅 IntgRing 𝑆))
Theorem	irredminply 33750	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 33751	Lemma for algextdeg 33759. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
Theorem	algextdeglem2 33752*	Lemma for algextdeg 33759. 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 33753*	Lemma for algextdeg 33759. 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 33754*	Lemma for algextdeg 33759. By lmhmqusker 33389, the surjective module homomorphism 𝐺 described in algextdeglem2 33752 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 33755*	Lemma for algextdeg 33759. 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 33756*	Lemma for algextdeg 33759. By r1pquslmic 33578, 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 33757*	Lemma for algextdeg 33759. 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 33758*	Lemma for algextdeg 33759. 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 33759	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 𝐴. Part of Proposition 1.4 of [Lang], p. 225. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿[:]𝐾) = (𝐷‘(𝑀‘𝐴)))
21.3.11.4  Quadratic Field Extensions
Theorem	rtelextdg2lem 33760	Lemma for rtelextdg2 33761: 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 33761	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.5  Towers of quadratic extentions
Theorem	fldext2chn 33762*	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 (2sqr3nconstr 33815), and of angle trisection (cos9thpinconstr 33825)
Syntax	cconstr 33763	Extend class notation with the set of constructible points.
class Constr
Definition	df-constr 33764*	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. Definition 7.4. in [Stewart] p. 92 (Contributed by Saveliy Skresanov, 19-Jan-2025.)
⊢ Constr = ∪ (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) “ ω)
Theorem	constrrtll 33765	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 33766	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 33767	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 33768	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 33769	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 33770*	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 33771	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 33772*	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 33773*	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 33774*	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 33775*	Lemma for constrss 33777. This lemma requires the additional condition that 0 is a constructible number; that condition is removed in constrss 33777. (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 33776*	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 33777*	Constructed points are in the next generation constructed points. Lemma 7.3 of [Stewart] p. 91 (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝑁 ∈ On)    ⇒   ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (𝐶‘suc 𝑁))
Theorem	constrmon 33778*	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 33779*	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 33780*	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 33781*	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 33782*	Lemma for constrextdg2 33783 (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 33783*	Any step (𝐶‘𝑁) of the construction of constructible numbers is contained in the last field of a tower of quadratic field extensions starting with ℚ. See Theorem 7.11 of [Stewart] p. 97. (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‘𝑣)))
Theorem	constrext2chnlem 33784*	Lemma for constrext2chn 33793. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ 𝐸 = (ℂfld ↾s 𝑒)    &   ⊢ 𝐹 = (ℂfld ↾s 𝑓)    &   ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐿 = (ℂfld ↾s (ℂfld fldGen (ℚ ∪ {𝐴})))    &   ⊢ (𝜑 → 𝐴 ∈ Constr)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛))
Theorem	constrfiss 33785*	For any finite set 𝐴 of constructible numbers, there is a 𝑛 -th step (𝐶‘𝑛) containing all numbers in 𝐴. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝐴 ⊆ Constr)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ω 𝐴 ⊆ (𝐶‘𝑛))
Theorem	constrllcllem 33786*	Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐷 ∈ Constr)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → 𝑋 = (𝐺 + (𝑅 · (𝐷 − 𝐺))))    &   ⊢ (𝜑 → (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐺))) ≠ 0)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrlccllem 33787*	Constructible numbers are closed under line-circle intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐸 ∈ Constr)    &   ⊢ (𝜑 → 𝐹 ∈ Constr)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐺)) = (abs‘(𝐸 − 𝐹)))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrcccllem 33788*	Constructible numbers are closed under circle-circle intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})    &   ⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐷 ∈ Constr)    &   ⊢ (𝜑 → 𝐸 ∈ Constr)    &   ⊢ (𝜑 → 𝐹 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐷)    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐺)))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrcbvlem 33789*	Technical lemma for eliminating the hypothesis of constr0 33771 and co. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
Theorem	constrllcl 33790	Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐷 ∈ Constr)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → 𝑋 = (𝐺 + (𝑅 · (𝐷 − 𝐺))))    &   ⊢ (𝜑 → (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐺))) ≠ 0)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrlccl 33791	Constructible numbers are closed under line-circle intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐸 ∈ Constr)    &   ⊢ (𝜑 → 𝐹 ∈ Constr)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐺)) = (abs‘(𝐸 − 𝐹)))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrcccl 33792	Constructible numbers are closed under circle-circle intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐶 ∈ Constr)    &   ⊢ (𝜑 → 𝐷 ∈ Constr)    &   ⊢ (𝜑 → 𝐸 ∈ Constr)    &   ⊢ (𝜑 → 𝐹 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐷)    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶)))    &   ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹)))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrext2chn 33793*	If a constructible number generates some subfield 𝐿 of ℂ, then the degree of the extension of 𝐿 over ℚ is a power of two. Theorem 7.12 of [Stewart] p. 98. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐿 = (ℂfld ↾s 𝑆)    &   ⊢ 𝑆 = (ℂfld fldGen (ℚ ∪ {𝐴}))    &   ⊢ (𝜑 → 𝐴 ∈ Constr)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛))
Theorem	constrcn 33794	Constructible numbers are complex numbers. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ℂ)
Theorem	nn0constr 33795	Nonnegative integers are constructible. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝑁 ∈ Constr)
Theorem	constraddcl 33796	Constructive numbers are closed under complex addition. Item (1) of Theorem 7.10 of [Stewart] p. 96 (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑌 ∈ Constr)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ Constr)
Theorem	constrnegcl 33797	Constructible numbers are closed under additive inverse. Item (2) of Theorem 7.10 of [Stewart] p. 96 (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → -𝑋 ∈ Constr)
Theorem	zconstr 33798	Integers are constructible. (Contributed by Thierry Arnoux, 3-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrdircl 33799	Constructible numbers are closed under taking the point on the unit circle having the same argument. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋 / (abs‘𝑋)) ∈ Constr)
Theorem	iconstr 33800	The imaginary unit i is constructible. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ i ∈ Constr