Theorem recn 8318

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8183   RRcr 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8277

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  mulrid  8329  recnd  8360  pnfnre  8373  mnfnre  8374  cnegexlem1  8508  cnegexlem2  8509  cnegexlem3  8510  cnegex  8511  renegcl  8594  resubcl  8597  negf1o  8716  mul02lem2  8722  ltaddneg  8759  ltaddnegr  8760  ltaddsub2  8772  leaddsub2  8774  leltadd  8782  ltaddpos  8787  ltaddpos2  8788  posdif  8790  lenegcon1  8801  lenegcon2  8802  addge01  8807  addge02  8808  leaddle0  8812  mullt0  8815  recexre  8914  msqge0  8952  mulge0  8955  aprcl  8982  recexap  8989  rerecapb  9181  ltm1  9184  prodgt02  9191  prodge02  9193  ltmul2  9194  lemul2  9195  lemul2a  9197  ltmulgt12  9203  lemulge12  9205  gt0div  9208  ge0div  9209  ltmuldiv2  9213  ltdivmul  9214  ltdivmul2  9216  ledivmul2  9218  lemuldiv2  9220  negiso  9293  cju  9299  nnge1  9336  halfpos  9547  lt2halves  9552  addltmul  9553  avgle1  9557  avgle2  9558  div4p1lem1div2  9570  nnrecl  9572  elznn0  9668  elznn  9669  nzadd  9706  zmulcl  9707  difgtsumgt  9723  elz2  9725  gtndiv  9751  zeo  9761  supminfex  10012  eqreznegel  10029  negm  10030  irradd  10061  irrmul  10063  divlt1lt  10141  divle1le  10142  xnegneg  10251  rexsub  10271  xnegid  10277  xaddcom  10279  xaddid1  10280  xnegdi  10286  xaddass  10287  xleaddadd  10305  divelunit  10420  fzonmapblen  10615  infssuzex  10682  expgt1  11034  mulexpzap  11036  leexp1a  11051  expubnd  11053  sqgt0ap  11065  lt2sq  11070  le2sq  11071  sqge0  11073  sumsqeq0  11075  bernneq  11118  bernneq2  11119  nn0ltexp2  11168  swrdccatin2  11522  swrdccat3blem  11532  crre  11643  crim  11644  reim0  11647  mulreap  11650  rere  11651  remul2  11659  redivap  11660  immul2  11666  imdivap  11667  cjre  11668  cjreim  11690  rennim  11789  sqrt0rlem  11790  resqrexlemover  11797  absreimsq  11854  absreim  11855  absnid  11860  leabs  11861  absre  11865  absresq  11866  sqabs  11870  ltabs  11875  absdiflt  11880  absdifle  11881  lenegsq  11883  abssuble0  11891  dfabsmax  12005  max0addsup  12007  negfi  12016  minclpr  12026  reefcl  12459  efgt0  12475  reeftlcl  12480  resinval  12506  recosval  12507  resin4p  12509  recos4p  12510  resincl  12511  recoscl  12512  retanclap  12513  efieq  12526  sinbnd  12543  cosbnd  12544  absefi  12560  odd2np1  12664  remetdval  15790  bl2ioo  15793  ioo2bl  15794  hoverb  15891  plyreres  16007  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  relogoprlem  16115  logcxp  16147  rpcxpcl  16153  cxpcom  16190  rprelogbdiv  16210  gausslemma2dlem1a  16399  triap  17301  trirec0  17317