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

Theorem rpcn 11100
Description: A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
Assertion
Ref Expression
rpcn  |-  ( A  e.  RR+  ->  A  e.  CC )

Proof of Theorem rpcn
StepHypRef Expression
1 rpre 11098 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 9513 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   CCcc 9381   RR+crp 11092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-resscn 9440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-in 3433  df-ss 3440  df-rp 11093
This theorem is referenced by:  rpcnne0  11109  ltdifltdiv  11779  modvalr  11812  flpmodeq  11814  negmod0  11817  modlt  11819  moddiffl  11820  modvalp1  11827  modid  11833  modid0  11834  modcyc  11844  modcyc2  11845  modadd1  11846  modm1p1mod0  11851  modmul1  11853  2txmodxeq0  11860  2submod  11861  moddi  11867  sqrlem2  12835  sqrdiv  12857  caurcvgr  13253  o1fsum  13378  divrcnv  13417  efgt1p2  13500  efgt1p  13501  rpmsubg  17985  uniioombl  21185  abelthlem8  22020  reefgim  22031  pilem1  22032  logneg  22152  advlogexp  22216  logcxp  22230  cxprec  22247  cxpmul  22249  abscxp  22253  logsqr  22265  dvcxp1  22296  dvcxp2  22297  dvsqr  22298  cxpcn2  22300  loglesqr  22312  rlimcnp  22475  efrlim  22479  cxplim  22481  sqrlim  22482  cxploglim  22487  logdifbnd  22503  harmonicbnd4  22520  logfaclbnd  22677  logexprlim  22680  logfacrlim2  22681  vmadivsum  22847  dchrisum0lem1a  22851  dchrvmasumlema  22865  dchrisum0lem1  22881  dchrisum0lem2  22883  mudivsum  22895  mulogsumlem  22896  logdivsum  22898  selberg2lem  22915  selberg2  22916  pntrmax  22929  selbergr  22933  pntibndlem1  22954  pntlem3  22974  blocnilem  24339  nmcexi  25565  nmcopexi  25566  nmcfnexi  25590  sqsscirc1  26472  rpdmgm  27145  heicant  28564  itg2addnclem3  28583  itg2gt0cn  28585  ftc1anclem6  28610  ftc1anclem8  28612  areacirclem1  28622  areacirclem4  28625  areacirc  28627  isbnd2  28820  cntotbnd  28833  heiborlem6  28853  heiborlem7  28854  irrapxlem5  29305  rrpsscn  29907  stirlinglem14  30020  taupilem3  35918  taupilem1  35921
  Copyright terms: Public domain W3C validator