Theorem recn 8260

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

Syntax hints:   -> wi 4   e. wcel 2203   CCcc 8125   RRcr 8126

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 2214  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  mulrid  8271  recnd  8302  pnfnre  8315  mnfnre  8316  cnegexlem1  8448  cnegexlem2  8449  cnegexlem3  8450  cnegex  8451  renegcl  8534  resubcl  8537  negf1o  8655  mul02lem2  8661  ltaddneg  8698  ltaddnegr  8699  ltaddsub2  8711  leaddsub2  8713  leltadd  8721  ltaddpos  8726  ltaddpos2  8727  posdif  8729  lenegcon1  8740  lenegcon2  8741  addge01  8746  addge02  8747  leaddle0  8751  mullt0  8754  recexre  8852  msqge0  8890  mulge0  8893  aprcl  8920  recexap  8927  rerecapb  9117  ltm1  9120  prodgt02  9127  prodge02  9129  ltmul2  9130  lemul2  9131  lemul2a  9133  ltmulgt12  9139  lemulge12  9141  gt0div  9144  ge0div  9145  ltmuldiv2  9149  ltdivmul  9150  ltdivmul2  9152  ledivmul2  9154  lemuldiv2  9156  negiso  9229  cju  9235  nnge1  9260  halfpos  9469  lt2halves  9474  addltmul  9475  avgle1  9479  avgle2  9480  div4p1lem1div2  9492  nnrecl  9494  elznn0  9592  elznn  9593  nzadd  9630  zmulcl  9631  difgtsumgt  9647  elz2  9649  gtndiv  9673  zeo  9683  supminfex  9929  eqreznegel  9946  negm  9947  irradd  9978  irrmul  9979  divlt1lt  10057  divle1le  10058  xnegneg  10166  rexsub  10186  xnegid  10192  xaddcom  10194  xaddid1  10195  xnegdi  10201  xaddass  10202  xleaddadd  10220  divelunit  10335  fzonmapblen  10526  infssuzex  10593  expgt1  10939  mulexpzap  10941  leexp1a  10956  expubnd  10958  sqgt0ap  10970  lt2sq  10975  le2sq  10976  sqge0  10978  sumsqeq0  10980  bernneq  11022  bernneq2  11023  nn0ltexp2  11071  swrdccatin2  11421  swrdccat3blem  11431  crre  11542  crim  11543  reim0  11546  mulreap  11549  rere  11550  remul2  11558  redivap  11559  immul2  11565  imdivap  11566  cjre  11567  cjreim  11588  rennim  11687  sqrt0rlem  11688  resqrexlemover  11695  absreimsq  11752  absreim  11753  absnid  11758  leabs  11759  absre  11762  absresq  11763  sqabs  11767  ltabs  11772  absdiflt  11777  absdifle  11778  lenegsq  11780  abssuble0  11788  dfabsmax  11902  max0addsup  11904  negfi  11913  minclpr  11922  reefcl  12354  efgt0  12370  reeftlcl  12375  resinval  12401  recosval  12402  resin4p  12404  recos4p  12405  resincl  12406  recoscl  12407  retanclap  12408  efieq  12421  sinbnd  12438  cosbnd  12439  absefi  12455  odd2np1  12559  remetdval  15412  bl2ioo  15415  ioo2bl  15416  hoverb  15513  plyreres  15629  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  relogoprlem  15733  logcxp  15762  rpcxpcl  15768  cxpcom  15803  rprelogbdiv  15822  gausslemma2dlem1a  15931  triap  16813  trirec0  16828