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 | ||
Assertion | cncdrg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resscdrg.1 | ||
2 | simp1 | ||
3 | 1 | resscdrg | |
4 | cnsubrg | ||
5 | 2 3 4 | syl2anc |