Theorem recn 8143

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8008   RRcr 8009

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 8102

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  8154  recnd  8186  pnfnre  8199  mnfnre  8200  cnegexlem1  8332  cnegexlem2  8333  cnegexlem3  8334  cnegex  8335  renegcl  8418  resubcl  8421  negf1o  8539  mul02lem2  8545  ltaddneg  8582  ltaddnegr  8583  ltaddsub2  8595  leaddsub2  8597  leltadd  8605  ltaddpos  8610  ltaddpos2  8611  posdif  8613  lenegcon1  8624  lenegcon2  8625  addge01  8630  addge02  8631  leaddle0  8635  mullt0  8638  recexre  8736  msqge0  8774  mulge0  8777  aprcl  8804  recexap  8811  rerecapb  9001  ltm1  9004  prodgt02  9011  prodge02  9013  ltmul2  9014  lemul2  9015  lemul2a  9017  ltmulgt12  9023  lemulge12  9025  gt0div  9028  ge0div  9029  ltmuldiv2  9033  ltdivmul  9034  ltdivmul2  9036  ledivmul2  9038  lemuldiv2  9040  negiso  9113  cju  9119  nnge1  9144  halfpos  9353  lt2halves  9358  addltmul  9359  avgle1  9363  avgle2  9364  div4p1lem1div2  9376  nnrecl  9378  elznn0  9472  elznn  9473  nzadd  9510  zmulcl  9511  difgtsumgt  9527  elz2  9529  gtndiv  9553  zeo  9563  supminfex  9804  eqreznegel  9821  negm  9822  irradd  9853  irrmul  9854  divlt1lt  9932  divle1le  9933  xnegneg  10041  rexsub  10061  xnegid  10067  xaddcom  10069  xaddid1  10070  xnegdi  10076  xaddass  10077  xleaddadd  10095  divelunit  10210  fzonmapblen  10399  infssuzex  10465  expgt1  10811  mulexpzap  10813  leexp1a  10828  expubnd  10830  sqgt0ap  10842  lt2sq  10847  le2sq  10848  sqge0  10850  sumsqeq0  10852  bernneq  10894  bernneq2  10895  nn0ltexp2  10943  swrdccatin2  11276  swrdccat3blem  11286  crre  11383  crim  11384  reim0  11387  mulreap  11390  rere  11391  remul2  11399  redivap  11400  immul2  11406  imdivap  11407  cjre  11408  cjreim  11429  rennim  11528  sqrt0rlem  11529  resqrexlemover  11536  absreimsq  11593  absreim  11594  absnid  11599  leabs  11600  absre  11603  absresq  11604  sqabs  11608  ltabs  11613  absdiflt  11618  absdifle  11619  lenegsq  11621  abssuble0  11629  dfabsmax  11743  max0addsup  11745  negfi  11754  minclpr  11763  reefcl  12194  efgt0  12210  reeftlcl  12215  resinval  12241  recosval  12242  resin4p  12244  recos4p  12245  resincl  12246  recoscl  12247  retanclap  12248  efieq  12261  sinbnd  12278  cosbnd  12279  absefi  12295  odd2np1  12399  remetdval  15236  bl2ioo  15239  ioo2bl  15240  hoverb  15337  plyreres  15453  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  relogoprlem  15557  logcxp  15586  rpcxpcl  15592  cxpcom  15627  rprelogbdiv  15646  gausslemma2dlem1a  15752  triap  16457  trirec0  16472