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

Theorem recni 8849
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 8794 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3177 1  |-  A  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   CCcc 8735   RRcr 8736
This theorem is referenced by:  renegcli  9108  resubcli  9109  recgt0ii  9662  ledivp1i  9682  ltdivp1i  9683  nncni  9756  2cn  9816  3cn  9818  4cn  9820  5p2e7  9860  5p3e8  9861  5p4e9  9862  5p5e10  9863  6p2e8  9864  6p3e9  9865  6p4e10  9866  7p2e9  9867  7p3e10  9868  8p2e10  9869  5t2e10  9875  8th4div3  9935  halfpm6th  9936  nn0cni  9977  numltc  10144  sqge0i  11191  lt2sqi  11192  le2sqi  11193  sq11i  11194  crreczi  11226  faclbnd4lem1  11306  rddif  11824  sqrmsq2i  11871  abs3lemi  11893  geo2sum  12329  geo2lim  12331  0.999...  12337  efcllem  12359  efi4p  12417  ef01bndlem  12464  cos2bnd  12468  sin4lt0  12475  eirrlem  12482  rpnnen2lem3  12495  rpnnen2lem9  12501  rpnnen2lem11  12503  dvdslelem  12573  divalglem1  12593  divalglem2  12594  divalglem5  12596  divalglem6  12597  divalglem9  12600  prmreclem6  12968  modsubi  13087  prmlem1  13109  pcoass  18522  iscmet3lem3  18716  mbfi1fseqlem6  19075  aaliou3lem2  19723  aaliou3lem7  19729  sinhalfpilem  19834  cosneghalfpi  19838  efhalfpi  19839  cospi  19840  efipi  19841  sin2pi  19843  cos2pi  19844  ef2pi  19845  ef2kpi  19846  efper  19847  sinperlem  19848  sin2kpi  19851  cos2kpi  19852  sin2pim  19853  cos2pim  19854  sinmpi  19855  cosmpi  19856  sinppi  19857  cosppi  19858  efimpi  19859  sinhalfpip  19860  sinhalfpim  19861  coshalfpip  19862  coshalfpim  19863  ptolemy  19864  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  sinq12gt0  19875  sinq34lt0t  19877  cosq14gt0  19878  cosq14ge0  19879  sincosq1eq  19880  sincos4thpi  19881  tan4thpi  19882  sincos6thpi  19883  sincos3rdpi  19884  pige3  19885  abssinper  19886  sinkpi  19887  coskpi  19888  sineq0  19889  coseq1  19890  efeq1  19891  cosne0  19892  sinord  19896  resinf1o  19898  efif1olem2  19905  efif1olem4  19907  efifo  19909  eff1o  19911  logneg  19941  logm1  19942  eflogeq  19955  argimgt0  19966  logimul  19968  logneg2  19969  logf1o2  19997  ecxp  20020  cxpsqrlem  20049  cxpsqr  20050  abscxpbnd  20093  root1eq1  20095  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  pythag  20115  1cubrlem  20137  quartlem3  20155  acosf  20170  acosneg  20183  asinsin  20188  acoscos  20189  asin1  20190  acos1  20191  reasinsin  20192  acosbnd  20196  sinacos  20201  atanlogsublem  20211  atanlogsub  20212  atantan  20219  atanbndlem  20221  atanbnd  20222  atan1  20224  log2tlbnd  20241  log2ublem1  20242  birthday  20249  basellem1  20318  basellem8  20325  basellem9  20326  cht2  20410  mumullem2  20418  chtublem  20450  chtub  20451  bposlem6  20528  bposlem7  20529  bposlem8  20530  bposlem9  20531  lgsdir2lem1  20562  lgsdir2lem5  20566  chebbnd1lem3  20620  chebbnd1  20621  chto1ub  20625  mulogsumlem  20680  mulog2sumlem1  20683  mulog2sumlem2  20684  mulog2sumlem3  20685  pntibndlem3  20741  nmblolbii  21377  ip0i  21403  ip1ilem  21404  ipasslem10  21417  siilem1  21429  siii  21431  normlem1  21689  normlem3  21691  normlem5  21693  normlem6  21694  norm-ii-i  21716  normsubi  21720  norm3adifii  21727  norm3lem  21728  normpar2i  21735  bcsiALT  21758  pjneli  22302  lnophmlem2  22597  nmbdoplbi  22604  nmcoplbi  22608  nmophmi  22611  nmbdfnlbi  22629  nmcfnlbi  22632  cnlnadjlem2  22648  cnlnadjlem7  22653  nmopadjlem  22669  nmopcoi  22675  nmopcoadji  22681  nmopcoadj0i  22683  unierri  22684  opsqrlem1  22720  ballotlem2  23047  log2le1  23409  subfaclim  23719  subfacval3  23720  circum  24007  bpoly2  24792  bpoly3  24793  bpoly4  24794  dvreacos  24924  areacirc  24931  cntrset  25602  fdc  26455  cntotbnd  26520  rmspecsqrnq  26991  proot1ex  27520  itgsinexplem1  27748  stoweidlem13  27762  wallispilem4  27817  stirlinglem3  27825  stirlinglem4  27826  stirlinglem13  27835  stirlinglem15  27837  dpfrac1  28242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator