Theorem recn 8208

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 8167	. 2 |- RR C_ CC
2	1	sseli 3224	1 |- ( A e. RR -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8073   RRcr 8074

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 2213  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  mulrid  8219  recnd  8250  pnfnre  8263  mnfnre  8264  cnegexlem1  8396  cnegexlem2  8397  cnegexlem3  8398  cnegex  8399  renegcl  8482  resubcl  8485  negf1o  8603  mul02lem2  8609  ltaddneg  8646  ltaddnegr  8647  ltaddsub2  8659  leaddsub2  8661  leltadd  8669  ltaddpos  8674  ltaddpos2  8675  posdif  8677  lenegcon1  8688  lenegcon2  8689  addge01  8694  addge02  8695  leaddle0  8699  mullt0  8702  recexre  8800  msqge0  8838  mulge0  8841  aprcl  8868  recexap  8875  rerecapb  9065  ltm1  9068  prodgt02  9075  prodge02  9077  ltmul2  9078  lemul2  9079  lemul2a  9081  ltmulgt12  9087  lemulge12  9089  gt0div  9092  ge0div  9093  ltmuldiv2  9097  ltdivmul  9098  ltdivmul2  9100  ledivmul2  9102  lemuldiv2  9104  negiso  9177  cju  9183  nnge1  9208  halfpos  9417  lt2halves  9422  addltmul  9423  avgle1  9427  avgle2  9428  div4p1lem1div2  9440  nnrecl  9442  elznn0  9538  elznn  9539  nzadd  9576  zmulcl  9577  difgtsumgt  9593  elz2  9595  gtndiv  9619  zeo  9629  supminfex  9875  eqreznegel  9892  negm  9893  irradd  9924  irrmul  9925  divlt1lt  10003  divle1le  10004  xnegneg  10112  rexsub  10132  xnegid  10138  xaddcom  10140  xaddid1  10141  xnegdi  10147  xaddass  10148  xleaddadd  10166  divelunit  10281  fzonmapblen  10472  infssuzex  10539  expgt1  10885  mulexpzap  10887  leexp1a  10902  expubnd  10904  sqgt0ap  10916  lt2sq  10921  le2sq  10922  sqge0  10924  sumsqeq0  10926  bernneq  10968  bernneq2  10969  nn0ltexp2  11017  swrdccatin2  11359  swrdccat3blem  11369  crre  11480  crim  11481  reim0  11484  mulreap  11487  rere  11488  remul2  11496  redivap  11497  immul2  11503  imdivap  11504  cjre  11505  cjreim  11526  rennim  11625  sqrt0rlem  11626  resqrexlemover  11633  absreimsq  11690  absreim  11691  absnid  11696  leabs  11697  absre  11700  absresq  11701  sqabs  11705  ltabs  11710  absdiflt  11715  absdifle  11716  lenegsq  11718  abssuble0  11726  dfabsmax  11840  max0addsup  11842  negfi  11851  minclpr  11860  reefcl  12292  efgt0  12308  reeftlcl  12313  resinval  12339  recosval  12340  resin4p  12342  recos4p  12343  resincl  12344  recoscl  12345  retanclap  12346  efieq  12359  sinbnd  12376  cosbnd  12377  absefi  12393  odd2np1  12497  remetdval  15341  bl2ioo  15344  ioo2bl  15345  hoverb  15442  plyreres  15558  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  relogoprlem  15662  logcxp  15691  rpcxpcl  15697  cxpcom  15732  rprelogbdiv  15751  gausslemma2dlem1a  15860  triap  16744  trirec0  16759