Theorem recn 8302

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

Syntax hints:   -> wi 4   e. wcel 2209   CCcc 8167   RRcr 8168

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8261

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  mulrid  8313  recnd  8344  pnfnre  8357  mnfnre  8358  cnegexlem1  8491  cnegexlem2  8492  cnegexlem3  8493  cnegex  8494  renegcl  8577  resubcl  8580  negf1o  8699  mul02lem2  8705  ltaddneg  8742  ltaddnegr  8743  ltaddsub2  8755  leaddsub2  8757  leltadd  8765  ltaddpos  8770  ltaddpos2  8771  posdif  8773  lenegcon1  8784  lenegcon2  8785  addge01  8790  addge02  8791  leaddle0  8795  mullt0  8798  recexre  8896  msqge0  8934  mulge0  8937  aprcl  8964  recexap  8971  rerecapb  9163  ltm1  9166  prodgt02  9173  prodge02  9175  ltmul2  9176  lemul2  9177  lemul2a  9179  ltmulgt12  9185  lemulge12  9187  gt0div  9190  ge0div  9191  ltmuldiv2  9195  ltdivmul  9196  ltdivmul2  9198  ledivmul2  9200  lemuldiv2  9202  negiso  9275  cju  9281  nnge1  9306  halfpos  9515  lt2halves  9520  addltmul  9521  avgle1  9525  avgle2  9526  div4p1lem1div2  9538  nnrecl  9540  elznn0  9638  elznn  9639  nzadd  9676  zmulcl  9677  difgtsumgt  9693  elz2  9695  gtndiv  9720  zeo  9730  supminfex  9976  eqreznegel  9993  negm  9994  irradd  10025  irrmul  10026  divlt1lt  10104  divle1le  10105  xnegneg  10214  rexsub  10234  xnegid  10240  xaddcom  10242  xaddid1  10243  xnegdi  10249  xaddass  10250  xleaddadd  10268  divelunit  10383  fzonmapblen  10577  infssuzex  10644  expgt1  10992  mulexpzap  10994  leexp1a  11009  expubnd  11011  sqgt0ap  11023  lt2sq  11028  le2sq  11029  sqge0  11031  sumsqeq0  11033  bernneq  11076  bernneq2  11077  nn0ltexp2  11125  swrdccatin2  11479  swrdccat3blem  11489  crre  11600  crim  11601  reim0  11604  mulreap  11607  rere  11608  remul2  11616  redivap  11617  immul2  11623  imdivap  11624  cjre  11625  cjreim  11647  rennim  11746  sqrt0rlem  11747  resqrexlemover  11754  absreimsq  11811  absreim  11812  absnid  11817  leabs  11818  absre  11821  absresq  11822  sqabs  11826  ltabs  11831  absdiflt  11836  absdifle  11837  lenegsq  11839  abssuble0  11847  dfabsmax  11961  max0addsup  11963  negfi  11972  minclpr  11981  reefcl  12413  efgt0  12429  reeftlcl  12434  resinval  12460  recosval  12461  resin4p  12463  recos4p  12464  resincl  12465  recoscl  12466  retanclap  12467  efieq  12480  sinbnd  12497  cosbnd  12498  absefi  12514  odd2np1  12618  remetdval  15571  bl2ioo  15574  ioo2bl  15575  hoverb  15672  plyreres  15788  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  relogoprlem  15892  logcxp  15922  rpcxpcl  15928  cxpcom  15963  rprelogbdiv  15982  gausslemma2dlem1a  16091  triap  16983  trirec0  16998