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

Theorem recn 8827
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 8794 . 2  |-  RR  C_  CC
21sseli 3176 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   CCcc 8735   RRcr 8736
This theorem is referenced by:  mulid1  8835  recnd  8861  pnfnre  8874  mnfnre  8875  mul02  8990  renegcli  9108  resubcl  9111  ltaddsub2  9249  leaddsub2  9251  leltadd  9258  ltaddpos  9264  ltaddpos2  9265  posdif  9267  lenegcon1  9278  lenegcon2  9279  addge01  9284  addge02  9285  mullt0  9293  recex  9400  ltm1  9596  prodgt02  9602  prodge02  9604  ltmul2  9607  lemul1  9608  lemul2  9609  lemul1a  9610  lemul2a  9611  ltmulgt12  9617  lemulge12  9619  gt0div  9622  ge0div  9623  ltmuldiv2  9627  ltdivmul  9628  ledivmul  9629  ledivmulOLD  9630  ltdivmul2  9631  lt2mul2div  9632  ledivmul2  9633  ledivmul2OLD  9634  lemuldiv2  9636  ltdiv2  9641  ltrec1  9643  lerec2  9644  ledivdiv  9645  lediv2  9646  ltdiv23  9647  lediv23  9648  lediv12a  9649  recp1lt1  9654  ledivp1  9658  infm3lem  9712  supmul  9722  riotaneg  9729  negiso  9730  cju  9742  nnge1  9772  halfpos  9942  lt2halves  9946  addltmul  9947  avgle1  9951  avgle2  9952  avgle  9953  nnrecl  9963  elznn0  10038  elznn  10039  elz2  10040  zmulcl  10066  gtndiv  10089  zeo  10097  uzindOLD  10106  eqreznegel  10303  negn0  10304  supminf  10305  rebtwnz  10315  irradd  10340  irrmul  10341  max0sub  10523  xnegneg  10541  rexsub  10560  xnegid  10563  xaddcom  10565  xaddid1  10566  xnegdi  10568  xaddass  10569  rexmul  10591  xmulasslem3  10606  xadddilem  10614  flzadd  10951  intfrac2  10962  fldiv2  10965  mod0  10978  negmod0  10979  modlt  10981  modfrac  10984  flmod  10985  intfrac  10986  modmulnn  10988  modid  10993  modcyc  10999  modcyc2  11000  modadd1  11001  modmul1  11002  moddi  11007  modsubdir  11008  modirr  11009  expgt1  11140  mulexpz  11142  leexp1a  11160  expubnd  11162  sqgt0  11172  lt2sq  11177  le2sq  11178  sqge0  11180  sumsqeq0  11182  sqlecan  11209  bernneq  11227  bernneq2  11228  expnbnd  11230  digit2  11234  digit1  11235  crre  11599  crim  11600  reim0  11603  mulre  11606  rere  11607  remul2  11615  rediv  11616  immul2  11622  imdiv  11623  cjre  11624  cjreim  11645  rennim  11724  resqrex  11736  resqreu  11738  resqrcl  11739  resqrthlem  11740  sqrneglem  11752  sqrneg  11753  absreimsq  11777  absreim  11778  absnid  11783  leabs  11784  absre  11786  absresq  11787  sqabs  11792  max0add  11795  absz  11796  absdiflt  11801  absdifle  11802  lenegsq  11804  abssuble0  11812  absmax  11813  rddif  11824  absrdbnd  11825  o1rlimmul  12092  caurcvg2  12150  reefcl  12368  efgt0  12383  reeftlcl  12388  resinval  12415  recosval  12416  resin4p  12418  recos4p  12419  resincl  12420  recoscl  12421  retancl  12422  resinhcl  12436  rpcoshcl  12437  retanhcl  12439  tanhlt1  12440  tanhbnd  12441  efieq  12443  sinbnd  12460  cosbnd  12461  absefi  12476  odd2np1  12587  bezoutlem1  12717  xrsdsreclb  16418  resubdrg  16423  remetdval  18295  bl2ioo  18298  ioo2bl  18299  cnperf  18325  icccvx  18448  tchcph  18667  shft2rab  18867  volsup2  18960  volcn  18961  c1lip1  19344  plyreres  19663  aalioulem3  19714  taylthlem2  19753  reeff1o  19823  reefgim  19826  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  sinq12gt0  19875  pige3  19885  efif1olem4  19907  efifo  19909  relogrn  19919  logrnaddcl  19931  relogoprlem  19944  advlog  20001  advlogexp  20002  logtayl  20007  recxpcl  20022  rpcxpcl  20023  cxpge0  20030  dvcxp1  20082  logreclem  20116  angpieqvd  20128  atanre  20181  basellem9  20326  log2sumbnd  20693  readdsubgo  21020  nvsge0  21229  nmoub3i  21351  nmlnoubi  21374  isblo3i  21379  ipasslem3  21411  ipasslem9  21416  ipasslem11  21418  hmopm  22601  riesz1  22645  leopmuli  22713  leopmul  22714  leopmul2i  22715  leopnmid  22718  nmopleid  22719  cdj1i  23013  cdj3lem1  23014  cdj3i  23021  addltmulALT  23026  rexdiv  23109  xdivid  23111  xdiv0  23112  elunitcn  23282  modaddabs  24011  lediv2aALT  24013  divelunit  24080  mulge0b  24086  mulle0b  24087  brbtwn2  24533  colinearalglem4  24537  colinearalg  24538  nndivlub  24897  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem5  24929  areacirclem6  24930  areacirc  24931  truni1  25505  dmse1  25603  mslb1  25607  2wsms  25608  iintlem1  25610  trran  25614  trnij  25615  cnvtr  25616  lvsovso  25626  clsmulrv  25683  divclrvd  25695  rdr  26435  expmordi  27032  lhe4.4ex1a  27546  expgrowthi  27550  mulltgt0  27693  refsum2cnlem1  27708  fmul01  27710  fmul01lt1lem1  27714  fmul01lt1lem2  27715  eluzelcn  27724  dvcosre  27741  itgsin0pilem1  27744  itgsinexplem1  27748  stoweidlem7  27756  stoweidlem10  27759  stoweidlem11  27760  stoweidlem13  27762  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem23  27772  stoweidlem24  27773  stoweidlem26  27775  stoweidlem32  27781  stoweidlem34  27783  stoweidlem36  27785  stoweidlem44  27793  stoweid  27812  reseccl  28223  recsccl  28224  recotcl  28225  dpfrac1  28242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator