Theorem elrpd 9474

Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
elrpd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
elrpd.2	⊢ (𝜑 → 0 < 𝐴)

Assertion

Ref	Expression
elrpd	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Proof of Theorem elrpd

Step	Hyp	Ref	Expression
1		elrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		elrpd.2	. 2 ⊢ (𝜑 → 0 < 𝐴)
3		elrp 9436	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 413	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 1480   class class class wbr 3924  ℝcr 7612  0cc0 7613   < clt 7793  ℝ⁺crp 9434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rab 2423  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925  df-rp 9435

This theorem is referenced by:  mul2lt0rgt0  9540  mul2lt0np  9543  zltaddlt1le  9782  modqval  10090  ltexp2a  10338  leexp2a  10339  expnlbnd2  10410  resqrexlem1arp  10770  resqrexlemp1rp  10771  resqrexlemcalc2  10780  resqrexlemcalc3  10781  resqrexlemgt0  10785  resqrexlemglsq  10787  rpsqrtcl  10806  absrpclap  10826  rpmaxcl  10988  rpmincl  11002  xrminrpcl  11036  xrbdtri  11038  mulcn2  11074  reccn2ap  11075  climge0  11087  divcnv  11259  georeclim  11275  cvgratnnlembern  11285  cvgratnnlemsumlt  11290  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  cvgratz  11294  rpefcl  11380  efltim  11393  ef01bndlem  11452  bdmopn  12662  mulcncflem  12748  ivthinclemlopn  12772  ivthinclemuopn  12774  dveflem  12844  pilem3  12853  tanrpcl  12907  cosordlem  12919