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

Theorem rpcn 12387
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 12385 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21recnd 10658 1 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  cc 10524  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-rp 12378
This theorem is referenced by:  rpcnne0  12395  rpmtmip  12401  divge1  12445  ltdifltdiv  13199  modvalr  13235  flpmodeq  13237  mulmod0  13240  negmod0  13241  modlt  13243  moddiffl  13245  modvalp1  13253  modid  13259  modid0  13260  modcyc  13269  modcyc2  13270  modadd1  13271  muladdmodid  13274  modmuladdnn0  13278  negmod  13279  modm1p1mod0  13285  modmul1  13287  2txmodxeq0  13294  2submod  13295  moddi  13302  sqrlem2  14595  sqrtdiv  14617  caurcvgr  15022  o1fsum  15160  divrcnv  15199  efgt1p2  15459  efgt1p  15460  rpmsubg  20155  uniioombl  24193  abelthlem8  25034  pilem1  25046  logne0  25171  logneg  25179  advlogexp  25246  logcxp  25260  cxprec  25277  cxpmul  25279  abscxp  25283  logsqrt  25295  dvcxp1  25329  dvcxp2  25330  dvsqrt  25331  cxpcn2  25335  loglesqrt  25347  relogbreexp  25361  relogbzexp  25362  relogbmul  25363  relogbdiv  25365  relogbexp  25366  relogbcxp  25371  relogbcxpb  25373  relogbf  25377  logbgt0b  25379  rlimcnp  25551  efrlim  25555  cxplim  25557  sqrtlim  25558  cxploglim  25563  logdifbnd  25579  harmonicbnd4  25596  rpdmgm  25610  logfaclbnd  25806  logexprlim  25809  logfacrlim2  25810  vmadivsum  26066  dchrisum0lem1a  26070  dchrvmasumlema  26084  dchrisum0lem1  26100  dchrisum0lem2  26102  mudivsum  26114  mulogsumlem  26115  logdivsum  26117  selberg2lem  26134  selberg2  26135  pntrmax  26148  selbergr  26152  pntibndlem1  26173  pntlem3  26193  blocnilem  28587  nmcexi  29809  nmcopexi  29810  nmcfnexi  29834  dp20h  30581  dpexpp1  30610  0dp2dp  30611  sqsscirc1  31261  logdivsqrle  32031  taupilem3  34730  taupilem1  34732  poimirlem29  35083  heicant  35089  itg2addnclem3  35107  itg2gt0cn  35109  ftc1anclem6  35132  ftc1anclem8  35134  areacirclem1  35142  areacirclem4  35145  areacirc  35147  isbnd2  35218  cntotbnd  35231  heiborlem6  35251  heiborlem7  35252  irrapxlem5  39762  2timesgt  41914  xralrple2  41981  recnnltrp  42004  rpgtrecnn  42008  rrpsscn  42225  stirlinglem14  42724  fourierdlem73  42816  divge1b  44916  divgt1b  44917  fldivmod  44927  relogbmulbexp  44970  relogbdivb  44971  itschlc0yqe  45169  itschlc0xyqsol1  45175  itsclc0xyqsolr  45178  amgmwlem  45325
  Copyright terms: Public domain W3C validator