Theorem rpcnd 13193

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11225  ℝ⁺crp 13147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-rp 13148

This theorem is used by:  rpcnne0d  13200  ltaddrp2d  13225  prodge0ld  13257  iccf1o  13654  ltexp2r  14343  discr  14411  bcp1nk  14488  bcpasc  14492  01sqrexlem6  15443  sqrtdiv  15461  absdiv  15491  o1rlimmul  15815  isumrpcl  16041  isumltss  16046  expcnv  16062  mertenslem1  16082  bitsmod  16635  nmoi2  25079  reperflem  25168  icopnfcnv  25293  lebnumlem3  25314  nmoleub2lem2  25467  nmoleub3  25470  minveclem3  25780  pjthlem1  25788  ovollb2lem  25839  sca2rab  25863  ovolscalem1  25864  ovolsca  25866  itg2mulc  26098  itg2cnlem2  26113  c1liplem1  26346  lhop1  26364  aalioulem4  26692  aaliou2b  26698  aaliou3lem2  26700  aaliou3lem3  26701  aaliou3lem8  26702  aaliou3lem6  26705  aaliou3lem7  26706  itgulm  26765  dvradcnv  26778  pserdvlem2  26785  abelthlem7  26795  abelthlem8  26796  lognegb  26948  logno1  26994  advlog  27012  advlogexp  27013  cxprec  27044  divcxp  27045  cxpsqrt  27061  dvcxp1  27098  cxpcn3lem  27105  loglesqrt  27119  relogbval  27130  nnlogbexp  27139  logbrec  27140  asinlem3  27229  cxplim  27329  rlimcxp  27331  cxp2limlem  27333  cxp2lim  27334  cxploglim  27335  cxploglim2  27336  divsqrtsumlem  27337  divsqrtsumo1  27341  amgmlem  27347  zetacvg  27372  lgamucov  27395  basellem3  27440  basellem4  27441  basellem8  27445  chpval2  27575  logexprlim  27582  bclbnd  27637  bposlem9  27649  chebbnd1lem3  27828  chebbnd1  27829  chtppilimlem2  27831  chtppilim  27832  chebbnd2  27834  chto1lb  27835  chpchtlim  27836  chpo1ubb  27838  rplogsumlem1  27841  rplogsumlem2  27842  dchrvmasumlem1  27852  dchrvmasum2lem  27853  dchrisum0lema  27871  dchrisum0lem1b  27872  dchrisum0lem1  27873  dchrisum0lem2a  27874  dchrisum0lem2  27875  dchrisum0lem3  27876  dchrisum0  27877  mulogsumlem  27888  mulog2sumlem1  27891  mulog2sumlem2  27892  vmalogdivsum2  27895  log2sumbnd  27901  selberg3lem1  27914  selberg3lem2  27915  selberg4lem1  27917  selberg4  27918  selberg34r  27928  pntrlog2bndlem2  27935  pntrlog2bndlem3  27936  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntpbnd1a  27942  pntpbnd2  27944  pntibndlem1  27946  pntibndlem2  27948  pntlemd  27951  pntlemc  27952  pntlemb  27954  pntlemq  27958  pntlemr  27959  pntlemj  27960  pntlemf  27962  pntlemo  27964  pntlem3  27966  pntleml  27968  pnt  27971  padicabvcxp  27989  ostth2lem4  27993  ostth2  27994  ostth3  27995  smcnlem  31329  blocnilem  31436  ubthlem2  31503  bcm1n  33457  omssubadd  35002  probmeasb  35132  signsply0  35250  iprodgam  36685  faclimlem1  36686  faclimlem3  36688  faclim  36689  iprodfac  36690  knoppndvlem17  37572  mblfinlem3  38769  itg2addnclem3  38783  ftc1cnnclem  38801  geomcau  38885  cntotbnd  38922  heibor1lem  38935  rrndstprj2  38957  rrncmslem  38958  relogbzexpd  43218  lcmineqlem21  43291  aks4d1p1p1  43305  aks4d1p6  43323  2ap1caineq  43387  exp11d  43576  rplog11d  43591  pell1qrgaplem  44073  pellfund14  44098  rmxyneg  44120  rmxy1  44122  rmxy0  44123  jm2.23  44196  proot1ex  44390  amgm2d  45390  amgm3d  45391  amgm4d  45392  cvgdvgrat  45489  binomcxplemnn0  45525  binomcxplemnotnn0  45532  ltdivgt1  46573  xralrple4  46589  xralrple3  46590  0ellimcdiv  46864  limclner  46866  fprodsubrecnncnvlem  47122  fprodaddrecnncnvlem  47124  dvdivbd  47138  stoweidlem1  47216  stoweidlem3  47218  stoweidlem7  47222  stoweidlem11  47226  stoweidlem14  47229  stoweidlem24  47239  stoweidlem25  47240  stoweidlem26  47241  stoweidlem42  47257  stoweidlem51  47266  stoweidlem59  47274  stoweidlem62  47277  wallispilem4  47283  wallispilem5  47284  wallispi  47285  wallispi2lem1  47286  stirlinglem4  47292  stirlinglem8  47296  stirlinglem12  47300  stirlinglem15  47303  dirkercncflem4  47321  fourierdlem30  47352  fourierdlem73  47394  fourierdlem87  47408  qndenserrnbllem  47509  hoiqssbllem2  47838  dignn0flhalflem2  49933  itsclc0yqsol  50081  amgmwlem  51267  amgmlemALT  51268  amgmw2d  51269  young2d  51270