Theorem rpregt0d 12981

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11026  0cc0 11027   < clt 11168  ℝ⁺crp 12931

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12932

This theorem is referenced by:  reclt1d  12988  recgt1d  12989  ltrecd  12993  lerecd  12994  ltrec1d  12995  lerec2d  12996  lediv2ad  12997  ltdiv2d  12998  lediv2d  12999  ledivdivd  13000  divge0d  13015  ltmul1d  13016  ltmul2d  13017  lemul1d  13018  lemul2d  13019  ltdiv1d  13020  lediv1d  13021  ltmuldivd  13022  ltmuldiv2d  13023  lemuldivd  13024  lemuldiv2d  13025  ltdivmuld  13026  ltdivmul2d  13027  ledivmuld  13028  ledivmul2d  13029  ltdiv23d  13042  lediv23d  13043  lt2mul2divd  13044  mertenslem1  15838  isprm6  16673  nmoi  24702  icopnfhmeo  24919  nmoleub2lem3  25091  lmnn  25239  ovolscalem1  25489  aaliou2b  26320  birthdaylem3  26934  fsumharmonic  26993  bcmono  27259  chtppilim  27457  dchrisum0lem1a  27468  dchrvmasumiflem1  27483  dchrisum0lem1b  27497  dchrisum0lem1  27498  mulog2sumlem2  27517  selberg3lem1  27539  pntrsumo1  27547  pntibndlem1  27571  pntibndlem3  27574  pntlemr  27584  pntlemj  27585  ostth3  27620  minvecolem3  30967  lnconi  32124  poimirlem29  37981  poimirlem30  37982  poimirlem31  37983  poimirlem32  37984  aks4d1p1p2  42520  stoweidlem14  46457  stoweidlem34  46477  stoweidlem42  46485  stoweidlem51  46494  stoweidlem59  46502  stirlinglem5  46521  elbigolo1  49030