Theorem recn 8312

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   RRcr 8178

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  mulrid  8323  recnd  8354  pnfnre  8367  mnfnre  8368  cnegexlem1  8502  cnegexlem2  8503  cnegexlem3  8504  cnegex  8505  renegcl  8588  resubcl  8591  negf1o  8710  mul02lem2  8716  ltaddneg  8753  ltaddnegr  8754  ltaddsub2  8766  leaddsub2  8768  leltadd  8776  ltaddpos  8781  ltaddpos2  8782  posdif  8784  lenegcon1  8795  lenegcon2  8796  addge01  8801  addge02  8802  leaddle0  8806  mullt0  8809  recexre  8908  msqge0  8946  mulge0  8949  aprcl  8976  recexap  8983  rerecapb  9175  ltm1  9178  prodgt02  9185  prodge02  9187  ltmul2  9188  lemul2  9189  lemul2a  9191  ltmulgt12  9197  lemulge12  9199  gt0div  9202  ge0div  9203  ltmuldiv2  9207  ltdivmul  9208  ltdivmul2  9210  ledivmul2  9212  lemuldiv2  9214  negiso  9287  cju  9293  nnge1  9329  halfpos  9540  lt2halves  9545  addltmul  9546  avgle1  9550  avgle2  9551  div4p1lem1div2  9563  nnrecl  9565  elznn0  9663  elznn  9664  nzadd  9701  zmulcl  9702  difgtsumgt  9718  elz2  9720  gtndiv  9745  zeo  9755  supminfex  10006  eqreznegel  10023  negm  10024  irradd  10055  irrmul  10057  divlt1lt  10135  divle1le  10136  xnegneg  10245  rexsub  10265  xnegid  10271  xaddcom  10273  xaddid1  10274  xnegdi  10280  xaddass  10281  xleaddadd  10299  divelunit  10414  fzonmapblen  10609  infssuzex  10676  expgt1  11027  mulexpzap  11029  leexp1a  11044  expubnd  11046  sqgt0ap  11058  lt2sq  11063  le2sq  11064  sqge0  11066  sumsqeq0  11068  bernneq  11111  bernneq2  11112  nn0ltexp2  11161  swrdccatin2  11515  swrdccat3blem  11525  crre  11636  crim  11637  reim0  11640  mulreap  11643  rere  11644  remul2  11652  redivap  11653  immul2  11659  imdivap  11660  cjre  11661  cjreim  11683  rennim  11782  sqrt0rlem  11783  resqrexlemover  11790  absreimsq  11847  absreim  11848  absnid  11853  leabs  11854  absre  11858  absresq  11859  sqabs  11863  ltabs  11868  absdiflt  11873  absdifle  11874  lenegsq  11876  abssuble0  11884  dfabsmax  11998  max0addsup  12000  negfi  12009  minclpr  12018  reefcl  12451  efgt0  12467  reeftlcl  12472  resinval  12498  recosval  12499  resin4p  12501  recos4p  12502  resincl  12503  recoscl  12504  retanclap  12505  efieq  12518  sinbnd  12535  cosbnd  12536  absefi  12552  odd2np1  12656  remetdval  15697  bl2ioo  15700  ioo2bl  15701  hoverb  15798  plyreres  15914  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  relogoprlem  16020  logcxp  16052  rpcxpcl  16058  cxpcom  16093  rprelogbdiv  16112  gausslemma2dlem1a  16275  triap  17176  trirec0  17191