Theorem recn 8058

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7923   RRcr 7924

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  mulrid  8069  recnd  8101  pnfnre  8114  mnfnre  8115  cnegexlem1  8247  cnegexlem2  8248  cnegexlem3  8249  cnegex  8250  renegcl  8333  resubcl  8336  negf1o  8454  mul02lem2  8460  ltaddneg  8497  ltaddnegr  8498  ltaddsub2  8510  leaddsub2  8512  leltadd  8520  ltaddpos  8525  ltaddpos2  8526  posdif  8528  lenegcon1  8539  lenegcon2  8540  addge01  8545  addge02  8546  leaddle0  8550  mullt0  8553  recexre  8651  msqge0  8689  mulge0  8692  aprcl  8719  recexap  8726  rerecapb  8916  ltm1  8919  prodgt02  8926  prodge02  8928  ltmul2  8929  lemul2  8930  lemul2a  8932  ltmulgt12  8938  lemulge12  8940  gt0div  8943  ge0div  8944  ltmuldiv2  8948  ltdivmul  8949  ltdivmul2  8951  ledivmul2  8953  lemuldiv2  8955  negiso  9028  cju  9034  nnge1  9059  halfpos  9268  lt2halves  9273  addltmul  9274  avgle1  9278  avgle2  9279  div4p1lem1div2  9291  nnrecl  9293  elznn0  9387  elznn  9388  nzadd  9425  zmulcl  9426  difgtsumgt  9442  elz2  9444  gtndiv  9468  zeo  9478  supminfex  9718  eqreznegel  9735  negm  9736  irradd  9767  irrmul  9768  divlt1lt  9846  divle1le  9847  xnegneg  9955  rexsub  9975  xnegid  9981  xaddcom  9983  xaddid1  9984  xnegdi  9990  xaddass  9991  xleaddadd  10009  divelunit  10124  fzonmapblen  10311  infssuzex  10376  expgt1  10722  mulexpzap  10724  leexp1a  10739  expubnd  10741  sqgt0ap  10753  lt2sq  10758  le2sq  10759  sqge0  10761  sumsqeq0  10763  bernneq  10805  bernneq2  10806  nn0ltexp2  10854  crre  11168  crim  11169  reim0  11172  mulreap  11175  rere  11176  remul2  11184  redivap  11185  immul2  11191  imdivap  11192  cjre  11193  cjreim  11214  rennim  11313  sqrt0rlem  11314  resqrexlemover  11321  absreimsq  11378  absreim  11379  absnid  11384  leabs  11385  absre  11388  absresq  11389  sqabs  11393  ltabs  11398  absdiflt  11403  absdifle  11404  lenegsq  11406  abssuble0  11414  dfabsmax  11528  max0addsup  11530  negfi  11539  minclpr  11548  reefcl  11979  efgt0  11995  reeftlcl  12000  resinval  12026  recosval  12027  resin4p  12029  recos4p  12030  resincl  12031  recoscl  12032  retanclap  12033  efieq  12046  sinbnd  12063  cosbnd  12064  absefi  12080  odd2np1  12184  remetdval  15019  bl2ioo  15022  ioo2bl  15023  hoverb  15120  plyreres  15236  sincosq1sgn  15298  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  relogoprlem  15340  logcxp  15369  rpcxpcl  15375  cxpcom  15410  rprelogbdiv  15429  gausslemma2dlem1a  15535  triap  15968  trirec0  15983