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

Theorem rpcn 10362
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 10360 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 8861 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   CCcc 8735   RR+crp 10354
This theorem is referenced by:  rpcnne0  10371  negmod0  10979  modlt  10981  moddiffl  10982  modid  10993  modcyc  10999  modcyc2  11000  modadd1  11001  modmul1  11002  moddi  11007  sqrlem2  11729  sqrdiv  11751  caurcvgr  12146  o1fsum  12271  divrcnv  12311  efgt1p2  12394  efgt1p  12395  rpmsubg  16435  uniioombl  18944  abelthlem8  19815  reefgim  19826  pilem1  19827  logneg  19941  advlogexp  20002  logcxp  20016  cxprec  20033  cxpmul  20035  abscxp  20039  logsqr  20051  dvcxp1  20082  dvcxp2  20083  dvsqr  20084  cxpcn2  20086  loglesqr  20098  rlimcnp  20260  efrlim  20264  cxplim  20266  sqrlim  20267  cxploglim  20272  logdifbnd  20288  harmonicbnd4  20304  logfaclbnd  20461  logexprlim  20464  logfacrlim2  20465  vmadivsum  20631  dchrisum0lem1a  20635  dchrvmasumlema  20649  dchrisum0lem1  20665  dchrisum0lem2  20667  mudivsum  20679  mulogsumlem  20680  logdivsum  20682  selberg2lem  20699  selberg2  20700  pntrmax  20713  selbergr  20717  pntibndlem1  20738  pntlem3  20758  blocnilem  21382  nmcexi  22606  nmcopexi  22607  nmcfnexi  22631  sqsscirc1  23292  rnlogbval  23402  probmeasb  23633  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  areacirclem5  24929  areacirc  24931  rdr  26435  isbnd2  26507  cntotbnd  26520  heiborlem6  26540  heiborlem7  26541  irrapxlem5  26911  rrpsscn  27719  stoweidlem1  27750  stoweidlem3  27752  stoweidlem7  27756  stoweidlem11  27760  stoweidlem14  27763  stoweidlem24  27773  stoweidlem25  27774  stoweidlem42  27791  stoweidlem51  27800  stirlinglem14  27836
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-or 359  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-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166  df-rp 10355
  Copyright terms: Public domain W3C validator