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	ply1annig1p 33701*	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 33702*	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 33701, 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 33703*	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 33704*	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 33705	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 33706	The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 )
Theorem	minplyirredlem 33707	Lemma for minplyirred 33708. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    &   ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴))    &   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸))    &   ⊢ (𝜑 → 𝐺 ≠ 𝑍)    &   ⊢ (𝜑 → 𝐻 ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃))
Theorem	minplyirred 33708	A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃))
Theorem	irngnminplynz 33709	Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)
Theorem	minplym1p 33710	A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	minplynzm1p 33711	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 33712	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 33713	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 33714	Lemma for algextdeg 33722. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
Theorem	algextdeglem2 33715*	Lemma for algextdeg 33722. 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 33716*	Lemma for algextdeg 33722. 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 33717*	Lemma for algextdeg 33722. By lmhmqusker 33395, the surjective module homomorphism 𝐺 described in algextdeglem2 33715 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 33718*	Lemma for algextdeg 33722. 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 33719*	Lemma for algextdeg 33722. By r1pquslmic 33583, 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 33720*	Lemma for algextdeg 33722. 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 33721*	Lemma for algextdeg 33722. 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 33722	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.4  Quadratic Field Extensions
Theorem	rtelextdg2lem 33723	Lemma for rtelextdg2 33724: 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 33724	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 33725*	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 33778), and of angle trisection (cos9thpinconstr 33788)
Syntax	cconstr 33726	Extend class notation with the set of constructible points.
class Constr
Definition	df-constr 33727*	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 33728	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 33729	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 33730	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 33731	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 33732	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 33733*	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 33734	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 33735*	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 33736*	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 33737*	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 33738*	Lemma for constrss 33740. This lemma requires the additional condition that 0 is a constructible number; that condition is removed in constrss 33740. (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 33739*	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 33740*	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 33741*	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 33742*	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 33743*	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 33744*	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 33745*	Lemma for constrextdg2 33746 (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 33746*	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 33747*	Lemma for constrext2chn 33756. (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 33748*	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 33749*	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 33750*	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 33751*	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 33752*	Technical lemma for eliminating the hypothesis of constr0 33734 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 33753	Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐷 ∈ Constr)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → 𝑋 = (𝐺 + (𝑅 · (𝐷 − 𝐺))))    &   ⊢ (𝜑 → (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐺))) ≠ 0)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrlccl 33754	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 33755	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 33756*	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 33757	Constructible numbers are complex numbers. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ℂ)
Theorem	nn0constr 33758	Nonnegative integers are constructible. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝑁 ∈ Constr)
Theorem	constraddcl 33759	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 33760	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 33761	Integers are constructible. (Contributed by Thierry Arnoux, 3-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrdircl 33762	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 33763	The imaginary unit i is constructible. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ i ∈ Constr
Theorem	constrremulcl 33764	If two real numbers 𝑋 and 𝑌 are constructible, then, so is their product. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑌 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ Constr)
Theorem	constrcjcl 33765	Constructible numbers are closed under complex conjugate. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (∗‘𝑋) ∈ Constr)
Theorem	constrrecl 33766	Constructible numbers are closed under taking the real part. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (ℜ‘𝑋) ∈ Constr)
Theorem	constrimcl 33767	Constructible numbers are closed under taking the imaginary part. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (ℑ‘𝑋) ∈ Constr)
Theorem	constrmulcl 33768	Constructible numbers are closed under complex multiplication. Item (3) of Theorem 7.10 of [Stewart] p. 96 (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑌 ∈ Constr)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ Constr)
Theorem	constrreinvcl 33769	If a real number 𝑋 is constructible, then, so is its inverse. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → (1 / 𝑋) ∈ Constr)
Theorem	constrinvcl 33770	Constructible numbers are closed under complex inverse. Item (4) of Theorem 7.10 of [Stewart] p. 96 (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / 𝑋) ∈ Constr)
Theorem	constrcon 33771*	Contradiction of constructibility: If a complex number 𝐴 has minimal polynomial 𝐹 over ℚ of a degree that is not a power of 2, then 𝐴 is not constructible. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐷 = (deg1‘(ℂfld ↾s ℚ))    &   ⊢ 𝑀 = (ℂfld minPoly ℚ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 = (𝑀‘𝐴))    &   ⊢ (𝜑 → (𝐷‘𝐹) ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐷‘𝐹) ≠ (2↑𝑛))    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ Constr)
Theorem	constrsdrg 33772	Constructible numbers form a subfield of the complex numbers. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ Constr ∈ (SubDRing‘ℂfld)
Theorem	constrfld 33773	The constructible numbers form a field. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (ℂfld ↾s Constr) ∈ Field
Theorem	constrresqrtcl 33774	If a positive real number 𝑋 is constructible, then, so is its square root. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝑋)    ⇒   ⊢ (𝜑 → (√‘𝑋) ∈ Constr)
Theorem	constrabscl 33775	Constructible numbers are closed under absolute value (modulus). (Contributed by Thierry Arnoux, 6-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (abs‘𝑋) ∈ Constr)
Theorem	constrsqrtcl 33776	Constructible numbers are closed under taking the square root. This is not generally the case for the cubic root operation, see 2sqr3nconstr 33778. Item (5) of Theorem 7.10 of [Stewart] p. 96 (Proposed by Saveliy Skresanov, 3-Nov-2025.) (Contributed by Thierry Arnoux, 6-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (√‘𝑋) ∈ Constr)
21.3.12.1  Impossible constructions
Theorem	2sqr3minply 33777	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)
Theorem	2sqr3nconstr 33778	Doubling the cube is an impossible construction, i.e. the cube root of 2 is not constructible with straightedge and compass. Given a cube of edge of length one, a cube of double volume would have an edge of length (2↑𝑐(1 / 3)), however that number is not constructible. This is the first part of Metamath 100 proof #8. Theorem 7.13 of [Stewart] p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 26-Oct-2025.)
⊢ (2↑𝑐(1 / 3)) ∉ Constr
Theorem	cos9thpiminplylem1 33779	The polynomial ((𝑋↑3) + ((-3 · (𝑋↑2)) + 1)) has no integer roots. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝑋↑3) + ((-3 · (𝑋↑2)) + 1)) ≠ 0)
Theorem	cos9thpiminplylem2 33780	The polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)) has no rational roots. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℚ)    ⇒   ⊢ (𝜑 → ((𝑋↑3) + ((-3 · 𝑋) + 1)) ≠ 0)
Theorem	cos9thpiminplylem3 33781	Lemma for cos9thpiminply 33785. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    ⇒   ⊢ ((𝑂↑2) + (𝑂 + 1)) = 0
Theorem	cos9thpiminplylem4 33782	Lemma for cos9thpiminply 33785. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    ⇒   ⊢ ((𝑍↑6) + (𝑍↑3)) = -1
Theorem	cos9thpiminplylem5 33783	The constructed complex number 𝐴 is a root of the polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)). (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    &   ⊢ 𝐴 = (𝑍 + (1 / 𝑍))    ⇒   ⊢ ((𝐴↑3) + ((-3 · 𝐴) + 1)) = 0
Theorem	cos9thpiminplylem6 33784	Evaluation of the polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)). (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    &   ⊢ 𝐴 = (𝑍 + (1 / 𝑍))    &   ⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑃 = (Poly1‘𝑄)    &   ⊢ 𝐾 = (algSc‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑄)    &   ⊢ 𝐷 = (deg1‘𝑄)    &   ⊢ 𝐹 = ((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1)))    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝑌) = ((𝑌↑3) + ((-3 · 𝑌) + 1)))
Theorem	cos9thpiminply 33785	The polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)) is the minimal polynomial for 𝐴 over ℚ, and its degree is 3. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    &   ⊢ 𝐴 = (𝑍 + (1 / 𝑍))    &   ⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ 𝑃 = (Poly1‘𝑄)    &   ⊢ 𝐾 = (algSc‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑄)    &   ⊢ 𝐷 = (deg1‘𝑄)    &   ⊢ 𝐹 = ((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1)))    &   ⊢ 𝑀 = (ℂfld minPoly ℚ)    ⇒   ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)
Theorem	cos9thpinconstrlem1 33786	The complex number 𝑂, representing an angle of (2 · π) / 3, is constructible. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    ⇒   ⊢ 𝑂 ∈ Constr
Theorem	cos9thpinconstrlem2 33787	The complex number 𝐴 is not constructible. (Contributed by Thierry Arnoux, 15-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    &   ⊢ 𝐴 = (𝑍 + (1 / 𝑍))    ⇒   ⊢ ¬ 𝐴 ∈ Constr
Theorem	cos9thpinconstr 33788	Trisecting an angle is an impossible construction. Given for example 𝑂 = (exp‘((i · (2 · π)) / 3)), which represents an angle of ((2 · π) / 3), the cube root of 𝑂 is not constructible with straightedge and compass, while 𝑂 itself is constructible. This is the second part of Metamath 100 proof #8. Theorem 7.14 of [Stewart] p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 15-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    ⇒   ⊢ (𝑂 ∈ Constr ∧ 𝑍 ∉ Constr)
Theorem	trisecnconstr 33789	Not all angles can be trisected. (Contributed by Thierry Arnoux, 15-Nov-2025.)
⊢ ¬ ∀𝑜 ∈ Constr (𝑜↑𝑐(1 / 3)) ∈ Constr
21.3.13  Matrices
21.3.13.1  Submatrices
Syntax	csmat 33790	Syntax for a function generating submatrices.
class subMat1
Definition	df-smat 33791*	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 22471. (Contributed by Thierry Arnoux, 18-Aug-2020.)
⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
Theorem	smatfval 33792*	Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)))
Theorem	smatrcl 33793	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 33794	Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋)    &   ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌)    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌))
Theorem	smattl 33795	Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽))
Theorem	smattr 33796	Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽))
Theorem	smatbl 33797	Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1)))
Theorem	smatbr 33798	Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1)))
Theorem	smatcl 33799	Closure of the square submatrix: if 𝑀 is a square matrix of dimension 𝑁 with indices in (1...𝑁), then a submatrix of 𝑀 is of dimension (𝑁 − 1). (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐶 = (Base‘((1...(𝑁 − 1)) Mat 𝑅))    &   ⊢ 𝑆 = (𝐾(subMat1‘𝑀)𝐿)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐶)
Theorem	matmpo 33800*	Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗)))