Theorem rpcnd 11874

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

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 |- ( ph -> A e. RR+ )
2	1	rpred 11872	. 2 |- ( ph -> A e. RR )
3	2	recnd 10068	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-rp 11833

This theorem is referenced by:  rpcnne0d  11881  ltaddrp2d  11906  iccf1o  12316  ltexp2r  12917  discr  13001  bcp1nk  13104  bcpasc  13108  sqrlem6  13988  sqrtdiv  14006  absdiv  14035  o1rlimmul  14349  isumrpcl  14575  isumltss  14580  expcnv  14596  mertenslem1  14616  bitsmod  15158  nmoi2  22534  reperflem  22621  icchmeo  22740  icopnfcnv  22741  lebnumlem3  22762  nmoleub2lem2  22916  nmoleub3  22919  minveclem3  23200  pjthlem1  23208  ovollb2lem  23256  sca2rab  23280  ovolscalem1  23281  ovolsca  23283  itg2mulc  23514  itg2cnlem2  23529  c1liplem1  23759  lhop1  23777  aalioulem4  24090  aaliou2b  24096  aaliou3lem2  24098  aaliou3lem3  24099  aaliou3lem8  24100  aaliou3lem6  24103  aaliou3lem7  24104  itgulm  24162  dvradcnv  24175  pserdvlem2  24182  abelthlem7  24192  abelthlem8  24193  lognegb  24336  logno1  24382  advlog  24400  advlogexp  24401  cxprec  24432  divcxp  24433  cxpsqrt  24449  dvcxp1  24481  cxpcn3lem  24488  loglesqrt  24499  relogbval  24510  nnlogbexp  24519  logbrec  24520  asinlem3  24598  cxplim  24698  rlimcxp  24700  cxp2limlem  24702  cxp2lim  24703  cxploglim  24704  cxploglim2  24705  divsqrtsumlem  24706  divsqrtsumo1  24710  amgmlem  24716  zetacvg  24741  lgamucov  24764  basellem3  24809  basellem4  24810  chpval2  24943  logexprlim  24950  bclbnd  25005  bposlem9  25017  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem2  25163  chtppilim  25164  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ubb  25170  rplogsumlem1  25173  rplogsumlem2  25174  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  vmalogdivsum2  25227  log2sumbnd  25233  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  selberg4  25250  selberg34r  25260  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem1  25278  pntibndlem2  25280  pntlemd  25283  pntlemc  25284  pntlemb  25286  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemo  25296  pntlem3  25298  pntleml  25300  pnt  25303  padicabvcxp  25321  ostth2lem4  25325  ostth2  25326  ostth3  25327  smcnlem  27552  blocnilem  27659  ubthlem2  27727  bcm1n  29554  probmeasb  30492  signsply0  30628  iprodgam  31628  faclimlem1  31629  faclimlem3  31631  faclim  31632  iprodfac  31633  knoppndvlem17  32519  mblfinlem3  33448  itg2addnclem3  33463  ftc1cnnclem  33483  geomcau  33555  cntotbnd  33595  heibor1lem  33608  rrndstprj2  33630  rrncmslem  33631  pell1qrgaplem  37437  pellfund14  37462  rmxyneg  37485  rmxy1  37487  rmxy0  37488  jm2.23  37563  proot1ex  37779  amgm2d  38501  amgm3d  38502  amgm4d  38503  cvgdvgrat  38512  binomcxplemnn0  38548  binomcxplemnotnn0  38555  ltdivgt1  39572  xralrple4  39589  xralrple3  39590  0ellimcdiv  39881  limclner  39883  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvdivbd  40138  stoweidlem1  40218  stoweidlem3  40220  stoweidlem7  40224  stoweidlem11  40228  stoweidlem14  40231  stoweidlem24  40241  stoweidlem25  40242  stoweidlem26  40243  stoweidlem42  40259  stoweidlem51  40268  stoweidlem59  40276  stoweidlem62  40279  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  stirlinglem4  40294  stirlinglem8  40298  stirlinglem12  40302  stirlinglem15  40305  dirkercncflem4  40323  fourierdlem30  40354  fourierdlem73  40396  fourierdlem87  40410  qndenserrnbllem  40514  hoiqssbllem2  40837  dignn0flhalflem2  42410  amgmwlem  42548  amgmlemALT  42549  amgmw2d  42550  young2d  42551