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

Theorem rpcnd 11350
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 11348 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9674 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1889   CCcc 9542   RR+crp 11309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-resscn 9601
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-in 3413  df-ss 3420  df-rp 11310
This theorem is referenced by:  rpcnne0d  11357  ltaddrp2d  11379  iccf1o  11783  ltexp2r  12336  discr  12416  bcp1nk  12509  bcpasc  12513  sqrlem6  13323  sqrtdiv  13341  absdiv  13370  o1rlimmul  13694  isumrpcl  13913  isumltss  13918  expcnv  13934  mertenslem1  13952  bitsmod  14422  nmoi2  21747  nmoi2OLD  21763  reperflem  21848  icchmeo  21981  icopnfcnv  21982  lebnumlem3  22003  lebnumlem3OLD  22006  nmoleub2lem2  22142  nmoleub3  22145  minveclem3  22383  minveclem3OLD  22395  pjthlem1  22403  ovollb2lem  22453  sca2rab  22477  ovolscalem1  22478  ovolsca  22480  itg2mulc  22717  itg2cnlem2  22732  c1liplem1  22960  lhop1  22978  aalioulem4  23303  aaliou2b  23309  aaliou3lem2  23311  aaliou3lem3  23312  aaliou3lem8  23313  aaliou3lem6  23316  aaliou3lem7  23317  itgulm  23375  dvradcnv  23388  pserdvlem2  23395  abelthlem7  23405  abelthlem8  23406  lognegb  23551  logno1  23593  advlog  23611  advlogexp  23612  cxprec  23643  divcxp  23644  cxpsqrt  23660  dvcxp1  23692  cxpcn3lem  23699  loglesqrt  23710  relogbval  23721  nnlogbexp  23730  logbrec  23731  asinlem3  23809  cxplim  23909  rlimcxp  23911  cxp2limlem  23913  cxp2lim  23914  cxploglim  23915  cxploglim2  23916  divsqrtsumlem  23917  divsqrtsumo1  23921  amgmlem  23927  zetacvg  23952  lgamucov  23975  basellem3  24021  basellem4  24022  chpval2  24158  logexprlim  24165  bclbnd  24220  bposlem9  24232  chebbnd1lem3  24321  chebbnd1  24322  chtppilimlem2  24324  chtppilim  24325  chebbnd2  24327  chto1lb  24328  chpchtlim  24329  chpo1ubb  24331  rplogsumlem1  24334  rplogsumlem2  24335  dchrvmasumlem1  24345  dchrvmasum2lem  24346  dchrisum0lema  24364  dchrisum0lem1b  24365  dchrisum0lem1  24366  dchrisum0lem2a  24367  dchrisum0lem2  24368  dchrisum0lem3  24369  dchrisum0  24370  mulogsumlem  24381  mulog2sumlem1  24384  mulog2sumlem2  24385  vmalogdivsum2  24388  log2sumbnd  24394  selberg3lem1  24407  selberg3lem2  24408  selberg4lem1  24410  selberg4  24411  selberg34r  24421  pntrlog2bndlem2  24428  pntrlog2bndlem3  24429  pntrlog2bndlem4  24430  pntrlog2bndlem5  24431  pntpbnd1a  24435  pntpbnd2  24437  pntibndlem1  24439  pntibndlem2  24441  pntlemd  24444  pntlemc  24445  pntlemb  24447  pntlemq  24451  pntlemr  24452  pntlemj  24453  pntlemf  24455  pntlemo  24457  pntlem3  24459  pntleml  24461  pnt  24464  padicabvcxp  24482  ostth2lem4  24486  ostth2  24487  ostth3  24488  smcnlem  26345  blocnilem  26457  ubthlem2  26525  bcm1n  28383  probmeasb  29275  signsply0  29452  iprodgam  30390  faclimlem1  30391  faclimlem3  30393  faclim  30394  iprodfac  30395  mblfinlem3  31991  itg2addnclem3  32007  ftc1cnnclem  32027  geomcau  32100  cntotbnd  32140  heibor1lem  32153  rrndstprj2  32175  rrncmslem  32176  pell1qrgaplem  35731  pellfund14  35758  rmxyneg  35780  rmxy1  35782  rmxy0  35783  jm2.23  35863  proot1ex  36090  amgm2d  36661  amgm3d  36662  amgm4d  36663  cvgdvgrat  36673  binomcxplemnn0  36709  binomcxplemnotnn0  36716  ltdivgt1  37589  0ellimcdiv  37740  limclner  37742  dvdivbd  37805  stoweidlem1  37871  stoweidlem3  37873  stoweidlem7  37877  stoweidlem11  37881  stoweidlem14  37884  stoweidlem24  37894  stoweidlem25  37895  stoweidlem26  37896  stoweidlem42  37913  stoweidlem51  37922  stoweidlem59  37930  stoweidlem62  37933  stoweidlem62OLD  37934  wallispilem4  37940  wallispilem5  37941  wallispi  37942  wallispi2lem1  37943  stirlinglem4  37949  stirlinglem8  37953  stirlinglem12  37957  stirlinglem15  37960  dirkercncflem4  37978  fourierdlem30  38009  fourierdlem73  38053  fourierdlem87  38067  qndenserrnbllem  38173  hoiqssbllem2  38455  dignn0flhalflem2  40531
  Copyright terms: Public domain W3C validator