Theorem recn 7882

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

Syntax hints:   -> wi 4   e. wcel 2136   CCcc 7747   RRcr 7748

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3121  df-ss 3128

This theorem is referenced by:  mulid1  7892  recnd  7923  pnfnre  7936  mnfnre  7937  cnegexlem1  8069  cnegexlem2  8070  cnegexlem3  8071  cnegex  8072  renegcl  8155  resubcl  8158  negf1o  8276  mul02lem2  8282  ltaddneg  8318  ltaddnegr  8319  ltaddsub2  8331  leaddsub2  8333  leltadd  8341  ltaddpos  8346  ltaddpos2  8347  posdif  8349  lenegcon1  8360  lenegcon2  8361  addge01  8366  addge02  8367  leaddle0  8371  mullt0  8374  recexre  8472  msqge0  8510  mulge0  8513  aprcl  8540  recexap  8546  ltm1  8737  prodgt02  8744  prodge02  8746  ltmul2  8747  lemul2  8748  lemul2a  8750  ltmulgt12  8756  lemulge12  8758  gt0div  8761  ge0div  8762  ltmuldiv2  8766  ltdivmul  8767  ltdivmul2  8769  ledivmul2  8771  lemuldiv2  8773  negiso  8846  cju  8852  nnge1  8876  halfpos  9084  lt2halves  9088  addltmul  9089  avgle1  9093  avgle2  9094  div4p1lem1div2  9106  nnrecl  9108  elznn0  9202  elznn  9203  nzadd  9239  zmulcl  9240  difgtsumgt  9256  elz2  9258  gtndiv  9282  zeo  9292  supminfex  9531  eqreznegel  9548  negm  9549  irradd  9580  irrmul  9581  divlt1lt  9656  divle1le  9657  xnegneg  9765  rexsub  9785  xnegid  9791  xaddcom  9793  xaddid1  9794  xnegdi  9800  xaddass  9801  xleaddadd  9819  divelunit  9934  fzonmapblen  10118  expgt1  10489  mulexpzap  10491  leexp1a  10506  expubnd  10508  sqgt0ap  10519  lt2sq  10524  le2sq  10525  sqge0  10527  sumsqeq0  10529  bernneq  10571  bernneq2  10572  nn0ltexp2  10619  crre  10795  crim  10796  reim0  10799  mulreap  10802  rere  10803  remul2  10811  redivap  10812  immul2  10818  imdivap  10819  cjre  10820  cjreim  10841  rennim  10940  sqrt0rlem  10941  resqrexlemover  10948  absreimsq  11005  absreim  11006  absnid  11011  leabs  11012  absre  11015  absresq  11016  sqabs  11020  ltabs  11025  absdiflt  11030  absdifle  11031  lenegsq  11033  abssuble0  11041  dfabsmax  11155  max0addsup  11157  negfi  11165  minclpr  11174  reefcl  11605  efgt0  11621  reeftlcl  11626  resinval  11652  recosval  11653  resin4p  11655  recos4p  11656  resincl  11657  recoscl  11658  retanclap  11659  efieq  11672  sinbnd  11689  cosbnd  11690  absefi  11705  odd2np1  11806  infssuzex  11878  remetdval  13139  bl2ioo  13142  ioo2bl  13143  sincosq1sgn  13347  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  relogoprlem  13389  logcxp  13418  rpcxpcl  13424  cxpcom  13457  rprelogbdiv  13475  triap  13868  trirec0  13883