Theorem recn 8132

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   RRcr 7998

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 8091

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 3203  df-ss 3210

This theorem is referenced by:  mulrid  8143  recnd  8175  pnfnre  8188  mnfnre  8189  cnegexlem1  8321  cnegexlem2  8322  cnegexlem3  8323  cnegex  8324  renegcl  8407  resubcl  8410  negf1o  8528  mul02lem2  8534  ltaddneg  8571  ltaddnegr  8572  ltaddsub2  8584  leaddsub2  8586  leltadd  8594  ltaddpos  8599  ltaddpos2  8600  posdif  8602  lenegcon1  8613  lenegcon2  8614  addge01  8619  addge02  8620  leaddle0  8624  mullt0  8627  recexre  8725  msqge0  8763  mulge0  8766  aprcl  8793  recexap  8800  rerecapb  8990  ltm1  8993  prodgt02  9000  prodge02  9002  ltmul2  9003  lemul2  9004  lemul2a  9006  ltmulgt12  9012  lemulge12  9014  gt0div  9017  ge0div  9018  ltmuldiv2  9022  ltdivmul  9023  ltdivmul2  9025  ledivmul2  9027  lemuldiv2  9029  negiso  9102  cju  9108  nnge1  9133  halfpos  9342  lt2halves  9347  addltmul  9348  avgle1  9352  avgle2  9353  div4p1lem1div2  9365  nnrecl  9367  elznn0  9461  elznn  9462  nzadd  9499  zmulcl  9500  difgtsumgt  9516  elz2  9518  gtndiv  9542  zeo  9552  supminfex  9792  eqreznegel  9809  negm  9810  irradd  9841  irrmul  9842  divlt1lt  9920  divle1le  9921  xnegneg  10029  rexsub  10049  xnegid  10055  xaddcom  10057  xaddid1  10058  xnegdi  10064  xaddass  10065  xleaddadd  10083  divelunit  10198  fzonmapblen  10387  infssuzex  10453  expgt1  10799  mulexpzap  10801  leexp1a  10816  expubnd  10818  sqgt0ap  10830  lt2sq  10835  le2sq  10836  sqge0  10838  sumsqeq0  10840  bernneq  10882  bernneq2  10883  nn0ltexp2  10931  swrdccatin2  11261  swrdccat3blem  11271  crre  11368  crim  11369  reim0  11372  mulreap  11375  rere  11376  remul2  11384  redivap  11385  immul2  11391  imdivap  11392  cjre  11393  cjreim  11414  rennim  11513  sqrt0rlem  11514  resqrexlemover  11521  absreimsq  11578  absreim  11579  absnid  11584  leabs  11585  absre  11588  absresq  11589  sqabs  11593  ltabs  11598  absdiflt  11603  absdifle  11604  lenegsq  11606  abssuble0  11614  dfabsmax  11728  max0addsup  11730  negfi  11739  minclpr  11748  reefcl  12179  efgt0  12195  reeftlcl  12200  resinval  12226  recosval  12227  resin4p  12229  recos4p  12230  resincl  12231  recoscl  12232  retanclap  12233  efieq  12246  sinbnd  12263  cosbnd  12264  absefi  12280  odd2np1  12384  remetdval  15221  bl2ioo  15224  ioo2bl  15225  hoverb  15322  plyreres  15438  sincosq1sgn  15500  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  relogoprlem  15542  logcxp  15571  rpcxpcl  15577  cxpcom  15612  rprelogbdiv  15631  gausslemma2dlem1a  15737  triap  16397  trirec0  16412