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 \in SubRing (ℂ_{fld}) \land F \in DivRing \land F \in CMetSp) \to K \in \{ℝ, ℂ\}$

Step	Hyp	Ref	Expression
1		resscdrg.1	$⊢ F = ℂ_{fld} ↾_{𝑠} K$
2		simp1	$⊢ (K \in SubRing (ℂ_{fld}) \land F \in DivRing \land F \in CMetSp) \to K \in SubRing (ℂ_{fld})$
3	1	resscdrg	$⊢ (K \in SubRing (ℂ_{fld}) \land F \in DivRing \land F \in CMetSp) \to ℝ \subseteq K$
4		cnsubrg	$⊢ (K \in SubRing (ℂ_{fld}) \land ℝ \subseteq K) \to K \in \{ℝ, ℂ\}$
5	2 3 4	syl2anc	$⊢ (K \in SubRing (ℂ_{fld}) \land F \in DivRing \land F \in CMetSp) \to K \in \{ℝ, ℂ\}$