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

Theorem rpcn 11826
Description: A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
Assertion
Ref Expression
rpcn (𝐴 ∈ ℝ+𝐴 ∈ ℂ)

Proof of Theorem rpcn
StepHypRef Expression
1 rpre 11824 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21recnd 10053 1 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  cc 9919  +crp 11817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-in 3574  df-ss 3581  df-rp 11818
This theorem is referenced by:  rpcnne0  11835  divge1  11883  ltdifltdiv  12618  modvalr  12654  flpmodeq  12656  mulmod0  12659  negmod0  12660  modlt  12662  moddiffl  12664  modvalp1  12672  modid  12678  modid0  12679  modcyc  12688  modcyc2  12689  modadd1  12690  muladdmodid  12693  modmuladdnn0  12697  negmod  12698  modm1p1mod0  12704  modmul1  12706  2txmodxeq0  12713  2submod  12714  moddi  12721  sqrlem2  13965  sqrtdiv  13987  caurcvgr  14385  o1fsum  14526  divrcnv  14565  efgt1p2  14825  efgt1p  14826  rpmsubg  19791  uniioombl  23338  abelthlem8  24174  reefgim  24185  pilem1  24186  logne0  24307  logneg  24315  advlogexp  24382  logcxp  24396  cxprec  24413  cxpmul  24415  abscxp  24419  logsqrt  24431  dvcxp1  24462  dvcxp2  24463  dvsqrt  24464  cxpcn2  24468  loglesqrt  24480  relogbreexp  24494  relogbzexp  24495  relogbmul  24496  relogbdiv  24498  relogbexp  24499  relogbcxp  24504  relogbcxpb  24506  relogbf  24510  rlimcnp  24673  efrlim  24677  cxplim  24679  sqrtlim  24680  cxploglim  24685  logdifbnd  24701  harmonicbnd4  24718  rpdmgm  24732  logfaclbnd  24928  logexprlim  24931  logfacrlim2  24932  vmadivsum  25152  dchrisum0lem1a  25156  dchrvmasumlema  25170  dchrisum0lem1  25186  dchrisum0lem2  25188  mudivsum  25200  mulogsumlem  25201  logdivsum  25203  selberg2lem  25220  selberg2  25221  pntrmax  25234  selbergr  25238  pntibndlem1  25259  pntlem3  25279  blocnilem  27629  nmcexi  28855  nmcopexi  28856  nmcfnexi  28880  dp20h  29560  dpexpp1  29590  0dp2dp  29591  sqsscirc1  29928  logdivsqrle  30702  taupilem3  33136  taupilem1  33138  poimirlem29  33409  heicant  33415  itg2addnclem3  33434  itg2gt0cn  33436  ftc1anclem6  33461  ftc1anclem8  33463  areacirclem1  33471  areacirclem4  33474  areacirc  33476  isbnd2  33553  cntotbnd  33566  heiborlem6  33586  heiborlem7  33587  irrapxlem5  37209  2timesgt  39313  xralrple2  39383  recnnltrp  39406  rpgtrecnn  39410  rrpsscn  39620  stirlinglem14  40067  fourierdlem73  40159  divge1b  42067  divgt1b  42068  fldivmod  42078  relogbmulbexp  42120  relogbdivb  42121  amgmwlem  42313
  Copyright terms: Public domain W3C validator