Description: The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | recld2.1 | |- J = ( TopOpen ` CCfld ) |
|
| Assertion | reperf | |- ( J |`t RR ) e. Perf |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | recld2.1 | |- J = ( TopOpen ` CCfld ) |
|
| 2 | readdcl | |- ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR ) |
|
| 3 | ax-resscn | |- RR C_ CC |
|
| 4 | 1 2 3 | reperflem | |- ( J |`t RR ) e. Perf |