Metamath Proof Explorer

Theorem constrfld

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

Ref Expression
Assertion constrfld 
|- ( CCfld |`s Constr ) e. Field

Proof

Step Hyp Ref Expression
1 cnfldfld 
 |-  CCfld e. Field
2 constrsdrg 
 |-  Constr e. ( SubDRing ` CCfld )
3 fldsdrgfld 
 |-  ( ( CCfld e. Field /\ Constr e. ( SubDRing ` CCfld ) ) -> ( CCfld |`s Constr ) e. Field )
4 1 2 3 mp2an 
 |-  ( CCfld |`s Constr ) e. Field