Theorem rpregt0d 13197

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   class class class wbr 5106  ℝcr 11226  0cc0 11227   < clt 11370  ℝ⁺crp 13147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-rp 13148

This theorem is used by:  reclt1d  13204  recgt1d  13205  ltrecd  13209  lerecd  13210  ltrec1d  13211  lerec2d  13212  lediv2ad  13213  ltdiv2d  13214  lediv2d  13215  ledivdivd  13216  divge0d  13231  ltmul1d  13232  ltmul2d  13233  lemul1d  13234  lemul2d  13235  ltdiv1d  13236  lediv1d  13237  ltmuldivd  13238  ltmuldiv2d  13239  lemuldivd  13240  lemuldiv2d  13241  ltdivmuld  13242  ltdivmul2d  13243  ledivmuld  13244  ledivmul2d  13245  ltdiv23d  13258  lediv23d  13259  lt2mul2divd  13260  mertenslem1  16082  isprm6  16919  nmoi  25077  icopnfhmeo  25294  nmoleub2lem3  25466  lmnn  25614  ovolscalem1  25864  aaliou2b  26698  birthdaylem3  27311  fsumharmonic  27369  bcmono  27634  chtppilim  27832  dchrisum0lem1a  27843  dchrvmasumiflem1  27858  dchrisum0lem1b  27872  dchrisum0lem1  27873  mulog2sumlem2  27892  selberg3lem1  27914  pntrsumo1  27922  pntibndlem1  27946  pntibndlem3  27949  pntlemr  27959  pntlemj  27960  ostth3  27995  minvecolem3  31508  lnconi  32665  poimirlem29  38759  poimirlem30  38760  poimirlem31  38761  poimirlem32  38762  aks4d1p1p2  43312  stoweidlem14  47229  stoweidlem34  47249  stoweidlem42  47257  stoweidlem51  47266  stoweidlem59  47274  stirlinglem5  47293  elbigolo1  49874