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

Theorem rpcnd 12960
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 12958 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 11184 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 11050  +crp 12916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11109
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918  df-ss 3928  df-rp 12917
This theorem is referenced by:  rpcnne0d  12967  ltaddrp2d  12992  prodge0ld  13024  iccf1o  13414  ltexp2r  14079  discr  14144  bcp1nk  14218  bcpasc  14222  01sqrexlem6  15133  sqrtdiv  15151  absdiv  15181  o1rlimmul  15502  isumrpcl  15729  isumltss  15734  expcnv  15750  mertenslem1  15770  bitsmod  16317  nmoi2  24097  reperflem  24184  icchmeo  24307  icopnfcnv  24308  lebnumlem3  24329  nmoleub2lem2  24482  nmoleub3  24485  minveclem3  24796  pjthlem1  24804  ovollb2lem  24855  sca2rab  24879  ovolscalem1  24880  ovolsca  24882  itg2mulc  25115  itg2cnlem2  25130  c1liplem1  25363  lhop1  25381  aalioulem4  25698  aaliou2b  25704  aaliou3lem2  25706  aaliou3lem3  25707  aaliou3lem8  25708  aaliou3lem6  25711  aaliou3lem7  25712  itgulm  25770  dvradcnv  25783  pserdvlem2  25790  abelthlem7  25800  abelthlem8  25801  lognegb  25948  logno1  25994  advlog  26012  advlogexp  26013  cxprec  26044  divcxp  26045  cxpsqrt  26061  dvcxp1  26096  cxpcn3lem  26103  loglesqrt  26114  relogbval  26125  nnlogbexp  26134  logbrec  26135  asinlem3  26224  cxplim  26324  rlimcxp  26326  cxp2limlem  26328  cxp2lim  26329  cxploglim  26330  cxploglim2  26331  divsqrtsumlem  26332  divsqrtsumo1  26336  amgmlem  26342  zetacvg  26367  lgamucov  26390  basellem3  26435  basellem4  26436  chpval2  26569  logexprlim  26576  bclbnd  26631  bposlem9  26643  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem2  26825  chtppilim  26826  chebbnd2  26828  chto1lb  26829  chpchtlim  26830  chpo1ubb  26832  rplogsumlem1  26835  rplogsumlem2  26836  dchrvmasumlem1  26846  dchrvmasum2lem  26847  dchrisum0lema  26865  dchrisum0lem1b  26866  dchrisum0lem1  26867  dchrisum0lem2a  26868  dchrisum0lem2  26869  dchrisum0lem3  26870  dchrisum0  26871  mulogsumlem  26882  mulog2sumlem1  26885  mulog2sumlem2  26886  vmalogdivsum2  26889  log2sumbnd  26895  selberg3lem1  26908  selberg3lem2  26909  selberg4lem1  26911  selberg4  26912  selberg34r  26922  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntpbnd1a  26936  pntpbnd2  26938  pntibndlem1  26940  pntibndlem2  26942  pntlemd  26945  pntlemc  26946  pntlemb  26948  pntlemq  26952  pntlemr  26953  pntlemj  26954  pntlemf  26956  pntlemo  26958  pntlem3  26960  pntleml  26962  pnt  26965  padicabvcxp  26983  ostth2lem4  26987  ostth2  26988  ostth3  26989  smcnlem  29642  blocnilem  29749  ubthlem2  29816  bcm1n  31701  probmeasb  33033  signsply0  33166  iprodgam  34318  faclimlem1  34319  faclimlem3  34321  faclim  34322  iprodfac  34323  knoppndvlem17  34994  mblfinlem3  36120  itg2addnclem3  36134  ftc1cnnclem  36152  geomcau  36221  cntotbnd  36258  heibor1lem  36271  rrndstprj2  36293  rrncmslem  36294  relogbzexpd  40435  lcmineqlem21  40509  aks4d1p1p1  40523  aks4d1p6  40541  2ap1caineq  40556  exp11d  40814  pell1qrgaplem  41199  pellfund14  41224  rmxyneg  41247  rmxy1  41249  rmxy0  41250  jm2.23  41323  proot1ex  41531  amgm2d  42478  amgm3d  42479  amgm4d  42480  cvgdvgrat  42600  binomcxplemnn0  42636  binomcxplemnotnn0  42643  ltdivgt1  43597  xralrple4  43614  xralrple3  43615  0ellimcdiv  43897  limclner  43899  fprodsubrecnncnvlem  44155  fprodaddrecnncnvlem  44157  dvdivbd  44171  stoweidlem1  44249  stoweidlem3  44251  stoweidlem7  44255  stoweidlem11  44259  stoweidlem14  44262  stoweidlem24  44272  stoweidlem25  44273  stoweidlem26  44274  stoweidlem42  44290  stoweidlem51  44299  stoweidlem59  44307  stoweidlem62  44310  wallispilem4  44316  wallispilem5  44317  wallispi  44318  wallispi2lem1  44319  stirlinglem4  44325  stirlinglem8  44329  stirlinglem12  44333  stirlinglem15  44336  dirkercncflem4  44354  fourierdlem30  44385  fourierdlem73  44427  fourierdlem87  44441  qndenserrnbllem  44542  hoiqssbllem2  44871  dignn0flhalflem2  46709  itsclc0yqsol  46857  amgmwlem  47256  amgmlemALT  47257  amgmw2d  47258  young2d  47259
  Copyright terms: Public domain W3C validator