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

Theorem rpcnd 10392
Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpcnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem rpcnd
StepHypRef Expression
1 rpred.1 . . 3  |-  ( ph  ->  A  e.  RR+ )
21rpred 10390 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 8861 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   CCcc 8735   RR+crp 10354
This theorem is referenced by:  rpcnne0d  10399  ltaddrp2d  10420  iccf1o  10778  ltexp2r  11158  discr  11238  bcp1nk  11329  bcpasc  11333  sqrlem6  11733  sqrdiv  11751  absdiv  11780  o1rlimmul  12092  isumrpcl  12302  isumltss  12307  expcnv  12322  mertenslem1  12340  bitsmod  12627  nmoi2  18239  reperflem  18323  icchmeo  18439  icopnfcnv  18440  lebnumlem3  18461  nmoleub2lem2  18597  nmoleub3  18600  minveclem3  18793  pjthlem1  18801  ovollb2lem  18847  sca2rab  18871  ovolscalem1  18872  ovolsca  18874  itg2mulc  19102  itg2cnlem2  19117  c1liplem1  19343  lhop1  19361  aalioulem4  19715  aaliou2b  19721  aaliou3lem2  19723  aaliou3lem3  19724  aaliou3lem8  19725  aaliou3lem6  19728  aaliou3lem7  19729  itgulm  19784  dvradcnv  19797  pserdvlem2  19804  abelthlem7  19814  abelthlem8  19815  lognegb  19943  logno1  19983  advlog  20001  advlogexp  20002  cxprec  20033  divcxp  20034  cxpsqr  20050  dvcxp1  20082  cxpcn3lem  20087  loglesqr  20098  asinlem3  20167  cxplim  20266  rlimcxp  20268  cxp2limlem  20270  cxp2lim  20271  cxploglim  20272  cxploglim2  20273  divsqrsumlem  20274  divsqrsumo1  20278  amgmlem  20284  basellem3  20320  basellem4  20321  chpval2  20457  logexprlim  20464  bclbnd  20519  bposlem9  20531  chebbnd1lem3  20620  chebbnd1  20621  chtppilimlem2  20623  chtppilim  20624  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ubb  20630  rplogsumlem1  20633  rplogsumlem2  20634  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  dchrisum0  20669  mulogsumlem  20680  mulog2sumlem1  20683  mulog2sumlem2  20684  vmalogdivsum2  20687  log2sumbnd  20693  selberg3lem1  20706  selberg3lem2  20707  selberg4lem1  20709  selberg4  20710  selberg34r  20720  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem1  20738  pntibndlem2  20740  pntlemd  20743  pntlemc  20744  pntlemb  20746  pntlemq  20750  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemo  20756  pntlem3  20758  pntleml  20760  pnt  20763  padicabvcxp  20781  ostth2lem4  20785  ostth2  20786  smcnlem  21270  blocnilem  21382  ubthlem2  21450  bcm1n  23032  rnlogbval  23402  nnlogbexp  23406  logbrec  23407  zetacvg  23689  mslb1  25607  2wsms  25608  geomcau  26475  cntotbnd  26520  heibor1lem  26533  rrndstprj2  26555  rrncmslem  26556  pell1qrgaplem  26958  pellfund14  26983  rmxyneg  27005  rmxy1  27007  rmxy0  27008  jm2.23  27089  proot1ex  27520  stoweidlem62  27811  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  stirlinglem4  27826  stirlinglem8  27830  stirlinglem12  27834  stirlinglem15  27837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166  df-rp 10355
  Copyright terms: Public domain W3C validator