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

Theorem rpcnd 12087
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 12085 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10280 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cc 10146  +crp 12045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-in 3722  df-ss 3729  df-rp 12046
This theorem is referenced by:  rpcnne0d  12094  ltaddrp2d  12119  iccf1o  12529  ltexp2r  13131  discr  13215  bcp1nk  13318  bcpasc  13322  sqrlem6  14207  sqrtdiv  14225  absdiv  14254  o1rlimmul  14568  isumrpcl  14794  isumltss  14799  expcnv  14815  mertenslem1  14835  bitsmod  15380  nmoi2  22755  reperflem  22842  icchmeo  22961  icopnfcnv  22962  lebnumlem3  22983  nmoleub2lem2  23136  nmoleub3  23139  minveclem3  23420  pjthlem1  23428  ovollb2lem  23476  sca2rab  23500  ovolscalem1  23501  ovolsca  23503  itg2mulc  23733  itg2cnlem2  23748  c1liplem1  23978  lhop1  23996  aalioulem4  24309  aaliou2b  24315  aaliou3lem2  24317  aaliou3lem3  24318  aaliou3lem8  24319  aaliou3lem6  24322  aaliou3lem7  24323  itgulm  24381  dvradcnv  24394  pserdvlem2  24401  abelthlem7  24411  abelthlem8  24412  lognegb  24556  logno1  24602  advlog  24620  advlogexp  24621  cxprec  24652  divcxp  24653  cxpsqrt  24669  dvcxp1  24701  cxpcn3lem  24708  loglesqrt  24719  relogbval  24730  nnlogbexp  24739  logbrec  24740  asinlem3  24818  cxplim  24918  rlimcxp  24920  cxp2limlem  24922  cxp2lim  24923  cxploglim  24924  cxploglim2  24925  divsqrtsumlem  24926  divsqrtsumo1  24930  amgmlem  24936  zetacvg  24961  lgamucov  24984  basellem3  25029  basellem4  25030  chpval2  25163  logexprlim  25170  bclbnd  25225  bposlem9  25237  chebbnd1lem3  25380  chebbnd1  25381  chtppilimlem2  25383  chtppilim  25384  chebbnd2  25386  chto1lb  25387  chpchtlim  25388  chpo1ubb  25390  rplogsumlem1  25393  rplogsumlem2  25394  dchrvmasumlem1  25404  dchrvmasum2lem  25405  dchrisum0lema  25423  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0lem3  25428  dchrisum0  25429  mulogsumlem  25440  mulog2sumlem1  25443  mulog2sumlem2  25444  vmalogdivsum2  25447  log2sumbnd  25453  selberg3lem1  25466  selberg3lem2  25467  selberg4lem1  25469  selberg4  25470  selberg34r  25480  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem4  25489  pntrlog2bndlem5  25490  pntpbnd1a  25494  pntpbnd2  25496  pntibndlem1  25498  pntibndlem2  25500  pntlemd  25503  pntlemc  25504  pntlemb  25506  pntlemq  25510  pntlemr  25511  pntlemj  25512  pntlemf  25514  pntlemo  25516  pntlem3  25518  pntleml  25520  pnt  25523  padicabvcxp  25541  ostth2lem4  25545  ostth2  25546  ostth3  25547  smcnlem  27882  blocnilem  27989  ubthlem2  28057  bcm1n  29884  probmeasb  30822  signsply0  30958  iprodgam  31956  faclimlem1  31957  faclimlem3  31959  faclim  31960  iprodfac  31961  knoppndvlem17  32846  mblfinlem3  33779  itg2addnclem3  33794  ftc1cnnclem  33814  geomcau  33886  cntotbnd  33926  heibor1lem  33939  rrndstprj2  33961  rrncmslem  33962  pell1qrgaplem  37957  pellfund14  37982  rmxyneg  38005  rmxy1  38007  rmxy0  38008  jm2.23  38083  proot1ex  38299  amgm2d  39021  amgm3d  39022  amgm4d  39023  cvgdvgrat  39032  binomcxplemnn0  39068  binomcxplemnotnn0  39075  ltdivgt1  40088  xralrple4  40105  xralrple3  40106  0ellimcdiv  40402  limclner  40404  fprodsubrecnncnvlem  40642  fprodaddrecnncnvlem  40644  dvdivbd  40659  stoweidlem1  40739  stoweidlem3  40741  stoweidlem7  40745  stoweidlem11  40749  stoweidlem14  40752  stoweidlem24  40762  stoweidlem25  40763  stoweidlem26  40764  stoweidlem42  40780  stoweidlem51  40789  stoweidlem59  40797  stoweidlem62  40800  wallispilem4  40806  wallispilem5  40807  wallispi  40808  wallispi2lem1  40809  stirlinglem4  40815  stirlinglem8  40819  stirlinglem12  40823  stirlinglem15  40826  dirkercncflem4  40844  fourierdlem30  40875  fourierdlem73  40917  fourierdlem87  40931  qndenserrnbllem  41035  hoiqssbllem2  41361  dignn0flhalflem2  42938  amgmwlem  43079  amgmlemALT  43080  amgmw2d  43081  young2d  43082
  Copyright terms: Public domain W3C validator