Metamath Proof Explorer

Theorem cnfldfld

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

Ref Expression
Assertion cnfldfld 
|- CCfld e. Field

Proof

Step Hyp Ref Expression
1 cndrng 
 |-  CCfld e. DivRing
2 cncrng 
 |-  CCfld e. CRing
3 isfld 
 |-  ( CCfld e. Field <-> ( CCfld e. DivRing /\ CCfld e. CRing ) )
4 1 2 3 mpbir2an 
 |-  CCfld e. Field