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

Theorem rpcn 12932
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 12930 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21recnd 11190 1 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 11056  +crp 12922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11115
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-in 3922  df-ss 3932  df-rp 12923
This theorem is referenced by:  rpcnne0  12940  rpmtmip  12946  divge1  12990  ltdifltdiv  13746  modvalr  13784  flpmodeq  13786  mulmod0  13789  negmod0  13790  modlt  13792  moddiffl  13794  modvalp1  13802  modid  13808  modid0  13809  modcyc  13818  modcyc2  13819  modadd1  13820  muladdmodid  13823  modmuladdnn0  13827  negmod  13828  modm1p1mod0  13834  modmul1  13836  2txmodxeq0  13843  2submod  13844  moddi  13851  01sqrexlem2  15135  sqrtdiv  15157  caurcvgr  15565  o1fsum  15705  divrcnv  15744  efgt1p2  16003  efgt1p  16004  rpmsubg  20877  uniioombl  24969  abelthlem8  25814  pilem1  25826  logne0  25951  logneg  25959  advlogexp  26026  logcxp  26040  cxprec  26057  cxpmul  26059  abscxp  26063  logsqrt  26075  dvcxp1  26109  dvcxp2  26110  dvsqrt  26111  cxpcn2  26115  loglesqrt  26127  relogbreexp  26141  relogbzexp  26142  relogbmul  26143  relogbdiv  26145  relogbexp  26146  relogbcxp  26151  relogbcxpb  26153  relogbf  26157  logbgt0b  26159  rlimcnp  26331  efrlim  26335  cxplim  26337  sqrtlim  26338  cxploglim  26343  logdifbnd  26359  harmonicbnd4  26376  rpdmgm  26390  logfaclbnd  26586  logexprlim  26589  logfacrlim2  26590  vmadivsum  26846  dchrisum0lem1a  26850  dchrvmasumlema  26864  dchrisum0lem1  26880  dchrisum0lem2  26882  mudivsum  26894  mulogsumlem  26895  logdivsum  26897  selberg2lem  26914  selberg2  26915  pntrmax  26928  selbergr  26932  pntibndlem1  26953  pntlem3  26973  blocnilem  29788  nmcexi  31010  nmcopexi  31011  nmcfnexi  31035  dp20h  31777  dpexpp1  31806  0dp2dp  31807  sqsscirc1  32529  logdivsqrle  33303  taupilem3  35819  taupilem1  35821  poimirlem29  36136  heicant  36142  itg2addnclem3  36160  itg2gt0cn  36162  ftc1anclem6  36185  ftc1anclem8  36187  areacirclem1  36195  areacirclem4  36198  areacirc  36200  isbnd2  36271  cntotbnd  36284  heiborlem6  36304  heiborlem7  36305  dvrelog3  40551  irrapxlem5  41178  2timesgt  43596  xralrple2  43662  recnnltrp  43685  rpgtrecnn  43688  rrpsscn  43903  stirlinglem14  44402  fourierdlem73  44494  divge1b  46667  divgt1b  46668  fldivmod  46678  relogbmulbexp  46721  relogbdivb  46722  itschlc0yqe  46920  itschlc0xyqsol1  46926  itsclc0xyqsolr  46929  amgmwlem  47323
  Copyright terms: Public domain W3C validator