Theorem recn 8155

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8020   RRcr 8021

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 8114

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 3204  df-ss 3211

This theorem is referenced by:  mulrid  8166  recnd  8198  pnfnre  8211  mnfnre  8212  cnegexlem1  8344  cnegexlem2  8345  cnegexlem3  8346  cnegex  8347  renegcl  8430  resubcl  8433  negf1o  8551  mul02lem2  8557  ltaddneg  8594  ltaddnegr  8595  ltaddsub2  8607  leaddsub2  8609  leltadd  8617  ltaddpos  8622  ltaddpos2  8623  posdif  8625  lenegcon1  8636  lenegcon2  8637  addge01  8642  addge02  8643  leaddle0  8647  mullt0  8650  recexre  8748  msqge0  8786  mulge0  8789  aprcl  8816  recexap  8823  rerecapb  9013  ltm1  9016  prodgt02  9023  prodge02  9025  ltmul2  9026  lemul2  9027  lemul2a  9029  ltmulgt12  9035  lemulge12  9037  gt0div  9040  ge0div  9041  ltmuldiv2  9045  ltdivmul  9046  ltdivmul2  9048  ledivmul2  9050  lemuldiv2  9052  negiso  9125  cju  9131  nnge1  9156  halfpos  9365  lt2halves  9370  addltmul  9371  avgle1  9375  avgle2  9376  div4p1lem1div2  9388  nnrecl  9390  elznn0  9484  elznn  9485  nzadd  9522  zmulcl  9523  difgtsumgt  9539  elz2  9541  gtndiv  9565  zeo  9575  supminfex  9821  eqreznegel  9838  negm  9839  irradd  9870  irrmul  9871  divlt1lt  9949  divle1le  9950  xnegneg  10058  rexsub  10078  xnegid  10084  xaddcom  10086  xaddid1  10087  xnegdi  10093  xaddass  10094  xleaddadd  10112  divelunit  10227  fzonmapblen  10416  infssuzex  10483  expgt1  10829  mulexpzap  10831  leexp1a  10846  expubnd  10848  sqgt0ap  10860  lt2sq  10865  le2sq  10866  sqge0  10868  sumsqeq0  10870  bernneq  10912  bernneq2  10913  nn0ltexp2  10961  swrdccatin2  11300  swrdccat3blem  11310  crre  11408  crim  11409  reim0  11412  mulreap  11415  rere  11416  remul2  11424  redivap  11425  immul2  11431  imdivap  11432  cjre  11433  cjreim  11454  rennim  11553  sqrt0rlem  11554  resqrexlemover  11561  absreimsq  11618  absreim  11619  absnid  11624  leabs  11625  absre  11628  absresq  11629  sqabs  11633  ltabs  11638  absdiflt  11643  absdifle  11644  lenegsq  11646  abssuble0  11654  dfabsmax  11768  max0addsup  11770  negfi  11779  minclpr  11788  reefcl  12219  efgt0  12235  reeftlcl  12240  resinval  12266  recosval  12267  resin4p  12269  recos4p  12270  resincl  12271  recoscl  12272  retanclap  12273  efieq  12286  sinbnd  12303  cosbnd  12304  absefi  12320  odd2np1  12424  remetdval  15261  bl2ioo  15264  ioo2bl  15265  hoverb  15362  plyreres  15478  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  relogoprlem  15582  logcxp  15611  rpcxpcl  15617  cxpcom  15652  rprelogbdiv  15671  gausslemma2dlem1a  15777  triap  16569  trirec0  16584