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

Theorem rprege0d 12430
Description: A positive real is real and greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rprege0d (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))

Proof of Theorem rprege0d
StepHypRef Expression
1 rpred.1 . . 3 (𝜑𝐴 ∈ ℝ+)
21rpred 12423 . 2 (𝜑𝐴 ∈ ℝ)
31rpge0d 12427 . 2 (𝜑 → 0 ≤ 𝐴)
42, 3jca 514 1 (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2108   class class class wbr 5057  cr 10528  0cc0 10529  cle 10668  +crp 12381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-addrcl 10590  ax-rnegex 10600  ax-cnre 10602  ax-pre-lttri 10603
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-rp 12382
This theorem is referenced by:  eirrlem  15549  prmreclem3  16246  prmreclem6  16249  cxprec  25261  cxpsqrt  25278  cxpcn3lem  25320  cxplim  25541  cxploglim2  25548  divsqrtsumlem  25549  divsqrtsumo1  25553  fsumharmonic  25581  zetacvg  25584  logfacubnd  25789  logfacbnd3  25791  bposlem1  25852  bposlem4  25855  bposlem7  25858  bposlem9  25860  2sqmod  26004  dchrmusum2  26062  dchrvmasumlem3  26067  dchrisum0flblem2  26077  dchrisum0fno1  26079  dchrisum0lema  26082  dchrisum0lem1b  26083  dchrisum0lem1  26084  dchrisum0lem2a  26085  dchrisum0lem2  26086  dchrisum0lem3  26087  chpdifbndlem2  26122  selberg3lem1  26125  pntrsumo1  26133  pntrlog2bndlem2  26146  pntrlog2bndlem4  26148  pntrlog2bndlem6a  26150  pntpbnd2  26155  pntibndlem2  26159  pntlemb  26165  pntlemg  26166  pntlemh  26167  pntlemn  26168  pntlemr  26170  pntlemj  26171  pntlemf  26173  pntlemk  26174  pntlemo  26175  blocnilem  28573  ubthlem2  28640  minvecolem4  28649  eulerpartlemgc  31613  irrapxlem4  39413  irrapxlem5  39414  stirlinglem3  42352  stirlinglem15  42364  inlinecirc02plem  44764  amgmlemALT  44895
  Copyright terms: Public domain W3C validator