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

Theorem rpcn 11273
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 11271 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21recnd 9652 1  |-  ( A  e.  RR+  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   CCcc 9520   RR+crp 11265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-resscn 9579
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-in 3421  df-ss 3428  df-rp 11266
This theorem is referenced by:  rpcnne0  11282  ltdifltdiv  12004  modvalr  12037  flpmodeq  12039  mulmod0  12042  negmod0  12043  modlt  12045  moddiffl  12046  modvalp1  12053  modid  12059  modid0  12060  modcyc  12070  modcyc2  12071  modadd1  12072  muladdmodid  12075  negmod  12076  modm1p1mod0  12079  modmul1  12081  2txmodxeq0  12088  2submod  12089  moddi  12095  sqrlem2  13226  sqrtdiv  13248  caurcvgr  13645  o1fsum  13778  divrcnv  13815  efgt1p2  14058  efgt1p  14059  rpmsubg  18801  uniioombl  22290  abelthlem8  23126  reefgim  23137  pilem1  23138  logne0  23259  logneg  23267  advlogexp  23330  logcxp  23344  cxprec  23361  cxpmul  23363  abscxp  23367  logsqrt  23379  dvcxp1  23410  dvcxp2  23411  dvsqrt  23412  cxpcn2  23416  loglesqrt  23428  relogbreexp  23442  relogbzexp  23443  relogbmul  23444  relogbdiv  23446  relogbexp  23447  relogbcxp  23452  relogbcxpb  23454  relogbf  23458  rlimcnp  23621  efrlim  23625  cxplim  23627  sqrtlim  23628  cxploglim  23633  logdifbnd  23649  harmonicbnd4  23666  rpdmgm  23680  logfaclbnd  23878  logexprlim  23881  logfacrlim2  23882  vmadivsum  24048  dchrisum0lem1a  24052  dchrvmasumlema  24066  dchrisum0lem1  24082  dchrisum0lem2  24084  mudivsum  24096  mulogsumlem  24097  logdivsum  24099  selberg2lem  24116  selberg2  24117  pntrmax  24130  selbergr  24134  pntibndlem1  24155  pntlem3  24175  blocnilem  26133  nmcexi  27358  nmcopexi  27359  nmcfnexi  27383  sqsscirc1  28343  taupilem3  31245  taupilem1  31247  heicant  31421  itg2addnclem3  31441  itg2gt0cn  31443  ftc1anclem6  31468  ftc1anclem8  31470  areacirclem1  31478  areacirclem4  31481  areacirc  31483  isbnd2  31561  cntotbnd  31574  heiborlem6  31594  heiborlem7  31595  irrapxlem5  35123  2timesgt  36848  divge1  36882  rrpsscn  36950  stirlinglem14  37237  fourierdlem73  37330  divge1b  38627  divgt1b  38628  fldivmod  38641  relogbmulbexp  38692  relogbdivb  38693
  Copyright terms: Public domain W3C validator