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

Theorem rpcn 10620
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 10618 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 9114 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8988   RR+crp 10612
This theorem is referenced by:  rpcnne0  10629  negmod0  11256  modlt  11258  moddiffl  11259  modid  11270  modcyc  11276  modcyc2  11277  modadd1  11278  modmul1  11279  moddi  11284  sqrlem2  12049  sqrdiv  12071  caurcvgr  12467  o1fsum  12592  divrcnv  12632  efgt1p2  12715  efgt1p  12716  rpmsubg  16762  uniioombl  19481  abelthlem8  20355  reefgim  20366  pilem1  20367  logneg  20482  advlogexp  20546  logcxp  20560  cxprec  20577  cxpmul  20579  abscxp  20583  logsqr  20595  dvcxp1  20626  dvcxp2  20627  dvsqr  20628  cxpcn2  20630  loglesqr  20642  rlimcnp  20804  efrlim  20808  cxplim  20810  sqrlim  20811  cxploglim  20816  logdifbnd  20832  harmonicbnd4  20849  logfaclbnd  21006  logexprlim  21009  logfacrlim2  21010  vmadivsum  21176  dchrisum0lem1a  21180  dchrvmasumlema  21194  dchrisum0lem1  21210  dchrisum0lem2  21212  mudivsum  21224  mulogsumlem  21225  logdivsum  21227  selberg2lem  21244  selberg2  21245  pntrmax  21258  selbergr  21262  pntibndlem1  21283  pntlem3  21303  blocnilem  22305  nmcexi  23529  nmcopexi  23530  nmcfnexi  23554  sqsscirc1  24306  rpdmgm  24809  itg2addnclem3  26258  itg2gt0cn  26260  ftc1anclem6  26285  ftc1anclem8  26287  dvreasin  26290  areacirclem1  26292  areacirclem4  26295  areacirc  26297  isbnd2  26492  cntotbnd  26505  heiborlem6  26525  heiborlem7  26526  irrapxlem5  26889  rrpsscn  27695  stirlinglem14  27812  ltdifltdiv  28148  modvalr  28149  flpmodeq  28150  modvalp1  28151  2submod  28152  modid0  28159  2txmodxeq0  28162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-resscn 9047
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-in 3327  df-ss 3334  df-rp 10613
  Copyright terms: Public domain W3C validator