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

Theorem recn 9069
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 9036 . 2  |-  RR  C_  CC
21sseli 3336 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8977   RRcr 8978
This theorem is referenced by:  mulid1  9077  recnd  9103  pnfnre  9116  mnfnre  9117  mul02  9233  renegcli  9351  resubcl  9354  ltaddsub2  9492  leaddsub2  9494  leltadd  9501  ltaddpos  9507  ltaddpos2  9508  posdif  9510  lenegcon1  9521  lenegcon2  9522  addge01  9527  addge02  9528  mullt0  9536  recex  9643  ltm1  9839  prodgt02  9845  prodge02  9847  ltmul2  9850  lemul1  9851  lemul2  9852  lemul1a  9853  lemul2a  9854  ltmulgt12  9860  lemulge12  9862  gt0div  9865  ge0div  9866  ltmuldiv2  9870  ltdivmul  9871  ledivmul  9872  ledivmulOLD  9873  ltdivmul2  9874  lt2mul2div  9875  ledivmul2  9876  ledivmul2OLD  9877  lemuldiv2  9879  ltdiv2  9884  ltrec1  9886  lerec2  9887  ledivdiv  9888  lediv2  9889  ltdiv23  9890  lediv23  9891  lediv12a  9892  recp1lt1  9897  ledivp1  9901  infm3lem  9955  supmul  9965  riotaneg  9972  negiso  9973  cju  9985  nnge1  10015  halfpos  10187  lt2halves  10191  addltmul  10192  avgle1  10196  avgle2  10197  avgle  10198  nnrecl  10208  elznn0  10285  elznn  10286  elz2  10287  zmulcl  10313  gtndiv  10336  zeo  10344  uzindOLD  10353  eqreznegel  10550  negn0  10551  supminf  10552  rebtwnz  10562  irradd  10587  irrmul  10588  max0sub  10771  xnegneg  10789  rexsub  10808  xnegid  10811  xaddcom  10813  xaddid1  10814  xnegdi  10816  xaddass  10817  rexmul  10839  xmulasslem3  10854  xadddilem  10862  flzadd  11216  intfrac2  11227  fldiv2  11230  mod0  11243  negmod0  11244  modlt  11246  modfrac  11249  flmod  11250  intfrac  11251  modmulnn  11253  modid  11258  modcyc  11264  modcyc2  11265  modadd1  11266  modmul1  11267  moddi  11272  modsubdir  11273  modirr  11274  expgt1  11406  mulexpz  11408  leexp1a  11426  expubnd  11428  sqgt0  11438  lt2sq  11443  le2sq  11444  sqge0  11446  sumsqeq0  11448  sqlecan  11475  bernneq  11493  bernneq2  11494  expnbnd  11496  digit2  11500  digit1  11501  crre  11907  crim  11908  reim0  11911  mulre  11914  rere  11915  remul2  11923  rediv  11924  immul2  11930  imdiv  11931  cjre  11932  cjreim  11953  rennim  12032  resqrex  12044  resqreu  12046  resqrcl  12047  resqrthlem  12048  sqrneglem  12060  sqrneg  12061  absreimsq  12085  absreim  12086  absnid  12091  leabs  12092  absre  12094  absresq  12095  sqabs  12100  max0add  12103  absz  12104  absdiflt  12109  absdifle  12110  lenegsq  12112  abssuble0  12120  absmax  12121  rddif  12132  absrdbnd  12133  o1rlimmul  12400  caurcvg2  12459  reefcl  12677  efgt0  12692  reeftlcl  12697  resinval  12724  recosval  12725  resin4p  12727  recos4p  12728  resincl  12729  recoscl  12730  retancl  12731  resinhcl  12745  rpcoshcl  12746  retanhcl  12748  tanhlt1  12749  tanhbnd  12750  efieq  12752  sinbnd  12769  cosbnd  12770  absefi  12785  odd2np1  12896  bezoutlem1  13026  xrsdsreclb  16733  resubdrg  16738  remetdval  18808  bl2ioo  18811  ioo2bl  18812  cnperf  18839  icccvx  18963  tchcph  19182  shft2rab  19392  volsup2  19485  volcn  19486  c1lip1  19869  plyreres  20188  aalioulem3  20239  taylthlem2  20278  reeff1o  20351  reefgim  20354  sincosq1sgn  20394  sincosq2sgn  20395  sincosq3sgn  20396  sincosq4sgn  20397  sinq12gt0  20403  pige3  20413  efif1olem4  20435  efifo  20437  relogrn  20447  logrnaddcl  20460  relogoprlem  20473  advlog  20533  advlogexp  20534  logtayl  20539  recxpcl  20554  rpcxpcl  20555  cxpge0  20562  dvcxp1  20614  logreclem  20648  angpieqvd  20660  atanre  20713  basellem9  20859  log2sumbnd  21226  readdsubgo  21929  nvsge0  22140  nmoub3i  22262  nmlnoubi  22285  isblo3i  22290  ipasslem3  22322  ipasslem9  22327  ipasslem11  22329  hmopm  23512  riesz1  23556  leopmuli  23624  leopmul  23625  leopmul2i  23626  leopnmid  23629  nmopleid  23630  cdj1i  23924  cdj3lem1  23925  cdj3i  23932  addltmulALT  23937  rexdiv  24160  xdivid  24162  xdiv0  24163  remulg  24258  rmulccn  24302  modaddabs  25103  lediv2aALT  25105  divelunit  25173  mulge0b  25179  mulle0b  25180  brbtwn2  25792  colinearalglem4  25796  colinearalg  25797  nndivlub  26156  mblfinlem  26190  mblfinlem3  26192  itg2addnclem  26202  itg2addnclem2  26203  dvreasin  26226  areacirclem2  26228  areacirclem3  26229  areacirclem4  26230  areacirclem5  26232  areacirclem6  26233  areacirc  26234  expmordi  26947  lhe4.4ex1a  27461  expgrowthi  27465  mulltgt0  27607  refsum2cnlem1  27622  fmul01lt1lem1  27628  dvcosre  27655  itgsin0pilem1  27658  itgsinexplem1  27662  stoweidlem7  27670  stoweidlem10  27673  stoweidlem19  27682  stoweidlem34  27697  stoweid  27726  fzonmapblen  28046  ltdifltdiv  28054  flpmodeq  28056  modvalp1  28057  modadd2mod  28060  modaddmulmod  28064  shwrdeqrep  28160  reseccl  28354  recsccl  28355  recotcl  28356  dpfrac1  28373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9036
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator