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

Theorem recn 9082
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 9049 . 2  |-  RR  C_  CC
21sseli 3346 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   CCcc 8990   RRcr 8991
This theorem is referenced by:  mulid1  9090  recnd  9116  pnfnre  9129  mnfnre  9130  mul02  9246  renegcli  9364  resubcl  9367  ltaddsub2  9505  leaddsub2  9507  leltadd  9514  ltaddpos  9520  ltaddpos2  9521  posdif  9523  lenegcon1  9534  lenegcon2  9535  addge01  9540  addge02  9541  mullt0  9549  recex  9656  ltm1  9852  prodgt02  9858  prodge02  9860  ltmul2  9863  lemul1  9864  lemul2  9865  lemul1a  9866  lemul2a  9867  ltmulgt12  9873  lemulge12  9875  gt0div  9878  ge0div  9879  ltmuldiv2  9883  ltdivmul  9884  ledivmul  9885  ledivmulOLD  9886  ltdivmul2  9887  lt2mul2div  9888  ledivmul2  9889  ledivmul2OLD  9890  lemuldiv2  9892  ltdiv2  9897  ltrec1  9899  lerec2  9900  ledivdiv  9901  lediv2  9902  ltdiv23  9903  lediv23  9904  lediv12a  9905  recp1lt1  9910  ledivp1  9914  infm3lem  9968  supmul  9978  riotaneg  9985  negiso  9986  cju  9998  nnge1  10028  halfpos  10200  lt2halves  10204  addltmul  10205  avgle1  10209  avgle2  10210  avgle  10211  nnrecl  10221  elznn0  10298  elznn  10299  elz2  10300  zmulcl  10326  gtndiv  10349  zeo  10357  uzindOLD  10366  eqreznegel  10563  negn0  10564  supminf  10565  rebtwnz  10575  irradd  10600  irrmul  10601  max0sub  10784  xnegneg  10802  rexsub  10821  xnegid  10824  xaddcom  10826  xaddid1  10827  xnegdi  10829  xaddass  10830  rexmul  10852  xmulasslem3  10867  xadddilem  10875  flzadd  11230  intfrac2  11241  fldiv2  11244  mod0  11257  negmod0  11258  modlt  11260  modfrac  11263  flmod  11264  intfrac  11265  modmulnn  11267  modid  11272  modcyc  11278  modcyc2  11279  modadd1  11280  modmul1  11281  moddi  11286  modsubdir  11287  modirr  11288  expgt1  11420  mulexpz  11422  leexp1a  11440  expubnd  11442  sqgt0  11452  lt2sq  11457  le2sq  11458  sqge0  11460  sumsqeq0  11462  sqlecan  11489  bernneq  11507  bernneq2  11508  expnbnd  11510  digit2  11514  digit1  11515  crre  11921  crim  11922  reim0  11925  mulre  11928  rere  11929  remul2  11937  rediv  11938  immul2  11944  imdiv  11945  cjre  11946  cjreim  11967  rennim  12046  resqrex  12058  resqreu  12060  resqrcl  12061  resqrthlem  12062  sqrneglem  12074  sqrneg  12075  absreimsq  12099  absreim  12100  absnid  12105  leabs  12106  absre  12108  absresq  12109  sqabs  12114  max0add  12117  absz  12118  absdiflt  12123  absdifle  12124  lenegsq  12126  abssuble0  12134  absmax  12135  rddif  12146  absrdbnd  12147  o1rlimmul  12414  caurcvg2  12473  reefcl  12691  efgt0  12706  reeftlcl  12711  resinval  12738  recosval  12739  resin4p  12741  recos4p  12742  resincl  12743  recoscl  12744  retancl  12745  resinhcl  12759  rpcoshcl  12760  retanhcl  12762  tanhlt1  12763  tanhbnd  12764  efieq  12766  sinbnd  12783  cosbnd  12784  absefi  12799  odd2np1  12910  bezoutlem1  13040  xrsdsreclb  16747  resubdrg  16752  remetdval  18822  bl2ioo  18825  ioo2bl  18826  cnperf  18853  icccvx  18977  tchcph  19196  shft2rab  19406  volsup2  19499  volcn  19500  c1lip1  19883  plyreres  20202  aalioulem3  20253  taylthlem2  20292  reeff1o  20365  reefgim  20368  sincosq1sgn  20408  sincosq2sgn  20409  sincosq3sgn  20410  sincosq4sgn  20411  sinq12gt0  20417  pige3  20427  efif1olem4  20449  efifo  20451  relogrn  20461  logrnaddcl  20474  relogoprlem  20487  advlog  20547  advlogexp  20548  logtayl  20553  recxpcl  20568  rpcxpcl  20569  cxpge0  20576  dvcxp1  20628  logreclem  20662  angpieqvd  20674  atanre  20727  basellem9  20873  log2sumbnd  21240  readdsubgo  21943  nvsge0  22154  nmoub3i  22276  nmlnoubi  22299  isblo3i  22304  ipasslem3  22336  ipasslem9  22341  ipasslem11  22343  hmopm  23526  riesz1  23570  leopmuli  23638  leopmul  23639  leopmul2i  23640  leopnmid  23643  nmopleid  23644  cdj1i  23938  cdj3lem1  23939  cdj3i  23946  addltmulALT  23951  rexdiv  24174  xdivid  24176  xdiv0  24177  remulg  24272  rmulccn  24316  modaddabs  25117  lediv2aALT  25119  divelunit  25187  mulge0b  25193  mulle0b  25194  brbtwn2  25846  colinearalglem4  25850  colinearalg  25851  nndivlub  26210  mblfinlem2  26246  mblfinlem4  26248  itg2addnclem  26258  itg2addnclem2  26259  dvreasin  26292  areacirclem1  26294  areacirclem2  26295  areacirclem4  26297  areacirclem5  26298  areacirc  26299  expmordi  27012  lhe4.4ex1a  27525  expgrowthi  27529  mulltgt0  27671  refsum2cnlem1  27686  fmul01lt1lem1  27692  dvcosre  27719  itgsin0pilem1  27722  itgsinexplem1  27726  stoweidlem7  27734  stoweidlem10  27737  stoweidlem19  27746  stoweidlem34  27761  stoweid  27790  2leaddle2  28103  leaddle0  28104  fzonmapblen  28145  ltdifltdiv  28159  flpmodeq  28161  modvalp1  28162  modadd2mod  28165  modaddmulmod  28169  swrdccatin2  28232  swrdccat3blem  28240  2cshwmod  28279  cshweqrep  28296  reseccl  28558  recsccl  28559  recotcl  28560  dpfrac1  28577
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9049
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator