Theorem rpgt0 12402

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536  0cc0 10537   < clt 10675  ℝ⁺crp 12390

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-rp 12391

This theorem is referenced by:  rpge0  12403  rpgecl  12418  0nrp  12425  rpgt0d  12435  addlelt  12504  0mod  13271  sgnrrp  14450  sqrlem2  14603  sqrlem4  14605  sqrlem6  14607  resqrex  14610  rpsqrtcl  14624  climconst  14900  rlimconst  14901  divrcnv  15207  rprisefaccl  15377  blcntrps  23022  blcntr  23023  stdbdmet  23126  stdbdmopn  23128  prdsxmslem2  23139  metustid  23164  nmoix  23338  metdseq0  23462  lebnumii  23570  itgulm  24996  pilem2  25040  cos02pilt1  25111  tanregt0  25123  logdmnrp  25224  cxple2  25280  asinneg  25464  asin1  25472  reasinsin  25474  atanbndlem  25503  atanbnd  25504  atan1  25506  rlimcnp  25543  chtrpcl  25752  ppiltx  25754  bposlem8  25867  pntlem3  26185  padicabvcxp  26208  0cnop  29756  0cnfn  29757  rpdp2cl  30558  xdivpnfrp  30609  pnfinf  30812  hgt750lem2  31923  taupilem1  34605  itg2gt0cn  34962  areacirclem1  34997  areacirclem4  35000  prdstotbnd  35087  prdsbnd2  35088  irrapxlem3  39441  neglt  41570  xralrple2  41642  constlimc  41925  0cnv  42043  ioodvbdlimc1lem1  42236  fourierdlem103  42514  fourierdlem104  42515  etransclem18  42557  etransclem46  42585  hoidmvlelem3  42899