Metamath Proof Explorer

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