Theorem recn 8128

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7993   RRcr 7994

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8087

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  mulrid  8139  recnd  8171  pnfnre  8184  mnfnre  8185  cnegexlem1  8317  cnegexlem2  8318  cnegexlem3  8319  cnegex  8320  renegcl  8403  resubcl  8406  negf1o  8524  mul02lem2  8530  ltaddneg  8567  ltaddnegr  8568  ltaddsub2  8580  leaddsub2  8582  leltadd  8590  ltaddpos  8595  ltaddpos2  8596  posdif  8598  lenegcon1  8609  lenegcon2  8610  addge01  8615  addge02  8616  leaddle0  8620  mullt0  8623  recexre  8721  msqge0  8759  mulge0  8762  aprcl  8789  recexap  8796  rerecapb  8986  ltm1  8989  prodgt02  8996  prodge02  8998  ltmul2  8999  lemul2  9000  lemul2a  9002  ltmulgt12  9008  lemulge12  9010  gt0div  9013  ge0div  9014  ltmuldiv2  9018  ltdivmul  9019  ltdivmul2  9021  ledivmul2  9023  lemuldiv2  9025  negiso  9098  cju  9104  nnge1  9129  halfpos  9338  lt2halves  9343  addltmul  9344  avgle1  9348  avgle2  9349  div4p1lem1div2  9361  nnrecl  9363  elznn0  9457  elznn  9458  nzadd  9495  zmulcl  9496  difgtsumgt  9512  elz2  9514  gtndiv  9538  zeo  9548  supminfex  9788  eqreznegel  9805  negm  9806  irradd  9837  irrmul  9838  divlt1lt  9916  divle1le  9917  xnegneg  10025  rexsub  10045  xnegid  10051  xaddcom  10053  xaddid1  10054  xnegdi  10060  xaddass  10061  xleaddadd  10079  divelunit  10194  fzonmapblen  10383  infssuzex  10448  expgt1  10794  mulexpzap  10796  leexp1a  10811  expubnd  10813  sqgt0ap  10825  lt2sq  10830  le2sq  10831  sqge0  10833  sumsqeq0  10835  bernneq  10877  bernneq2  10878  nn0ltexp2  10926  swrdccatin2  11256  swrdccat3blem  11266  crre  11363  crim  11364  reim0  11367  mulreap  11370  rere  11371  remul2  11379  redivap  11380  immul2  11386  imdivap  11387  cjre  11388  cjreim  11409  rennim  11508  sqrt0rlem  11509  resqrexlemover  11516  absreimsq  11573  absreim  11574  absnid  11579  leabs  11580  absre  11583  absresq  11584  sqabs  11588  ltabs  11593  absdiflt  11598  absdifle  11599  lenegsq  11601  abssuble0  11609  dfabsmax  11723  max0addsup  11725  negfi  11734  minclpr  11743  reefcl  12174  efgt0  12190  reeftlcl  12195  resinval  12221  recosval  12222  resin4p  12224  recos4p  12225  resincl  12226  recoscl  12227  retanclap  12228  efieq  12241  sinbnd  12258  cosbnd  12259  absefi  12275  odd2np1  12379  remetdval  15215  bl2ioo  15218  ioo2bl  15219  hoverb  15316  plyreres  15432  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  relogoprlem  15536  logcxp  15565  rpcxpcl  15571  cxpcom  15606  rprelogbdiv  15625  gausslemma2dlem1a  15731  triap  16356  trirec0  16371