Theorem elrpd 9815

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

Syntax hints:   → wi 4   ∈ wcel 2176   class class class wbr 4044  ℝcr 7924  0cc0 7925   < clt 8107  ℝ⁺crp 9775

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rab 2493  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045  df-rp 9776

This theorem is referenced by:  mul2lt0rgt0  9882  mul2lt0np  9885  zltaddlt1le  10129  modqval  10469  ltexp2a  10736  leexp2a  10737  expnlbnd2  10810  nn0ltexp2  10854  resqrexlem1arp  11316  resqrexlemp1rp  11317  resqrexlemcalc2  11326  resqrexlemcalc3  11327  resqrexlemgt0  11331  resqrexlemglsq  11333  rpsqrtcl  11352  absrpclap  11372  rpmaxcl  11534  rpmincl  11549  xrminrpcl  11585  xrbdtri  11587  mulcn2  11623  reccn2ap  11624  climge0  11636  divcnv  11808  georeclim  11824  cvgratnnlembern  11834  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  rpefcl  11996  efltim  12009  ef01bndlem  12067  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem16  12602  bdmopn  14976  mulcncflem  15079  ivthinclemlopn  15108  ivthinclemuopn  15110  dveflem  15198  reeff1olem  15243  pilem3  15255  tanrpcl  15309  cosordlem  15321  rplogcl  15351  logdivlti  15353  cxplt  15388  cxple  15389  rpabscxpbnd  15412  ltexp2  15413  iooref1o  15973