Theorem recni 8154

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 8087	. 2 |- RR C_ CC
2		recni.1	. 2 |- A e. RR
3	1, 2	sselii 3221	1 |- A e. CC

Syntax hints:   e. wcel 2200   CCcc 7993   RRcr 7994

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8087

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  resubcli  8405  ltapii  8778  nncni  9116  2cn  9177  3cn  9181  4cn  9184  5cn  9186  6cn  9188  7cn  9190  8cn  9192  9cn  9194  halfcn  9321  8th4div3  9326  nn0cni  9377  numltc  9599  sqge0i  10843  lt2sqi  10844  le2sqi  10845  sq11i  10846  sqrtmsq2i  11641  0.999...  12027  ef01bndlem  12262  sin4lt0  12273  eirraplem  12283  eirr  12285  egt2lt3  12286  sqrt2irraplemnn  12696  modsubi  12937  picn  15455  sinhalfpilem  15459  cosneghalfpi  15466  sinhalfpip  15488  sinhalfpim  15489  coshalfpip  15490  coshalfpim  15491  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  cosq23lt0  15501  coseq00topi  15503  sincosq1eq  15507  sincos4thpi  15508  tan4thpi  15509  sincos6thpi  15510  2logb9irrALT  15642  taupi  16400