Theorem rpge0 12947

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 12942	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2		rpgt0 12946	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3		0re 11137	. . 3 ⊢ 0 ∈ ℝ
4		ltle 11225	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
5	3, 4	mpan 691	. 2 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴))
6	1, 2, 5	sylc 65	1 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028  0cc0 11029   < clt 11170   ≤ cle 11171  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-rp 12934

This theorem is referenced by:  rprege0  12949  rpge0d  12981  xralrple  13148  xlemul1  13233  infmrp1  13288  01sqrexlem1  15195  rpsqrtcl  15217  divrcnv  15808  ef01bndlem  16142  stdbdmet  24491  reconnlem2  24803  cphsqrtcl3  25164  iscmet3lem3  25267  minveclem3  25406  itg2const2  25718  itg2mulclem  25723  aalioulem2  26310  pige3ALT  26497  argregt0  26587  argrege0  26588  2irrexpq  26708  cxpcn3  26725  cxplim  26949  cxp2lim  26954  divsqrtsumlem  26957  logdiflbnd  26972  basellem4  27061  ppiltx  27154  bposlem8  27268  bposlem9  27269  chebbnd1  27449  mulog2sumlem2  27512  selbergb  27526  selberg2b  27529  nmcexi  32112  nmcopexi  32113  nmcfnexi  32137  sqsscirc1  34068  divsqrtid  34754  logdivsqrle  34810  hgt750lem2  34812  subfacval3  35387  ptrecube  37955  heicant  37990  itg2addnclem  38006  itg2gt0cn  38010  areacirclem1  38043  areacirclem4  38046  areacirc  38048  cntotbnd  38131  rpabsid  42767  xralrple4  45820  xralrple3  45821  fourierdlem103  46655  blenre  49062  itscnhlinecirc02plem3  49272  itscnhlinecirc02p  49273