Theorem rpregt0d 12967

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  0cc0 11038   < clt 11178  ℝ⁺crp 12917

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12918

This theorem is referenced by:  reclt1d  12974  recgt1d  12975  ltrecd  12979  lerecd  12980  ltrec1d  12981  lerec2d  12982  lediv2ad  12983  ltdiv2d  12984  lediv2d  12985  ledivdivd  12986  divge0d  13001  ltmul1d  13002  ltmul2d  13003  lemul1d  13004  lemul2d  13005  ltdiv1d  13006  lediv1d  13007  ltmuldivd  13008  ltmuldiv2d  13009  lemuldivd  13010  lemuldiv2d  13011  ltdivmuld  13012  ltdivmul2d  13013  ledivmuld  13014  ledivmul2d  13015  ltdiv23d  13028  lediv23d  13029  lt2mul2divd  13030  mertenslem1  15819  isprm6  16653  nmoi  24684  icopnfhmeo  24909  nmoleub2lem3  25083  lmnn  25231  ovolscalem1  25482  aaliou2b  26317  birthdaylem3  26931  fsumharmonic  26990  bcmono  27256  chtppilim  27454  dchrisum0lem1a  27465  dchrvmasumiflem1  27480  dchrisum0lem1b  27494  dchrisum0lem1  27495  mulog2sumlem2  27514  selberg3lem1  27536  pntrsumo1  27544  pntibndlem1  27568  pntibndlem3  27571  pntlemr  27581  pntlemj  27582  ostth3  27617  minvecolem3  30963  lnconi  32120  poimirlem29  37889  poimirlem30  37890  poimirlem31  37891  poimirlem32  37892  aks4d1p1p2  42429  stoweidlem14  46361  stoweidlem34  46381  stoweidlem42  46389  stoweidlem51  46398  stoweidlem59  46406  stirlinglem5  46425  elbigolo1  48906