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

Theorem rpcn 11670
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 11668 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21recnd 9921 1 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9787  +crp 11661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-resscn 9846
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-in 3543  df-ss 3550  df-rp 11662
This theorem is referenced by:  rpcnne0  11679  divge1  11727  ltdifltdiv  12449  modvalr  12485  flpmodeq  12487  mulmod0  12490  negmod0  12491  modlt  12493  moddiffl  12495  modvalp1  12503  modid  12509  modid0  12510  modcyc  12519  modcyc2  12520  modadd1  12521  muladdmodid  12524  modmuladdnn0  12528  negmod  12529  modm1p1mod0  12535  modmul1  12537  2txmodxeq0  12544  2submod  12545  moddi  12552  sqrlem2  13775  sqrtdiv  13797  caurcvgr  14195  o1fsum  14329  divrcnv  14366  efgt1p2  14626  efgt1p  14627  rpmsubg  19572  uniioombl  23077  abelthlem8  23911  reefgim  23922  pilem1  23923  logne0  24044  logneg  24052  advlogexp  24115  logcxp  24129  cxprec  24146  cxpmul  24148  abscxp  24152  logsqrt  24164  dvcxp1  24195  dvcxp2  24196  dvsqrt  24197  cxpcn2  24201  loglesqrt  24213  relogbreexp  24227  relogbzexp  24228  relogbmul  24229  relogbdiv  24231  relogbexp  24232  relogbcxp  24237  relogbcxpb  24239  relogbf  24243  rlimcnp  24406  efrlim  24410  cxplim  24412  sqrtlim  24413  cxploglim  24418  logdifbnd  24434  harmonicbnd4  24451  rpdmgm  24465  logfaclbnd  24661  logexprlim  24664  logfacrlim2  24665  vmadivsum  24885  dchrisum0lem1a  24889  dchrvmasumlema  24903  dchrisum0lem1  24919  dchrisum0lem2  24921  mudivsum  24933  mulogsumlem  24934  logdivsum  24936  selberg2lem  24953  selberg2  24954  pntrmax  24967  selbergr  24971  pntibndlem1  24992  pntlem3  25012  blocnilem  26846  nmcexi  28072  nmcopexi  28073  nmcfnexi  28097  sqsscirc1  29085  taupilem3  32142  taupilem1  32144  poimirlem29  32408  heicant  32414  itg2addnclem3  32433  itg2gt0cn  32435  ftc1anclem6  32460  ftc1anclem8  32462  areacirclem1  32470  areacirclem4  32473  areacirc  32475  isbnd2  32552  cntotbnd  32565  heiborlem6  32585  heiborlem7  32586  irrapxlem5  36208  2timesgt  38241  xralrple2  38312  recnnltrp  38335  rpgtrecnn  38339  rrpsscn  38456  stirlinglem14  38781  fourierdlem73  38873  divge1b  42095  divgt1b  42096  fldivmod  42106  relogbmulbexp  42152  relogbdivb  42153  amgmwlem  42317
  Copyright terms: Public domain W3C validator