Theorem recn 8312

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   RRcr 8178

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  mulrid  8323  recnd  8354  pnfnre  8367  mnfnre  8368  cnegexlem1  8501  cnegexlem2  8502  cnegexlem3  8503  cnegex  8504  renegcl  8587  resubcl  8590  negf1o  8709  mul02lem2  8715  ltaddneg  8752  ltaddnegr  8753  ltaddsub2  8765  leaddsub2  8767  leltadd  8775  ltaddpos  8780  ltaddpos2  8781  posdif  8783  lenegcon1  8794  lenegcon2  8795  addge01  8800  addge02  8801  leaddle0  8805  mullt0  8808  recexre  8906  msqge0  8944  mulge0  8947  aprcl  8974  recexap  8981  rerecapb  9173  ltm1  9176  prodgt02  9183  prodge02  9185  ltmul2  9186  lemul2  9187  lemul2a  9189  ltmulgt12  9195  lemulge12  9197  gt0div  9200  ge0div  9201  ltmuldiv2  9205  ltdivmul  9206  ltdivmul2  9208  ledivmul2  9210  lemuldiv2  9212  negiso  9285  cju  9291  nnge1  9327  halfpos  9536  lt2halves  9541  addltmul  9542  avgle1  9546  avgle2  9547  div4p1lem1div2  9559  nnrecl  9561  elznn0  9659  elznn  9660  nzadd  9697  zmulcl  9698  difgtsumgt  9714  elz2  9716  gtndiv  9741  zeo  9751  supminfex  9997  eqreznegel  10014  negm  10015  irradd  10046  irrmul  10047  divlt1lt  10125  divle1le  10126  xnegneg  10235  rexsub  10255  xnegid  10261  xaddcom  10263  xaddid1  10264  xnegdi  10270  xaddass  10271  xleaddadd  10289  divelunit  10404  fzonmapblen  10599  infssuzex  10666  expgt1  11014  mulexpzap  11016  leexp1a  11031  expubnd  11033  sqgt0ap  11045  lt2sq  11050  le2sq  11051  sqge0  11053  sumsqeq0  11055  bernneq  11098  bernneq2  11099  nn0ltexp2  11147  swrdccatin2  11501  swrdccat3blem  11511  crre  11622  crim  11623  reim0  11626  mulreap  11629  rere  11630  remul2  11638  redivap  11639  immul2  11645  imdivap  11646  cjre  11647  cjreim  11669  rennim  11768  sqrt0rlem  11769  resqrexlemover  11776  absreimsq  11833  absreim  11834  absnid  11839  leabs  11840  absre  11843  absresq  11844  sqabs  11848  ltabs  11853  absdiflt  11858  absdifle  11859  lenegsq  11861  abssuble0  11869  dfabsmax  11983  max0addsup  11985  negfi  11994  minclpr  12003  reefcl  12435  efgt0  12451  reeftlcl  12456  resinval  12482  recosval  12483  resin4p  12485  recos4p  12486  resincl  12487  recoscl  12488  retanclap  12489  efieq  12502  sinbnd  12519  cosbnd  12520  absefi  12536  odd2np1  12640  remetdval  15648  bl2ioo  15651  ioo2bl  15652  hoverb  15749  plyreres  15865  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  relogoprlem  15969  logcxp  15999  rpcxpcl  16005  cxpcom  16040  rprelogbdiv  16059  gausslemma2dlem1a  16177  triap  17078  trirec0  17093