Theorem rpregt0d 11878

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

Hypothesis

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

Assertion

Ref	Expression
rpregt0d	⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem rpregt0d

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 11872	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1	rpgt0d 11875	. 2 ⊢ (𝜑 → 0 < 𝐴)
4	2, 3	jca 554	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990   class class class wbr 4653  ℝcr 9935  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:  reclt1d  11885  recgt1d  11886  ltrecd  11890  lerecd  11891  ltrec1d  11892  lerec2d  11893  lediv2ad  11894  ltdiv2d  11895  lediv2d  11896  ledivdivd  11897  divge0d  11912  ltmul1d  11913  ltmul2d  11914  lemul1d  11915  lemul2d  11916  ltdiv1d  11917  lediv1d  11918  ltmuldivd  11919  ltmuldiv2d  11920  lemuldivd  11921  lemuldiv2d  11922  ltdivmuld  11923  ltdivmul2d  11924  ledivmuld  11925  ledivmul2d  11926  ltdiv23d  11937  lediv23d  11938  lt2mul2divd  11939  mertenslem1  14616  isprm6  15426  nmoi  22532  icopnfhmeo  22742  nmoleub2lem3  22915  lmnn  23061  ovolscalem1  23281  aaliou2b  24096  birthdaylem3  24680  fsumharmonic  24738  bcmono  25002  chtppilim  25164  dchrisum0lem1a  25175  dchrvmasumiflem1  25190  dchrisum0lem1b  25204  dchrisum0lem1  25205  mulog2sumlem2  25224  selberg3lem1  25246  pntrsumo1  25254  pntibndlem1  25278  pntibndlem3  25281  pntlemr  25291  pntlemj  25292  ostth3  25327  minvecolem3  27732  lnconi  28892  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  stoweidlem14  40231  stoweidlem34  40251  stoweidlem42  40259  stoweidlem51  40268  stoweidlem59  40276  stirlinglem5  40295  elbigolo1  42351