Theorem elrpd 9664

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

Syntax hints:   → wi 4   ∈ wcel 2146   class class class wbr 3998  ℝcr 7785  0cc0 7786   < clt 7966  ℝ⁺crp 9624

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999  df-rp 9625

This theorem is referenced by:  mul2lt0rgt0  9731  mul2lt0np  9734  zltaddlt1le  9978  modqval  10294  ltexp2a  10542  leexp2a  10543  expnlbnd2  10615  nn0ltexp2  10658  resqrexlem1arp  10982  resqrexlemp1rp  10983  resqrexlemcalc2  10992  resqrexlemcalc3  10993  resqrexlemgt0  10997  resqrexlemglsq  10999  rpsqrtcl  11018  absrpclap  11038  rpmaxcl  11200  rpmincl  11214  xrminrpcl  11250  xrbdtri  11252  mulcn2  11288  reccn2ap  11289  climge0  11301  divcnv  11473  georeclim  11489  cvgratnnlembern  11499  cvgratnnlemsumlt  11504  cvgratnnlemfm  11505  cvgratnnlemrate  11506  cvgratnn  11507  cvgratz  11508  rpefcl  11661  efltim  11674  ef01bndlem  11732  pythagtriplem12  12242  pythagtriplem14  12244  pythagtriplem16  12246  bdmopn  13584  mulcncflem  13670  ivthinclemlopn  13694  ivthinclemuopn  13696  dveflem  13767  reeff1olem  13772  pilem3  13784  tanrpcl  13838  cosordlem  13850  rplogcl  13880  logdivlti  13882  cxplt  13916  cxple  13917  rpabscxpbnd  13939  ltexp2  13940  iooref1o  14352