Theorem constrfld

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

	Ref	Expression
Assertion	constrfld	⊢ ( ℂfld ↾s Constr ) ∈ Field

Proof

Step	Hyp	Ref	Expression
1		cnfldfld	⊢ ℂfld ∈ Field
2		constrsdrg	⊢ Constr ∈ ( SubDRing ‘ ℂfld )
3		fldsdrgfld	⊢ ( ( ℂfld ∈ Field ∧ Constr ∈ ( SubDRing ‘ ℂfld ) ) → ( ℂfld ↾s Constr ) ∈ Field )
4	1 2 3	mp2an	⊢ ( ℂfld ↾s Constr ) ∈ Field