MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recn Unicode version

Theorem recn 8843
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
StepHypRef Expression
1 ax-resscn 8810 . 2  |-  RR  C_  CC
21sseli 3189 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   CCcc 8751   RRcr 8752
This theorem is referenced by:  mulid1  8851  recnd  8877  pnfnre  8890  mnfnre  8891  mul02  9006  renegcli  9124  resubcl  9127  ltaddsub2  9265  leaddsub2  9267  leltadd  9274  ltaddpos  9280  ltaddpos2  9281  posdif  9283  lenegcon1  9294  lenegcon2  9295  addge01  9300  addge02  9301  mullt0  9309  recex  9416  ltm1  9612  prodgt02  9618  prodge02  9620  ltmul2  9623  lemul1  9624  lemul2  9625  lemul1a  9626  lemul2a  9627  ltmulgt12  9633  lemulge12  9635  gt0div  9638  ge0div  9639  ltmuldiv2  9643  ltdivmul  9644  ledivmul  9645  ledivmulOLD  9646  ltdivmul2  9647  lt2mul2div  9648  ledivmul2  9649  ledivmul2OLD  9650  lemuldiv2  9652  ltdiv2  9657  ltrec1  9659  lerec2  9660  ledivdiv  9661  lediv2  9662  ltdiv23  9663  lediv23  9664  lediv12a  9665  recp1lt1  9670  ledivp1  9674  infm3lem  9728  supmul  9738  riotaneg  9745  negiso  9746  cju  9758  nnge1  9788  halfpos  9958  lt2halves  9962  addltmul  9963  avgle1  9967  avgle2  9968  avgle  9969  nnrecl  9979  elznn0  10054  elznn  10055  elz2  10056  zmulcl  10082  gtndiv  10105  zeo  10113  uzindOLD  10122  eqreznegel  10319  negn0  10320  supminf  10321  rebtwnz  10331  irradd  10356  irrmul  10357  max0sub  10539  xnegneg  10557  rexsub  10576  xnegid  10579  xaddcom  10581  xaddid1  10582  xnegdi  10584  xaddass  10585  rexmul  10607  xmulasslem3  10622  xadddilem  10630  flzadd  10967  intfrac2  10978  fldiv2  10981  mod0  10994  negmod0  10995  modlt  10997  modfrac  11000  flmod  11001  intfrac  11002  modmulnn  11004  modid  11009  modcyc  11015  modcyc2  11016  modadd1  11017  modmul1  11018  moddi  11023  modsubdir  11024  modirr  11025  expgt1  11156  mulexpz  11158  leexp1a  11176  expubnd  11178  sqgt0  11188  lt2sq  11193  le2sq  11194  sqge0  11196  sumsqeq0  11198  sqlecan  11225  bernneq  11243  bernneq2  11244  expnbnd  11246  digit2  11250  digit1  11251  crre  11615  crim  11616  reim0  11619  mulre  11622  rere  11623  remul2  11631  rediv  11632  immul2  11638  imdiv  11639  cjre  11640  cjreim  11661  rennim  11740  resqrex  11752  resqreu  11754  resqrcl  11755  resqrthlem  11756  sqrneglem  11768  sqrneg  11769  absreimsq  11793  absreim  11794  absnid  11799  leabs  11800  absre  11802  absresq  11803  sqabs  11808  max0add  11811  absz  11812  absdiflt  11817  absdifle  11818  lenegsq  11820  abssuble0  11828  absmax  11829  rddif  11840  absrdbnd  11841  o1rlimmul  12108  caurcvg2  12166  reefcl  12384  efgt0  12399  reeftlcl  12404  resinval  12431  recosval  12432  resin4p  12434  recos4p  12435  resincl  12436  recoscl  12437  retancl  12438  resinhcl  12452  rpcoshcl  12453  retanhcl  12455  tanhlt1  12456  tanhbnd  12457  efieq  12459  sinbnd  12476  cosbnd  12477  absefi  12492  odd2np1  12603  bezoutlem1  12733  xrsdsreclb  16434  resubdrg  16439  remetdval  18311  bl2ioo  18314  ioo2bl  18315  cnperf  18341  icccvx  18464  tchcph  18683  shft2rab  18883  volsup2  18976  volcn  18977  c1lip1  19360  plyreres  19679  aalioulem3  19730  taylthlem2  19769  reeff1o  19839  reefgim  19842  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  sinq12gt0  19891  pige3  19901  efif1olem4  19923  efifo  19925  relogrn  19935  logrnaddcl  19947  relogoprlem  19960  advlog  20017  advlogexp  20018  logtayl  20023  recxpcl  20038  rpcxpcl  20039  cxpge0  20046  dvcxp1  20098  logreclem  20132  angpieqvd  20144  atanre  20197  basellem9  20342  log2sumbnd  20709  readdsubgo  21036  nvsge0  21245  nmoub3i  21367  nmlnoubi  21390  isblo3i  21395  ipasslem3  21427  ipasslem9  21432  ipasslem11  21434  hmopm  22617  riesz1  22661  leopmuli  22729  leopmul  22730  leopmul2i  22731  leopnmid  22734  nmopleid  22735  cdj1i  23029  cdj3lem1  23030  cdj3i  23037  addltmulALT  23042  rexdiv  23125  xdivid  23127  xdiv0  23128  elunitcn  23297  modaddabs  24026  lediv2aALT  24028  divelunit  24095  mulge0b  24101  mulle0b  24102  brbtwn2  24604  colinearalglem4  24608  colinearalg  24609  nndivlub  24968  itg2addnclem  25002  itg2addnclem2  25003  dvreasin  25025  areacirclem2  25027  areacirclem3  25028  areacirclem4  25029  areacirclem5  25031  areacirclem6  25032  areacirc  25033  truni1  25607  dmse1  25705  mslb1  25709  2wsms  25710  iintlem1  25712  trran  25716  trnij  25717  cnvtr  25718  lvsovso  25728  clsmulrv  25785  divclrvd  25797  rdr  26537  expmordi  27134  lhe4.4ex1a  27648  expgrowthi  27652  mulltgt0  27795  refsum2cnlem1  27810  fmul01  27812  fmul01lt1lem1  27816  fmul01lt1lem2  27817  eluzelcn  27826  dvcosre  27843  itgsin0pilem1  27846  itgsinexplem1  27850  stoweidlem7  27858  stoweidlem10  27861  stoweidlem11  27862  stoweidlem13  27864  stoweidlem19  27870  stoweidlem20  27871  stoweidlem22  27873  stoweidlem23  27874  stoweidlem24  27875  stoweidlem26  27877  stoweidlem32  27883  stoweidlem34  27885  stoweidlem36  27887  stoweidlem44  27895  stoweid  27914  reseccl  28476  recsccl  28477  recotcl  28478  dpfrac1  28495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator