Theorem recn 8165

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   RRcr 8031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  mulrid  8176  recnd  8208  pnfnre  8221  mnfnre  8222  cnegexlem1  8354  cnegexlem2  8355  cnegexlem3  8356  cnegex  8357  renegcl  8440  resubcl  8443  negf1o  8561  mul02lem2  8567  ltaddneg  8604  ltaddnegr  8605  ltaddsub2  8617  leaddsub2  8619  leltadd  8627  ltaddpos  8632  ltaddpos2  8633  posdif  8635  lenegcon1  8646  lenegcon2  8647  addge01  8652  addge02  8653  leaddle0  8657  mullt0  8660  recexre  8758  msqge0  8796  mulge0  8799  aprcl  8826  recexap  8833  rerecapb  9023  ltm1  9026  prodgt02  9033  prodge02  9035  ltmul2  9036  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  gt0div  9050  ge0div  9051  ltmuldiv2  9055  ltdivmul  9056  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  negiso  9135  cju  9141  nnge1  9166  halfpos  9375  lt2halves  9380  addltmul  9381  avgle1  9385  avgle2  9386  div4p1lem1div2  9398  nnrecl  9400  elznn0  9494  elznn  9495  nzadd  9532  zmulcl  9533  difgtsumgt  9549  elz2  9551  gtndiv  9575  zeo  9585  supminfex  9831  eqreznegel  9848  negm  9849  irradd  9880  irrmul  9881  divlt1lt  9959  divle1le  9960  xnegneg  10068  rexsub  10088  xnegid  10094  xaddcom  10096  xaddid1  10097  xnegdi  10103  xaddass  10104  xleaddadd  10122  divelunit  10237  fzonmapblen  10427  infssuzex  10494  expgt1  10840  mulexpzap  10842  leexp1a  10857  expubnd  10859  sqgt0ap  10871  lt2sq  10876  le2sq  10877  sqge0  10879  sumsqeq0  10881  bernneq  10923  bernneq2  10924  nn0ltexp2  10972  swrdccatin2  11314  swrdccat3blem  11324  crre  11435  crim  11436  reim0  11439  mulreap  11442  rere  11443  remul2  11451  redivap  11452  immul2  11458  imdivap  11459  cjre  11460  cjreim  11481  rennim  11580  sqrt0rlem  11581  resqrexlemover  11588  absreimsq  11645  absreim  11646  absnid  11651  leabs  11652  absre  11655  absresq  11656  sqabs  11660  ltabs  11665  absdiflt  11670  absdifle  11671  lenegsq  11673  abssuble0  11681  dfabsmax  11795  max0addsup  11797  negfi  11806  minclpr  11815  reefcl  12247  efgt0  12263  reeftlcl  12268  resinval  12294  recosval  12295  resin4p  12297  recos4p  12298  resincl  12299  recoscl  12300  retanclap  12301  efieq  12314  sinbnd  12331  cosbnd  12332  absefi  12348  odd2np1  12452  remetdval  15290  bl2ioo  15293  ioo2bl  15294  hoverb  15391  plyreres  15507  sincosq1sgn  15569  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  relogoprlem  15611  logcxp  15640  rpcxpcl  15646  cxpcom  15681  rprelogbdiv  15700  gausslemma2dlem1a  15806  triap  16684  trirec0  16699