Metamath Proof Explorer

Theorem constrfld

Description: The constructible numbers form a field. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Assertion constrfld ⊢ ℂ fld ↾ 𝑠 Constr ∈ Field

Proof

Step Hyp Ref Expression
1 cnfldfld ⊢ ℂ fld ∈ Field
2 constrsdrg ⊢ Constr ∈ SubDRing ⁡ ℂ fld
3 fldsdrgfld ⊢ ℂ fld ∈ Field ∧ Constr ∈ SubDRing ⁡ ℂ fld → ℂ fld ↾ 𝑠 Constr ∈ Field
4 1 2 3 mp2an ⊢ ℂ fld ↾ 𝑠 Constr ∈ Field