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

Theorem recn 9628
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 9595 . 2  |-  RR  C_  CC
21sseli 3466 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   CCcc 9536   RRcr 9537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-resscn 9595
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  mulid1  9639  recnd  9668  pnfnre  9681  mnfnre  9682  mul02  9810  renegcli  9934  resubcl  9937  negn0  10047  negf1o  10048  ltaddsub2  10088  leaddsub2  10090  leltadd  10097  ltaddpos  10103  ltaddpos2  10104  posdif  10106  lenegcon1  10117  lenegcon2  10118  addge01  10123  addge02  10124  leaddle0  10128  mullt0  10132  recex  10243  ltm1  10444  prodgt02  10450  prodge02  10452  ltmul2  10455  lemul1  10456  lemul2  10457  lemul1a  10458  lemul2a  10459  ltmulgt12  10465  lemulge12  10467  gt0div  10470  ge0div  10471  mulge0b  10474  mulle0b  10475  ltmuldiv2  10478  ltdivmul  10479  ledivmul  10480  ltdivmul2  10481  lt2mul2div  10482  ledivmul2  10483  ledivmul2OLD  10484  lemuldiv2  10486  ltdiv2  10491  ltrec1  10493  lerec2  10494  ledivdiv  10495  lediv2  10496  ltdiv23  10497  lediv23  10498  lediv12a  10499  recp1lt1  10504  ledivp1  10508  negfi  10554  fiminre  10555  infm3lem  10567  supmul  10579  riotaneg  10586  negiso  10587  cju  10605  nnge1  10635  halfpos  10843  lt2halves  10847  addltmul  10848  avgle1  10852  avgle2  10853  avgle  10854  nnrecl  10867  elznn0  10952  elznn  10953  elz2  10954  zmulcl  10985  gtndiv  11013  zeo  11021  eqreznegel  11249  supminf  11250  supminfOLD  11251  rebtwnz  11263  irradd  11288  irrmul  11289  max0sub  11489  xnegneg  11507  rexsub  11526  xnegid  11529  xaddcom  11531  xaddid1  11532  xnegdi  11534  xaddass  11535  rexmul  11557  xmulasslem3  11572  xadddilem  11580  divelunit  11772  fzonmapblen  11959  ico01fl0  12050  flzadd  12056  ltdifltdiv  12063  dfceil2  12065  intfrac2  12082  fldiv2  12085  flpmodeq  12098  mod0  12100  negmod0  12102  modlt  12104  modfrac  12107  flmod  12108  intfrac  12109  modmulnn  12111  modvalp1  12112  modid  12118  modcyc  12129  modcyc2  12130  modadd1  12131  modaddabs  12132  muladdmodid  12134  negmod  12135  modadd2mod  12137  modmul1  12140  modaddmulmod  12153  moddi  12154  modsubdir  12155  modirr  12157  expgt1  12307  mulexpz  12309  leexp1a  12328  expubnd  12330  sqgt0  12340  lt2sq  12345  le2sq  12346  sqge0  12348  sumsqeq0  12350  sqlecan  12378  bernneq  12395  bernneq2  12396  expnbnd  12398  digit2  12402  digit1  12403  swrdccatin2  12828  swrdccat3blem  12836  cshweqrep  12905  crre  13156  crim  13157  reim0  13160  mulre  13163  rere  13164  remul2  13172  rediv  13173  immul2  13179  imdiv  13180  cjre  13181  cjreim  13202  rennim  13281  resqrex  13293  resqreu  13295  resqrtcl  13296  resqrtthlem  13297  sqrtneglem  13309  sqrtneg  13310  absreimsq  13334  absreim  13335  absnid  13340  leabs  13341  absre  13343  absresq  13344  sqabs  13349  max0add  13352  absz  13353  absdiflt  13359  absdifle  13360  lenegsq  13362  abssuble0  13370  absmax  13371  rddif  13382  absrdbnd  13383  o1rlimmul  13660  caurcvg2  13722  reefcl  14119  efgt0  14135  reeftlcl  14140  resinval  14167  recosval  14168  resin4p  14170  recos4p  14171  resincl  14172  recoscl  14173  retancl  14174  resinhcl  14188  rpcoshcl  14189  retanhcl  14191  tanhlt1  14192  tanhbnd  14193  efieq  14195  sinbnd  14212  cosbnd  14213  absefi  14228  odd2np1  14343  bezoutlem1  14477  xrsdsreclb  18950  remulg  19106  resubdrg  19107  remetdval  21718  bl2ioo  21721  ioo2bl  21722  cnperf  21749  icccvx  21874  tchcph  22104  shft2rab  22339  volsup2  22440  volcn  22441  c1lip1  22826  plyreres  23104  aalioulem3  23155  taylthlem2  23194  reeff1o  23267  reefgim  23270  sincosq1sgn  23318  sincosq2sgn  23319  sincosq3sgn  23320  sincosq4sgn  23321  sinq12gt0  23327  pige3  23337  efif1olem4  23359  efifo  23361  relogrn  23376  logrnaddcl  23389  relogoprlem  23405  advlog  23464  advlogexp  23465  logtayl  23470  recxpcl  23485  rpcxpcl  23486  cxpge0  23493  dvcxp1  23545  logreclem  23564  relogbreexp  23577  relogbcxp  23587  angpieqvd  23622  atanre  23676  basellem9  23878  log2sumbnd  24245  brbtwn2  24781  colinearalglem4  24785  colinearalg  24786  readdsubgo  25926  nvsge0  26137  nmoub3i  26259  nmlnoubi  26282  isblo3i  26287  ipasslem3  26319  ipasslem9  26324  ipasslem11  26326  hmopm  27509  riesz1  27553  leopmuli  27621  leopmul  27622  leopmul2i  27623  leopnmid  27626  nmopleid  27627  cdj1i  27921  cdj3lem1  27922  cdj3i  27929  addltmulALT  27934  rexdiv  28233  xdivid  28235  xdiv0  28236  rmulccn  28573  sgnneg  29199  lediv2aALT  30109  nndivlub  30903  cos2h  31640  tan2h  31641  poimir  31677  mblfinlem2  31682  mblfinlem4  31684  dvtanlemOLD  31695  itg2addnclem  31697  itg2addnclem2  31698  dvasin  31732  areacirclem1  31736  areacirclem2  31737  areacirclem4  31739  areacirclem5  31740  areacirc  31741  expmordi  35501  areaquad  35800  radcnvrat  36300  lhe4.4ex1a  36315  expgrowthi  36319  mulltgt0  36983  refsum2cnlem1  36998  dstregt0  37100  ltaddneg  37117  suplesup  37171  fmul01lt1lem1  37234  lptre2pt  37292  dvcosre  37353  itgsin0pilem1  37395  itgsinexplem1  37399  volioc  37418  stoweidlem7  37436  stoweidlem10  37439  stoweidlem19  37448  stoweidlem34  37464  stoweid  37494  dirker2re  37523  dirkerdenne0  37524  dirkerper  37527  dirkertrigeq  37532  dirkeritg  37533  fourierdlem39  37577  fourierdlem42  37580  fourierdlem47  37585  fourierdlem56  37594  fourierdlem57  37595  fourierdlem58  37596  fourierdlem60  37598  fourierdlem61  37599  fourierdlem73  37611  fourierdlem76  37614  fourierdlem77  37615  fourierdlem92  37630  fourierdlem97  37635  etransclem46  37712  m1mod0mod1  38122  bgoldbtbndlem2  38300  2leaddle2  38402  ltsubsubaddltsub  38406  divlt1lt  39079  flsubz  39090  rege1logbrege0  39139  nn0digval  39181  reseccl  39243  recsccl  39244  recotcl  39245  dpfrac1  39262
  Copyright terms: Public domain W3C validator