Theorem recn 8164

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8029   RRcr 8030

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  mulrid  8175  recnd  8207  pnfnre  8220  mnfnre  8221  cnegexlem1  8353  cnegexlem2  8354  cnegexlem3  8355  cnegex  8356  renegcl  8439  resubcl  8442  negf1o  8560  mul02lem2  8566  ltaddneg  8603  ltaddnegr  8604  ltaddsub2  8616  leaddsub2  8618  leltadd  8626  ltaddpos  8631  ltaddpos2  8632  posdif  8634  lenegcon1  8645  lenegcon2  8646  addge01  8651  addge02  8652  leaddle0  8656  mullt0  8659  recexre  8757  msqge0  8795  mulge0  8798  aprcl  8825  recexap  8832  rerecapb  9022  ltm1  9025  prodgt02  9032  prodge02  9034  ltmul2  9035  lemul2  9036  lemul2a  9038  ltmulgt12  9044  lemulge12  9046  gt0div  9049  ge0div  9050  ltmuldiv2  9054  ltdivmul  9055  ltdivmul2  9057  ledivmul2  9059  lemuldiv2  9061  negiso  9134  cju  9140  nnge1  9165  halfpos  9374  lt2halves  9379  addltmul  9380  avgle1  9384  avgle2  9385  div4p1lem1div2  9397  nnrecl  9399  elznn0  9493  elznn  9494  nzadd  9531  zmulcl  9532  difgtsumgt  9548  elz2  9550  gtndiv  9574  zeo  9584  supminfex  9830  eqreznegel  9847  negm  9848  irradd  9879  irrmul  9880  divlt1lt  9958  divle1le  9959  xnegneg  10067  rexsub  10087  xnegid  10093  xaddcom  10095  xaddid1  10096  xnegdi  10102  xaddass  10103  xleaddadd  10121  divelunit  10236  fzonmapblen  10425  infssuzex  10492  expgt1  10838  mulexpzap  10840  leexp1a  10855  expubnd  10857  sqgt0ap  10869  lt2sq  10874  le2sq  10875  sqge0  10877  sumsqeq0  10879  bernneq  10921  bernneq2  10922  nn0ltexp2  10970  swrdccatin2  11309  swrdccat3blem  11319  crre  11417  crim  11418  reim0  11421  mulreap  11424  rere  11425  remul2  11433  redivap  11434  immul2  11440  imdivap  11441  cjre  11442  cjreim  11463  rennim  11562  sqrt0rlem  11563  resqrexlemover  11570  absreimsq  11627  absreim  11628  absnid  11633  leabs  11634  absre  11637  absresq  11638  sqabs  11642  ltabs  11647  absdiflt  11652  absdifle  11653  lenegsq  11655  abssuble0  11663  dfabsmax  11777  max0addsup  11779  negfi  11788  minclpr  11797  reefcl  12228  efgt0  12244  reeftlcl  12249  resinval  12275  recosval  12276  resin4p  12278  recos4p  12279  resincl  12280  recoscl  12281  retanclap  12282  efieq  12295  sinbnd  12312  cosbnd  12313  absefi  12329  odd2np1  12433  remetdval  15270  bl2ioo  15273  ioo2bl  15274  hoverb  15371  plyreres  15487  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  relogoprlem  15591  logcxp  15620  rpcxpcl  15626  cxpcom  15661  rprelogbdiv  15680  gausslemma2dlem1a  15786  triap  16633  trirec0  16648