Theorem rpregt0d 13171

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ℝcr 11200  0cc0 11201   < clt 11344  ℝ⁺crp 13121

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13122

This theorem is used by:  reclt1d  13178  recgt1d  13179  ltrecd  13183  lerecd  13184  ltrec1d  13185  lerec2d  13186  lediv2ad  13187  ltdiv2d  13188  lediv2d  13189  ledivdivd  13190  divge0d  13205  ltmul1d  13206  ltmul2d  13207  lemul1d  13208  lemul2d  13209  ltdiv1d  13210  lediv1d  13211  ltmuldivd  13212  ltmuldiv2d  13213  lemuldivd  13214  lemuldiv2d  13215  ltdivmuld  13216  ltdivmul2d  13217  ledivmuld  13218  ledivmul2d  13219  ltdiv23d  13232  lediv23d  13233  lt2mul2divd  13234  mertenslem1  16054  isprm6  16891  nmoi  25048  icopnfhmeo  25265  nmoleub2lem3  25437  lmnn  25585  ovolscalem1  25835  aaliou2b  26669  birthdaylem3  27282  fsumharmonic  27340  bcmono  27605  chtppilim  27803  dchrisum0lem1a  27814  dchrvmasumiflem1  27829  dchrisum0lem1b  27843  dchrisum0lem1  27844  mulog2sumlem2  27863  selberg3lem1  27885  pntrsumo1  27893  pntibndlem1  27917  pntibndlem3  27920  pntlemr  27930  pntlemj  27931  ostth3  27966  minvecolem3  31479  lnconi  32636  poimirlem29  38643  poimirlem30  38644  poimirlem31  38645  poimirlem32  38646  aks4d1p1p2  43196  stoweidlem14  47100  stoweidlem34  47120  stoweidlem42  47128  stoweidlem51  47137  stoweidlem59  47145  stirlinglem5  47164  elbigolo1  49745