Theorem rpgt0d 11875

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 11844	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 1990   class class class wbr 4653  0cc0 9936   < clt 10074  ℝ⁺crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-rp 11833

This theorem is referenced by:  rpregt0d  11878  ltmulgt11d  11907  ltmulgt12d  11908  gt0divd  11909  ge0divd  11910  lediv12ad  11931  expgt0  12893  nnesq  12988  bccl2  13110  sqrlem7  13989  sqrtgt0d  14151  iseralt  14415  fsumlt  14532  geomulcvg  14607  eirrlem  14932  sqrt2irrlem  14977  sqrt2irrlemOLD  14978  prmind2  15398  4sqlem11  15659  4sqlem12  15660  ssblex  22233  nrginvrcn  22496  mulc1cncf  22708  nmoleub2lem2  22916  itg2mulclem  23513  itggt0  23608  dvgt0  23767  ftc1lem5  23803  aaliou3lem2  24098  abelthlem8  24193  tanord  24284  tanregt0  24285  logccv  24409  cxpcn3lem  24488  jensenlem2  24714  dmlogdmgm  24750  basellem1  24807  sgmnncl  24873  chpdifbndlem2  25243  pntibndlem1  25278  pntibnd  25282  pntlemc  25284  abvcxp  25304  ostth2lem1  25307  ostth2lem3  25324  ostth2  25326  xrge0iifhom  29983  omssubadd  30362  sgnmulrp2  30605  signsply0  30628  sinccvglem  31566  unblimceq0lem  32497  unbdqndv2lem2  32501  knoppndvlem14  32516  taupilem1  33167  poimirlem29  33438  heicant  33444  itggt0cn  33482  ftc1cnnc  33484  bfplem1  33621  rrncmslem  33631  irrapxlem4  37389  irrapxlem5  37390  imo72b2lem1  38471  dvdivbd  40138  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem1  40218  stoweidlem7  40224  stoweidlem11  40228  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem49  40266  stoweidlem52  40269  stoweidlem60  40277  wallispi  40287  stirlinglem6  40296  stirlinglem11  40301  fourierdlem30  40354  qndenserrnbl  40515  ovnsubaddlem1  40784  hoiqssbllem2  40837  pimrecltpos  40919  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000