Theorem rpcnd 13029

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 13027	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11200	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 11061  ℝ⁺crp 12983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-resscn 11120

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-ss 3916  df-rp 12984

This theorem is referenced by:  rpcnne0d  13036  ltaddrp2d  13061  prodge0ld  13093  iccf1o  13490  ltexp2r  14176  discr  14243  bcp1nk  14320  bcpasc  14324  01sqrexlem6  15250  sqrtdiv  15268  absdiv  15298  o1rlimmul  15622  isumrpcl  15849  isumltss  15854  expcnv  15870  mertenslem1  15890  bitsmod  16446  nmoi2  24763  reperflem  24852  icopnfcnv  24977  lebnumlem3  24998  nmoleub2lem2  25151  nmoleub3  25154  minveclem3  25464  pjthlem1  25472  ovollb2lem  25523  sca2rab  25547  ovolscalem1  25548  ovolsca  25550  itg2mulc  25782  itg2cnlem2  25797  c1liplem1  26031  lhop1  26049  aalioulem4  26369  aaliou2b  26375  aaliou3lem2  26377  aaliou3lem3  26378  aaliou3lem8  26379  aaliou3lem6  26382  aaliou3lem7  26383  itgulm  26441  dvradcnv  26454  pserdvlem2  26461  abelthlem7  26471  abelthlem8  26472  lognegb  26625  logno1  26671  advlog  26689  advlogexp  26690  cxprec  26721  divcxp  26722  cxpsqrt  26738  dvcxp1  26775  cxpcn3lem  26782  loglesqrt  26796  relogbval  26807  nnlogbexp  26816  logbrec  26817  asinlem3  26906  cxplim  27006  rlimcxp  27008  cxp2limlem  27010  cxp2lim  27011  cxploglim  27012  cxploglim2  27013  divsqrtsumlem  27014  divsqrtsumo1  27018  amgmlem  27024  zetacvg  27049  lgamucov  27072  basellem3  27117  basellem4  27118  chpval2  27252  logexprlim  27259  bclbnd  27314  bposlem9  27326  chebbnd1lem3  27505  chebbnd1  27506  chtppilimlem2  27508  chtppilim  27509  chebbnd2  27511  chto1lb  27512  chpchtlim  27513  chpo1ubb  27515  rplogsumlem1  27518  rplogsumlem2  27519  dchrvmasumlem1  27529  dchrvmasum2lem  27530  dchrisum0lema  27548  dchrisum0lem1b  27549  dchrisum0lem1  27550  dchrisum0lem2a  27551  dchrisum0lem2  27552  dchrisum0lem3  27553  dchrisum0  27554  mulogsumlem  27565  mulog2sumlem1  27568  mulog2sumlem2  27569  vmalogdivsum2  27572  log2sumbnd  27578  selberg3lem1  27591  selberg3lem2  27592  selberg4lem1  27594  selberg4  27595  selberg34r  27605  pntrlog2bndlem2  27612  pntrlog2bndlem3  27613  pntrlog2bndlem4  27614  pntrlog2bndlem5  27615  pntpbnd1a  27619  pntpbnd2  27621  pntibndlem1  27623  pntibndlem2  27625  pntlemd  27628  pntlemc  27629  pntlemb  27631  pntlemq  27635  pntlemr  27636  pntlemj  27637  pntlemf  27639  pntlemo  27641  pntlem3  27643  pntleml  27645  pnt  27648  padicabvcxp  27666  ostth2lem4  27670  ostth2  27671  ostth3  27672  smcnlem  30839  blocnilem  30946  ubthlem2  31013  bcm1n  32940  probmeasb  34681  signsply0  34802  iprodgam  36040  faclimlem1  36041  faclimlem3  36043  faclim  36044  iprodfac  36045  knoppndvlem17  36914  mblfinlem3  38106  itg2addnclem3  38120  ftc1cnnclem  38138  geomcau  38206  cntotbnd  38243  heibor1lem  38256  rrndstprj2  38278  rrncmslem  38279  relogbzexpd  42541  lcmineqlem21  42614  aks4d1p1p1  42628  aks4d1p6  42646  2ap1caineq  42710  exp11d  42883  rplog11d  42904  pell1qrgaplem  43398  pellfund14  43423  rmxyneg  43445  rmxy1  43447  rmxy0  43448  jm2.23  43521  proot1ex  43721  amgm2d  44722  amgm3d  44723  amgm4d  44724  cvgdvgrat  44837  binomcxplemnn0  44873  binomcxplemnotnn0  44880  ltdivgt1  45880  xralrple4  45896  xralrple3  45897  0ellimcdiv  46171  limclner  46173  fprodsubrecnncnvlem  46429  fprodaddrecnncnvlem  46431  dvdivbd  46445  stoweidlem1  46523  stoweidlem3  46525  stoweidlem7  46529  stoweidlem11  46533  stoweidlem14  46536  stoweidlem24  46546  stoweidlem25  46547  stoweidlem26  46548  stoweidlem42  46564  stoweidlem51  46573  stoweidlem59  46581  stoweidlem62  46584  wallispilem4  46590  wallispilem5  46591  wallispi  46592  wallispi2lem1  46593  stirlinglem4  46599  stirlinglem8  46603  stirlinglem12  46607  stirlinglem15  46610  dirkercncflem4  46628  fourierdlem30  46659  fourierdlem73  46701  fourierdlem87  46715  qndenserrnbllem  46816  hoiqssbllem2  47145  dignn0flhalflem2  49186  itsclc0yqsol  49334  amgmwlem  50371  amgmlemALT  50372  amgmw2d  50373  young2d  50374