Theorem recn 8005

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

Syntax hints:   -> wi 4   e. wcel 2164   CCcc 7870   RRcr 7871

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  mulrid  8016  recnd  8048  pnfnre  8061  mnfnre  8062  cnegexlem1  8194  cnegexlem2  8195  cnegexlem3  8196  cnegex  8197  renegcl  8280  resubcl  8283  negf1o  8401  mul02lem2  8407  ltaddneg  8443  ltaddnegr  8444  ltaddsub2  8456  leaddsub2  8458  leltadd  8466  ltaddpos  8471  ltaddpos2  8472  posdif  8474  lenegcon1  8485  lenegcon2  8486  addge01  8491  addge02  8492  leaddle0  8496  mullt0  8499  recexre  8597  msqge0  8635  mulge0  8638  aprcl  8665  recexap  8672  rerecapb  8862  ltm1  8865  prodgt02  8872  prodge02  8874  ltmul2  8875  lemul2  8876  lemul2a  8878  ltmulgt12  8884  lemulge12  8886  gt0div  8889  ge0div  8890  ltmuldiv2  8894  ltdivmul  8895  ltdivmul2  8897  ledivmul2  8899  lemuldiv2  8901  negiso  8974  cju  8980  nnge1  9005  halfpos  9213  lt2halves  9218  addltmul  9219  avgle1  9223  avgle2  9224  div4p1lem1div2  9236  nnrecl  9238  elznn0  9332  elznn  9333  nzadd  9369  zmulcl  9370  difgtsumgt  9386  elz2  9388  gtndiv  9412  zeo  9422  supminfex  9662  eqreznegel  9679  negm  9680  irradd  9711  irrmul  9712  divlt1lt  9790  divle1le  9791  xnegneg  9899  rexsub  9919  xnegid  9925  xaddcom  9927  xaddid1  9928  xnegdi  9934  xaddass  9935  xleaddadd  9953  divelunit  10068  fzonmapblen  10254  expgt1  10648  mulexpzap  10650  leexp1a  10665  expubnd  10667  sqgt0ap  10679  lt2sq  10684  le2sq  10685  sqge0  10687  sumsqeq0  10689  bernneq  10731  bernneq2  10732  nn0ltexp2  10780  crre  11001  crim  11002  reim0  11005  mulreap  11008  rere  11009  remul2  11017  redivap  11018  immul2  11024  imdivap  11025  cjre  11026  cjreim  11047  rennim  11146  sqrt0rlem  11147  resqrexlemover  11154  absreimsq  11211  absreim  11212  absnid  11217  leabs  11218  absre  11221  absresq  11222  sqabs  11226  ltabs  11231  absdiflt  11236  absdifle  11237  lenegsq  11239  abssuble0  11247  dfabsmax  11361  max0addsup  11363  negfi  11371  minclpr  11380  reefcl  11811  efgt0  11827  reeftlcl  11832  resinval  11858  recosval  11859  resin4p  11861  recos4p  11862  resincl  11863  recoscl  11864  retanclap  11865  efieq  11878  sinbnd  11895  cosbnd  11896  absefi  11912  odd2np1  12014  infssuzex  12086  remetdval  14707  bl2ioo  14710  ioo2bl  14711  hoverb  14802  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  relogoprlem  15003  logcxp  15032  rpcxpcl  15038  cxpcom  15071  rprelogbdiv  15089  gausslemma2dlem1a  15174  triap  15519  trirec0  15534