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

Theorem rpcn 11219
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 11217 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 9613 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   CCcc 9481   RR+crp 11211
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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-resscn 9540
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-in 3478  df-ss 3485  df-rp 11212
This theorem is referenced by:  rpcnne0  11228  ltdifltdiv  11924  modvalr  11957  flpmodeq  11959  negmod0  11962  modlt  11964  moddiffl  11965  modvalp1  11972  modid  11978  modid0  11979  modcyc  11989  modcyc2  11990  modadd1  11991  modm1p1mod0  11996  modmul1  11998  2txmodxeq0  12005  2submod  12006  moddi  12012  sqrlem2  13029  sqrdiv  13051  caurcvgr  13447  o1fsum  13578  divrcnv  13618  efgt1p2  13701  efgt1p  13702  rpmsubg  18244  uniioombl  21728  abelthlem8  22563  reefgim  22574  pilem1  22575  logneg  22695  advlogexp  22759  logcxp  22773  cxprec  22790  cxpmul  22792  abscxp  22796  logsqr  22808  dvcxp1  22839  dvcxp2  22840  dvsqr  22841  cxpcn2  22843  loglesqr  22855  rlimcnp  23018  efrlim  23022  cxplim  23024  sqrlim  23025  cxploglim  23030  logdifbnd  23046  harmonicbnd4  23063  logfaclbnd  23220  logexprlim  23223  logfacrlim2  23224  vmadivsum  23390  dchrisum0lem1a  23394  dchrvmasumlema  23408  dchrisum0lem1  23424  dchrisum0lem2  23426  mudivsum  23438  mulogsumlem  23439  logdivsum  23441  selberg2lem  23458  selberg2  23459  pntrmax  23472  selbergr  23476  pntibndlem1  23497  pntlem3  23517  blocnilem  25383  nmcexi  26609  nmcopexi  26610  nmcfnexi  26634  sqsscirc1  27514  rpdmgm  28195  heicant  29615  itg2addnclem3  29634  itg2gt0cn  29636  ftc1anclem6  29661  ftc1anclem8  29663  areacirclem1  29673  areacirclem4  29676  areacirc  29678  isbnd2  29871  cntotbnd  29884  heiborlem6  29904  heiborlem7  29905  irrapxlem5  30355  rrpsscn  31095  stirlinglem14  31344  fourierdlem73  31437  fourierdlem87  31451  taupilem3  36641  taupilem1  36644
  Copyright terms: Public domain W3C validator