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	minplyirred 33701	A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃))
Theorem	irngnminplynz 33702	Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)
Theorem	minplym1p 33703	A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	minplynzm1p 33704	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 33705	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 33706	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 33707	Lemma for algextdeg 33715. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
Theorem	algextdeglem2 33708*	Lemma for algextdeg 33715. 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 33709*	Lemma for algextdeg 33715. 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 33710*	Lemma for algextdeg 33715. By lmhmqusker 33388, the surjective module homomorphism 𝐺 described in algextdeglem2 33708 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 33711*	Lemma for algextdeg 33715. 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 33712*	Lemma for algextdeg 33715. By r1pquslmic 33576, 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 33713*	Lemma for algextdeg 33715. 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 33714*	Lemma for algextdeg 33715. 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 33715	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 33716	Lemma for rtelextdg2 33717: 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 33717	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 33718*	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 33771), and of angle trisection (cos9thpinconstr 33781)
Syntax	cconstr 33719	Extend class notation with the set of constructible points.
class Constr
Definition	df-constr 33720*	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 33721	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 33722	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 33723	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 33724	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 33725	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 33726*	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 33727	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 33728*	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 33729*	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 33730*	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 33731*	Lemma for constrss 33733. This lemma requires the additional condition that 0 is a constructible number; that condition is removed in constrss 33733. (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 33732*	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 33733*	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 33734*	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 33735*	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 33736*	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 33737*	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 33738*	Lemma for constrextdg2 33739 (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 33739*	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 33740*	Lemma for constrext2chn 33749. (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 33741*	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 33742*	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 33743*	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 33744*	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 33745*	Technical lemma for eliminating the hypothesis of constr0 33727 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 33746	Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ Constr)    &   ⊢ (𝜑 → 𝐵 ∈ Constr)    &   ⊢ (𝜑 → 𝐺 ∈ Constr)    &   ⊢ (𝜑 → 𝐷 ∈ Constr)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴))))    &   ⊢ (𝜑 → 𝑋 = (𝐺 + (𝑅 · (𝐷 − 𝐺))))    &   ⊢ (𝜑 → (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐺))) ≠ 0)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrlccl 33747	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 33748	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 33749*	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 33750	Constructible numbers are complex numbers. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → 𝑋 ∈ ℂ)
Theorem	nn0constr 33751	Nonnegative integers are constructible. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝑁 ∈ Constr)
Theorem	constraddcl 33752	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 33753	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 33754	Integers are constructible. (Contributed by Thierry Arnoux, 3-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑋 ∈ Constr)
Theorem	constrdircl 33755	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 33756	The imaginary unit i is constructible. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ i ∈ Constr
Theorem	constrremulcl 33757	If two real numbers 𝑋 and 𝑌 are constructible, then, so is their product. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑌 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ Constr)
Theorem	constrcjcl 33758	Constructible numbers are closed under complex conjugate. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (∗‘𝑋) ∈ Constr)
Theorem	constrrecl 33759	Constructible numbers are closed under taking the real part. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (ℜ‘𝑋) ∈ Constr)
Theorem	constrimcl 33760	Constructible numbers are closed under taking the imaginary part. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (ℑ‘𝑋) ∈ Constr)
Theorem	constrmulcl 33761	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 33762	If a real number 𝑋 is constructible, then, so is its inverse. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → (1 / 𝑋) ∈ Constr)
Theorem	constrinvcl 33763	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 33764*	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 33765	Constructible numbers form a subfield of the complex numbers. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ Constr ∈ (SubDRing‘ℂfld)
Theorem	constrfld 33766	The constructible numbers form a field. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (ℂfld ↾s Constr) ∈ Field
Theorem	constrresqrtcl 33767	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 33768	Constructible numbers are closed under absolute value (modulus). (Contributed by Thierry Arnoux, 6-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ Constr)    ⇒   ⊢ (𝜑 → (abs‘𝑋) ∈ Constr)
Theorem	constrsqrtcl 33769	Constructible numbers are closed under taking the square root. This is not generally the case for the cubic root operation, see 2sqr3nconstr 33771. 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 33770	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 33771	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 33772	The polynomial ((𝑋↑3) + ((-3 · (𝑋↑2)) + 1)) has no integer roots. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝑋↑3) + ((-3 · (𝑋↑2)) + 1)) ≠ 0)
Theorem	cos9thpiminplylem2 33773	The polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)) has no rational roots. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝑋 ∈ ℚ)    ⇒   ⊢ (𝜑 → ((𝑋↑3) + ((-3 · 𝑋) + 1)) ≠ 0)
Theorem	cos9thpiminplylem3 33774	Lemma for cos9thpiminply 33778. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    ⇒   ⊢ ((𝑂↑2) + (𝑂 + 1)) = 0
Theorem	cos9thpiminplylem4 33775	Lemma for cos9thpiminply 33778. (Contributed by Thierry Arnoux, 14-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    ⇒   ⊢ ((𝑍↑6) + (𝑍↑3)) = -1
Theorem	cos9thpiminplylem5 33776	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 33777	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 33778	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 33779	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 33780	The complex number 𝐴 is not constructible. (Contributed by Thierry Arnoux, 15-Nov-2025.)
⊢ 𝑂 = (exp‘((i · (2 · π)) / 3))    &   ⊢ 𝑍 = (𝑂↑𝑐(1 / 3))    &   ⊢ 𝐴 = (𝑍 + (1 / 𝑍))    ⇒   ⊢ ¬ 𝐴 ∈ Constr
Theorem	cos9thpinconstr 33781	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 33782	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 33783	Syntax for a function generating submatrices.
class subMat1
Definition	df-smat 33784*	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 22464. (Contributed by Thierry Arnoux, 18-Aug-2020.)
⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
Theorem	smatfval 33785*	Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)))
Theorem	smatrcl 33786	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 33787	Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋)    &   ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌)    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌))
Theorem	smattl 33788	Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽))
Theorem	smattr 33789	Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽))
Theorem	smatbl 33790	Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1)))
Theorem	smatbr 33791	Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1)))
Theorem	smatcl 33792	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 33793*	Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗)))
Theorem	1smat1 33794	The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 22470. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 1 = (1r‘((1...𝑁) Mat 𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅)))
Theorem	submat1n 33795	One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁))
Theorem	submatres 33796	Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑀 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))))
Theorem	submateqlem1 33797	Lemma for submateq 33799. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾})))
Theorem	submateqlem2 33798	Lemma for submateq 33799. (Contributed by Thierry Arnoux, 26-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 < 𝐾)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾})))
Theorem	submateq 33799*	Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗))    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽))
Theorem	submatminr1 33800	If we take a submatrix by removing the row 𝐼 and column 𝐽, then the result is the same on the matrix with row 𝐼 and column 𝐽 modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ 𝐸 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝐸)𝐽))