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

Theorem rpcn 10378
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 10376 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 8877 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   CCcc 8751   RR+crp 10370
This theorem is referenced by:  rpcnne0  10387  negmod0  10995  modlt  10997  moddiffl  10998  modid  11009  modcyc  11015  modcyc2  11016  modadd1  11017  modmul1  11018  moddi  11023  sqrlem2  11745  sqrdiv  11767  caurcvgr  12162  o1fsum  12287  divrcnv  12327  efgt1p2  12410  efgt1p  12411  rpmsubg  16451  uniioombl  18960  abelthlem8  19831  reefgim  19842  pilem1  19843  logneg  19957  advlogexp  20018  logcxp  20032  cxprec  20049  cxpmul  20051  abscxp  20055  logsqr  20067  dvcxp1  20098  dvcxp2  20099  dvsqr  20100  cxpcn2  20102  loglesqr  20114  rlimcnp  20276  efrlim  20280  cxplim  20282  sqrlim  20283  cxploglim  20288  logdifbnd  20304  harmonicbnd4  20320  logfaclbnd  20477  logexprlim  20480  logfacrlim2  20481  vmadivsum  20647  dchrisum0lem1a  20651  dchrvmasumlema  20665  dchrisum0lem1  20681  dchrisum0lem2  20683  mudivsum  20695  mulogsumlem  20696  logdivsum  20698  selberg2lem  20715  selberg2  20716  pntrmax  20729  selbergr  20733  pntibndlem1  20754  pntlem3  20774  blocnilem  21398  nmcexi  22622  nmcopexi  22623  nmcfnexi  22647  sqsscirc1  23307  rnlogbval  23417  probmeasb  23648  faclimlem5  24121  itg2addnc  25005  itg2gt0cn  25006  dvreasin  25026  areacirclem2  25028  areacirclem3  25029  areacirclem5  25032  areacirc  25034  rdr  26538  isbnd2  26610  cntotbnd  26623  heiborlem6  26643  heiborlem7  26644  irrapxlem5  27014  rrpsscn  27822  stoweidlem1  27853  stoweidlem3  27855  stoweidlem7  27859  stoweidlem11  27863  stoweidlem14  27866  stoweidlem24  27876  stoweidlem25  27877  stoweidlem42  27894  stoweidlem51  27903  stirlinglem14  27939
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-in 3172  df-ss 3179  df-rp 10371
  Copyright terms: Public domain W3C validator