Theorem recn 7848

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

Syntax hints:   -> wi 4   e. wcel 2128   CCcc 7713   RRcr 7714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-resscn 7807

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  mulid1  7858  recnd  7889  pnfnre  7902  mnfnre  7903  cnegexlem1  8033  cnegexlem2  8034  cnegexlem3  8035  cnegex  8036  renegcl  8119  resubcl  8122  negf1o  8240  mul02lem2  8246  ltaddneg  8282  ltaddnegr  8283  ltaddsub2  8295  leaddsub2  8297  leltadd  8305  ltaddpos  8310  ltaddpos2  8311  posdif  8313  lenegcon1  8324  lenegcon2  8325  addge01  8330  addge02  8331  leaddle0  8335  mullt0  8338  recexre  8436  msqge0  8474  mulge0  8477  aprcl  8504  recexap  8510  ltm1  8700  prodgt02  8707  prodge02  8709  ltmul2  8710  lemul2  8711  lemul2a  8713  ltmulgt12  8719  lemulge12  8721  gt0div  8724  ge0div  8725  ltmuldiv2  8729  ltdivmul  8730  ltdivmul2  8732  ledivmul2  8734  lemuldiv2  8736  negiso  8809  cju  8815  nnge1  8839  halfpos  9047  lt2halves  9051  addltmul  9052  avgle1  9056  avgle2  9057  div4p1lem1div2  9069  nnrecl  9071  elznn0  9165  elznn  9166  nzadd  9202  zmulcl  9203  elz2  9218  gtndiv  9242  zeo  9252  supminfex  9491  eqreznegel  9505  negm  9506  irradd  9537  irrmul  9538  divlt1lt  9613  divle1le  9614  xnegneg  9719  rexsub  9739  xnegid  9745  xaddcom  9747  xaddid1  9748  xnegdi  9754  xaddass  9755  xleaddadd  9773  divelunit  9888  fzonmapblen  10068  expgt1  10439  mulexpzap  10441  leexp1a  10456  expubnd  10458  sqgt0ap  10469  lt2sq  10474  le2sq  10475  sqge0  10477  sumsqeq0  10479  bernneq  10520  bernneq2  10521  crre  10739  crim  10740  reim0  10743  mulreap  10746  rere  10747  remul2  10755  redivap  10756  immul2  10762  imdivap  10763  cjre  10764  cjreim  10785  rennim  10884  sqrt0rlem  10885  resqrexlemover  10892  absreimsq  10949  absreim  10950  absnid  10955  leabs  10956  absre  10959  absresq  10960  sqabs  10964  ltabs  10969  absdiflt  10974  absdifle  10975  lenegsq  10977  abssuble0  10985  dfabsmax  11099  max0addsup  11101  negfi  11109  minclpr  11118  reefcl  11547  efgt0  11563  reeftlcl  11568  resinval  11594  recosval  11595  resin4p  11597  recos4p  11598  resincl  11599  recoscl  11600  retanclap  11601  efieq  11614  sinbnd  11631  cosbnd  11632  absefi  11647  odd2np1  11745  infssuzex  11817  remetdval  12899  bl2ioo  12902  ioo2bl  12903  sincosq1sgn  13107  sincosq2sgn  13108  sincosq3sgn  13109  sincosq4sgn  13110  sinq12gt0  13111  relogoprlem  13149  logcxp  13178  rpcxpcl  13184  cxpcom  13217  rprelogbdiv  13234  triap  13563  trirec0  13578