MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpcn Structured version   Visualization version   GIF version

Theorem rpcn 12058
Description: A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
Assertion
Ref Expression
rpcn (𝐴 ∈ ℝ+𝐴 ∈ ℂ)

Proof of Theorem rpcn
StepHypRef Expression
1 rpre 12056 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21recnd 10356 1 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cc 10222  +crp 12049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-resscn 10281
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112  df-in 3783  df-ss 3790  df-rp 12050
This theorem is referenced by:  rpcnne0  12067  divge1  12115  ltdifltdiv  12862  modvalr  12898  flpmodeq  12900  mulmod0  12903  negmod0  12904  modlt  12906  moddiffl  12908  modvalp1  12916  modid  12922  modid0  12923  modcyc  12932  modcyc2  12933  modadd1  12934  muladdmodid  12937  modmuladdnn0  12941  negmod  12942  modm1p1mod0  12948  modmul1  12950  2txmodxeq0  12957  2submod  12958  moddi  12965  sqrlem2  14210  sqrtdiv  14232  caurcvgr  14630  o1fsum  14770  divrcnv  14809  efgt1p2  15067  efgt1p  15068  rpmsubg  20021  uniioombl  23576  abelthlem8  24413  reefgim  24424  pilem1  24425  logne0  24546  logneg  24554  advlogexp  24621  logcxp  24635  cxprec  24652  cxpmul  24654  abscxp  24658  logsqrt  24670  dvcxp1  24701  dvcxp2  24702  dvsqrt  24703  cxpcn2  24707  loglesqrt  24719  relogbreexp  24733  relogbzexp  24734  relogbmul  24735  relogbdiv  24737  relogbexp  24738  relogbcxp  24743  relogbcxpb  24745  relogbf  24749  rlimcnp  24912  efrlim  24916  cxplim  24918  sqrtlim  24919  cxploglim  24924  logdifbnd  24940  harmonicbnd4  24957  rpdmgm  24971  logfaclbnd  25167  logexprlim  25170  logfacrlim2  25171  vmadivsum  25391  dchrisum0lem1a  25395  dchrvmasumlema  25409  dchrisum0lem1  25425  dchrisum0lem2  25427  mudivsum  25439  mulogsumlem  25440  logdivsum  25442  selberg2lem  25459  selberg2  25460  pntrmax  25473  selbergr  25477  pntibndlem1  25498  pntlem3  25518  blocnilem  27993  nmcexi  29219  nmcopexi  29220  nmcfnexi  29244  dp20h  29918  dpexpp1  29947  0dp2dp  29948  sqsscirc1  30285  logdivsqrle  31059  taupilem3  33484  taupilem1  33486  poimirlem29  33753  heicant  33759  itg2addnclem3  33777  itg2gt0cn  33779  ftc1anclem6  33804  ftc1anclem8  33806  areacirclem1  33814  areacirclem4  33817  areacirc  33819  isbnd2  33895  cntotbnd  33908  heiborlem6  33928  heiborlem7  33929  irrapxlem5  37893  2timesgt  39983  xralrple2  40051  recnnltrp  40074  rpgtrecnn  40078  rrpsscn  40301  stirlinglem14  40784  fourierdlem73  40876  divge1b  42871  divgt1b  42872  fldivmod  42882  relogbmulbexp  42924  relogbdivb  42925  amgmwlem  43120
  Copyright terms: Public domain W3C validator