Theorem rpgt0 11882

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

Syntax hints:   → wi 4   ∈ wcel 2030   class class class wbr 4685  ℝcr 9973  0cc0 9974   < clt 10112  ℝ⁺crp 11870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-rp 11871

This theorem is referenced by:  rpge0  11883  rpgecl  11897  0nrp  11903  rpgt0d  11913  addlelt  11980  0mod  12741  sgnrrp  13875  sqrlem2  14028  sqrlem4  14030  sqrlem6  14032  resqrex  14035  rpsqrtcl  14049  climconst  14318  rlimconst  14319  divrcnv  14628  rprisefaccl  14798  blcntrps  22264  blcntr  22265  stdbdmet  22368  stdbdmopn  22370  prdsxmslem2  22381  metustid  22406  nmoix  22580  metdseq0  22704  lebnumii  22812  itgulm  24207  pilem2  24251  tanregt0  24330  logdmnrp  24432  cxple2  24488  asinneg  24658  asin1  24666  reasinsin  24668  atanbndlem  24697  atanbnd  24698  atan1  24700  rlimcnp  24737  chtrpcl  24946  ppiltx  24948  bposlem8  25061  pntlem3  25343  padicabvcxp  25366  0cnop  28966  0cnfn  28967  rpdp2cl  29717  xdivpnfrp  29769  pnfinf  29865  hgt750lem2  30858  taupilem1  33297  itg2gt0cn  33595  areacirclem1  33630  areacirclem4  33633  prdstotbnd  33723  prdsbnd2  33724  irrapxlem3  37705  neglt  39810  xralrple2  39883  constlimc  40174  0cnv  40292  ioodvbdlimc1lem1  40464  fourierdlem103  40744  fourierdlem104  40745  etransclem18  40787  etransclem46  40815  hoidmvlelem3  41132