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

Theorem recn 9582
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 9549 . 2  |-  RR  C_  CC
21sseli 3500 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   CCcc 9490   RRcr 9491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9549
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  mulid1  9593  recnd  9622  pnfnre  9635  mnfnre  9636  mul02  9757  renegcli  9880  resubcl  9883  ltaddsub2  10027  leaddsub2  10029  leltadd  10036  ltaddpos  10042  ltaddpos2  10043  posdif  10045  lenegcon1  10056  lenegcon2  10057  addge01  10062  addge02  10063  leaddle0  10067  mullt0  10072  recex  10181  ltm1  10382  prodgt02  10388  prodge02  10390  ltmul2  10393  lemul1  10394  lemul2  10395  lemul1a  10396  lemul2a  10397  ltmulgt12  10403  lemulge12  10405  gt0div  10408  ge0div  10409  mulge0b  10412  mulle0b  10413  ltmuldiv2  10416  ltdivmul  10417  ledivmul  10418  ledivmulOLD  10419  ltdivmul2  10420  lt2mul2div  10421  ledivmul2  10422  ledivmul2OLD  10423  lemuldiv2  10425  ltdiv2  10430  ltrec1  10432  lerec2  10433  ledivdiv  10434  lediv2  10435  ltdiv23  10436  lediv23  10437  lediv12a  10438  recp1lt1  10443  ledivp1  10447  infm3lem  10501  supmul  10511  riotaneg  10518  negiso  10519  cju  10532  nnge1  10562  halfpos  10769  lt2halves  10773  addltmul  10774  avgle1  10778  avgle2  10779  avgle  10780  nnrecl  10793  elznn0  10879  elznn  10880  elz2  10881  zmulcl  10911  gtndiv  10938  zeo  10946  uzindOLD  10955  eqreznegel  11167  negn0  11168  supminf  11169  rebtwnz  11181  irradd  11206  irrmul  11207  max0sub  11395  xnegneg  11413  rexsub  11432  xnegid  11435  xaddcom  11437  xaddid1  11438  xnegdi  11440  xaddass  11441  rexmul  11463  xmulasslem3  11478  xadddilem  11486  divelunit  11662  fzonmapblen  11836  flzadd  11927  ltdifltdiv  11934  dfceil2  11936  intfrac2  11953  fldiv2  11956  flpmodeq  11969  mod0  11971  negmod0  11972  modlt  11974  modfrac  11977  flmod  11978  intfrac  11979  modmulnn  11981  modvalp1  11982  modid  11988  modcyc  11999  modcyc2  12000  modadd1  12001  modaddabs  12002  modadd2mod  12005  modmul1  12008  modaddmulmod  12021  moddi  12022  modsubdir  12023  modirr  12025  expgt1  12172  mulexpz  12174  leexp1a  12192  expubnd  12194  sqgt0  12204  lt2sq  12209  le2sq  12210  sqge0  12212  sumsqeq0  12214  sqlecan  12242  bernneq  12260  bernneq2  12261  expnbnd  12263  digit2  12267  digit1  12268  swrdccatin2  12675  swrdccat3blem  12683  cshweqrep  12752  crre  12910  crim  12911  reim0  12914  mulre  12917  rere  12918  remul2  12926  rediv  12927  immul2  12933  imdiv  12934  cjre  12935  cjreim  12956  rennim  13035  resqrex  13047  resqreu  13049  resqrtcl  13050  resqrtthlem  13051  sqrtneglem  13063  sqrtneg  13064  absreimsq  13088  absreim  13089  absnid  13094  leabs  13095  absre  13097  absresq  13098  sqabs  13103  max0add  13106  absz  13107  absdiflt  13113  absdifle  13114  lenegsq  13116  abssuble0  13124  absmax  13125  rddif  13136  absrdbnd  13137  o1rlimmul  13404  caurcvg2  13463  reefcl  13684  efgt0  13699  reeftlcl  13704  resinval  13731  recosval  13732  resin4p  13734  recos4p  13735  resincl  13736  recoscl  13737  retancl  13738  resinhcl  13752  rpcoshcl  13753  retanhcl  13755  tanhlt1  13756  tanhbnd  13757  efieq  13759  sinbnd  13776  cosbnd  13777  absefi  13792  odd2np1  13905  bezoutlem1  14035  xrsdsreclb  18261  remulg  18438  resubdrg  18439  remetdval  21057  bl2ioo  21060  ioo2bl  21061  cnperf  21088  icccvx  21213  tchcph  21443  shft2rab  21682  volsup2  21777  volcn  21778  c1lip1  22161  plyreres  22441  aalioulem3  22492  taylthlem2  22531  reeff1o  22604  reefgim  22607  sincosq1sgn  22652  sincosq2sgn  22653  sincosq3sgn  22654  sincosq4sgn  22655  sinq12gt0  22661  pige3  22671  efif1olem4  22693  efifo  22695  relogrn  22705  logrnaddcl  22718  relogoprlem  22731  advlog  22791  advlogexp  22792  logtayl  22797  recxpcl  22812  rpcxpcl  22813  cxpge0  22820  dvcxp1  22872  logreclem  22906  angpieqvd  22918  atanre  22972  basellem9  23118  log2sumbnd  23485  brbtwn2  23912  colinearalglem4  23916  colinearalg  23917  readdsubgo  25059  nvsge0  25270  nmoub3i  25392  nmlnoubi  25415  isblo3i  25420  ipasslem3  25452  ipasslem9  25457  ipasslem11  25459  hmopm  26644  riesz1  26688  leopmuli  26756  leopmul  26757  leopmul2i  26758  leopnmid  26761  nmopleid  26762  cdj1i  27056  cdj3lem1  27057  cdj3i  27064  addltmulALT  27069  rexdiv  27318  xdivid  27320  xdiv0  27321  rmulccn  27574  sgnneg  28147  lediv2aALT  28546  nndivlub  29528  cos2h  29651  tan2h  29652  mblfinlem2  29657  mblfinlem4  29659  dvtanlem  29669  itg2addnclem  29671  itg2addnclem2  29672  dvasin  29708  areacirclem1  29712  areacirclem2  29713  areacirclem4  29715  areacirclem5  29716  areacirc  29717  expmordi  30515  lhe4.4ex1a  30862  expgrowthi  30866  mulltgt0  31003  refsum2cnlem1  31018  dstregt0  31068  ltaddneg  31089  fmul01lt1lem1  31162  lptre2pt  31210  sinaover2ne0  31232  dvcosre  31267  itgsin0pilem1  31295  itgsinexplem1  31299  volioc  31318  stoweidlem7  31335  stoweidlem10  31338  stoweidlem19  31347  stoweidlem34  31362  stoweid  31391  dirker2re  31420  dirkerdenne0  31421  dirkerval2  31422  dirkerper  31424  dirkertrigeq  31429  dirkeritg  31430  fourierdlem39  31474  fourierdlem47  31482  fourierdlem72  31507  fourierdlem73  31508  fourierdlem77  31512  2leaddle2  31815  ltsubsubaddltsub  31819  reseccl  32246  recsccl  32247  recotcl  32248  dpfrac1  32265  bj-flbi3  33697
  Copyright terms: Public domain W3C validator