Theorem rpgt0 11673

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

Assertion

Ref	Expression
rpgt0	⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Proof of Theorem rpgt0

Step	Hyp	Ref	Expression
1		elrp 11663	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 478	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 1976   class class class wbr 4574  ℝcr 9788  0cc0 9789   < clt 9927  ℝ⁺crp 11661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-rp 11662

This theorem is referenced by:  rpge0  11674  rpgecl  11688  0nrp  11694  rpgt0d  11704  addlelt  11771  0mod  12515  sgnrrp  13622  sqrlem2  13775  sqrlem4  13777  sqrlem6  13779  resqrex  13782  rpsqrtcl  13796  climconst  14065  rlimconst  14066  divrcnv  14366  rprisefaccl  14536  blcntrps  21965  blcntr  21966  stdbdmet  22069  stdbdmopn  22071  prdsxmslem2  22082  metustid  22107  nmoix  22272  metdseq0  22393  lebnumii  22501  itgulm  23880  pilem2  23924  tanregt0  24003  logdmnrp  24101  cxple2  24157  asinneg  24327  asin1  24335  reasinsin  24337  atanbndlem  24366  atanbnd  24367  atan1  24369  rlimcnp  24406  chtrpcl  24615  ppiltx  24617  bposlem8  24730  pntlem3  25012  padicabvcxp  25035  0cnop  28025  0cnfn  28026  xdivpnfrp  28775  pnfinf  28871  taupilem1  32144  itg2gt0cn  32435  areacirclem1  32470  areacirclem4  32473  prdstotbnd  32563  prdsbnd2  32564  irrapxlem3  36206  neglt  38237  xralrple2  38312  constlimc  38492  ioodvbdlimc1lem1  38622  fourierdlem103  38903  fourierdlem104  38904  etransclem18  38946  etransclem46  38974  hoidmvlelem3  39288