Theorem rpregt0d 12425

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 12419	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1	rpgt0d 12422	. 2 ⊢ (𝜑 → 0 < 𝐴)
4	2, 3	jca 515	1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378

This theorem is referenced by:  reclt1d  12432  recgt1d  12433  ltrecd  12437  lerecd  12438  ltrec1d  12439  lerec2d  12440  lediv2ad  12441  ltdiv2d  12442  lediv2d  12443  ledivdivd  12444  divge0d  12459  ltmul1d  12460  ltmul2d  12461  lemul1d  12462  lemul2d  12463  ltdiv1d  12464  lediv1d  12465  ltmuldivd  12466  ltmuldiv2d  12467  lemuldivd  12468  lemuldiv2d  12469  ltdivmuld  12470  ltdivmul2d  12471  ledivmuld  12472  ledivmul2d  12473  ltdiv23d  12486  lediv23d  12487  lt2mul2divd  12488  mertenslem1  15232  isprm6  16048  nmoi  23334  icopnfhmeo  23548  nmoleub2lem3  23720  lmnn  23867  ovolscalem1  24117  aaliou2b  24937  birthdaylem3  25539  fsumharmonic  25597  bcmono  25861  chtppilim  26059  dchrisum0lem1a  26070  dchrvmasumiflem1  26085  dchrisum0lem1b  26099  dchrisum0lem1  26100  mulog2sumlem2  26119  selberg3lem1  26141  pntrsumo1  26149  pntibndlem1  26173  pntibndlem3  26176  pntlemr  26186  pntlemj  26187  ostth3  26222  minvecolem3  28659  lnconi  29816  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  stoweidlem14  42656  stoweidlem34  42676  stoweidlem42  42684  stoweidlem51  42693  stoweidlem59  42701  stirlinglem5  42720  elbigolo1  44971