Theorem rprege0d 12779

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

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 12772	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1	rpge0d 12776	. 2 ⊢ (𝜑 → 0 ≤ 𝐴)
4	2, 3	jca 512	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870  0cc0 10871   ≤ cle 11010  ℝ⁺crp 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-addrcl 10932  ax-rnegex 10942  ax-cnre 10944  ax-pre-lttri 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-rp 12731

This theorem is referenced by:  eirrlem  15913  prmreclem3  16619  prmreclem6  16622  cxprec  25841  cxpsqrt  25858  cxpcn3lem  25900  cxplim  26121  cxploglim2  26128  divsqrtsumlem  26129  divsqrtsumo1  26133  fsumharmonic  26161  zetacvg  26164  logfacubnd  26369  logfacbnd3  26371  bposlem1  26432  bposlem4  26435  bposlem7  26438  bposlem9  26440  2sqmod  26584  dchrmusum2  26642  dchrvmasumlem3  26647  dchrisum0flblem2  26657  dchrisum0fno1  26659  dchrisum0lema  26662  dchrisum0lem1b  26663  dchrisum0lem1  26664  dchrisum0lem2a  26665  dchrisum0lem2  26666  dchrisum0lem3  26667  chpdifbndlem2  26702  selberg3lem1  26705  pntrsumo1  26713  pntrlog2bndlem2  26726  pntrlog2bndlem4  26728  pntrlog2bndlem6a  26730  pntpbnd2  26735  pntibndlem2  26739  pntlemb  26745  pntlemg  26746  pntlemh  26747  pntlemn  26748  pntlemr  26750  pntlemj  26751  pntlemf  26753  pntlemk  26754  pntlemo  26755  blocnilem  29166  ubthlem2  29233  minvecolem4  29242  eulerpartlemgc  32329  irrapxlem4  40647  irrapxlem5  40648  stirlinglem3  43617  stirlinglem15  43629  inlinecirc02plem  46132  amgmlemALT  46507