Theorem recn 8276

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   RRcr 8142

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 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  mulrid  8287  recnd  8318  pnfnre  8331  mnfnre  8332  cnegexlem1  8464  cnegexlem2  8465  cnegexlem3  8466  cnegex  8467  renegcl  8550  resubcl  8553  negf1o  8672  mul02lem2  8678  ltaddneg  8715  ltaddnegr  8716  ltaddsub2  8728  leaddsub2  8730  leltadd  8738  ltaddpos  8743  ltaddpos2  8744  posdif  8746  lenegcon1  8757  lenegcon2  8758  addge01  8763  addge02  8764  leaddle0  8768  mullt0  8771  recexre  8869  msqge0  8907  mulge0  8910  aprcl  8937  recexap  8944  rerecapb  9134  ltm1  9137  prodgt02  9144  prodge02  9146  ltmul2  9147  lemul2  9148  lemul2a  9150  ltmulgt12  9156  lemulge12  9158  gt0div  9161  ge0div  9162  ltmuldiv2  9166  ltdivmul  9167  ltdivmul2  9169  ledivmul2  9171  lemuldiv2  9173  negiso  9246  cju  9252  nnge1  9277  halfpos  9486  lt2halves  9491  addltmul  9492  avgle1  9496  avgle2  9497  div4p1lem1div2  9509  nnrecl  9511  elznn0  9609  elznn  9610  nzadd  9647  zmulcl  9648  difgtsumgt  9664  elz2  9666  gtndiv  9691  zeo  9701  supminfex  9947  eqreznegel  9964  negm  9965  irradd  9996  irrmul  9997  divlt1lt  10075  divle1le  10076  xnegneg  10185  rexsub  10205  xnegid  10211  xaddcom  10213  xaddid1  10214  xnegdi  10220  xaddass  10221  xleaddadd  10239  divelunit  10354  fzonmapblen  10548  infssuzex  10615  expgt1  10963  mulexpzap  10965  leexp1a  10980  expubnd  10982  sqgt0ap  10994  lt2sq  10999  le2sq  11000  sqge0  11002  sumsqeq0  11004  bernneq  11047  bernneq2  11048  nn0ltexp2  11096  swrdccatin2  11446  swrdccat3blem  11456  crre  11567  crim  11568  reim0  11571  mulreap  11574  rere  11575  remul2  11583  redivap  11584  immul2  11590  imdivap  11591  cjre  11592  cjreim  11613  rennim  11712  sqrt0rlem  11713  resqrexlemover  11720  absreimsq  11777  absreim  11778  absnid  11783  leabs  11784  absre  11787  absresq  11788  sqabs  11792  ltabs  11797  absdiflt  11802  absdifle  11803  lenegsq  11805  abssuble0  11813  dfabsmax  11927  max0addsup  11929  negfi  11938  minclpr  11947  reefcl  12379  efgt0  12395  reeftlcl  12400  resinval  12426  recosval  12427  resin4p  12429  recos4p  12430  resincl  12431  recoscl  12432  retanclap  12433  efieq  12446  sinbnd  12463  cosbnd  12464  absefi  12480  odd2np1  12584  remetdval  15538  bl2ioo  15541  ioo2bl  15542  hoverb  15639  plyreres  15755  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  relogoprlem  15859  logcxp  15888  rpcxpcl  15894  cxpcom  15929  rprelogbdiv  15948  gausslemma2dlem1a  16057  triap  16939  trirec0  16954