Theorem recn 7538

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

Syntax hints:   -> wi 4   e. wcel 1439   CCcc 7411   RRcr 7412

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-resscn 7500

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3008  df-ss 3015

This theorem is referenced by:  mulid1  7548  recnd  7579  pnfnre  7592  mnfnre  7593  cnegexlem1  7720  cnegexlem2  7721  cnegexlem3  7722  cnegex  7723  renegcl  7806  resubcl  7809  negf1o  7923  mul02lem2  7929  ltaddneg  7965  ltaddnegr  7966  ltaddsub2  7978  leaddsub2  7980  leltadd  7988  ltaddpos  7993  ltaddpos2  7994  posdif  7996  lenegcon1  8007  lenegcon2  8008  addge01  8013  addge02  8014  leaddle0  8018  mullt0  8021  recexre  8118  msqge0  8156  mulge0  8159  recexap  8185  ltm1  8370  prodgt02  8377  prodge02  8379  ltmul2  8380  lemul2  8381  lemul2a  8383  ltmulgt12  8389  lemulge12  8391  gt0div  8394  ge0div  8395  ltmuldiv2  8399  ltdivmul  8400  ltdivmul2  8402  ledivmul2  8404  lemuldiv2  8406  negiso  8479  cju  8484  nnge1  8508  halfpos  8710  lt2halves  8714  addltmul  8715  avgle1  8719  avgle2  8720  div4p1lem1div2  8732  nnrecl  8734  elznn0  8828  elznn  8829  nzadd  8865  zmulcl  8866  elz2  8881  gtndiv  8904  zeo  8914  supminfex  9148  eqreznegel  9162  negm  9163  irradd  9194  irrmul  9195  divlt1lt  9264  divle1le  9265  xnegneg  9358  divelunit  9482  fzonmapblen  9661  expgt1  10056  mulexpzap  10058  leexp1a  10073  expubnd  10075  sqgt0ap  10086  lt2sq  10091  le2sq  10092  sqge0  10094  sumsqeq0  10096  bernneq  10137  bernneq2  10138  crre  10354  crim  10355  reim0  10358  mulreap  10361  rere  10362  remul2  10370  redivap  10371  immul2  10377  imdivap  10378  cjre  10379  cjreim  10400  rennim  10498  sqrt0rlem  10499  resqrexlemover  10506  absreimsq  10563  absreim  10564  absnid  10569  leabs  10570  absre  10573  absresq  10574  sqabs  10578  ltabs  10583  absdiflt  10588  absdifle  10589  lenegsq  10591  abssuble0  10599  dfabsmax  10713  max0addsup  10715  negfi  10722  reefcl  11021  efgt0  11037  reeftlcl  11042  resinval  11069  recosval  11070  resin4p  11072  recos4p  11073  resincl  11074  recoscl  11075  retanclap  11076  efieq  11089  sinbnd  11106  cosbnd  11107  absefi  11121  odd2np1  11214  infssuzex  11286