Theorem recn 7941

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7806   RRcr 7807

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 7900

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  7951  recnd  7982  pnfnre  7995  mnfnre  7996  cnegexlem1  8128  cnegexlem2  8129  cnegexlem3  8130  cnegex  8131  renegcl  8214  resubcl  8217  negf1o  8335  mul02lem2  8341  ltaddneg  8377  ltaddnegr  8378  ltaddsub2  8390  leaddsub2  8392  leltadd  8400  ltaddpos  8405  ltaddpos2  8406  posdif  8408  lenegcon1  8419  lenegcon2  8420  addge01  8425  addge02  8426  leaddle0  8430  mullt0  8433  recexre  8531  msqge0  8569  mulge0  8572  aprcl  8599  recexap  8606  rerecapb  8796  ltm1  8799  prodgt02  8806  prodge02  8808  ltmul2  8809  lemul2  8810  lemul2a  8812  ltmulgt12  8818  lemulge12  8820  gt0div  8823  ge0div  8824  ltmuldiv2  8828  ltdivmul  8829  ltdivmul2  8831  ledivmul2  8833  lemuldiv2  8835  negiso  8908  cju  8914  nnge1  8938  halfpos  9146  lt2halves  9150  addltmul  9151  avgle1  9155  avgle2  9156  div4p1lem1div2  9168  nnrecl  9170  elznn0  9264  elznn  9265  nzadd  9301  zmulcl  9302  difgtsumgt  9318  elz2  9320  gtndiv  9344  zeo  9354  supminfex  9593  eqreznegel  9610  negm  9611  irradd  9642  irrmul  9643  divlt1lt  9720  divle1le  9721  xnegneg  9829  rexsub  9849  xnegid  9855  xaddcom  9857  xaddid1  9858  xnegdi  9864  xaddass  9865  xleaddadd  9883  divelunit  9998  fzonmapblen  10182  expgt1  10553  mulexpzap  10555  leexp1a  10570  expubnd  10572  sqgt0ap  10583  lt2sq  10588  le2sq  10589  sqge0  10591  sumsqeq0  10593  bernneq  10635  bernneq2  10636  nn0ltexp2  10683  crre  10859  crim  10860  reim0  10863  mulreap  10866  rere  10867  remul2  10875  redivap  10876  immul2  10882  imdivap  10883  cjre  10884  cjreim  10905  rennim  11004  sqrt0rlem  11005  resqrexlemover  11012  absreimsq  11069  absreim  11070  absnid  11075  leabs  11076  absre  11079  absresq  11080  sqabs  11084  ltabs  11089  absdiflt  11094  absdifle  11095  lenegsq  11097  abssuble0  11105  dfabsmax  11219  max0addsup  11221  negfi  11229  minclpr  11238  reefcl  11669  efgt0  11685  reeftlcl  11690  resinval  11716  recosval  11717  resin4p  11719  recos4p  11720  resincl  11721  recoscl  11722  retanclap  11723  efieq  11736  sinbnd  11753  cosbnd  11754  absefi  11769  odd2np1  11870  infssuzex  11942  remetdval  13910  bl2ioo  13913  ioo2bl  13914  sincosq1sgn  14118  sincosq2sgn  14119  sincosq3sgn  14120  sincosq4sgn  14121  sinq12gt0  14122  relogoprlem  14160  logcxp  14189  rpcxpcl  14195  cxpcom  14228  rprelogbdiv  14246  triap  14637  trirec0  14652