Theorem recn 7907

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

Syntax hints:   -> wi 4   e. wcel 2141   CCcc 7772   RRcr 7773

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7866

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  mulid1  7917  recnd  7948  pnfnre  7961  mnfnre  7962  cnegexlem1  8094  cnegexlem2  8095  cnegexlem3  8096  cnegex  8097  renegcl  8180  resubcl  8183  negf1o  8301  mul02lem2  8307  ltaddneg  8343  ltaddnegr  8344  ltaddsub2  8356  leaddsub2  8358  leltadd  8366  ltaddpos  8371  ltaddpos2  8372  posdif  8374  lenegcon1  8385  lenegcon2  8386  addge01  8391  addge02  8392  leaddle0  8396  mullt0  8399  recexre  8497  msqge0  8535  mulge0  8538  aprcl  8565  recexap  8571  ltm1  8762  prodgt02  8769  prodge02  8771  ltmul2  8772  lemul2  8773  lemul2a  8775  ltmulgt12  8781  lemulge12  8783  gt0div  8786  ge0div  8787  ltmuldiv2  8791  ltdivmul  8792  ltdivmul2  8794  ledivmul2  8796  lemuldiv2  8798  negiso  8871  cju  8877  nnge1  8901  halfpos  9109  lt2halves  9113  addltmul  9114  avgle1  9118  avgle2  9119  div4p1lem1div2  9131  nnrecl  9133  elznn0  9227  elznn  9228  nzadd  9264  zmulcl  9265  difgtsumgt  9281  elz2  9283  gtndiv  9307  zeo  9317  supminfex  9556  eqreznegel  9573  negm  9574  irradd  9605  irrmul  9606  divlt1lt  9681  divle1le  9682  xnegneg  9790  rexsub  9810  xnegid  9816  xaddcom  9818  xaddid1  9819  xnegdi  9825  xaddass  9826  xleaddadd  9844  divelunit  9959  fzonmapblen  10143  expgt1  10514  mulexpzap  10516  leexp1a  10531  expubnd  10533  sqgt0ap  10544  lt2sq  10549  le2sq  10550  sqge0  10552  sumsqeq0  10554  bernneq  10596  bernneq2  10597  nn0ltexp2  10644  crre  10821  crim  10822  reim0  10825  mulreap  10828  rere  10829  remul2  10837  redivap  10838  immul2  10844  imdivap  10845  cjre  10846  cjreim  10867  rennim  10966  sqrt0rlem  10967  resqrexlemover  10974  absreimsq  11031  absreim  11032  absnid  11037  leabs  11038  absre  11041  absresq  11042  sqabs  11046  ltabs  11051  absdiflt  11056  absdifle  11057  lenegsq  11059  abssuble0  11067  dfabsmax  11181  max0addsup  11183  negfi  11191  minclpr  11200  reefcl  11631  efgt0  11647  reeftlcl  11652  resinval  11678  recosval  11679  resin4p  11681  recos4p  11682  resincl  11683  recoscl  11684  retanclap  11685  efieq  11698  sinbnd  11715  cosbnd  11716  absefi  11731  odd2np1  11832  infssuzex  11904  remetdval  13333  bl2ioo  13336  ioo2bl  13337  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  relogoprlem  13583  logcxp  13612  rpcxpcl  13618  cxpcom  13651  rprelogbdiv  13669  triap  14061  trirec0  14076