Theorem recn 8093

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

Syntax hints:   -> wi 4   e. wcel 2178   CCcc 7958   RRcr 7959

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  mulrid  8104  recnd  8136  pnfnre  8149  mnfnre  8150  cnegexlem1  8282  cnegexlem2  8283  cnegexlem3  8284  cnegex  8285  renegcl  8368  resubcl  8371  negf1o  8489  mul02lem2  8495  ltaddneg  8532  ltaddnegr  8533  ltaddsub2  8545  leaddsub2  8547  leltadd  8555  ltaddpos  8560  ltaddpos2  8561  posdif  8563  lenegcon1  8574  lenegcon2  8575  addge01  8580  addge02  8581  leaddle0  8585  mullt0  8588  recexre  8686  msqge0  8724  mulge0  8727  aprcl  8754  recexap  8761  rerecapb  8951  ltm1  8954  prodgt02  8961  prodge02  8963  ltmul2  8964  lemul2  8965  lemul2a  8967  ltmulgt12  8973  lemulge12  8975  gt0div  8978  ge0div  8979  ltmuldiv2  8983  ltdivmul  8984  ltdivmul2  8986  ledivmul2  8988  lemuldiv2  8990  negiso  9063  cju  9069  nnge1  9094  halfpos  9303  lt2halves  9308  addltmul  9309  avgle1  9313  avgle2  9314  div4p1lem1div2  9326  nnrecl  9328  elznn0  9422  elznn  9423  nzadd  9460  zmulcl  9461  difgtsumgt  9477  elz2  9479  gtndiv  9503  zeo  9513  supminfex  9753  eqreznegel  9770  negm  9771  irradd  9802  irrmul  9803  divlt1lt  9881  divle1le  9882  xnegneg  9990  rexsub  10010  xnegid  10016  xaddcom  10018  xaddid1  10019  xnegdi  10025  xaddass  10026  xleaddadd  10044  divelunit  10159  fzonmapblen  10348  infssuzex  10413  expgt1  10759  mulexpzap  10761  leexp1a  10776  expubnd  10778  sqgt0ap  10790  lt2sq  10795  le2sq  10796  sqge0  10798  sumsqeq0  10800  bernneq  10842  bernneq2  10843  nn0ltexp2  10891  swrdccatin2  11220  swrdccat3blem  11230  crre  11283  crim  11284  reim0  11287  mulreap  11290  rere  11291  remul2  11299  redivap  11300  immul2  11306  imdivap  11307  cjre  11308  cjreim  11329  rennim  11428  sqrt0rlem  11429  resqrexlemover  11436  absreimsq  11493  absreim  11494  absnid  11499  leabs  11500  absre  11503  absresq  11504  sqabs  11508  ltabs  11513  absdiflt  11518  absdifle  11519  lenegsq  11521  abssuble0  11529  dfabsmax  11643  max0addsup  11645  negfi  11654  minclpr  11663  reefcl  12094  efgt0  12110  reeftlcl  12115  resinval  12141  recosval  12142  resin4p  12144  recos4p  12145  resincl  12146  recoscl  12147  retanclap  12148  efieq  12161  sinbnd  12178  cosbnd  12179  absefi  12195  odd2np1  12299  remetdval  15134  bl2ioo  15137  ioo2bl  15138  hoverb  15235  plyreres  15351  sincosq1sgn  15413  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  relogoprlem  15455  logcxp  15484  rpcxpcl  15490  cxpcom  15525  rprelogbdiv  15544  gausslemma2dlem1a  15650  triap  16170  trirec0  16185