Theorem rpcnd 12432

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

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 12430	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 10668	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10534  ℝ⁺crp 12388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-resscn 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3942  df-ss 3951  df-rp 12389

This theorem is referenced by:  rpcnne0d  12439  ltaddrp2d  12464  prodge0ld  12496  iccf1o  12881  ltexp2r  13536  discr  13600  bcp1nk  13676  bcpasc  13680  sqrlem6  14606  sqrtdiv  14624  absdiv  14654  o1rlimmul  14974  isumrpcl  15197  isumltss  15202  expcnv  15218  mertenslem1  15239  bitsmod  15784  nmoi2  23338  reperflem  23425  icchmeo  23544  icopnfcnv  23545  lebnumlem3  23566  nmoleub2lem2  23719  nmoleub3  23722  minveclem3  24031  pjthlem1  24039  ovollb2lem  24088  sca2rab  24112  ovolscalem1  24113  ovolsca  24115  itg2mulc  24347  itg2cnlem2  24362  c1liplem1  24592  lhop1  24610  aalioulem4  24923  aaliou2b  24929  aaliou3lem2  24931  aaliou3lem3  24932  aaliou3lem8  24933  aaliou3lem6  24936  aaliou3lem7  24937  itgulm  24995  dvradcnv  25008  pserdvlem2  25015  abelthlem7  25025  abelthlem8  25026  lognegb  25172  logno1  25218  advlog  25236  advlogexp  25237  cxprec  25268  divcxp  25269  cxpsqrt  25285  dvcxp1  25320  cxpcn3lem  25327  loglesqrt  25338  relogbval  25349  nnlogbexp  25358  logbrec  25359  asinlem3  25448  cxplim  25548  rlimcxp  25550  cxp2limlem  25552  cxp2lim  25553  cxploglim  25554  cxploglim2  25555  divsqrtsumlem  25556  divsqrtsumo1  25560  amgmlem  25566  zetacvg  25591  lgamucov  25614  basellem3  25659  basellem4  25660  chpval2  25793  logexprlim  25800  bclbnd  25855  bposlem9  25867  chebbnd1lem3  26046  chebbnd1  26047  chtppilimlem2  26049  chtppilim  26050  chebbnd2  26052  chto1lb  26053  chpchtlim  26054  chpo1ubb  26056  rplogsumlem1  26059  rplogsumlem2  26060  dchrvmasumlem1  26070  dchrvmasum2lem  26071  dchrisum0lema  26089  dchrisum0lem1b  26090  dchrisum0lem1  26091  dchrisum0lem2a  26092  dchrisum0lem2  26093  dchrisum0lem3  26094  dchrisum0  26095  mulogsumlem  26106  mulog2sumlem1  26109  mulog2sumlem2  26110  vmalogdivsum2  26113  log2sumbnd  26119  selberg3lem1  26132  selberg3lem2  26133  selberg4lem1  26135  selberg4  26136  selberg34r  26146  pntrlog2bndlem2  26153  pntrlog2bndlem3  26154  pntrlog2bndlem4  26155  pntrlog2bndlem5  26156  pntpbnd1a  26160  pntpbnd2  26162  pntibndlem1  26164  pntibndlem2  26166  pntlemd  26169  pntlemc  26170  pntlemb  26172  pntlemq  26176  pntlemr  26177  pntlemj  26178  pntlemf  26180  pntlemo  26182  pntlem3  26184  pntleml  26186  pnt  26189  padicabvcxp  26207  ostth2lem4  26211  ostth2  26212  ostth3  26213  smcnlem  28473  blocnilem  28580  ubthlem2  28647  bcm1n  30517  probmeasb  31688  signsply0  31821  iprodgam  32974  faclimlem1  32975  faclimlem3  32977  faclim  32978  iprodfac  32979  knoppndvlem17  33867  mblfinlem3  34930  itg2addnclem3  34944  ftc1cnnclem  34964  geomcau  35033  cntotbnd  35073  heibor1lem  35086  rrndstprj2  35108  rrncmslem  35109  cxpgt0d  39178  exp11d  39187  pell1qrgaplem  39468  pellfund14  39493  rmxyneg  39515  rmxy1  39517  rmxy0  39518  jm2.23  39591  proot1ex  39799  amgm2d  40549  amgm3d  40550  amgm4d  40551  cvgdvgrat  40643  binomcxplemnn0  40679  binomcxplemnotnn0  40686  ltdivgt1  41622  xralrple4  41639  xralrple3  41640  0ellimcdiv  41928  limclner  41930  fprodsubrecnncnvlem  42189  fprodaddrecnncnvlem  42191  dvdivbd  42206  stoweidlem1  42285  stoweidlem3  42287  stoweidlem7  42291  stoweidlem11  42295  stoweidlem14  42298  stoweidlem24  42308  stoweidlem25  42309  stoweidlem26  42310  stoweidlem42  42326  stoweidlem51  42335  stoweidlem59  42343  stoweidlem62  42346  wallispilem4  42352  wallispilem5  42353  wallispi  42354  wallispi2lem1  42355  stirlinglem4  42361  stirlinglem8  42365  stirlinglem12  42369  stirlinglem15  42372  dirkercncflem4  42390  fourierdlem30  42421  fourierdlem73  42463  fourierdlem87  42477  qndenserrnbllem  42578  hoiqssbllem2  42904  dignn0flhalflem2  44675  itsclc0yqsol  44750  amgmwlem  44902  amgmlemALT  44903  amgmw2d  44904  young2d  44905