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

Theorem recn 9580
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 9547 . 2  |-  RR  C_  CC
21sseli 3482 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   CCcc 9488   RRcr 9489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9547
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  mulid1  9591  recnd  9620  pnfnre  9633  mnfnre  9634  mul02  9756  renegcli  9880  resubcl  9883  ltaddsub2  10028  leaddsub2  10030  leltadd  10037  ltaddpos  10043  ltaddpos2  10044  posdif  10046  lenegcon1  10057  lenegcon2  10058  addge01  10063  addge02  10064  leaddle0  10068  mullt0  10073  recex  10182  ltm1  10383  prodgt02  10389  prodge02  10391  ltmul2  10394  lemul1  10395  lemul2  10396  lemul1a  10397  lemul2a  10398  ltmulgt12  10404  lemulge12  10406  gt0div  10409  ge0div  10410  mulge0b  10413  mulle0b  10414  ltmuldiv2  10417  ltdivmul  10418  ledivmul  10419  ledivmulOLD  10420  ltdivmul2  10421  lt2mul2div  10422  ledivmul2  10423  ledivmul2OLD  10424  lemuldiv2  10426  ltdiv2  10431  ltrec1  10433  lerec2  10434  ledivdiv  10435  lediv2  10436  ltdiv23  10437  lediv23  10438  lediv12a  10439  recp1lt1  10444  ledivp1  10448  infm3lem  10502  supmul  10512  riotaneg  10519  negiso  10520  cju  10533  nnge1  10563  halfpos  10770  lt2halves  10774  addltmul  10775  avgle1  10779  avgle2  10780  avgle  10781  nnrecl  10794  elznn0  10880  elznn  10881  elz2  10882  zmulcl  10913  gtndiv  10941  zeo  10949  uzindOLD  10958  eqreznegel  11171  negn0  11172  supminf  11173  rebtwnz  11185  irradd  11210  irrmul  11211  max0sub  11399  xnegneg  11417  rexsub  11436  xnegid  11439  xaddcom  11441  xaddid1  11442  xnegdi  11444  xaddass  11445  rexmul  11467  xmulasslem3  11482  xadddilem  11490  divelunit  11666  fzonmapblen  11842  flzadd  11933  ltdifltdiv  11940  dfceil2  11942  intfrac2  11959  fldiv2  11962  flpmodeq  11975  mod0  11977  negmod0  11978  modlt  11980  modfrac  11983  flmod  11984  intfrac  11985  modmulnn  11987  modvalp1  11988  modid  11994  modcyc  12005  modcyc2  12006  modadd1  12007  modaddabs  12008  modadd2mod  12011  modmul1  12014  modaddmulmod  12027  moddi  12028  modsubdir  12029  modirr  12031  expgt1  12178  mulexpz  12180  leexp1a  12198  expubnd  12200  sqgt0  12210  lt2sq  12215  le2sq  12216  sqge0  12218  sumsqeq0  12220  sqlecan  12248  bernneq  12266  bernneq2  12267  expnbnd  12269  digit2  12273  digit1  12274  swrdccatin2  12686  swrdccat3blem  12694  cshweqrep  12763  crre  12921  crim  12922  reim0  12925  mulre  12928  rere  12929  remul2  12937  rediv  12938  immul2  12944  imdiv  12945  cjre  12946  cjreim  12967  rennim  13046  resqrex  13058  resqreu  13060  resqrtcl  13061  resqrtthlem  13062  sqrtneglem  13074  sqrtneg  13075  absreimsq  13099  absreim  13100  absnid  13105  leabs  13106  absre  13108  absresq  13109  sqabs  13114  max0add  13117  absz  13118  absdiflt  13124  absdifle  13125  lenegsq  13127  abssuble0  13135  absmax  13136  rddif  13147  absrdbnd  13148  o1rlimmul  13415  caurcvg2  13474  reefcl  13695  efgt0  13710  reeftlcl  13715  resinval  13742  recosval  13743  resin4p  13745  recos4p  13746  resincl  13747  recoscl  13748  retancl  13749  resinhcl  13763  rpcoshcl  13764  retanhcl  13766  tanhlt1  13767  tanhbnd  13768  efieq  13770  sinbnd  13787  cosbnd  13788  absefi  13803  odd2np1  13918  bezoutlem1  14048  xrsdsreclb  18333  remulg  18510  resubdrg  18511  remetdval  21160  bl2ioo  21163  ioo2bl  21164  cnperf  21191  icccvx  21316  tchcph  21546  shft2rab  21785  volsup2  21880  volcn  21881  c1lip1  22264  plyreres  22544  aalioulem3  22595  taylthlem2  22634  reeff1o  22707  reefgim  22710  sincosq1sgn  22756  sincosq2sgn  22757  sincosq3sgn  22758  sincosq4sgn  22759  sinq12gt0  22765  pige3  22775  efif1olem4  22797  efifo  22799  relogrn  22814  logrnaddcl  22827  relogoprlem  22840  advlog  22900  advlogexp  22901  logtayl  22906  recxpcl  22921  rpcxpcl  22922  cxpge0  22929  dvcxp1  22981  logreclem  23015  angpieqvd  23027  atanre  23081  basellem9  23227  log2sumbnd  23594  brbtwn2  24073  colinearalglem4  24077  colinearalg  24078  readdsubgo  25220  nvsge0  25431  nmoub3i  25553  nmlnoubi  25576  isblo3i  25581  ipasslem3  25613  ipasslem9  25618  ipasslem11  25620  hmopm  26805  riesz1  26849  leopmuli  26917  leopmul  26918  leopmul2i  26919  leopnmid  26922  nmopleid  26923  cdj1i  27217  cdj3lem1  27218  cdj3i  27225  addltmulALT  27230  rexdiv  27488  xdivid  27490  xdiv0  27491  rmulccn  27776  sgnneg  28345  lediv2aALT  28909  nndivlub  29891  cos2h  30014  tan2h  30015  mblfinlem2  30020  mblfinlem4  30022  dvtanlem  30032  itg2addnclem  30034  itg2addnclem2  30035  dvasin  30071  areacirclem1  30075  areacirclem2  30076  areacirclem4  30078  areacirclem5  30079  areacirc  30080  expmordi  30851  areaquad  31153  radcnvrat  31164  lhe4.4ex1a  31203  expgrowthi  31207  mulltgt0  31344  refsum2cnlem1  31359  dstregt0  31408  ltaddneg  31429  fmul01lt1lem1  31502  lptre2pt  31550  dvcosre  31606  itgsin0pilem1  31634  itgsinexplem1  31638  volioc  31657  stoweidlem7  31674  stoweidlem10  31677  stoweidlem19  31686  stoweidlem34  31701  stoweid  31730  dirker2re  31759  dirkerdenne0  31760  dirkerper  31763  dirkertrigeq  31768  dirkeritg  31769  fourierdlem39  31813  fourierdlem42  31816  fourierdlem47  31821  fourierdlem56  31830  fourierdlem57  31831  fourierdlem58  31832  fourierdlem60  31834  fourierdlem61  31835  fourierdlem73  31847  fourierdlem76  31850  fourierdlem77  31851  fourierdlem92  31866  fourierdlem97  31871  2leaddle2  32154  ltsubsubaddltsub  32158  reseccl  32857  recsccl  32858  recotcl  32859  dpfrac1  32876  bj-flbi3  34310
  Copyright terms: Public domain W3C validator