Theorem rpcnd 13050

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℂcc 11086  ℝ⁺crp 13004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-rp 13005

This theorem is referenced by:  rpcnne0d  13057  ltaddrp2d  13082  prodge0ld  13114  iccf1o  13511  ltexp2r  14197  discr  14264  bcp1nk  14341  bcpasc  14345  01sqrexlem6  15286  sqrtdiv  15304  absdiv  15334  o1rlimmul  15658  isumrpcl  15885  isumltss  15890  expcnv  15906  mertenslem1  15926  bitsmod  16482  nmoi2  24844  reperflem  24933  icopnfcnv  25058  lebnumlem3  25079  nmoleub2lem2  25232  nmoleub3  25235  minveclem3  25545  pjthlem1  25553  ovollb2lem  25604  sca2rab  25628  ovolscalem1  25629  ovolsca  25631  itg2mulc  25863  itg2cnlem2  25878  c1liplem1  26112  lhop1  26130  aalioulem4  26453  aaliou2b  26459  aaliou3lem2  26461  aaliou3lem3  26462  aaliou3lem8  26463  aaliou3lem6  26466  aaliou3lem7  26467  itgulm  26525  dvradcnv  26538  pserdvlem2  26545  abelthlem7  26555  abelthlem8  26556  lognegb  26709  logno1  26755  advlog  26773  advlogexp  26774  cxprec  26805  divcxp  26806  cxpsqrt  26822  dvcxp1  26859  cxpcn3lem  26866  loglesqrt  26880  relogbval  26891  nnlogbexp  26900  logbrec  26901  asinlem3  26990  cxplim  27090  rlimcxp  27092  cxp2limlem  27094  cxp2lim  27095  cxploglim  27096  cxploglim2  27097  divsqrtsumlem  27098  divsqrtsumo1  27102  amgmlem  27108  zetacvg  27133  lgamucov  27156  basellem3  27201  basellem4  27202  chpval2  27336  logexprlim  27343  bclbnd  27398  bposlem9  27410  chebbnd1lem3  27589  chebbnd1  27590  chtppilimlem2  27592  chtppilim  27593  chebbnd2  27595  chto1lb  27596  chpchtlim  27597  chpo1ubb  27599  rplogsumlem1  27602  rplogsumlem2  27603  dchrvmasumlem1  27613  dchrvmasum2lem  27614  dchrisum0lema  27632  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  dchrisum0lem3  27637  dchrisum0  27638  mulogsumlem  27649  mulog2sumlem1  27652  mulog2sumlem2  27653  vmalogdivsum2  27656  log2sumbnd  27662  selberg3lem1  27675  selberg3lem2  27676  selberg4lem1  27678  selberg4  27679  selberg34r  27689  pntrlog2bndlem2  27696  pntrlog2bndlem3  27697  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  pntpbnd1a  27703  pntpbnd2  27705  pntibndlem1  27707  pntibndlem2  27709  pntlemd  27712  pntlemc  27713  pntlemb  27715  pntlemq  27719  pntlemr  27720  pntlemj  27721  pntlemf  27723  pntlemo  27725  pntlem3  27727  pntleml  27729  pnt  27732  padicabvcxp  27750  ostth2lem4  27754  ostth2  27755  ostth3  27756  smcnlem  30954  blocnilem  31061  ubthlem2  31128  bcm1n  33048  probmeasb  34732  signsply0  34850  iprodgam  36100  faclimlem1  36101  faclimlem3  36103  faclim  36104  iprodfac  36105  knoppndvlem17  36974  mblfinlem3  38165  itg2addnclem3  38179  ftc1cnnclem  38197  geomcau  38265  cntotbnd  38302  heibor1lem  38315  rrndstprj2  38337  rrncmslem  38338  relogbzexpd  42600  lcmineqlem21  42673  aks4d1p1p1  42687  aks4d1p6  42705  2ap1caineq  42769  exp11d  42942  rplog11d  42963  pell1qrgaplem  43457  pellfund14  43482  rmxyneg  43504  rmxy1  43506  rmxy0  43507  jm2.23  43580  proot1ex  43780  amgm2d  44781  amgm3d  44782  amgm4d  44783  cvgdvgrat  44882  binomcxplemnn0  44918  binomcxplemnotnn0  44925  ltdivgt1  45931  xralrple4  45947  xralrple3  45948  0ellimcdiv  46222  limclner  46224  fprodsubrecnncnvlem  46480  fprodaddrecnncnvlem  46482  dvdivbd  46496  stoweidlem1  46574  stoweidlem3  46576  stoweidlem7  46580  stoweidlem11  46584  stoweidlem14  46587  stoweidlem24  46597  stoweidlem25  46598  stoweidlem26  46599  stoweidlem42  46615  stoweidlem51  46624  stoweidlem59  46632  stoweidlem62  46635  wallispilem4  46641  wallispilem5  46642  wallispi  46643  wallispi2lem1  46644  stirlinglem4  46650  stirlinglem8  46654  stirlinglem12  46658  stirlinglem15  46661  dirkercncflem4  46679  fourierdlem30  46710  fourierdlem73  46752  fourierdlem87  46766  qndenserrnbllem  46867  hoiqssbllem2  47196  dignn0flhalflem2  49248  itsclc0yqsol  49396  amgmwlem  50432  amgmlemALT  50433  amgmw2d  50434  young2d  50435