Theorem rpgt0d 12437

Description: A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpgt0d	⊢ (𝜑 → 0 < 𝐴)

Proof of Theorem rpgt0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpgt0 12404	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5068  0cc0 10539   < clt 10677  ℝ⁺crp 12392

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-rp 12393

This theorem is referenced by:  rpregt0d  12440  ltmulgt11d  12469  ltmulgt12d  12470  gt0divd  12471  ge0divd  12472  lediv12ad  12493  prodge0rd  12499  expgt0  13465  nnesq  13591  bccl2  13686  sqrlem7  14610  sqrtgt0d  14774  iseralt  15043  fsumlt  15157  geomulcvg  15234  eirrlem  15559  sqrt2irrlem  15603  prmind2  16031  4sqlem11  16293  4sqlem12  16294  ssblex  23040  nrginvrcn  23303  mulc1cncf  23515  nmoleub2lem2  23722  itg2mulclem  24349  itggt0  24444  dvgt0  24603  ftc1lem5  24639  aaliou3lem2  24934  abelthlem8  25029  tanord  25124  tanregt0  25125  logccv  25248  cxpcn3lem  25330  jensenlem2  25567  dmlogdmgm  25603  basellem1  25660  sgmnncl  25726  chpdifbndlem2  26132  pntibndlem1  26167  pntibnd  26171  pntlemc  26173  abvcxp  26193  ostth2lem1  26196  ostth2lem3  26213  ostth2  26215  xrge0iifhom  31182  omssubadd  31560  sgnmulrp2  31803  signsply0  31823  sinccvglem  32917  unblimceq0lem  33847  unbdqndv2lem2  33851  knoppndvlem14  33866  taupilem1  34604  poimirlem29  34923  heicant  34929  itggt0cn  34966  ftc1cnnc  34968  bfplem1  35102  rrncmslem  35112  irrapxlem4  39429  irrapxlem5  39430  imo72b2lem1  40528  dvdivbd  42215  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  stoweidlem1  42293  stoweidlem7  42299  stoweidlem11  42303  stoweidlem25  42317  stoweidlem26  42318  stoweidlem34  42326  stoweidlem49  42341  stoweidlem52  42344  stoweidlem60  42352  wallispi  42362  stirlinglem6  42371  stirlinglem11  42376  fourierdlem30  42429  qndenserrnbl  42587  ovnsubaddlem1  42859  hoiqssbllem2  42912  pimrecltpos  42994  smfmullem1  43073  smfmullem2  43074  smfmullem3  43075