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

Theorem recn 8829
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 8796 . 2  |-  RR  C_  CC
21sseli 3178 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   CCcc 8737   RRcr 8738
This theorem is referenced by:  mulid1  8837  recnd  8863  pnfnre  8876  mnfnre  8877  mul02  8992  renegcli  9110  resubcl  9113  ltaddsub2  9251  leaddsub2  9253  leltadd  9260  ltaddpos  9266  ltaddpos2  9267  posdif  9269  lenegcon1  9280  lenegcon2  9281  addge01  9286  addge02  9287  mullt0  9295  recex  9402  ltm1  9598  prodgt02  9604  prodge02  9606  ltmul2  9609  lemul1  9610  lemul2  9611  lemul1a  9612  lemul2a  9613  ltmulgt12  9619  lemulge12  9621  gt0div  9624  ge0div  9625  ltmuldiv2  9629  ltdivmul  9630  ledivmul  9631  ledivmulOLD  9632  ltdivmul2  9633  lt2mul2div  9634  ledivmul2  9635  ledivmul2OLD  9636  lemuldiv2  9638  ltdiv2  9643  ltrec1  9645  lerec2  9646  ledivdiv  9647  lediv2  9648  ltdiv23  9649  lediv23  9650  lediv12a  9651  recp1lt1  9656  ledivp1  9660  infm3lem  9714  supmul  9724  riotaneg  9731  negiso  9732  cju  9744  nnge1  9774  halfpos  9944  lt2halves  9948  addltmul  9949  avgle1  9953  avgle2  9954  avgle  9955  nnrecl  9965  elznn0  10040  elznn  10041  elz2  10042  zmulcl  10068  gtndiv  10091  zeo  10099  uzindOLD  10108  eqreznegel  10305  negn0  10306  supminf  10307  rebtwnz  10317  irradd  10342  irrmul  10343  max0sub  10525  xnegneg  10543  rexsub  10562  xnegid  10565  xaddcom  10567  xaddid1  10568  xnegdi  10570  xaddass  10571  rexmul  10593  xmulasslem3  10608  xadddilem  10616  flzadd  10953  intfrac2  10964  fldiv2  10967  mod0  10980  negmod0  10981  modlt  10983  modfrac  10986  flmod  10987  intfrac  10988  modmulnn  10990  modid  10995  modcyc  11001  modcyc2  11002  modadd1  11003  modmul1  11004  moddi  11009  modsubdir  11010  modirr  11011  expgt1  11142  mulexpz  11144  leexp1a  11162  expubnd  11164  sqgt0  11174  lt2sq  11179  le2sq  11180  sqge0  11182  sumsqeq0  11184  sqlecan  11211  bernneq  11229  bernneq2  11230  expnbnd  11232  digit2  11236  digit1  11237  crre  11601  crim  11602  reim0  11605  mulre  11608  rere  11609  remul2  11617  rediv  11618  immul2  11624  imdiv  11625  cjre  11626  cjreim  11647  rennim  11726  resqrex  11738  resqreu  11740  resqrcl  11741  resqrthlem  11742  sqrneglem  11754  sqrneg  11755  absreimsq  11779  absreim  11780  absnid  11785  leabs  11786  absre  11788  absresq  11789  sqabs  11794  max0add  11797  absz  11798  absdiflt  11803  absdifle  11804  lenegsq  11806  abssuble0  11814  absmax  11815  rddif  11826  absrdbnd  11827  o1rlimmul  12094  caurcvg2  12152  reefcl  12370  efgt0  12385  reeftlcl  12390  resinval  12417  recosval  12418  resin4p  12420  recos4p  12421  resincl  12422  recoscl  12423  retancl  12424  resinhcl  12438  rpcoshcl  12439  retanhcl  12441  tanhlt1  12442  tanhbnd  12443  efieq  12445  sinbnd  12462  cosbnd  12463  absefi  12478  odd2np1  12589  bezoutlem1  12719  xrsdsreclb  16420  resubdrg  16425  remetdval  18297  bl2ioo  18300  ioo2bl  18301  cnperf  18327  icccvx  18450  tchcph  18669  shft2rab  18869  volsup2  18962  volcn  18963  c1lip1  19346  plyreres  19665  aalioulem3  19716  taylthlem2  19755  reeff1o  19825  reefgim  19828  sincosq1sgn  19868  sincosq2sgn  19869  sincosq3sgn  19870  sincosq4sgn  19871  sinq12gt0  19877  pige3  19887  efif1olem4  19909  efifo  19911  relogrn  19921  logrnaddcl  19933  relogoprlem  19946  advlog  20003  advlogexp  20004  logtayl  20009  recxpcl  20024  rpcxpcl  20025  cxpge0  20032  dvcxp1  20084  logreclem  20118  angpieqvd  20130  atanre  20183  basellem9  20328  log2sumbnd  20695  readdsubgo  21022  nvsge0  21231  nmoub3i  21353  nmlnoubi  21376  isblo3i  21381  ipasslem3  21413  ipasslem9  21418  ipasslem11  21420  hmopm  22603  riesz1  22647  leopmuli  22715  leopmul  22716  leopmul2i  22717  leopnmid  22720  nmopleid  22721  cdj1i  23015  cdj3lem1  23016  cdj3i  23023  addltmulALT  23028  rexdiv  23111  xdivid  23113  xdiv0  23114  elunitcn  23284  modaddabs  24013  lediv2aALT  24015  divelunit  24082  mulge0b  24088  mulle0b  24089  brbtwn2  24535  colinearalglem4  24539  colinearalg  24540  nndivlub  24899  dvreasin  24925  itg2addnclem  24933  itg2addnclem2  24934  areacirclem2  24936  areacirclem3  24937  areacirclem4  24938  areacirclem5  24940  areacirclem6  24941  areacirc  24942  truni1  25516  dmse1  25614  mslb1  25618  2wsms  25619  iintlem1  25621  trran  25625  trnij  25626  cnvtr  25627  lvsovso  25637  clsmulrv  25694  divclrvd  25706  rdr  26446  expmordi  27043  lhe4.4ex1a  27557  expgrowthi  27561  mulltgt0  27704  refsum2cnlem1  27719  fmul01  27721  fmul01lt1lem1  27725  fmul01lt1lem2  27726  eluzelcn  27735  dvcosre  27752  itgsin0pilem1  27755  itgsinexplem1  27759  stoweidlem7  27767  stoweidlem10  27770  stoweidlem11  27771  stoweidlem13  27773  stoweidlem19  27779  stoweidlem20  27780  stoweidlem22  27782  stoweidlem23  27783  stoweidlem24  27784  stoweidlem26  27786  stoweidlem32  27792  stoweidlem34  27794  stoweidlem36  27796  stoweidlem44  27804  stoweid  27823  reseccl  28234  recsccl  28235  recotcl  28236  dpfrac1  28253
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-resscn 8796
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator