Theorem elrpd 9972

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 9934	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 417	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4093  ℝcr 8074  0cc0 8075   < clt 8256  ℝ⁺crp 9932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-rp 9933

This theorem is referenced by:  mul2lt0rgt0  10039  mul2lt0np  10042  zltaddlt1le  10287  modqval  10632  ltexp2a  10899  leexp2a  10900  expnlbnd2  10973  nn0ltexp2  11017  resqrexlem1arp  11628  resqrexlemp1rp  11629  resqrexlemcalc2  11638  resqrexlemcalc3  11639  resqrexlemgt0  11643  resqrexlemglsq  11645  rpsqrtcl  11664  absrpclap  11684  rpmaxcl  11846  rpmincl  11861  xrminrpcl  11897  xrbdtri  11899  mulcn2  11935  reccn2ap  11936  climge0  11948  divcnv  12121  georeclim  12137  cvgratnnlembern  12147  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratnn  12155  cvgratz  12156  rpefcl  12309  efltim  12322  ef01bndlem  12380  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  bdmopn  15298  mulcncflem  15401  ivthinclemlopn  15430  ivthinclemuopn  15432  dveflem  15520  reeff1olem  15565  pilem3  15577  tanrpcl  15631  cosordlem  15643  rplogcl  15673  logdivlti  15675  cxplt  15710  cxple  15711  rpabscxpbnd  15734  ltexp2  15735  iooref1o  16749