Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | recn | $${\u22a2}{A}\in \mathbb{R}\to {A}\in \u2102$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn | $${\u22a2}\mathbb{R}\subseteq \u2102$$ | |
2 | 1 | sseli | $${\u22a2}{A}\in \mathbb{R}\to {A}\in \u2102$$ |