Theorem rpgt0 12389

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 12379	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 500	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378

This theorem is referenced by:  rpge0  12390  rpgecl  12405  0nrp  12412  rpgt0d  12422  addlelt  12491  0mod  13265  sgnrrp  14442  sqrlem2  14595  sqrlem4  14597  sqrlem6  14599  resqrex  14602  rpsqrtcl  14616  climconst  14892  rlimconst  14893  divrcnv  15199  rprisefaccl  15369  blcntrps  23019  blcntr  23020  stdbdmet  23123  stdbdmopn  23125  prdsxmslem2  23136  metustid  23161  nmoix  23335  metdseq0  23459  lebnumii  23571  itgulm  25003  pilem2  25047  cos02pilt1  25118  tanregt0  25131  logdmnrp  25232  cxple2  25288  asinneg  25472  asin1  25480  reasinsin  25482  atanbndlem  25511  atanbnd  25512  atan1  25514  rlimcnp  25551  chtrpcl  25760  ppiltx  25762  bposlem8  25875  pntlem3  26193  padicabvcxp  26216  0cnop  29762  0cnfn  29763  rpdp2cl  30584  xdivpnfrp  30635  pnfinf  30862  hgt750lem2  32033  taupilem1  34735  itg2gt0cn  35112  areacirclem1  35145  areacirclem4  35148  prdstotbnd  35232  prdsbnd2  35233  irrapxlem3  39765  neglt  41915  xralrple2  41986  constlimc  42266  0cnv  42384  ioodvbdlimc1lem1  42573  fourierdlem103  42851  fourierdlem104  42852  etransclem18  42894  etransclem46  42922  hoidmvlelem3  43236