Theorem rpge0 13027

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 13022	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2		rpgt0 13026	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3		0re 11253	. . 3 ⊢ 0 ∈ ℝ
4		ltle 11339	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
5	3, 4	mpan 688	. 2 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴))
6	1, 2, 5	sylc 65	1 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5149  ℝcr 11144  0cc0 11145   < clt 11285   ≤ cle 11286  ℝ⁺crp 13014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11202  ax-1cn 11203  ax-addrcl 11206  ax-rnegex 11216  ax-cnre 11218  ax-pre-lttri 11219

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-rp 13015

This theorem is referenced by:  rprege0  13029  rpge0d  13060  xralrple  13224  xlemul1  13309  infmrp1  13363  01sqrexlem1  15233  rpsqrtcl  15255  divrcnv  15842  ef01bndlem  16172  stdbdmet  24486  reconnlem2  24804  cphsqrtcl3  25176  iscmet3lem3  25279  minveclem3  25418  itg2const2  25732  itg2mulclem  25737  aalioulem2  26330  pige3ALT  26516  argregt0  26606  argrege0  26607  2irrexpq  26727  cxpcn3  26745  cxplim  26969  cxp2lim  26974  divsqrtsumlem  26977  logdiflbnd  26992  basellem4  27081  ppiltx  27174  bposlem8  27289  bposlem9  27290  chebbnd1  27470  mulog2sumlem2  27533  selbergb  27547  selberg2b  27550  nmcexi  31928  nmcopexi  31929  nmcfnexi  31953  sqsscirc1  33660  divsqrtid  34377  logdivsqrle  34433  hgt750lem2  34435  subfacval3  34950  ptrecube  37244  heicant  37279  itg2addnclem  37295  itg2gt0cn  37299  areacirclem1  37332  areacirclem4  37335  areacirc  37337  cntotbnd  37420  xralrple4  44898  xralrple3  44899  fourierdlem103  45740  blenre  47838  itscnhlinecirc02plem3  48048  itscnhlinecirc02p  48049