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

Theorem rpcnd 11709
Description: A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rpcnd (𝜑𝐴 ∈ ℂ)

Proof of Theorem rpcnd
StepHypRef Expression
1 rpred.1 . . 3 (𝜑𝐴 ∈ ℝ+)
21rpred 11707 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 9925 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cc 9791  +crp 11667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9850
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-rp 11668
This theorem is referenced by:  rpcnne0d  11716  ltaddrp2d  11741  iccf1o  12146  ltexp2r  12737  discr  12821  bcp1nk  12924  bcpasc  12928  sqrlem6  13785  sqrtdiv  13803  absdiv  13832  o1rlimmul  14146  isumrpcl  14363  isumltss  14368  expcnv  14384  mertenslem1  14404  bitsmod  14945  nmoi2  22292  reperflem  22377  icchmeo  22496  icopnfcnv  22497  lebnumlem3  22518  nmoleub2lem2  22672  nmoleub3  22675  minveclem3  22953  pjthlem1  22961  ovollb2lem  23008  sca2rab  23032  ovolscalem1  23033  ovolsca  23035  itg2mulc  23265  itg2cnlem2  23280  c1liplem1  23508  lhop1  23526  aalioulem4  23839  aaliou2b  23845  aaliou3lem2  23847  aaliou3lem3  23848  aaliou3lem8  23849  aaliou3lem6  23852  aaliou3lem7  23853  itgulm  23911  dvradcnv  23924  pserdvlem2  23931  abelthlem7  23941  abelthlem8  23942  lognegb  24085  logno1  24127  advlog  24145  advlogexp  24146  cxprec  24177  divcxp  24178  cxpsqrt  24194  dvcxp1  24226  cxpcn3lem  24233  loglesqrt  24244  relogbval  24255  nnlogbexp  24264  logbrec  24265  asinlem3  24343  cxplim  24443  rlimcxp  24445  cxp2limlem  24447  cxp2lim  24448  cxploglim  24449  cxploglim2  24450  divsqrtsumlem  24451  divsqrtsumo1  24455  amgmlem  24461  zetacvg  24486  lgamucov  24509  basellem3  24554  basellem4  24555  chpval2  24688  logexprlim  24695  bclbnd  24750  bposlem9  24762  chebbnd1lem3  24905  chebbnd1  24906  chtppilimlem2  24908  chtppilim  24909  chebbnd2  24911  chto1lb  24912  chpchtlim  24913  chpo1ubb  24915  rplogsumlem1  24918  rplogsumlem2  24919  dchrvmasumlem1  24929  dchrvmasum2lem  24930  dchrisum0lema  24948  dchrisum0lem1b  24949  dchrisum0lem1  24950  dchrisum0lem2a  24951  dchrisum0lem2  24952  dchrisum0lem3  24953  dchrisum0  24954  mulogsumlem  24965  mulog2sumlem1  24968  mulog2sumlem2  24969  vmalogdivsum2  24972  log2sumbnd  24978  selberg3lem1  24991  selberg3lem2  24992  selberg4lem1  24994  selberg4  24995  selberg34r  25005  pntrlog2bndlem2  25012  pntrlog2bndlem3  25013  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  pntpbnd1a  25019  pntpbnd2  25021  pntibndlem1  25023  pntibndlem2  25025  pntlemd  25028  pntlemc  25029  pntlemb  25031  pntlemq  25035  pntlemr  25036  pntlemj  25037  pntlemf  25039  pntlemo  25041  pntlem3  25043  pntleml  25045  pnt  25048  padicabvcxp  25066  ostth2lem4  25070  ostth2  25071  ostth3  25072  smcnlem  26730  blocnilem  26837  ubthlem2  26905  bcm1n  28735  probmeasb  29613  signsply0  29748  iprodgam  30675  faclimlem1  30676  faclimlem3  30678  faclim  30679  iprodfac  30680  knoppndvlem17  31483  mblfinlem3  32412  itg2addnclem3  32427  ftc1cnnclem  32447  geomcau  32519  cntotbnd  32559  heibor1lem  32572  rrndstprj2  32594  rrncmslem  32595  pell1qrgaplem  36249  pellfund14  36274  rmxyneg  36297  rmxy1  36299  rmxy0  36300  jm2.23  36375  proot1ex  36592  amgm2d  37317  amgm3d  37318  amgm4d  37319  cvgdvgrat  37328  binomcxplemnn0  37364  binomcxplemnotnn0  37371  ltdivgt1  38307  xralrple4  38324  xralrple3  38325  0ellimcdiv  38510  limclner  38512  fprodsubrecnncnvlem  38588  fprodaddrecnncnvlem  38590  dvdivbd  38607  stoweidlem1  38688  stoweidlem3  38690  stoweidlem7  38694  stoweidlem11  38698  stoweidlem14  38701  stoweidlem24  38711  stoweidlem25  38712  stoweidlem26  38713  stoweidlem42  38729  stoweidlem51  38738  stoweidlem59  38746  stoweidlem62  38749  wallispilem4  38755  wallispilem5  38756  wallispi  38757  wallispi2lem1  38758  stirlinglem4  38764  stirlinglem8  38768  stirlinglem12  38772  stirlinglem15  38775  dirkercncflem4  38793  fourierdlem30  38824  fourierdlem73  38866  fourierdlem87  38880  qndenserrnbllem  38984  hoiqssbllem2  39307  dignn0flhalflem2  42200  amgmwlem  42310  amgmlemALT  42311  amgmw2d  42312  young2d  42313
  Copyright terms: Public domain W3C validator