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

Theorem recn 9372
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 9339 . 2  |-  RR  C_  CC
21sseli 3352 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9280   RRcr 9281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-resscn 9339
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342
This theorem is referenced by:  mulid1  9383  recnd  9412  pnfnre  9425  mnfnre  9426  mul02  9547  renegcli  9670  resubcl  9673  ltaddsub2  9814  leaddsub2  9816  leltadd  9823  ltaddpos  9829  ltaddpos2  9830  posdif  9832  lenegcon1  9843  lenegcon2  9844  addge01  9849  addge02  9850  leaddle0  9854  mullt0  9859  recex  9968  ltm1  10169  prodgt02  10175  prodge02  10177  ltmul2  10180  lemul1  10181  lemul2  10182  lemul1a  10183  lemul2a  10184  ltmulgt12  10190  lemulge12  10192  gt0div  10195  ge0div  10196  mulge0b  10199  mulle0b  10200  ltmuldiv2  10203  ltdivmul  10204  ledivmul  10205  ledivmulOLD  10206  ltdivmul2  10207  lt2mul2div  10208  ledivmul2  10209  ledivmul2OLD  10210  lemuldiv2  10212  ltdiv2  10217  ltrec1  10219  lerec2  10220  ledivdiv  10221  lediv2  10222  ltdiv23  10223  lediv23  10224  lediv12a  10225  recp1lt1  10230  ledivp1  10234  infm3lem  10288  supmul  10298  riotaneg  10305  negiso  10306  cju  10318  nnge1  10348  halfpos  10555  lt2halves  10559  addltmul  10560  avgle1  10564  avgle2  10565  avgle  10566  nnrecl  10577  elznn0  10661  elznn  10662  elz2  10663  zmulcl  10693  gtndiv  10719  zeo  10727  uzindOLD  10736  eqreznegel  10940  negn0  10941  supminf  10942  rebtwnz  10952  irradd  10977  irrmul  10978  max0sub  11166  xnegneg  11184  rexsub  11203  xnegid  11206  xaddcom  11208  xaddid1  11209  xnegdi  11211  xaddass  11212  rexmul  11234  xmulasslem3  11249  xadddilem  11257  divelunit  11427  fzonmapblen  11592  flzadd  11671  ltdifltdiv  11678  dfceil2  11680  intfrac2  11697  fldiv2  11700  flpmodeq  11713  mod0  11715  negmod0  11716  modlt  11718  modfrac  11721  flmod  11722  intfrac  11723  modmulnn  11725  modvalp1  11726  modid  11732  modcyc  11743  modcyc2  11744  modadd1  11745  modaddabs  11746  modadd2mod  11749  modmul1  11752  modaddmulmod  11765  moddi  11766  modsubdir  11767  modirr  11769  expgt1  11902  mulexpz  11904  leexp1a  11922  expubnd  11924  sqgt0  11934  lt2sq  11939  le2sq  11940  sqge0  11942  sumsqeq0  11944  sqlecan  11972  bernneq  11990  bernneq2  11991  expnbnd  11993  digit2  11997  digit1  11998  swrdccatin2  12378  swrdccat3blem  12386  cshweqrep  12455  crre  12603  crim  12604  reim0  12607  mulre  12610  rere  12611  remul2  12619  rediv  12620  immul2  12626  imdiv  12627  cjre  12628  cjreim  12649  rennim  12728  resqrex  12740  resqreu  12742  resqrcl  12743  resqrthlem  12744  sqrneglem  12756  sqrneg  12757  absreimsq  12781  absreim  12782  absnid  12787  leabs  12788  absre  12790  absresq  12791  sqabs  12796  max0add  12799  absz  12800  absdiflt  12805  absdifle  12806  lenegsq  12808  abssuble0  12816  absmax  12817  rddif  12828  absrdbnd  12829  o1rlimmul  13096  caurcvg2  13155  reefcl  13372  efgt0  13387  reeftlcl  13392  resinval  13419  recosval  13420  resin4p  13422  recos4p  13423  resincl  13424  recoscl  13425  retancl  13426  resinhcl  13440  rpcoshcl  13441  retanhcl  13443  tanhlt1  13444  tanhbnd  13445  efieq  13447  sinbnd  13464  cosbnd  13465  absefi  13480  odd2np1  13592  bezoutlem1  13722  xrsdsreclb  17860  remulg  18037  resubdrg  18038  remetdval  20366  bl2ioo  20369  ioo2bl  20370  cnperf  20397  icccvx  20522  tchcph  20752  shft2rab  20991  volsup2  21085  volcn  21086  c1lip1  21469  plyreres  21749  aalioulem3  21800  taylthlem2  21839  reeff1o  21912  reefgim  21915  sincosq1sgn  21960  sincosq2sgn  21961  sincosq3sgn  21962  sincosq4sgn  21963  sinq12gt0  21969  pige3  21979  efif1olem4  22001  efifo  22003  relogrn  22013  logrnaddcl  22026  relogoprlem  22039  advlog  22099  advlogexp  22100  logtayl  22105  recxpcl  22120  rpcxpcl  22121  cxpge0  22128  dvcxp1  22180  logreclem  22214  angpieqvd  22226  atanre  22280  basellem9  22426  log2sumbnd  22793  brbtwn2  23151  colinearalglem4  23155  colinearalg  23156  readdsubgo  23840  nvsge0  24051  nmoub3i  24173  nmlnoubi  24196  isblo3i  24201  ipasslem3  24233  ipasslem9  24238  ipasslem11  24240  hmopm  25425  riesz1  25469  leopmuli  25537  leopmul  25538  leopmul2i  25539  leopnmid  25542  nmopleid  25543  cdj1i  25837  cdj3lem1  25838  cdj3i  25845  addltmulALT  25850  rexdiv  26101  xdivid  26103  xdiv0  26104  rmulccn  26358  sgnneg  26923  lediv2aALT  27322  nndivlub  28304  cos2h  28423  tan2h  28424  mblfinlem2  28429  mblfinlem4  28431  dvtanlem  28441  itg2addnclem  28443  itg2addnclem2  28444  dvasin  28480  areacirclem1  28484  areacirclem2  28485  areacirclem4  28487  areacirclem5  28488  areacirc  28489  expmordi  29288  lhe4.4ex1a  29603  expgrowthi  29607  mulltgt0  29744  refsum2cnlem1  29759  fmul01lt1lem1  29765  dvcosre  29788  itgsin0pilem1  29790  itgsinexplem1  29794  stoweidlem7  29802  stoweidlem10  29805  stoweidlem19  29814  stoweidlem34  29829  stoweid  29858  2leaddle2  30175  ltsubsubaddltsub  30467  reseccl  31088  recsccl  31089  recotcl  31090  dpfrac1  31107  bj-flbi3  32527
  Copyright terms: Public domain W3C validator