Theorem rpgt0 12992

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5149  ℝcr 11113  0cc0 11114   < clt 11254  ℝ⁺crp 12980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12981

This theorem is referenced by:  rpge0  12993  rpgecl  13008  0nrp  13015  rpgt0d  13025  addlelt  13094  0mod  13873  sgnrrp  15044  01sqrexlem2  15196  01sqrexlem4  15198  01sqrexlem6  15200  resqrex  15203  rpsqrtcl  15217  climconst  15493  rlimconst  15494  divrcnv  15804  rprisefaccl  15973  blcntrps  24140  blcntr  24141  stdbdmet  24247  stdbdmopn  24249  prdsxmslem2  24260  metustid  24285  nmoix  24468  metdseq0  24592  lebnumii  24714  itgulm  26154  pilem2  26198  cos02pilt1  26269  tanregt0  26282  logdmnrp  26383  cxple2  26439  asinneg  26625  asin1  26633  reasinsin  26635  atanbndlem  26664  atanbnd  26665  atan1  26667  rlimcnp  26704  chtrpcl  26913  ppiltx  26915  bposlem8  27028  pntlem3  27346  padicabvcxp  27369  0cnop  31497  0cnfn  31498  rpdp2cl  32313  xdivpnfrp  32364  pnfinf  32597  hgt750lem2  33960  taupilem1  36507  itg2gt0cn  36848  areacirclem1  36881  areacirclem4  36884  prdstotbnd  36967  prdsbnd2  36968  aks4d1p1p6  41246  irrapxlem3  41866  neglt  44294  xralrple2  44364  constlimc  44640  0cnv  44758  ioodvbdlimc1lem1  44947  fourierdlem103  45225  fourierdlem104  45226  etransclem18  45268  etransclem46  45296  hoidmvlelem3  45613