Theorem recn 8277

Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)

Assertion

Ref	Expression
recn	|- ( A e. RR -> A e. CC )

Proof of Theorem recn

Step	Hyp	Ref	Expression
1		ax-resscn 8236	. 2 |- RR C_ CC
2	1	sseli 3238	1 |- ( A e. RR -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8142   RRcr 8143

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8236

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  mulrid  8288  recnd  8319  pnfnre  8332  mnfnre  8333  cnegexlem1  8466  cnegexlem2  8467  cnegexlem3  8468  cnegex  8469  renegcl  8552  resubcl  8555  negf1o  8674  mul02lem2  8680  ltaddneg  8717  ltaddnegr  8718  ltaddsub2  8730  leaddsub2  8732  leltadd  8740  ltaddpos  8745  ltaddpos2  8746  posdif  8748  lenegcon1  8759  lenegcon2  8760  addge01  8765  addge02  8766  leaddle0  8770  mullt0  8773  recexre  8871  msqge0  8909  mulge0  8912  aprcl  8939  recexap  8946  rerecapb  9138  ltm1  9141  prodgt02  9148  prodge02  9150  ltmul2  9151  lemul2  9152  lemul2a  9154  ltmulgt12  9160  lemulge12  9162  gt0div  9165  ge0div  9166  ltmuldiv2  9170  ltdivmul  9171  ltdivmul2  9173  ledivmul2  9175  lemuldiv2  9177  negiso  9250  cju  9256  nnge1  9281  halfpos  9490  lt2halves  9495  addltmul  9496  avgle1  9500  avgle2  9501  div4p1lem1div2  9513  nnrecl  9515  elznn0  9613  elznn  9614  nzadd  9651  zmulcl  9652  difgtsumgt  9668  elz2  9670  gtndiv  9695  zeo  9705  supminfex  9951  eqreznegel  9968  negm  9969  irradd  10000  irrmul  10001  divlt1lt  10079  divle1le  10080  xnegneg  10189  rexsub  10209  xnegid  10215  xaddcom  10217  xaddid1  10218  xnegdi  10224  xaddass  10225  xleaddadd  10243  divelunit  10358  fzonmapblen  10552  infssuzex  10619  expgt1  10967  mulexpzap  10969  leexp1a  10984  expubnd  10986  sqgt0ap  10998  lt2sq  11003  le2sq  11004  sqge0  11006  sumsqeq0  11008  bernneq  11051  bernneq2  11052  nn0ltexp2  11100  swrdccatin2  11450  swrdccat3blem  11460  crre  11571  crim  11572  reim0  11575  mulreap  11578  rere  11579  remul2  11587  redivap  11588  immul2  11594  imdivap  11595  cjre  11596  cjreim  11618  rennim  11717  sqrt0rlem  11718  resqrexlemover  11725  absreimsq  11782  absreim  11783  absnid  11788  leabs  11789  absre  11792  absresq  11793  sqabs  11797  ltabs  11802  absdiflt  11807  absdifle  11808  lenegsq  11810  abssuble0  11818  dfabsmax  11932  max0addsup  11934  negfi  11943  minclpr  11952  reefcl  12384  efgt0  12400  reeftlcl  12405  resinval  12431  recosval  12432  resin4p  12434  recos4p  12435  resincl  12436  recoscl  12437  retanclap  12438  efieq  12451  sinbnd  12468  cosbnd  12469  absefi  12485  odd2np1  12589  remetdval  15543  bl2ioo  15546  ioo2bl  15547  hoverb  15644  plyreres  15760  sincosq1sgn  15822  sincosq2sgn  15823  sincosq3sgn  15824  sincosq4sgn  15825  sinq12gt0  15826  relogoprlem  15864  logcxp  15893  rpcxpcl  15899  cxpcom  15934  rprelogbdiv  15953  gausslemma2dlem1a  16062  triap  16954  trirec0  16969