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  9670  elznn  9671  nzadd  9708  zmulcl  9709  difgtsumgt  9725  elz2  9727  gtndiv  9752  zeo  9762  supminfex  10013  eqreznegel  10030  negm  10031  irradd  10062  irrmul  10064  divlt1lt  10142  divle1le  10143  xnegneg  10252  rexsub  10272  xnegid  10278  xaddcom  10280  xaddid1  10281  xnegdi  10287  xaddass  10288  xleaddadd  10306  divelunit  10421  fzonmapblen  10616  infssuzex  10683  expgt1  11035  mulexpzap  11037  leexp1a  11052  expubnd  11054  sqgt0ap  11066  lt2sq  11071  le2sq  11072  sqge0  11074  sumsqeq0  11076  bernneq  11119  bernneq2  11120  nn0ltexp2  11169  swrdccatin2  11523  swrdccat3blem  11533  crre  11644  crim  11645  reim0  11648  mulreap  11651  rere  11652  remul2  11660  redivap  11661  immul2  11667  imdivap  11668  cjre  11669  cjreim  11691  rennim  11790  sqrt0rlem  11791  resqrexlemover  11798  absreimsq  11855  absreim  11856  absnid  11861  leabs  11862  absre  11866  absresq  11867  sqabs  11871  ltabs  11876  absdiflt  11881  absdifle  11882  lenegsq  11884  abssuble0  11892  dfabsmax  12006  max0addsup  12008  negfi  12017  minclpr  12027  reefcl  12460  efgt0  12476  reeftlcl  12481  resinval  12507  recosval  12508  resin4p  12510  recos4p  12511  resincl  12512  recoscl  12513  retanclap  12514  efieq  12527  sinbnd  12544  cosbnd  12545  absefi  12561  odd2np1  12665  remetdval  15773  bl2ioo  15776  ioo2bl  15777  hoverb  15874  plyreres  15990  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  relogoprlem  16098  logcxp  16130  rpcxpcl  16136  cxpcom  16173  rprelogbdiv  16193  gausslemma2dlem1a  16382  triap  17284  trirec0  17300