Theorem recn 8313

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 8272	. 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 8178   RRcr 8179

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 8272

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  8324  recnd  8355  pnfnre  8368  mnfnre  8369  cnegexlem1  8503  cnegexlem2  8504  cnegexlem3  8505  cnegex  8506  renegcl  8589  resubcl  8592  negf1o  8711  mul02lem2  8717  ltaddneg  8754  ltaddnegr  8755  ltaddsub2  8767  leaddsub2  8769  leltadd  8777  ltaddpos  8782  ltaddpos2  8783  posdif  8785  lenegcon1  8796  lenegcon2  8797  addge01  8802  addge02  8803  leaddle0  8807  mullt0  8810  recexre  8909  msqge0  8947  mulge0  8950  aprcl  8977  recexap  8984  rerecapb  9176  ltm1  9179  prodgt02  9186  prodge02  9188  ltmul2  9189  lemul2  9190  lemul2a  9192  ltmulgt12  9198  lemulge12  9200  gt0div  9203  ge0div  9204  ltmuldiv2  9208  ltdivmul  9209  ltdivmul2  9211  ledivmul2  9213  lemuldiv2  9215  negiso  9288  cju  9294  nnge1  9330  halfpos  9541  lt2halves  9546  addltmul  9547  avgle1  9551  avgle2  9552  div4p1lem1div2  9564  nnrecl  9566  elznn0  9664  elznn  9665  nzadd  9702  zmulcl  9703  difgtsumgt  9719  elz2  9721  gtndiv  9746  zeo  9756  supminfex  10007  eqreznegel  10024  negm  10025  irradd  10056  irrmul  10058  divlt1lt  10136  divle1le  10137  xnegneg  10246  rexsub  10266  xnegid  10272  xaddcom  10274  xaddid1  10275  xnegdi  10281  xaddass  10282  xleaddadd  10300  divelunit  10415  fzonmapblen  10610  infssuzex  10677  expgt1  11029  mulexpzap  11031  leexp1a  11046  expubnd  11048  sqgt0ap  11060  lt2sq  11065  le2sq  11066  sqge0  11068  sumsqeq0  11070  bernneq  11113  bernneq2  11114  nn0ltexp2  11163  swrdccatin2  11517  swrdccat3blem  11527  crre  11638  crim  11639  reim0  11642  mulreap  11645  rere  11646  remul2  11654  redivap  11655  immul2  11661  imdivap  11662  cjre  11663  cjreim  11685  rennim  11784  sqrt0rlem  11785  resqrexlemover  11792  absreimsq  11849  absreim  11850  absnid  11855  leabs  11856  absre  11860  absresq  11861  sqabs  11865  ltabs  11870  absdiflt  11875  absdifle  11876  lenegsq  11878  abssuble0  11886  dfabsmax  12000  max0addsup  12002  negfi  12011  minclpr  12021  reefcl  12454  efgt0  12470  reeftlcl  12475  resinval  12501  recosval  12502  resin4p  12504  recos4p  12505  resincl  12506  recoscl  12507  retanclap  12508  efieq  12521  sinbnd  12538  cosbnd  12539  absefi  12555  odd2np1  12659  remetdval  15739  bl2ioo  15742  ioo2bl  15743  hoverb  15840  plyreres  15956  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  relogoprlem  16062  logcxp  16094  rpcxpcl  16100  cxpcom  16135  rprelogbdiv  16154  gausslemma2dlem1a  16343  triap  17244  trirec0  17260