Theorem rpge0 13001

Description: A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.)

Assertion

Ref	Expression
rpge0	⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)

Proof of Theorem rpge0

Step	Hyp	Ref	Expression
1		rpre 12996	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2		rpgt0 13000	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3		0re 11177	. . 3 ⊢ 0 ∈ ℝ
4		ltle 11265	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
5	3, 4	mpan 700	. 2 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴))
6	1, 2, 5	sylc 65	1 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5097  ℝcr 11066  0cc0 11067   < clt 11210   ≤ cle 11211  ℝ⁺crp 12987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-addrcl 11128  ax-rnegex 11138  ax-cnre 11140  ax-pre-lttri 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-rp 12988

This theorem is referenced by:  rprege0  13003  rpge0d  13035  xralrple  13202  xlemul1  13287  infmrp1  13342  01sqrexlem1  15260  rpsqrtcl  15282  divrcnv  15873  ef01bndlem  16207  stdbdmet  24564  reconnlem2  24876  cphsqrtcl3  25237  iscmet3lem3  25340  minveclem3  25479  itg2const2  25791  itg2mulclem  25796  aalioulem2  26385  pige3ALT  26573  argregt0  26663  argrege0  26664  2irrexpq  26784  cxpcn3  26801  cxplim  27024  cxp2lim  27029  divsqrtsumlem  27032  logdiflbnd  27047  basellem4  27136  ppiltx  27229  bposlem8  27343  bposlem9  27344  chebbnd1  27524  mulog2sumlem2  27587  selbergb  27601  selberg2b  27604  nmcexi  32186  nmcopexi  32187  nmcfnexi  32211  sqsscirc1  34166  divsqrtid  34849  logdivsqrle  34905  hgt750lem2  34907  subfacval3  35500  ptrecube  38080  heicant  38115  itg2addnclem  38131  itg2gt0cn  38135  areacirclem1  38168  areacirclem4  38171  areacirc  38173  cntotbnd  38256  rpabsid  42891  xralrple4  45909  xralrple3  45910  fourierdlem103  46744  blenre  49157  itscnhlinecirc02plem3  49367  itscnhlinecirc02p  49368