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

Theorem rpcnd 11912
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 11910 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10106 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cc 9972  +crp 11870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-in 3614  df-ss 3621  df-rp 11871
This theorem is referenced by:  rpcnne0d  11919  ltaddrp2d  11944  iccf1o  12354  ltexp2r  12957  discr  13041  bcp1nk  13144  bcpasc  13148  sqrlem6  14032  sqrtdiv  14050  absdiv  14079  o1rlimmul  14393  isumrpcl  14619  isumltss  14624  expcnv  14640  mertenslem1  14660  bitsmod  15205  nmoi2  22581  reperflem  22668  icchmeo  22787  icopnfcnv  22788  lebnumlem3  22809  nmoleub2lem2  22962  nmoleub3  22965  minveclem3  23246  pjthlem1  23254  ovollb2lem  23302  sca2rab  23326  ovolscalem1  23327  ovolsca  23329  itg2mulc  23559  itg2cnlem2  23574  c1liplem1  23804  lhop1  23822  aalioulem4  24135  aaliou2b  24141  aaliou3lem2  24143  aaliou3lem3  24144  aaliou3lem8  24145  aaliou3lem6  24148  aaliou3lem7  24149  itgulm  24207  dvradcnv  24220  pserdvlem2  24227  abelthlem7  24237  abelthlem8  24238  lognegb  24381  logno1  24427  advlog  24445  advlogexp  24446  cxprec  24477  divcxp  24478  cxpsqrt  24494  dvcxp1  24526  cxpcn3lem  24533  loglesqrt  24544  relogbval  24555  nnlogbexp  24564  logbrec  24565  asinlem3  24643  cxplim  24743  rlimcxp  24745  cxp2limlem  24747  cxp2lim  24748  cxploglim  24749  cxploglim2  24750  divsqrtsumlem  24751  divsqrtsumo1  24755  amgmlem  24761  zetacvg  24786  lgamucov  24809  basellem3  24854  basellem4  24855  chpval2  24988  logexprlim  24995  bclbnd  25050  bposlem9  25062  chebbnd1lem3  25205  chebbnd1  25206  chtppilimlem2  25208  chtppilim  25209  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ubb  25215  rplogsumlem1  25218  rplogsumlem2  25219  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  dchrisum0  25254  mulogsumlem  25265  mulog2sumlem1  25268  mulog2sumlem2  25269  vmalogdivsum2  25272  log2sumbnd  25278  selberg3lem1  25291  selberg3lem2  25292  selberg4lem1  25294  selberg4  25295  selberg34r  25305  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem1  25323  pntibndlem2  25325  pntlemd  25328  pntlemc  25329  pntlemb  25331  pntlemq  25335  pntlemr  25336  pntlemj  25337  pntlemf  25339  pntlemo  25341  pntlem3  25343  pntleml  25345  pnt  25348  padicabvcxp  25366  ostth2lem4  25370  ostth2  25371  ostth3  25372  smcnlem  27680  blocnilem  27787  ubthlem2  27855  bcm1n  29682  probmeasb  30620  signsply0  30756  iprodgam  31754  faclimlem1  31755  faclimlem3  31757  faclim  31758  iprodfac  31759  knoppndvlem17  32644  mblfinlem3  33578  itg2addnclem3  33593  ftc1cnnclem  33613  geomcau  33685  cntotbnd  33725  heibor1lem  33738  rrndstprj2  33760  rrncmslem  33761  pell1qrgaplem  37754  pellfund14  37779  rmxyneg  37802  rmxy1  37804  rmxy0  37805  jm2.23  37880  proot1ex  38096  amgm2d  38818  amgm3d  38819  amgm4d  38820  cvgdvgrat  38829  binomcxplemnn0  38865  binomcxplemnotnn0  38872  ltdivgt1  39885  xralrple4  39902  xralrple3  39903  0ellimcdiv  40199  limclner  40201  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  dvdivbd  40456  stoweidlem1  40536  stoweidlem3  40538  stoweidlem7  40542  stoweidlem11  40546  stoweidlem14  40549  stoweidlem24  40559  stoweidlem25  40560  stoweidlem26  40561  stoweidlem42  40577  stoweidlem51  40586  stoweidlem59  40594  stoweidlem62  40597  wallispilem4  40603  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  stirlinglem4  40612  stirlinglem8  40616  stirlinglem12  40620  stirlinglem15  40623  dirkercncflem4  40641  fourierdlem30  40672  fourierdlem73  40714  fourierdlem87  40728  qndenserrnbllem  40832  hoiqssbllem2  41158  dignn0flhalflem2  42735  amgmwlem  42876  amgmlemALT  42877  amgmw2d  42878  young2d  42879
  Copyright terms: Public domain W3C validator