Theorem recn 8057

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

Syntax hints:   -> wi 4   e. wcel 2175   CCcc 7922   RRcr 7923

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  mulrid  8068  recnd  8100  pnfnre  8113  mnfnre  8114  cnegexlem1  8246  cnegexlem2  8247  cnegexlem3  8248  cnegex  8249  renegcl  8332  resubcl  8335  negf1o  8453  mul02lem2  8459  ltaddneg  8496  ltaddnegr  8497  ltaddsub2  8509  leaddsub2  8511  leltadd  8519  ltaddpos  8524  ltaddpos2  8525  posdif  8527  lenegcon1  8538  lenegcon2  8539  addge01  8544  addge02  8545  leaddle0  8549  mullt0  8552  recexre  8650  msqge0  8688  mulge0  8691  aprcl  8718  recexap  8725  rerecapb  8915  ltm1  8918  prodgt02  8925  prodge02  8927  ltmul2  8928  lemul2  8929  lemul2a  8931  ltmulgt12  8937  lemulge12  8939  gt0div  8942  ge0div  8943  ltmuldiv2  8947  ltdivmul  8948  ltdivmul2  8950  ledivmul2  8952  lemuldiv2  8954  negiso  9027  cju  9033  nnge1  9058  halfpos  9267  lt2halves  9272  addltmul  9273  avgle1  9277  avgle2  9278  div4p1lem1div2  9290  nnrecl  9292  elznn0  9386  elznn  9387  nzadd  9424  zmulcl  9425  difgtsumgt  9441  elz2  9443  gtndiv  9467  zeo  9477  supminfex  9717  eqreznegel  9734  negm  9735  irradd  9766  irrmul  9767  divlt1lt  9845  divle1le  9846  xnegneg  9954  rexsub  9974  xnegid  9980  xaddcom  9982  xaddid1  9983  xnegdi  9989  xaddass  9990  xleaddadd  10008  divelunit  10123  fzonmapblen  10309  infssuzex  10374  expgt1  10720  mulexpzap  10722  leexp1a  10737  expubnd  10739  sqgt0ap  10751  lt2sq  10756  le2sq  10757  sqge0  10759  sumsqeq0  10761  bernneq  10803  bernneq2  10804  nn0ltexp2  10852  crre  11139  crim  11140  reim0  11143  mulreap  11146  rere  11147  remul2  11155  redivap  11156  immul2  11162  imdivap  11163  cjre  11164  cjreim  11185  rennim  11284  sqrt0rlem  11285  resqrexlemover  11292  absreimsq  11349  absreim  11350  absnid  11355  leabs  11356  absre  11359  absresq  11360  sqabs  11364  ltabs  11369  absdiflt  11374  absdifle  11375  lenegsq  11377  abssuble0  11385  dfabsmax  11499  max0addsup  11501  negfi  11510  minclpr  11519  reefcl  11950  efgt0  11966  reeftlcl  11971  resinval  11997  recosval  11998  resin4p  12000  recos4p  12001  resincl  12002  recoscl  12003  retanclap  12004  efieq  12017  sinbnd  12034  cosbnd  12035  absefi  12051  odd2np1  12155  remetdval  14990  bl2ioo  14993  ioo2bl  14994  hoverb  15091  plyreres  15207  sincosq1sgn  15269  sincosq2sgn  15270  sincosq3sgn  15271  sincosq4sgn  15272  sinq12gt0  15273  relogoprlem  15311  logcxp  15340  rpcxpcl  15346  cxpcom  15381  rprelogbdiv  15400  gausslemma2dlem1a  15506  triap  15930  trirec0  15945