Theorem rpcnd 12986

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11034  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907  df-rp 12941

This theorem is referenced by:  rpcnne0d  12993  ltaddrp2d  13018  prodge0ld  13050  iccf1o  13447  ltexp2r  14133  discr  14200  bcp1nk  14277  bcpasc  14281  01sqrexlem6  15207  sqrtdiv  15225  absdiv  15255  o1rlimmul  15579  isumrpcl  15806  isumltss  15811  expcnv  15827  mertenslem1  15847  bitsmod  16403  nmoi2  24720  reperflem  24809  icopnfcnv  24934  lebnumlem3  24955  nmoleub2lem2  25108  nmoleub3  25111  minveclem3  25421  pjthlem1  25429  ovollb2lem  25480  sca2rab  25504  ovolscalem1  25505  ovolsca  25507  itg2mulc  25739  itg2cnlem2  25754  c1liplem1  25988  lhop1  26006  aalioulem4  26326  aaliou2b  26332  aaliou3lem2  26334  aaliou3lem3  26335  aaliou3lem8  26336  aaliou3lem6  26339  aaliou3lem7  26340  itgulm  26398  dvradcnv  26411  pserdvlem2  26418  abelthlem7  26428  abelthlem8  26429  lognegb  26579  logno1  26625  advlog  26643  advlogexp  26644  cxprec  26675  divcxp  26676  cxpsqrt  26692  dvcxp1  26729  cxpcn3lem  26736  loglesqrt  26750  relogbval  26761  nnlogbexp  26770  logbrec  26771  asinlem3  26860  cxplim  26960  rlimcxp  26962  cxp2limlem  26964  cxp2lim  26965  cxploglim  26966  cxploglim2  26967  divsqrtsumlem  26968  divsqrtsumo1  26972  amgmlem  26978  zetacvg  27003  lgamucov  27026  basellem3  27071  basellem4  27072  chpval2  27206  logexprlim  27213  bclbnd  27268  bposlem9  27280  chebbnd1lem3  27459  chebbnd1  27460  chtppilimlem2  27462  chtppilim  27463  chebbnd2  27465  chto1lb  27466  chpchtlim  27467  chpo1ubb  27469  rplogsumlem1  27472  rplogsumlem2  27473  dchrvmasumlem1  27483  dchrvmasum2lem  27484  dchrisum0lema  27502  dchrisum0lem1b  27503  dchrisum0lem1  27504  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0lem3  27507  dchrisum0  27508  mulogsumlem  27519  mulog2sumlem1  27522  mulog2sumlem2  27523  vmalogdivsum2  27526  log2sumbnd  27532  selberg3lem1  27545  selberg3lem2  27546  selberg4lem1  27548  selberg4  27549  selberg34r  27559  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntpbnd1a  27573  pntpbnd2  27575  pntibndlem1  27577  pntibndlem2  27579  pntlemd  27582  pntlemc  27583  pntlemb  27585  pntlemq  27589  pntlemr  27590  pntlemj  27591  pntlemf  27593  pntlemo  27595  pntlem3  27597  pntleml  27599  pnt  27602  padicabvcxp  27620  ostth2lem4  27624  ostth2  27625  ostth3  27626  smcnlem  30793  blocnilem  30900  ubthlem2  30967  bcm1n  32894  probmeasb  34621  signsply0  34742  iprodgam  35971  faclimlem1  35972  faclimlem3  35974  faclim  35975  iprodfac  35976  knoppndvlem17  36835  mblfinlem3  38027  itg2addnclem3  38041  ftc1cnnclem  38059  geomcau  38127  cntotbnd  38164  heibor1lem  38177  rrndstprj2  38199  rrncmslem  38200  relogbzexpd  42462  lcmineqlem21  42535  aks4d1p1p1  42549  aks4d1p6  42567  2ap1caineq  42631  exp11d  42804  rplog11d  42825  pell1qrgaplem  43319  pellfund14  43344  rmxyneg  43366  rmxy1  43368  rmxy0  43369  jm2.23  43442  proot1ex  43642  amgm2d  44643  amgm3d  44644  amgm4d  44645  cvgdvgrat  44758  binomcxplemnn0  44794  binomcxplemnotnn0  44801  ltdivgt1  45802  xralrple4  45818  xralrple3  45819  0ellimcdiv  46093  limclner  46095  fprodsubrecnncnvlem  46351  fprodaddrecnncnvlem  46353  dvdivbd  46367  stoweidlem1  46445  stoweidlem3  46447  stoweidlem7  46451  stoweidlem11  46455  stoweidlem14  46458  stoweidlem24  46468  stoweidlem25  46469  stoweidlem26  46470  stoweidlem42  46486  stoweidlem51  46495  stoweidlem59  46503  stoweidlem62  46506  wallispilem4  46512  wallispilem5  46513  wallispi  46514  wallispi2lem1  46515  stirlinglem4  46521  stirlinglem8  46525  stirlinglem12  46529  stirlinglem15  46532  dirkercncflem4  46550  fourierdlem30  46581  fourierdlem73  46623  fourierdlem87  46637  qndenserrnbllem  46738  hoiqssbllem2  47067  dignn0flhalflem2  49108  itsclc0yqsol  49256  amgmwlem  50293  amgmlemALT  50294  amgmw2d  50295  young2d  50296