Theorem cnfldfld

Description: The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Assertion	cnfldfld	⊢ ℂfld ∈ Field

Proof

Step	Hyp	Ref	Expression
1		cndrng	⊢ ℂfld ∈ DivRing
2		cncrng	⊢ ℂfld ∈ CRing
3		isfld	⊢ ( ℂfld ∈ Field ↔ ( ℂfld ∈ DivRing ∧ ℂfld ∈ CRing ) )
4	1 2 3	mpbir2an	⊢ ℂfld ∈ Field