Theorem elrpd 10111

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   class class class wbr 4131  ℝcr 8184  0cc0 8185   < clt 8366  ℝ⁺crp 10071

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132  df-rp 10072

This theorem is used by:  mul2lt0rgt0  10178  mul2lt0np  10181  zltaddlt1le  10427  modqval  10782  ltexp2a  11049  leexp2a  11050  expnlbnd2  11124  nn0ltexp2  11169  resqrexlem1arp  11793  resqrexlemp1rp  11794  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemgt0  11808  resqrexlemglsq  11810  rpsqrtcl  11829  absrpclap  11849  rpmaxcl  12012  rpmincl  12028  xrminrpcl  12065  xrbdtri  12067  mulcn2  12103  reccn2ap  12104  climge0  12116  divcnv  12289  georeclim  12305  cvgratnnlembern  12315  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  rpefcl  12477  efltim  12490  ef01bndlem  12548  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  bdmopn  15730  mulcncflem  15833  ivthinclemlopn  15862  ivthinclemuopn  15864  dveflem  15952  reeff1olem  15997  pilem3  16010  tanrpcl  16064  cosordlem  16077  rplogcl  16109  logdivlti  16111  logdivlt  16124  logdivle  16125  cxplt  16151  cxple  16152  rpabscxpbnd  16175  ltexp2  16177  chtqrpcl  16279  chtqleppi  16294  iooref1o  17289