Theorem recn 7943

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

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

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 7902

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 3135  df-ss 3142

This theorem is referenced by:  mulrid  7953  recnd  7985  pnfnre  7998  mnfnre  7999  cnegexlem1  8131  cnegexlem2  8132  cnegexlem3  8133  cnegex  8134  renegcl  8217  resubcl  8220  negf1o  8338  mul02lem2  8344  ltaddneg  8380  ltaddnegr  8381  ltaddsub2  8393  leaddsub2  8395  leltadd  8403  ltaddpos  8408  ltaddpos2  8409  posdif  8411  lenegcon1  8422  lenegcon2  8423  addge01  8428  addge02  8429  leaddle0  8433  mullt0  8436  recexre  8534  msqge0  8572  mulge0  8575  aprcl  8602  recexap  8609  rerecapb  8799  ltm1  8802  prodgt02  8809  prodge02  8811  ltmul2  8812  lemul2  8813  lemul2a  8815  ltmulgt12  8821  lemulge12  8823  gt0div  8826  ge0div  8827  ltmuldiv2  8831  ltdivmul  8832  ltdivmul2  8834  ledivmul2  8836  lemuldiv2  8838  negiso  8911  cju  8917  nnge1  8941  halfpos  9149  lt2halves  9153  addltmul  9154  avgle1  9158  avgle2  9159  div4p1lem1div2  9171  nnrecl  9173  elznn0  9267  elznn  9268  nzadd  9304  zmulcl  9305  difgtsumgt  9321  elz2  9323  gtndiv  9347  zeo  9357  supminfex  9596  eqreznegel  9613  negm  9614  irradd  9645  irrmul  9646  divlt1lt  9723  divle1le  9724  xnegneg  9832  rexsub  9852  xnegid  9858  xaddcom  9860  xaddid1  9861  xnegdi  9867  xaddass  9868  xleaddadd  9886  divelunit  10001  fzonmapblen  10186  expgt1  10557  mulexpzap  10559  leexp1a  10574  expubnd  10576  sqgt0ap  10588  lt2sq  10593  le2sq  10594  sqge0  10596  sumsqeq0  10598  bernneq  10640  bernneq2  10641  nn0ltexp2  10688  crre  10865  crim  10866  reim0  10869  mulreap  10872  rere  10873  remul2  10881  redivap  10882  immul2  10888  imdivap  10889  cjre  10890  cjreim  10911  rennim  11010  sqrt0rlem  11011  resqrexlemover  11018  absreimsq  11075  absreim  11076  absnid  11081  leabs  11082  absre  11085  absresq  11086  sqabs  11090  ltabs  11095  absdiflt  11100  absdifle  11101  lenegsq  11103  abssuble0  11111  dfabsmax  11225  max0addsup  11227  negfi  11235  minclpr  11244  reefcl  11675  efgt0  11691  reeftlcl  11696  resinval  11722  recosval  11723  resin4p  11725  recos4p  11726  resincl  11727  recoscl  11728  retanclap  11729  efieq  11742  sinbnd  11759  cosbnd  11760  absefi  11775  odd2np1  11877  infssuzex  11949  remetdval  14009  bl2ioo  14012  ioo2bl  14013  sincosq1sgn  14217  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  sinq12gt0  14221  relogoprlem  14259  logcxp  14288  rpcxpcl  14294  cxpcom  14327  rprelogbdiv  14345  triap  14747  trirec0  14762