Theorem rpgt0d 12244

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

Syntax hints:   → wi 4   ∈ wcel 2048   class class class wbr 4923  0cc0 10327   < clt 10466  ℝ⁺crp 12197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-rp 12198

This theorem is referenced by:  rpregt0d  12247  ltmulgt11d  12276  ltmulgt12d  12277  gt0divd  12278  ge0divd  12279  lediv12ad  12300  prodge0rd  12306  expgt0  13270  nnesq  13396  bccl2  13491  sqrlem7  14459  sqrtgt0d  14623  iseralt  14892  fsumlt  15005  geomulcvg  15082  eirrlem  15407  sqrt2irrlem  15451  prmind2  15875  4sqlem11  16137  4sqlem12  16138  ssblex  22731  nrginvrcn  22994  mulc1cncf  23206  nmoleub2lem2  23413  itg2mulclem  24040  itggt0  24135  dvgt0  24294  ftc1lem5  24330  aaliou3lem2  24625  abelthlem8  24720  tanord  24813  tanregt0  24814  logccv  24937  cxpcn3lem  25019  jensenlem2  25257  dmlogdmgm  25293  basellem1  25350  sgmnncl  25416  chpdifbndlem2  25822  pntibndlem1  25857  pntibnd  25861  pntlemc  25863  abvcxp  25883  ostth2lem1  25886  ostth2lem3  25903  ostth2  25905  xrge0iifhom  30781  omssubadd  31160  sgnmulrp2  31404  signsply0  31428  sinccvglem  32375  unblimceq0lem  33305  unbdqndv2lem2  33309  knoppndvlem14  33324  taupilem1  33979  poimirlem29  34310  heicant  34316  itggt0cn  34353  ftc1cnnc  34355  bfplem1  34490  rrncmslem  34500  irrapxlem4  38763  irrapxlem5  38764  imo72b2lem1  39831  dvdivbd  41584  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  stoweidlem1  41663  stoweidlem7  41669  stoweidlem11  41673  stoweidlem25  41687  stoweidlem26  41688  stoweidlem34  41696  stoweidlem49  41711  stoweidlem52  41714  stoweidlem60  41722  wallispi  41732  stirlinglem6  41741  stirlinglem11  41746  fourierdlem30  41799  qndenserrnbl  41957  ovnsubaddlem1  42229  hoiqssbllem2  42282  pimrecltpos  42364  smfmullem1  42443  smfmullem2  42444  smfmullem3  42445