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

Theorem rpcnd 11021
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 11019 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9404 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9272   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-in 3330  df-ss 3337  df-rp 10984
This theorem is referenced by:  rpcnne0d  11028  ltaddrp2d  11049  iccf1o  11421  ltexp2r  11912  discr  11993  bcp1nk  12085  bcpasc  12089  sqrlem6  12729  sqrdiv  12747  absdiv  12776  o1rlimmul  13088  isumrpcl  13298  isumltss  13303  expcnv  13318  mertenslem1  13336  bitsmod  13624  nmoi2  20284  reperflem  20370  icchmeo  20488  icopnfcnv  20489  lebnumlem3  20510  nmoleub2lem2  20646  nmoleub3  20649  minveclem3  20891  pjthlem1  20899  ovollb2lem  20946  sca2rab  20970  ovolscalem1  20971  ovolsca  20973  itg2mulc  21200  itg2cnlem2  21215  c1liplem1  21443  lhop1  21461  aalioulem4  21776  aaliou2b  21782  aaliou3lem2  21784  aaliou3lem3  21785  aaliou3lem8  21786  aaliou3lem6  21789  aaliou3lem7  21790  itgulm  21848  dvradcnv  21861  pserdvlem2  21868  abelthlem7  21878  abelthlem8  21879  lognegb  22013  logno1  22056  advlog  22074  advlogexp  22075  cxprec  22106  divcxp  22107  cxpsqr  22123  dvcxp1  22155  cxpcn3lem  22160  loglesqr  22171  asinlem3  22241  cxplim  22340  rlimcxp  22342  cxp2limlem  22344  cxp2lim  22345  cxploglim  22346  cxploglim2  22347  divsqrsumlem  22348  divsqrsumo1  22352  amgmlem  22358  basellem3  22395  basellem4  22396  chpval2  22532  logexprlim  22539  bclbnd  22594  bposlem9  22606  chebbnd1lem3  22695  chebbnd1  22696  chtppilimlem2  22698  chtppilim  22699  chebbnd2  22701  chto1lb  22702  chpchtlim  22703  chpo1ubb  22705  rplogsumlem1  22708  rplogsumlem2  22709  dchrvmasumlem1  22719  dchrvmasum2lem  22720  dchrisum0lema  22738  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrisum0  22744  mulogsumlem  22755  mulog2sumlem1  22758  mulog2sumlem2  22759  vmalogdivsum2  22762  log2sumbnd  22768  selberg3lem1  22781  selberg3lem2  22782  selberg4lem1  22784  selberg4  22785  selberg34r  22795  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntpbnd1a  22809  pntpbnd2  22811  pntibndlem1  22813  pntibndlem2  22815  pntlemd  22818  pntlemc  22819  pntlemb  22821  pntlemq  22825  pntlemr  22826  pntlemj  22827  pntlemf  22829  pntlemo  22831  pntlem3  22833  pntleml  22835  pnt  22838  padicabvcxp  22856  ostth2lem4  22860  ostth2  22861  ostth3  22862  smcnlem  24043  blocnilem  24155  ubthlem2  24223  mul2lt0bi  25993  bcm1n  26030  rnlogbval  26411  nnlogbexp  26415  logbrec  26416  probmeasb  26765  zetacvg  26953  lgamucov  26976  iprodgam  27457  faclimlem1  27500  faclimlem3  27502  faclim  27503  iprodfac  27504  mblfinlem3  28383  itg2addnclem3  28398  ftc1cnnclem  28418  geomcau  28608  cntotbnd  28648  heibor1lem  28661  rrndstprj2  28683  rrncmslem  28684  pell1qrgaplem  29167  pellfund14  29192  rmxyneg  29214  rmxy1  29216  rmxy0  29217  jm2.23  29298  proot1ex  29522  stoweidlem1  29749  stoweidlem3  29751  stoweidlem7  29755  stoweidlem11  29759  stoweidlem14  29762  stoweidlem24  29772  stoweidlem25  29773  stoweidlem26  29774  stoweidlem42  29790  stoweidlem51  29799  stoweidlem59  29807  stoweidlem62  29810  wallispilem4  29816  wallispilem5  29817  wallispi  29818  wallispi2lem1  29819  stirlinglem4  29825  stirlinglem8  29829  stirlinglem12  29833  stirlinglem15  29836
  Copyright terms: Public domain W3C validator