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

Theorem recni 9519
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1  |-  A  e.  RR
Assertion
Ref Expression
recni  |-  A  e.  CC

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 9460 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3414 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   CCcc 9401   RRcr 9402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-resscn 9460
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  renegcli  9793  resubcli  9794  recgt0ii  10367  ledivp1i  10387  ltdivp1i  10388  nncni  10462  2cn  10523  3cn  10527  4cn  10530  5cn  10532  6cn  10534  7cn  10536  8cn  10538  9cn  10540  8th4div3  10676  nn0cni  10724  numltc  10915  sqge0i  12158  lt2sqi  12159  le2sqi  12160  sq11i  12161  crreczi  12193  faclbnd4lem1  12273  sqrtmsq2i  13222  abs3lemi  13244  0.999...  13692  ef01bndlem  13921  sin4lt0  13932  eirrlem  13939  rpnnen2lem3  13952  rpnnen2lem9  13958  rpnnen2lem11  13960  dvdslelem  14032  divalglem1  14054  divalglem2  14055  divalglem5  14057  divalglem6  14058  divalglem9  14061  prmreclem6  14441  modsubi  14560  pcoass  21609  aaliou3lem7  22830  picn  22937  sinhalfpilem  22941  cosneghalfpi  22948  sincosq1sgn  22976  sincosq2sgn  22977  sincosq3sgn  22978  sincosq4sgn  22979  sincos4thpi  22991  tan4thpi  22992  sincos6thpi  22993  pige3  22995  cosne0  23002  sinord  23006  resinf1o  23008  efif1olem2  23015  efif1olem4  23017  efifo  23019  logimul  23086  ecxp  23141  cxpsqrtlem  23170  elogb  23228  logblog  23250  ang180lem1  23259  ang180lem2  23260  1cubrlem  23288  quartlem3  23306  asinsin  23339  acoscos  23340  asin1  23341  reasinsin  23343  acosbnd  23347  atanlogsublem  23362  atanbnd  23373  atan1  23375  log2tlbnd  23392  log2ublem1  23393  log2le1  23397  birthday  23401  basellem8  23478  basellem9  23479  cht2  23563  mumullem2  23571  chtublem  23603  chtub  23604  bposlem6  23681  bposlem7  23682  bposlem8  23683  bposlem9  23684  chebbnd1lem3  23773  chebbnd1  23774  chto1ub  23778  mulogsumlem  23833  mulog2sumlem1  23836  mulog2sumlem2  23837  mulog2sumlem3  23838  pntibndlem3  23894  nmblolbii  25831  ip0i  25857  ip1ilem  25858  ipasslem10  25871  siilem1  25883  siii  25885  normlem1  26144  normlem3  26146  normlem5  26148  normlem6  26149  norm-ii-i  26171  normsubi  26175  norm3adifii  26182  norm3lem  26183  normpar2i  26190  bcsiALT  26213  pjneli  26758  lnophmlem2  27052  nmbdoplbi  27059  nmcoplbi  27063  nmophmi  27066  nmbdfnlbi  27084  nmcfnlbi  27087  cnlnadjlem2  27103  cnlnadjlem7  27108  nmopadjlem  27124  nmopcoi  27130  nmopcoadji  27136  nmopcoadj0i  27138  unierri  27139  opsqrlem1  27175  subfaclim  28821  subfacval3  28822  problem2  29209  problem3  29210  problem4  29211  problem5  29212  circum  29229  logi  29287  iexpire  29288  bpoly4  29974  dvtanlemOLD  30230  dvacos  30270  fdc  30404  rmspecsqrtnq  31007  arearect  31351  areaquad  31352  wallispilem2  32014  stirlinglem3  32024  stirlinglem4  32025  stirlinglem13  32034  stirlinglem15  32036  dirkerper  32044  fourierdlem24  32079  fourierdlem103  32158  fourierdlem104  32159  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  etransclem18  32201  etransclem23  32206  etransclem46  32229  etransclem47  32230  etransclem48  32231  etransc  32232  dpfrac1  33502  sineq0ALT  34084  taupilem1  38109
  Copyright terms: Public domain W3C validator