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

Theorem rprege0 12407
Description: A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.)
Assertion
Ref Expression
rprege0 (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))

Proof of Theorem rprege0
StepHypRef Expression
1 rpre 12400 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
2 rpge0 12405 . 2 (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
31, 2jca 514 1 (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2113   class class class wbr 5069  cr 10539  0cc0 10540  cle 10679  +crp 12392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-resscn 10597  ax-1cn 10598  ax-addrcl 10601  ax-rnegex 10611  ax-cnre 10613  ax-pre-lttri 10614
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684  df-rp 12393
This theorem is referenced by:  resqrex  14613  sqrtdiv  14628  o1fsum  15171  prmreclem3  16257  aaliou3lem3  24936  pige3ALT  25108  rpcxpcl  25262  cxprec  25272  harmoniclbnd  25589  harmonicbnd4  25591  basellem4  25664  logfaclbnd  25801  logfacrlim  25803  logexprlim  25804  bposlem7  25869  vmadivsum  26061  dchrisum0lem2a  26096  dchrisum0lem2  26097  dchrisum0  26099  mudivsum  26109  mulogsumlem  26110  selberglem2  26125  selberg2lem  26129  pntrsumo1  26144  minvecolem3  28656  ehl2eudis0lt  44720  itsclc0  44765  itsclc0b  44766
  Copyright terms: Public domain W3C validator