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

Theorem rpcn 12043
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 12041 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21recnd 10269 1 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2144  cc 10135  +crp 12034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-resscn 10194
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-in 3728  df-ss 3735  df-rp 12035
This theorem is referenced by:  rpcnne0  12052  divge1  12100  ltdifltdiv  12842  modvalr  12878  flpmodeq  12880  mulmod0  12883  negmod0  12884  modlt  12886  moddiffl  12888  modvalp1  12896  modid  12902  modid0  12903  modcyc  12912  modcyc2  12913  modadd1  12914  muladdmodid  12917  modmuladdnn0  12921  negmod  12922  modm1p1mod0  12928  modmul1  12930  2txmodxeq0  12937  2submod  12938  moddi  12945  sqrlem2  14191  sqrtdiv  14213  caurcvgr  14611  o1fsum  14751  divrcnv  14790  efgt1p2  15049  efgt1p  15050  rpmsubg  20024  uniioombl  23576  abelthlem8  24412  reefgim  24423  pilem1  24424  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  29920  dpexpp1  29950  0dp2dp  29951  sqsscirc1  30288  logdivsqrle  31062  taupilem3  33495  taupilem1  33497  poimirlem29  33764  heicant  33770  itg2addnclem3  33788  itg2gt0cn  33790  ftc1anclem6  33815  ftc1anclem8  33817  areacirclem1  33825  areacirclem4  33828  areacirc  33830  isbnd2  33907  cntotbnd  33920  heiborlem6  33940  heiborlem7  33941  irrapxlem5  37909  2timesgt  40012  xralrple2  40080  recnnltrp  40103  rpgtrecnn  40107  rrpsscn  40332  stirlinglem14  40815  fourierdlem73  40907  divge1b  42820  divgt1b  42821  fldivmod  42831  relogbmulbexp  42873  relogbdivb  42874  amgmwlem  43069
  Copyright terms: Public domain W3C validator