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

Theorem recn 8917
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 8884 . 2  |-  RR  C_  CC
21sseli 3252 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   CCcc 8825   RRcr 8826
This theorem is referenced by:  mulid1  8925  recnd  8951  pnfnre  8964  mnfnre  8965  mul02  9080  renegcli  9198  resubcl  9201  ltaddsub2  9339  leaddsub2  9341  leltadd  9348  ltaddpos  9354  ltaddpos2  9355  posdif  9357  lenegcon1  9368  lenegcon2  9369  addge01  9374  addge02  9375  mullt0  9383  recex  9490  ltm1  9686  prodgt02  9692  prodge02  9694  ltmul2  9697  lemul1  9698  lemul2  9699  lemul1a  9700  lemul2a  9701  ltmulgt12  9707  lemulge12  9709  gt0div  9712  ge0div  9713  ltmuldiv2  9717  ltdivmul  9718  ledivmul  9719  ledivmulOLD  9720  ltdivmul2  9721  lt2mul2div  9722  ledivmul2  9723  ledivmul2OLD  9724  lemuldiv2  9726  ltdiv2  9731  ltrec1  9733  lerec2  9734  ledivdiv  9735  lediv2  9736  ltdiv23  9737  lediv23  9738  lediv12a  9739  recp1lt1  9744  ledivp1  9748  infm3lem  9802  supmul  9812  riotaneg  9819  negiso  9820  cju  9832  nnge1  9862  halfpos  10034  lt2halves  10038  addltmul  10039  avgle1  10043  avgle2  10044  avgle  10045  nnrecl  10055  elznn0  10130  elznn  10131  elz2  10132  zmulcl  10158  gtndiv  10181  zeo  10189  uzindOLD  10198  eqreznegel  10395  negn0  10396  supminf  10397  rebtwnz  10407  irradd  10432  irrmul  10433  max0sub  10615  xnegneg  10633  rexsub  10652  xnegid  10655  xaddcom  10657  xaddid1  10658  xnegdi  10660  xaddass  10661  rexmul  10683  xmulasslem3  10698  xadddilem  10706  flzadd  11043  intfrac2  11054  fldiv2  11057  mod0  11070  negmod0  11071  modlt  11073  modfrac  11076  flmod  11077  intfrac  11078  modmulnn  11080  modid  11085  modcyc  11091  modcyc2  11092  modadd1  11093  modmul1  11094  moddi  11099  modsubdir  11100  modirr  11101  expgt1  11233  mulexpz  11235  leexp1a  11253  expubnd  11255  sqgt0  11265  lt2sq  11270  le2sq  11271  sqge0  11273  sumsqeq0  11275  sqlecan  11302  bernneq  11320  bernneq2  11321  expnbnd  11323  digit2  11327  digit1  11328  crre  11695  crim  11696  reim0  11699  mulre  11702  rere  11703  remul2  11711  rediv  11712  immul2  11718  imdiv  11719  cjre  11720  cjreim  11741  rennim  11820  resqrex  11832  resqreu  11834  resqrcl  11835  resqrthlem  11836  sqrneglem  11848  sqrneg  11849  absreimsq  11873  absreim  11874  absnid  11879  leabs  11880  absre  11882  absresq  11883  sqabs  11888  max0add  11891  absz  11892  absdiflt  11897  absdifle  11898  lenegsq  11900  abssuble0  11908  absmax  11909  rddif  11920  absrdbnd  11921  o1rlimmul  12188  caurcvg2  12247  reefcl  12465  efgt0  12480  reeftlcl  12485  resinval  12512  recosval  12513  resin4p  12515  recos4p  12516  resincl  12517  recoscl  12518  retancl  12519  resinhcl  12533  rpcoshcl  12534  retanhcl  12536  tanhlt1  12537  tanhbnd  12538  efieq  12540  sinbnd  12557  cosbnd  12558  absefi  12573  odd2np1  12684  bezoutlem1  12814  xrsdsreclb  16524  resubdrg  16529  remetdval  18397  bl2ioo  18400  ioo2bl  18401  cnperf  18428  icccvx  18552  tchcph  18771  shft2rab  18971  volsup2  19064  volcn  19065  c1lip1  19448  plyreres  19767  aalioulem3  19818  taylthlem2  19857  reeff1o  19930  reefgim  19933  sincosq1sgn  19973  sincosq2sgn  19974  sincosq3sgn  19975  sincosq4sgn  19976  sinq12gt0  19982  pige3  19992  efif1olem4  20014  efifo  20016  relogrn  20026  logrnaddcl  20039  relogoprlem  20052  advlog  20112  advlogexp  20113  logtayl  20118  recxpcl  20133  rpcxpcl  20134  cxpge0  20141  dvcxp1  20193  logreclem  20227  angpieqvd  20239  atanre  20292  basellem9  20438  log2sumbnd  20805  readdsubgo  21132  nvsge0  21343  nmoub3i  21465  nmlnoubi  21488  isblo3i  21493  ipasslem3  21525  ipasslem9  21530  ipasslem11  21532  hmopm  22715  riesz1  22759  leopmuli  22827  leopmul  22828  leopmul2i  22829  leopnmid  22832  nmopleid  22833  cdj1i  23127  cdj3lem1  23128  cdj3i  23135  addltmulALT  23140  rexdiv  23376  xdivid  23378  xdiv0  23379  remulg  23436  elunitcn  23452  modaddabs  24415  lediv2aALT  24417  divelunit  24486  mulge0b  24492  mulle0b  24493  brbtwn2  25092  colinearalglem4  25096  colinearalg  25097  nndivlub  25456  itg2addnclem  25492  itg2addnclem2  25493  dvreasin  25515  areacirclem2  25517  areacirclem3  25518  areacirclem4  25519  areacirclem5  25521  areacirclem6  25522  areacirc  25523  rdr  25759  expmordi  26355  lhe4.4ex1a  26869  expgrowthi  26873  mulltgt0  27016  refsum2cnlem1  27031  fmul01  27033  fmul01lt1lem1  27037  fmul01lt1lem2  27038  eluzelcn  27047  dvcosre  27064  itgsin0pilem1  27067  itgsinexplem1  27071  stoweidlem7  27079  stoweidlem10  27082  stoweidlem11  27083  stoweidlem13  27085  stoweidlem19  27091  stoweidlem20  27092  stoweidlem22  27094  stoweidlem23  27095  stoweidlem24  27096  stoweidlem26  27098  stoweidlem32  27104  stoweidlem34  27106  stoweidlem36  27108  stoweidlem44  27116  stoweid  27135  reseccl  27923  recsccl  27924  recotcl  27925  dpfrac1  27942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-resscn 8884
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator