Theorem recni 8084

Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)

Hypothesis

Ref	Expression
recni.1	|- A e. RR

Assertion

Ref	Expression
recni	|- A e. CC

Proof of Theorem recni

Step	Hyp	Ref	Expression
1		ax-resscn 8017	. 2 |- RR C_ CC
2		recni.1	. 2 |- A e. RR
3	1, 2	sselii 3190	1 |- A e. CC

Syntax hints:   e. wcel 2176   CCcc 7923   RRcr 7924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  resubcli  8335  ltapii  8708  nncni  9046  2cn  9107  3cn  9111  4cn  9114  5cn  9116  6cn  9118  7cn  9120  8cn  9122  9cn  9124  halfcn  9251  8th4div3  9256  nn0cni  9307  numltc  9529  sqge0i  10771  lt2sqi  10772  le2sqi  10773  sq11i  10774  sqrtmsq2i  11446  0.999...  11832  ef01bndlem  12067  sin4lt0  12078  eirraplem  12088  eirr  12090  egt2lt3  12091  sqrt2irraplemnn  12501  modsubi  12742  picn  15259  sinhalfpilem  15263  cosneghalfpi  15270  sinhalfpip  15292  sinhalfpim  15293  coshalfpip  15294  coshalfpim  15295  sincosq1sgn  15298  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  cosq23lt0  15305  coseq00topi  15307  sincosq1eq  15311  sincos4thpi  15312  tan4thpi  15313  sincos6thpi  15314  2logb9irrALT  15446  taupi  16012