Theorem rpge0 12816

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 12811	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2		rpgt0 12815	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3		0re 11050	. . 3 ⊢ 0 ∈ ℝ
4		ltle 11136	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
5	3, 4	mpan 687	. 2 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴))
6	1, 2, 5	sylc 65	1 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5087  ℝcr 10943  0cc0 10944   < clt 11082   ≤ cle 11083  ℝ⁺crp 12803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-resscn 11001  ax-1cn 11002  ax-addrcl 11005  ax-rnegex 11015  ax-cnre 11017  ax-pre-lttri 11018

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-rp 12804

This theorem is referenced by:  rprege0  12818  rpge0d  12849  xralrple  13012  xlemul1  13097  infmrp1  13151  sqrlem1  15026  rpsqrtcl  15048  divrcnv  15636  ef01bndlem  15965  stdbdmet  23744  reconnlem2  24062  cphsqrtcl3  24423  iscmet3lem3  24526  minveclem3  24665  itg2const2  24978  itg2mulclem  24983  aalioulem2  25565  pige3ALT  25748  argregt0  25837  argrege0  25838  2irrexpq  25957  cxpcn3  25973  cxplim  26193  cxp2lim  26198  divsqrtsumlem  26201  logdiflbnd  26216  basellem4  26305  ppiltx  26398  bposlem8  26511  bposlem9  26512  chebbnd1  26692  mulog2sumlem2  26755  selbergb  26769  selberg2b  26772  nmcexi  30497  nmcopexi  30498  nmcfnexi  30522  sqsscirc1  31964  divsqrtid  32680  logdivsqrle  32736  hgt750lem2  32738  subfacval3  33256  ptrecube  35833  heicant  35868  itg2addnclem  35884  itg2gt0cn  35888  areacirclem1  35921  areacirclem4  35924  areacirc  35926  cntotbnd  36010  xralrple4  43148  xralrple3  43149  fourierdlem103  43987  blenre  46172  itscnhlinecirc02plem3  46382  itscnhlinecirc02p  46383