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

Theorem rpcn 11257
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 11255 . 2
21recnd 9643 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   crp 11249
This theorem is referenced by:  rpcnne0  11266  ltdifltdiv  11966  modvalr  11999  flpmodeq  12001  negmod0  12004  modlt  12006  moddiffl  12007  modvalp1  12014  modid  12020  modid0  12021  modcyc  12031  modcyc2  12032  modadd1  12033  modm1p1mod0  12038  modmul1  12040  2txmodxeq0  12047  2submod  12048  moddi  12054  sqrlem2  13077  sqrtdiv  13099  caurcvgr  13496  o1fsum  13627  divrcnv  13664  efgt1p2  13849  efgt1p  13850  rpmsubg  18481  uniioombl  21998  abelthlem8  22834  reefgim  22845  pilem1  22846  logneg  22972  advlogexp  23036  logcxp  23050  cxprec  23067  cxpmul  23069  abscxp  23073  logsqrt  23085  dvcxp1  23116  dvcxp2  23117  dvsqrt  23118  cxpcn2  23120  loglesqrt  23132  rlimcnp  23295  efrlim  23299  cxplim  23301  sqrtlim  23302  cxploglim  23307  logdifbnd  23323  harmonicbnd4  23340  logfaclbnd  23497  logexprlim  23500  logfacrlim2  23501  vmadivsum  23667  dchrisum0lem1a  23671  dchrvmasumlema  23685  dchrisum0lem1  23701  dchrisum0lem2  23703  mudivsum  23715  mulogsumlem  23716  logdivsum  23718  selberg2lem  23735  selberg2  23736  pntrmax  23749  selbergr  23753  pntibndlem1  23774  pntlem3  23794  blocnilem  25719  nmcexi  26945  nmcopexi  26946  nmcfnexi  26970  sqsscirc1  27890  rpdmgm  28567  heicant  30049  itg2addnclem3  30068  itg2gt0cn  30070  ftc1anclem6  30095  ftc1anclem8  30097  areacirclem1  30107  areacirclem4  30110  areacirc  30112  isbnd2  30279  cntotbnd  30292  heiborlem6  30312  heiborlem7  30313  irrapxlem5  30762  2timesgt  31475  divge1  31513  rrpsscn  31582  stirlinglem14  31869  fourierdlem73  31962  taupilem3  37694  taupilem1  37696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3482  df-ss 3489  df-rp 11250
  Copyright terms: Public domain W3C validator