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

Theorem recn 9368
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 9335 . 2  |-  RR  C_  CC
21sseli 3349 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   CCcc 9276   RRcr 9277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-resscn 9335
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339
This theorem is referenced by:  mulid1  9379  recnd  9408  pnfnre  9421  mnfnre  9422  mul02  9543  renegcli  9666  resubcl  9669  ltaddsub2  9810  leaddsub2  9812  leltadd  9819  ltaddpos  9825  ltaddpos2  9826  posdif  9828  lenegcon1  9839  lenegcon2  9840  addge01  9845  addge02  9846  leaddle0  9850  mullt0  9855  recex  9964  ltm1  10165  prodgt02  10171  prodge02  10173  ltmul2  10176  lemul1  10177  lemul2  10178  lemul1a  10179  lemul2a  10180  ltmulgt12  10186  lemulge12  10188  gt0div  10191  ge0div  10192  mulge0b  10195  mulle0b  10196  ltmuldiv2  10199  ltdivmul  10200  ledivmul  10201  ledivmulOLD  10202  ltdivmul2  10203  lt2mul2div  10204  ledivmul2  10205  ledivmul2OLD  10206  lemuldiv2  10208  ltdiv2  10213  ltrec1  10215  lerec2  10216  ledivdiv  10217  lediv2  10218  ltdiv23  10219  lediv23  10220  lediv12a  10221  recp1lt1  10226  ledivp1  10230  infm3lem  10284  supmul  10294  riotaneg  10301  negiso  10302  cju  10314  nnge1  10344  halfpos  10551  lt2halves  10555  addltmul  10556  avgle1  10560  avgle2  10561  avgle  10562  nnrecl  10573  elznn0  10657  elznn  10658  elz2  10659  zmulcl  10689  gtndiv  10715  zeo  10723  uzindOLD  10732  eqreznegel  10936  negn0  10937  supminf  10938  rebtwnz  10948  irradd  10973  irrmul  10974  max0sub  11162  xnegneg  11180  rexsub  11199  xnegid  11202  xaddcom  11204  xaddid1  11205  xnegdi  11207  xaddass  11208  rexmul  11230  xmulasslem3  11245  xadddilem  11253  divelunit  11423  fzonmapblen  11588  flzadd  11667  ltdifltdiv  11674  dfceil2  11676  intfrac2  11693  fldiv2  11696  flpmodeq  11709  mod0  11711  negmod0  11712  modlt  11714  modfrac  11717  flmod  11718  intfrac  11719  modmulnn  11721  modvalp1  11722  modid  11728  modcyc  11739  modcyc2  11740  modadd1  11741  modaddabs  11742  modadd2mod  11745  modmul1  11748  modaddmulmod  11761  moddi  11762  modsubdir  11763  modirr  11765  expgt1  11898  mulexpz  11900  leexp1a  11918  expubnd  11920  sqgt0  11930  lt2sq  11935  le2sq  11936  sqge0  11938  sumsqeq0  11940  sqlecan  11968  bernneq  11986  bernneq2  11987  expnbnd  11989  digit2  11993  digit1  11994  swrdccatin2  12374  swrdccat3blem  12382  cshweqrep  12451  crre  12599  crim  12600  reim0  12603  mulre  12606  rere  12607  remul2  12615  rediv  12616  immul2  12622  imdiv  12623  cjre  12624  cjreim  12645  rennim  12724  resqrex  12736  resqreu  12738  resqrcl  12739  resqrthlem  12740  sqrneglem  12752  sqrneg  12753  absreimsq  12777  absreim  12778  absnid  12783  leabs  12784  absre  12786  absresq  12787  sqabs  12792  max0add  12795  absz  12796  absdiflt  12801  absdifle  12802  lenegsq  12804  abssuble0  12812  absmax  12813  rddif  12824  absrdbnd  12825  o1rlimmul  13092  caurcvg2  13151  reefcl  13368  efgt0  13383  reeftlcl  13388  resinval  13415  recosval  13416  resin4p  13418  recos4p  13419  resincl  13420  recoscl  13421  retancl  13422  resinhcl  13436  rpcoshcl  13437  retanhcl  13439  tanhlt1  13440  tanhbnd  13441  efieq  13443  sinbnd  13460  cosbnd  13461  absefi  13476  odd2np1  13588  bezoutlem1  13718  xrsdsreclb  17760  remulg  17937  resubdrg  17938  remetdval  20266  bl2ioo  20269  ioo2bl  20270  cnperf  20297  icccvx  20422  tchcph  20652  shft2rab  20891  volsup2  20985  volcn  20986  c1lip1  21369  plyreres  21692  aalioulem3  21743  taylthlem2  21782  reeff1o  21855  reefgim  21858  sincosq1sgn  21903  sincosq2sgn  21904  sincosq3sgn  21905  sincosq4sgn  21906  sinq12gt0  21912  pige3  21922  efif1olem4  21944  efifo  21946  relogrn  21956  logrnaddcl  21969  relogoprlem  21982  advlog  22042  advlogexp  22043  logtayl  22048  recxpcl  22063  rpcxpcl  22064  cxpge0  22071  dvcxp1  22123  logreclem  22157  angpieqvd  22169  atanre  22223  basellem9  22369  log2sumbnd  22736  brbtwn2  23070  colinearalglem4  23074  colinearalg  23075  readdsubgo  23759  nvsge0  23970  nmoub3i  24092  nmlnoubi  24115  isblo3i  24120  ipasslem3  24152  ipasslem9  24157  ipasslem11  24159  hmopm  25344  riesz1  25388  leopmuli  25456  leopmul  25457  leopmul2i  25458  leopnmid  25461  nmopleid  25462  cdj1i  25756  cdj3lem1  25757  cdj3i  25764  addltmulALT  25769  rexdiv  26018  xdivid  26020  xdiv0  26021  rmulccn  26278  sgnneg  26837  lediv2aALT  27235  nndivlub  28218  cos2h  28332  tan2h  28333  mblfinlem2  28338  mblfinlem4  28340  dvtanlem  28350  itg2addnclem  28352  itg2addnclem2  28353  dvasin  28389  areacirclem1  28393  areacirclem2  28394  areacirclem4  28396  areacirclem5  28397  areacirc  28398  expmordi  29197  lhe4.4ex1a  29512  expgrowthi  29516  mulltgt0  29653  refsum2cnlem1  29668  fmul01lt1lem1  29674  dvcosre  29697  itgsin0pilem1  29699  itgsinexplem1  29703  stoweidlem7  29711  stoweidlem10  29714  stoweidlem19  29723  stoweidlem34  29738  stoweid  29767  2leaddle2  30084  ltsubsubaddltsub  30376  reseccl  30912  recsccl  30913  recotcl  30914  dpfrac1  30931  bj-flbi3  32222
  Copyright terms: Public domain W3C validator