Metamath Proof Explorer


Theorem cncdrg

Description: The only complete subfields of the complex numbers are RR and CC . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis resscdrg.1 F = fld 𝑠 K
Assertion cncdrg K SubRing fld F DivRing F CMetSp K

Proof

Step Hyp Ref Expression
1 resscdrg.1 F = fld 𝑠 K
2 simp1 K SubRing fld F DivRing F CMetSp K SubRing fld
3 1 resscdrg K SubRing fld F DivRing F CMetSp K
4 cnsubrg K SubRing fld K K
5 2 3 4 syl2anc K SubRing fld F DivRing F CMetSp K