Theorem recn 7944

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7809   RRcr 7810

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  mulrid  7954  recnd  7986  pnfnre  7999  mnfnre  8000  cnegexlem1  8132  cnegexlem2  8133  cnegexlem3  8134  cnegex  8135  renegcl  8218  resubcl  8221  negf1o  8339  mul02lem2  8345  ltaddneg  8381  ltaddnegr  8382  ltaddsub2  8394  leaddsub2  8396  leltadd  8404  ltaddpos  8409  ltaddpos2  8410  posdif  8412  lenegcon1  8423  lenegcon2  8424  addge01  8429  addge02  8430  leaddle0  8434  mullt0  8437  recexre  8535  msqge0  8573  mulge0  8576  aprcl  8603  recexap  8610  rerecapb  8800  ltm1  8803  prodgt02  8810  prodge02  8812  ltmul2  8813  lemul2  8814  lemul2a  8816  ltmulgt12  8822  lemulge12  8824  gt0div  8827  ge0div  8828  ltmuldiv2  8832  ltdivmul  8833  ltdivmul2  8835  ledivmul2  8837  lemuldiv2  8839  negiso  8912  cju  8918  nnge1  8942  halfpos  9150  lt2halves  9154  addltmul  9155  avgle1  9159  avgle2  9160  div4p1lem1div2  9172  nnrecl  9174  elznn0  9268  elznn  9269  nzadd  9305  zmulcl  9306  difgtsumgt  9322  elz2  9324  gtndiv  9348  zeo  9358  supminfex  9597  eqreznegel  9614  negm  9615  irradd  9646  irrmul  9647  divlt1lt  9724  divle1le  9725  xnegneg  9833  rexsub  9853  xnegid  9859  xaddcom  9861  xaddid1  9862  xnegdi  9868  xaddass  9869  xleaddadd  9887  divelunit  10002  fzonmapblen  10187  expgt1  10558  mulexpzap  10560  leexp1a  10575  expubnd  10577  sqgt0ap  10589  lt2sq  10594  le2sq  10595  sqge0  10597  sumsqeq0  10599  bernneq  10641  bernneq2  10642  nn0ltexp2  10689  crre  10866  crim  10867  reim0  10870  mulreap  10873  rere  10874  remul2  10882  redivap  10883  immul2  10889  imdivap  10890  cjre  10891  cjreim  10912  rennim  11011  sqrt0rlem  11012  resqrexlemover  11019  absreimsq  11076  absreim  11077  absnid  11082  leabs  11083  absre  11086  absresq  11087  sqabs  11091  ltabs  11096  absdiflt  11101  absdifle  11102  lenegsq  11104  abssuble0  11112  dfabsmax  11226  max0addsup  11228  negfi  11236  minclpr  11245  reefcl  11676  efgt0  11692  reeftlcl  11697  resinval  11723  recosval  11724  resin4p  11726  recos4p  11727  resincl  11728  recoscl  11729  retanclap  11730  efieq  11743  sinbnd  11760  cosbnd  11761  absefi  11776  odd2np1  11878  infssuzex  11950  remetdval  14042  bl2ioo  14045  ioo2bl  14046  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  relogoprlem  14292  logcxp  14321  rpcxpcl  14327  cxpcom  14360  rprelogbdiv  14378  triap  14780  trirec0  14795