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

Theorem rpcnd 11197
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 11195 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9551 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1836   CCcc 9419   RR+crp 11157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-resscn 9478
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-in 3409  df-ss 3416  df-rp 11158
This theorem is referenced by:  rpcnne0d  11204  ltaddrp2d  11225  iccf1o  11603  ltexp2r  12144  discr  12224  bcp1nk  12316  bcpasc  12320  sqrlem6  13102  sqrtdiv  13120  absdiv  13149  o1rlimmul  13462  isumrpcl  13676  isumltss  13681  expcnv  13696  mertenslem1  13714  bitsmod  14107  nmoi2  21341  reperflem  21427  icchmeo  21545  icopnfcnv  21546  lebnumlem3  21567  nmoleub2lem2  21703  nmoleub3  21706  minveclem3  21948  pjthlem1  21956  ovollb2lem  22003  sca2rab  22027  ovolscalem1  22028  ovolsca  22030  itg2mulc  22258  itg2cnlem2  22273  c1liplem1  22501  lhop1  22519  aalioulem4  22835  aaliou2b  22841  aaliou3lem2  22843  aaliou3lem3  22844  aaliou3lem8  22845  aaliou3lem6  22848  aaliou3lem7  22849  itgulm  22907  dvradcnv  22920  pserdvlem2  22927  abelthlem7  22937  abelthlem8  22938  lognegb  23081  logno1  23123  advlog  23141  advlogexp  23142  cxprec  23173  divcxp  23174  cxpsqrt  23190  dvcxp1  23222  cxpcn3lem  23227  loglesqrt  23238  relogbval  23249  nnlogbexp  23258  logbrec  23259  asinlem3  23337  cxplim  23437  rlimcxp  23439  cxp2limlem  23441  cxp2lim  23442  cxploglim  23443  cxploglim2  23444  divsqrtsumlem  23445  divsqrtsumo1  23449  amgmlem  23455  basellem3  23492  basellem4  23493  chpval2  23629  logexprlim  23636  bclbnd  23691  bposlem9  23703  chebbnd1lem3  23792  chebbnd1  23793  chtppilimlem2  23795  chtppilim  23796  chebbnd2  23798  chto1lb  23799  chpchtlim  23800  chpo1ubb  23802  rplogsumlem1  23805  rplogsumlem2  23806  dchrvmasumlem1  23816  dchrvmasum2lem  23817  dchrisum0lema  23835  dchrisum0lem1b  23836  dchrisum0lem1  23837  dchrisum0lem2a  23838  dchrisum0lem2  23839  dchrisum0lem3  23840  dchrisum0  23841  mulogsumlem  23852  mulog2sumlem1  23855  mulog2sumlem2  23856  vmalogdivsum2  23859  log2sumbnd  23865  selberg3lem1  23878  selberg3lem2  23879  selberg4lem1  23881  selberg4  23882  selberg34r  23892  pntrlog2bndlem2  23899  pntrlog2bndlem3  23900  pntrlog2bndlem4  23901  pntrlog2bndlem5  23902  pntpbnd1a  23906  pntpbnd2  23908  pntibndlem1  23910  pntibndlem2  23912  pntlemd  23915  pntlemc  23916  pntlemb  23918  pntlemq  23922  pntlemr  23923  pntlemj  23924  pntlemf  23926  pntlemo  23928  pntlem3  23930  pntleml  23932  pnt  23935  padicabvcxp  23953  ostth2lem4  23957  ostth2  23958  ostth3  23959  smcnlem  25745  blocnilem  25857  ubthlem2  25925  bcm1n  27783  probmeasb  28588  signsply0  28727  zetacvg  28782  lgamucov  28805  iprodgam  29327  faclimlem1  29370  faclimlem3  29372  faclim  29373  iprodfac  29374  mblfinlem3  30254  itg2addnclem3  30270  ftc1cnnclem  30290  geomcau  30454  cntotbnd  30494  heibor1lem  30507  rrndstprj2  30529  rrncmslem  30530  pell1qrgaplem  31010  pellfund14  31035  rmxyneg  31057  rmxy1  31059  rmxy0  31060  jm2.23  31140  proot1ex  31365  cvgdvgrat  31398  binomcxplemnn0  31458  binomcxplemnotnn0  31465  0ellimcdiv  31856  limclner  31858  dvdivbd  31921  stoweidlem1  31984  stoweidlem3  31986  stoweidlem7  31990  stoweidlem11  31994  stoweidlem14  31997  stoweidlem24  32007  stoweidlem25  32008  stoweidlem26  32009  stoweidlem42  32025  stoweidlem51  32034  stoweidlem59  32042  stoweidlem62  32045  wallispilem4  32051  wallispilem5  32052  wallispi  32053  wallispi2lem1  32054  stirlinglem4  32060  stirlinglem8  32064  stirlinglem12  32068  stirlinglem15  32071  dirkercncflem4  32089  fourierdlem30  32120  fourierdlem73  32163  fourierdlem87  32177  dignn0flhalflem2  33472
  Copyright terms: Public domain W3C validator