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

Theorem rpcn 10995
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 10993 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 9408 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   CCcc 9276   RR+crp 10987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-resscn 9335
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-in 3332  df-ss 3339  df-rp 10988
This theorem is referenced by:  rpcnne0  11004  ltdifltdiv  11674  modvalr  11707  flpmodeq  11709  negmod0  11712  modlt  11714  moddiffl  11715  modvalp1  11722  modid  11728  modid0  11729  modcyc  11739  modcyc2  11740  modadd1  11741  modm1p1mod0  11746  modmul1  11748  2txmodxeq0  11755  2submod  11756  moddi  11762  sqrlem2  12729  sqrdiv  12751  caurcvgr  13147  o1fsum  13272  divrcnv  13311  efgt1p2  13394  efgt1p  13395  rpmsubg  17835  uniioombl  21028  abelthlem8  21863  reefgim  21874  pilem1  21875  logneg  21995  advlogexp  22059  logcxp  22073  cxprec  22090  cxpmul  22092  abscxp  22096  logsqr  22108  dvcxp1  22139  dvcxp2  22140  dvsqr  22141  cxpcn2  22143  loglesqr  22155  rlimcnp  22318  efrlim  22322  cxplim  22324  sqrlim  22325  cxploglim  22330  logdifbnd  22346  harmonicbnd4  22363  logfaclbnd  22520  logexprlim  22523  logfacrlim2  22524  vmadivsum  22690  dchrisum0lem1a  22694  dchrvmasumlema  22708  dchrisum0lem1  22724  dchrisum0lem2  22726  mudivsum  22738  mulogsumlem  22739  logdivsum  22741  selberg2lem  22758  selberg2  22759  pntrmax  22772  selbergr  22776  pntibndlem1  22797  pntlem3  22817  blocnilem  24139  nmcexi  25365  nmcopexi  25366  nmcfnexi  25390  sqsscirc1  26274  rpdmgm  26941  heicant  28351  itg2addnclem3  28370  itg2gt0cn  28372  ftc1anclem6  28397  ftc1anclem8  28399  areacirclem1  28409  areacirclem4  28412  areacirc  28414  isbnd2  28607  cntotbnd  28620  heiborlem6  28640  heiborlem7  28641  irrapxlem5  29092  rrpsscn  29694  stirlinglem14  29807  taupilem3  35334  taupilem1  35337
  Copyright terms: Public domain W3C validator