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 = ( CCfld |`s K )
Assertion	cncdrg	|- ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> K e. { RR , CC } )

Proof

Step	Hyp	Ref	Expression
1		resscdrg.1	|- F = ( CCfld |`s K )
2		simp1	|- ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> K e. ( SubRing ` CCfld ) )
3	1	resscdrg	|- ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> RR C_ K )
4		cnsubrg	|- ( ( K e. ( SubRing ` CCfld ) /\ RR C_ K ) -> K e. { RR , CC } )
5	2 3 4	syl2anc	|- ( ( K e. ( SubRing ` CCfld ) /\ F e. DivRing /\ F e. CMetSp ) -> K e. { RR , CC } )