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

Theorem recn 9642
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 9609 . 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 1873   CCcc 9550   RRcr 9551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-resscn 9609
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3449  df-ss 3456
This theorem is referenced by:  mulid1  9653  recnd  9682  pnfnre  9695  mnfnre  9696  mul02  9824  renegcli  9948  resubcl  9951  negn0  10061  negf1o  10062  ltaddsub2  10102  leaddsub2  10104  leltadd  10111  ltaddpos  10117  ltaddpos2  10118  posdif  10120  lenegcon1  10131  lenegcon2  10132  addge01  10137  addge02  10138  leaddle0  10142  mullt0  10146  recex  10257  ltm1  10458  prodgt02  10464  prodge02  10466  ltmul2  10469  lemul1  10470  lemul2  10471  lemul1a  10472  lemul2a  10473  ltmulgt12  10479  lemulge12  10481  gt0div  10484  ge0div  10485  mulge0b  10488  mulle0b  10489  ltmuldiv2  10492  ltdivmul  10493  ledivmul  10494  ltdivmul2  10495  lt2mul2div  10496  ledivmul2  10497  ledivmul2OLD  10498  lemuldiv2  10500  ltdiv2  10505  ltrec1  10506  lerec2  10507  ledivdiv  10508  lediv2  10509  ltdiv23  10510  lediv23  10511  lediv12a  10512  recp1lt1  10517  ledivp1  10521  negfi  10567  fiminre  10568  infm3lem  10580  supmul  10592  riotaneg  10599  negiso  10600  cju  10618  nnge1  10648  halfpos  10856  lt2halves  10860  addltmul  10861  avgle1  10865  avgle2  10866  avgle  10867  nnrecl  10880  elznn0  10965  elznn  10966  elz2  10967  zmulcl  10998  gtndiv  11026  zeo  11034  eqreznegel  11262  supminf  11263  supminfOLD  11264  rebtwnz  11276  irradd  11301  irrmul  11302  max0sub  11502  xnegneg  11520  rexsub  11539  xnegid  11542  xaddcom  11544  xaddid1  11545  xnegdi  11547  xaddass  11548  rexmul  11570  xmulasslem3  11585  xadddilem  11593  divelunit  11787  fzonmapblen  11974  ico01fl0  12065  flzadd  12071  ltdifltdiv  12078  dfceil2  12080  intfrac2  12097  fldiv2  12100  flpmodeq  12113  mod0  12115  negmod0  12117  modlt  12119  modfrac  12122  flmod  12123  intfrac  12124  modmulnn  12126  modvalp1  12127  modid  12133  modcyc  12144  modcyc2  12145  modadd1  12146  modaddabs  12147  muladdmodid  12149  negmod  12150  modadd2mod  12152  modmul1  12155  modaddmulmod  12168  moddi  12169  modsubdir  12170  modirr  12172  expgt1  12322  mulexpz  12324  leexp1a  12343  expubnd  12345  sqgt0  12355  lt2sq  12360  le2sq  12361  sqge0  12363  sumsqeq0  12365  sqlecan  12393  bernneq  12410  bernneq2  12411  expnbnd  12413  digit2  12417  digit1  12418  swrdccatin2  12851  swrdccat3blem  12859  cshweqrep  12928  crre  13183  crim  13184  reim0  13187  mulre  13190  rere  13191  remul2  13199  rediv  13200  immul2  13206  imdiv  13207  cjre  13208  cjreim  13229  rennim  13308  resqrex  13320  resqreu  13322  resqrtcl  13323  resqrtthlem  13324  sqrtneglem  13336  sqrtneg  13337  absreimsq  13361  absreim  13362  absnid  13367  leabs  13368  absre  13370  absresq  13371  sqabs  13376  max0add  13379  absz  13380  absdiflt  13386  absdifle  13387  lenegsq  13389  abssuble0  13397  absmax  13398  rddif  13409  absrdbnd  13410  o1rlimmul  13687  caurcvg2  13749  reefcl  14146  efgt0  14162  reeftlcl  14167  resinval  14194  recosval  14195  resin4p  14197  recos4p  14198  resincl  14199  recoscl  14200  retancl  14201  resinhcl  14215  rpcoshcl  14216  retanhcl  14218  tanhlt1  14219  tanhbnd  14220  efieq  14222  sinbnd  14239  cosbnd  14240  absefi  14255  odd2np1  14370  bezoutlem1  14508  xrsdsreclb  19020  remulg  19179  resubdrg  19180  remetdval  21811  bl2ioo  21814  ioo2bl  21815  cnperf  21842  icccvx  21982  tchcph  22215  shft2rab  22465  volsup2  22567  volcn  22568  c1lip1  22953  plyreres  23240  aalioulem3  23294  taylthlem2  23333  reeff1o  23406  reefgim  23409  sincosq1sgn  23457  sincosq2sgn  23458  sincosq3sgn  23459  sincosq4sgn  23460  sinq12gt0  23466  pige3  23476  efif1olem4  23498  efifo  23500  relogrn  23515  logrnaddcl  23528  relogoprlem  23544  advlog  23603  advlogexp  23604  logtayl  23609  recxpcl  23624  rpcxpcl  23625  cxpge0  23632  dvcxp1  23684  logreclem  23703  relogbreexp  23716  relogbcxp  23726  angpieqvd  23761  atanre  23815  basellem9  24019  log2sumbnd  24386  brbtwn2  24939  colinearalglem4  24943  colinearalg  24944  readdsubgo  26085  nvsge0  26296  nmoub3i  26418  nmlnoubi  26441  isblo3i  26446  ipasslem3  26478  ipasslem9  26483  ipasslem11  26485  hmopm  27678  riesz1  27722  leopmuli  27790  leopmul  27791  leopmul2i  27792  leopnmid  27795  nmopleid  27796  cdj1i  28090  cdj3lem1  28091  cdj3i  28098  addltmulALT  28103  rexdiv  28408  xdivid  28410  xdiv0  28411  rmulccn  28748  sgnneg  29425  lediv2aALT  30335  nndivlub  31129  cos2h  31906  tan2h  31907  poimir  31943  mblfinlem2  31948  mblfinlem4  31950  dvtanlemOLD  31961  itg2addnclem  31963  itg2addnclem2  31964  dvasin  31998  areacirclem1  32002  areacirclem2  32003  areacirclem4  32005  areacirclem5  32006  areacirc  32007  expmordi  35771  areaquad  36077  radcnvrat  36639  lhe4.4ex1a  36654  expgrowthi  36658  mulltgt0  37322  refsum2cnlem1  37337  dstregt0  37451  ltaddneg  37468  suplesup  37522  fmul01lt1lem1  37608  lptre2pt  37666  dvcosre  37727  itgsin0pilem1  37772  itgsinexplem1  37776  volioc  37795  stoweidlem7  37813  stoweidlem10  37816  stoweidlem19  37825  stoweidlem34  37841  stoweid  37871  dirker2re  37900  dirkerdenne0  37901  dirkerper  37904  dirkertrigeq  37909  dirkeritg  37910  fourierdlem39  37955  fourierdlem42  37958  fourierdlem42OLD  37959  fourierdlem47  37963  fourierdlem56  37972  fourierdlem57  37973  fourierdlem58  37974  fourierdlem60  37976  fourierdlem61  37977  fourierdlem73  37989  fourierdlem76  37992  fourierdlem77  37993  fourierdlem92  38008  fourierdlem97  38013  etransclem46  38091  volico  38273  m1mod0mod1  38599  bgoldbtbndlem2  38777  2leaddle2  38903  ltsubsubaddltsub  38907  divlt1lt  39929  flsubz  39939  rege1logbrege0  39988  nn0digval  40030  reseccl  40092  recsccl  40093  recotcl  40094  dpfrac1  40111
  Copyright terms: Public domain W3C validator