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

Theorem recn 9036
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 9003 . 2  |-  RR  C_  CC
21sseli 3304 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   CCcc 8944   RRcr 8945
This theorem is referenced by:  mulid1  9044  recnd  9070  pnfnre  9083  mnfnre  9084  mul02  9200  renegcli  9318  resubcl  9321  ltaddsub2  9459  leaddsub2  9461  leltadd  9468  ltaddpos  9474  ltaddpos2  9475  posdif  9477  lenegcon1  9488  lenegcon2  9489  addge01  9494  addge02  9495  mullt0  9503  recex  9610  ltm1  9806  prodgt02  9812  prodge02  9814  ltmul2  9817  lemul1  9818  lemul2  9819  lemul1a  9820  lemul2a  9821  ltmulgt12  9827  lemulge12  9829  gt0div  9832  ge0div  9833  ltmuldiv2  9837  ltdivmul  9838  ledivmul  9839  ledivmulOLD  9840  ltdivmul2  9841  lt2mul2div  9842  ledivmul2  9843  ledivmul2OLD  9844  lemuldiv2  9846  ltdiv2  9851  ltrec1  9853  lerec2  9854  ledivdiv  9855  lediv2  9856  ltdiv23  9857  lediv23  9858  lediv12a  9859  recp1lt1  9864  ledivp1  9868  infm3lem  9922  supmul  9932  riotaneg  9939  negiso  9940  cju  9952  nnge1  9982  halfpos  10154  lt2halves  10158  addltmul  10159  avgle1  10163  avgle2  10164  avgle  10165  nnrecl  10175  elznn0  10252  elznn  10253  elz2  10254  zmulcl  10280  gtndiv  10303  zeo  10311  uzindOLD  10320  eqreznegel  10517  negn0  10518  supminf  10519  rebtwnz  10529  irradd  10554  irrmul  10555  max0sub  10738  xnegneg  10756  rexsub  10775  xnegid  10778  xaddcom  10780  xaddid1  10781  xnegdi  10783  xaddass  10784  rexmul  10806  xmulasslem3  10821  xadddilem  10829  flzadd  11183  intfrac2  11194  fldiv2  11197  mod0  11210  negmod0  11211  modlt  11213  modfrac  11216  flmod  11217  intfrac  11218  modmulnn  11220  modid  11225  modcyc  11231  modcyc2  11232  modadd1  11233  modmul1  11234  moddi  11239  modsubdir  11240  modirr  11241  expgt1  11373  mulexpz  11375  leexp1a  11393  expubnd  11395  sqgt0  11405  lt2sq  11410  le2sq  11411  sqge0  11413  sumsqeq0  11415  sqlecan  11442  bernneq  11460  bernneq2  11461  expnbnd  11463  digit2  11467  digit1  11468  crre  11874  crim  11875  reim0  11878  mulre  11881  rere  11882  remul2  11890  rediv  11891  immul2  11897  imdiv  11898  cjre  11899  cjreim  11920  rennim  11999  resqrex  12011  resqreu  12013  resqrcl  12014  resqrthlem  12015  sqrneglem  12027  sqrneg  12028  absreimsq  12052  absreim  12053  absnid  12058  leabs  12059  absre  12061  absresq  12062  sqabs  12067  max0add  12070  absz  12071  absdiflt  12076  absdifle  12077  lenegsq  12079  abssuble0  12087  absmax  12088  rddif  12099  absrdbnd  12100  o1rlimmul  12367  caurcvg2  12426  reefcl  12644  efgt0  12659  reeftlcl  12664  resinval  12691  recosval  12692  resin4p  12694  recos4p  12695  resincl  12696  recoscl  12697  retancl  12698  resinhcl  12712  rpcoshcl  12713  retanhcl  12715  tanhlt1  12716  tanhbnd  12717  efieq  12719  sinbnd  12736  cosbnd  12737  absefi  12752  odd2np1  12863  bezoutlem1  12993  xrsdsreclb  16700  resubdrg  16705  remetdval  18773  bl2ioo  18776  ioo2bl  18777  cnperf  18804  icccvx  18928  tchcph  19147  shft2rab  19357  volsup2  19450  volcn  19451  c1lip1  19834  plyreres  20153  aalioulem3  20204  taylthlem2  20243  reeff1o  20316  reefgim  20319  sincosq1sgn  20359  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  sinq12gt0  20368  pige3  20378  efif1olem4  20400  efifo  20402  relogrn  20412  logrnaddcl  20425  relogoprlem  20438  advlog  20498  advlogexp  20499  logtayl  20504  recxpcl  20519  rpcxpcl  20520  cxpge0  20527  dvcxp1  20579  logreclem  20613  angpieqvd  20625  atanre  20678  basellem9  20824  log2sumbnd  21191  readdsubgo  21894  nvsge0  22105  nmoub3i  22227  nmlnoubi  22250  isblo3i  22255  ipasslem3  22287  ipasslem9  22292  ipasslem11  22294  hmopm  23477  riesz1  23521  leopmuli  23589  leopmul  23590  leopmul2i  23591  leopnmid  23594  nmopleid  23595  cdj1i  23889  cdj3lem1  23890  cdj3i  23897  addltmulALT  23902  rexdiv  24125  xdivid  24127  xdiv0  24128  remulg  24223  rmulccn  24267  modaddabs  25068  lediv2aALT  25070  divelunit  25138  mulge0b  25144  mulle0b  25145  brbtwn2  25748  colinearalglem4  25752  colinearalg  25753  nndivlub  26112  mblfinlem  26143  mblfinlem3  26145  itg2addnclem  26155  itg2addnclem2  26156  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  areacirclem5  26185  areacirclem6  26186  areacirc  26187  expmordi  26900  lhe4.4ex1a  27414  expgrowthi  27418  mulltgt0  27560  refsum2cnlem1  27575  fmul01lt1lem1  27581  dvcosre  27608  itgsin0pilem1  27611  itgsinexplem1  27615  stoweidlem7  27623  stoweidlem10  27626  stoweidlem19  27635  stoweidlem34  27650  stoweid  27679  reseccl  28210  recsccl  28211  recotcl  28212  dpfrac1  28229
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator